A Logic for Veracity: Development and Implementation

When a piece of information is put out into the world it gets subjected to many attempts, both accidental and deliberate, to degrade it or tamper with it. When we are dealing with precious information, that is information which has value (cultural, monetary, scientific etc.), then having assurance that the information is always reliable is vital. When that information is not kept hidden or otherwise protected then this becomes a very hard problem. It may even be insoluble. This is the essence of the veracity problem.

Veracity seems to be a term that is widely used, but it is also hard to pin-down its meaning. In this paper we shall take it to mean, reflecting the concerns in the previous paragraph, that we have an assurance that the information has stayed constant. So, we say a piece of information has veracity when we can check that it has not changed.

There is a long, deep, rich heritage of study of the concepts of truth and trust in many settings and many of them are formal, and very complicated and subtle. We want to start from scratch, not in order to just do something different, but in order to be able treat well, but lightly, those parts of veracity which can adequately be treated that way for our purposes (so, trust will be so treated). And then other parts (demonstrability, truth) will be looked at in more depth simply because they have not (as far as a literature search can show) been considered before, either with application in mind or in a formal way. Some examples that deal with adjacent ideas are [9, 6, 22, 21, 13, 12, 8, 16, 20, 10, 14, 7, 11], though they all miss more or less of the components of veracity in some way.

To cut to the chase: we will look at intuitionistic logic since it seems to be clearly what is needed, as we argue below. None of the classical modal logics work, for example, because of their classical basis, not because we do not like modal formalisms! The key to seeing this is that all those classical (and classical-including) logics lose information, which is precisely what a formalisation of veracity, as a starting point, must not do. Intuitionistic logic does not lose information, so obviously it is the place to start.

Some statements have a sort of immediate veracity, in the sense that they are newly minted by us and have not passed through any other hands.

Consider a couple of examples in more detail:

1. 1.

   A bar code that we have ourselves just printed and associated with a physical object might be an example in a supply chain: this act might generate the information that this bar code is stuck to this object that was produced by this person, at this time and this place, has these characteristics (composition, mass, etc.). We might say the information attests that “this bar code really does identify this object”;

2. 2.

   Or considering cultural objects, it might be an audio recording of a person giving their whakapapa (the Māori word that is usually condensed into the English word genealogy though it is a much richer concept) together with its meta-data that we have just ourselves recorded and catalogued. Here the information is attesting to the association between the meta-data and the audio data.

These cases in some sense wear their veracity on their sleeve: it is immediate, we have “a piece of veracity”, the information that this piece of data correctly describes this object since I, at just this moment, made the association. This is our atomic veracity. The claim or statement cannot be further analysed in terms of asking whose hands it has passed through, how it has be modified or added to since none of this has ever happened to it.

We might say (using logical terminology) that the piece of verifying information is a witness, proof, testimony, piece of evidence to the act of association, or the act of supporting a claim. The witness and the claim together are our judgements. It is these that we want to be able to objectify and then track. This track will be what we look to when someone says “how do we know that this bar code correctly identifies this object?”.

We might want to view this evidential information in more detail though. A witness might include information of who $p$, where $\ell$, when $t$, how $m$ etc. is was made. In this case, the witness would not be an atomic name but an “atomic” term. I.e. we might view a witness either as the atomic name $w$ or the atomic term $w(p,\ell,t,m)$. So a witness, a piece of evidence, might contain a lot of information, but from the point of view of the logic it is not further analysable.

One very important use for such a non-atomic a witness is that it contains the provenance that contributes to the witness for a claim. This is often the meta-data attached to a digital artefact, for example.

How the data about it “sticks” to the artefact (the bar code on the car part, the meta-data to the whakapapa audio file) is not what we are concerned about here. It is another technological problem that is being worked on and is outside our scope. So, we are assuming it is possible and has been, or will be, done³³3This might be wishful thinking, but it has such big stakes for such large companies that we can assume it will happen one day, and indeed we now have cameras which help prove the authenticity of photos [4], or the use of isotopes to track the provenance of food and prove its authenticity [1], or very, very close-up photos of objects from particular angles to support authenticity [5], and so on. In any case, veracity is still an interesting idea to try to reason about..

There is a special veracity claim $\bot$ which has no witnesses, i.e. it is the claim that never has veracity, and a judgement that makes a claim about it can never be upheld.

This leads to our first proof rule:

This rule says that if you, in the course of your reasoning, somehow have shown that the claim $\bot$ (that can never have veracity) does in fact have it, then you can show that $anything$ has veracity. We call this rule $\bot^{-}$ for “$\bot$ elimination”.

Martin-Löf makes this comment on his corresponding rule [15]:

“The explanation of this rule is that we understand that we shall never get an element $c\in N_{0}$, so that we shall never have to execute $R_{0}(c)$. Thus the set of instructions for executing a program of the form $R_{0}(c)$ is vacuous. It is similar to the programming statement abort introduced by Dijkstra.”

We use the same justification and motivation for our rule too.

Here we are formalising the idea that if two veracity claims $A$ and $B$ are witnessed then the combined claim that $A$ together with $B$ has veracity is also witnessed, and that witness we choose to denote by the pairing of the component witnesses.

Note that this is a simple use of the the idea also of information being preserved around claims and their witnesses even when they are composed together.

One immediate place where this information preservation becomes perhaps a little unfamiliar is when we try to think about what saying “we have claims $A$ and $B$ and we know that they each have a witness, so we know that one or the other has one: that is, a claim of $A$ or $B$ is witnessed”. We might choose to formalise this by saying

The point here is that (first) this rule has exactly the same premises as the one above, and avoiding such points of choice amongst rules is generally (for coherence) a good thing. But more importantly (at the formalisation level) is that we have lost information here. The conclusion does not record which of the alternatives we have relied on to reach it: did we justify the claim of one or the other because of the first witness, or the second?

Righting these two points means doing something like

So, if we have a witness to a claim of $A$ then we certainly have a witness to a claim of either $A$ or $B$, and we “tag” the witness in the conclusion so that we do not lose the information about which claim the claim of one or the other relies on.

Now consider the case where we know that a certain witness $c$ upholds the claim that $A\lor B$. What can we deduce, if anything, from this?

First note that our two introduction rules mean that a witness to a claim like this must in fact have a tag since tags are introduced by the only rule that could have allowed us to deduce the claim of $A\lor B$. So, we have a case analysis to do: if the witness to this composite claim is tagged with $i$ then we know it is $A$ that we relied on and similarly with $j$ and $B$. This preservation of all the information allows us to dismantle the composite claim:

Imagine that by assuming that claim $A$ has veracity, i.e. that the judgement $x\in A$ has been shown for some arbitrary witness $x$, we can show that claim $B$ has veracity, i.e. we can show $b\in B$.

Denote this state of affairs by a claim that depends on an assumption:

The $\vdash$ is a turnstile (because of its shape) and is a relation between judgements. As we will see, it relates a set of judgements (the assumptions) with a single judgement (the conclusion). We will call this generalised form a judgement too (since the conclusion is certainly a judgement, and it’s usually the focus of our concerns).

As is typical, we introduce an $implication\ claim$ to reflect this, i.e. to discharge the assumption, so the claim becomes

Given any witness $x$ to the claim $A$ then it is possible to construct a witness for the claim $B$. That is, there is a function which given any witness to $A$ will compute a witness to $B$, so

The witness to an implicative claim like $A\rightarrow B$ should be a function that takes a witness to the claim $A$ and turns it into a witness for the claim $B$.⁴⁴4For expression $e$ and variable $x$, the expression $(x)e$ is an expression where all free occurrences of $x$ in $e$ become bound by this $(x)$. The expression $(x)e$ called an abstraction (of $e$ by $x$). For expression $(x)e$ and expression $a$, $(x)e(a)$ is an expression where all occurrences of $x$ in $e$ bound by this $(x)$ are replaced by $a$. The expression $(x)e(a)$ is called the application of $(x)e$ to $a$. Note that $b$ in the example must be an abstraction for this judgement to be well-formed.

In general, this allows us to build a function that, given a whole set of basic veracity claims and their witnesses (the assumptions), builds for us a witness for a complex veracity claim. This function can then be read as a process to be followed which, given starting veracity claims, will assure that a complex veracity claim can be successfully and correctly made.

Implication allows us to define negation in terms of $\bot$: $\lnot A$ is $A\rightarrow\bot$. A witness to a claim of $\lnot A$ takes a witness to $A$ and gives us a witness to $\bot$. But $\bot$ has no witness, so a witness to $A$ is not possible, as expected by our informal understanding of saying a claim has no witnesses, i.e. that $\lnot A$ holds.

The requirement that to justify a disjunction of claims it has to be demonstrated which of the claims were justified before (which is the role that the tags on the witnesses are playing in the rules) means that, for example, the claim $A\lor\lnot A$ is also not justifiable without saying which claim is witnessed: $A\lor\lnot A$ doesn’t survive the question: yes, but can you show, whatever $A$ is, the witness that assures the veracity of the claim here?

And the view that witnesses to implications are functions leads us in the same direction: to the thought that this is reinterpreting intuitionistic logic

Note: in fact these rules that we have given in the narrative above (in order to motivate the whole idea) are not general enough. In particular, the elimination rules need to introduce non-canonical forms of expression, and then we need equality rules to “compute” the value (i.e. the canonical form) of a non-canonical form. The full logic has this, but it turns out that for the examples we were motivated by in the supply chain rules need only introduction rules, and that is what the examples later and the automation currently concentrates on. The full rules (that go beyond those needed for the supply chain examples) are in Appendix 0.A. And as an example of an even more general rule (which the given elimination rules are special cases of, and where we have to use the full logic of dependent claims to prove them, in fact) see Appendix 0.B.

Having introduced more than one actor we now need to think about how, from a veracity point of view, they can be related.

Keeping to the idea that we think of simple cases to guide us rather than trying to do everything we might wish all at once, the question: what relationship between actors is a useful one (there will be others) to consider? Fundamentally, surely, is one of trust: does this actor trust that actor? Once we know who trusts who we can plausibly expect things like $k$ trusting $\ell$ mean that any judgement that $\ell$ has accepted allows $k$ accept that judgement. So, roughly, we would say that $\vdash a^{\ell}\in A$ leads to $\vdash a^{k}\in A$ if $k$ trusts $\ell$. If we denote the trust relation by $T\subseteq Act\times Act$ then $k$ trusts $\ell$ will be $kTl$. We propose a rule

and we can picture the relation as

A note: in the rule $trust\ T$, the $kTl$ premise should be considered to be syntactic sugar intended to focus on one particular element of $T$ for the purposes of clarity, since the presence of $T$ in the name of the rule is enough to justify the inference given that the remaining premise and the conclusion show what must be checked (that indeed $kTl$) and that can be done by reviewing the definition of $T$. This means that a proof always takes place in the context of one or more trust relations, and that the name of the rule is actually a name $trust$ and an abbreviated proviso, namely $the\ required\ actors\ must\ be\ related\ to\ one\ another\ in\ an\ in-context\ trust\ relation$. $k$ and $\ell$ in the rule can be identified by noting that $k$ is the actor mentioned in the conclusion and $\ell$ the actor mentioned in the premise.

We can explore, even with this simple basis, how veracity works.

Given $T$ as

we have

Given this example we might ask: can $any$ binary relation between actors be a trust one? No; it surely needs to be at least reflexive and certainly not symmetric: we trust ourselves, and if we trust someone does it follow that they should trust us?

Note that the proof above seems to show that trust is also transitive: it turns out to be a property of our simple rule. Does that call the simple rule into question, since it a stretch to accept that if I trust someone, and they trust someone else, then I should trust that someone else?

Well, we make the point that trust here is “100% trust” which explains this rule and how transitivity emerges in this pointwise way. We will return to this below.

Another derivable rule which seems to be a good thing: if two people see veracity in two different things and one trusts the other then the first person believes the conjunction.

Here is a derivation (a proof tree) that shows the validity of this derived rule:

This brings the final augmentation, that we need degrees of trust to make things work. We write

Then the apparent transitivity above only works if $kT_{1.0}\ell$ and $lT_{1.0}m$, i.e. $k$ trusts $\ell$ completely, and the same for $\ell$ and $m$, i.e.

and that makes the apparent transitivity look reasonable.

So, we recast the $trust\ T$ rule as

If instead $kT_{0.5}\ell$ and $lT_{0.4}m$ then I would say $kT_{0.2}m$ and the proof above supports this, rewritten as

i.e. if $a_{1.0}^{m}\in A$ and $kT_{0.5}\ell$ and $lT_{0.4}m$

then $a_{0.2}^{k}\in A$.

For reasons of space, we have barely scratched the surface of the complete logic, but have sought to give motivation to the idea and then a few formal highlights. The complete logic can be summarised as: Martin-Löf’s intuitionistic type theory, with the trust rule, actors and weights added, and then the whole reinterpreted as we have shown above. In particular, where the original logic talked about proof objects (or programs) and propositions (or types, specifications) we talk about witnesses and claims, respectively. We also rest on Martin-Löf’s soundness argument for the logic [15] (though we have also shown the rules are sound more conventionally via a semantics that rests on defining the meaning of a claim as being the set of all its witnesses).

The type for proof trees constrains them to be correct proof trees of the root judgement, however the type does not constrain which assumptions can be made.

The intention is that when carrying out a proof either interactively or semi-automatically, the person constructing the proof will make use of only the assumptions and trust relations that are valid in their use-case. It is still possible to programmatically analyse a proof tree after it has been constructed to ensure that only certain assumptions and trust relations have been used.

In Figure 1 we demonstrate how the proofTreeOf Ps j type is defined, focusing on a selected rules. The full definition is available on GitHub⁵⁵5https://github.com/Coda-Coda/Veracity-Logic-Mechanised/tree/FM-24.

• –

  The base case is handled by the rule assume which allows us to assume that actor a holds claim C by the evidence e provided. This rule should only be used when it is appropriate to do so given the use-case.

• –

  The rule and_intro requires a proof tree showing that claim C1 is held by actor a with the evidence e1 as well as a proof tree that claim C2 is also held by actor a with the evidence e2. Given this, we have a proof tree that the conjunction of claims C1 and C2 is held by actor a with the evidence {{e1, e2}}. This corresponds to the rule labelled “$\wedge^{+}$” in Section 2.2.

• –

  The rule or_elim1 captures the rule labelled “$\vee^{-}1$” in Section 2.3.

• –

  The rule impl_elim allows the application of the function that is included in the evidence for a proof of C1 to C2, to potentially different evidence of C2. Such a function is referred to as $b$ in Section 2.4.

To construct a proof tree interactively, we can use Coq tactics as in Figure 2. As shown, the proof follows from the application of the impl_intro and and_intro rules, followed by assuming $C_{1}$, $C_{2}$ and $C_{3}$ involving the evidence $\ell$, $s$ and $c$, respectively. This is an example from a case study, as discussed in Section 0.C.2.

Once we have constructed proof trees we can use standard functional programming techniques to convert value of the proofTreeOf Ps j type to strings such as renderings in LaTeX or natural language. The code that implements this is omitted for brevity, but is available on GitHub⁶⁶6https://github.com/Coda-Coda/Veracity-Logic-Mechanised/tree/FM-24. In Figure 3, we show the result of rendering the proof from Figure 2. A natural language rendering of the same proof is included in Appendix 0.D. Both renderings are computed by Coq from a completed proof, a value of type proofTreeOf Ps j. The notation $P$, as a superscript to evidence, applies to all parts of the witness.

This section gives an insight into a technique for automating proof tree constructions using a much simplified version of the proofTreeOf type. Bringing this level of automation to the version of proofTreeOf Ps j described previously is left for future work.

Rather than incorporating evidence into the type proofTreeOf, we instead only include the actor and claim as a part of j here and omit the list of assumptions. Then we define a Coq function, computeEvidence, to compute the evidence for each line in the proof tree. A similar approach is taken for the list of assumptions.

The main automation approach taken is to define a function which takes a proof tree with holes and fills in all the holes by one level deeper. This function is then repeated multiple times up until a depth limit is reached. For each unique proof goal and use-case, the user must define the function that takes the proof tree one level deeper. For an example of such a function see Figure 4. This could be facilitated by a web page with a helpful user interface in the future.

The user-defined function is then passed to the function shown in Figure 5, which applies the user-defined step function to a proof tree with holes and returns a list of proof trees that have had any holes filled in ‘one level deeper’. This function is then generalised to take in a list of proof trees with holes, making use of flat_map. The resulting function, which both takes in and returns a list of proof trees with holes, is then repeated on its own output until the depth limit is reached. Typically, the initial list would be a list containing the single proof tree of the claim aiming to be proved with a hole as its evidence.

An important consideration with this approach to proof search is that in the context of these veracity proofs, it matters which proof we have of a certain claim’s veracity. Proof-irrelevance is not appropriate and so the usual techniques for proof search, which typically result in only one proof being found, are less useful. For example, there are four different proofs of the claim $C\wedge C\wedge C\wedge C$ generated using the step function shown in Figure 4. It would not be sufficient to only generate one of these proofs of this illustrative claim automatically because in realistic examples what can be assumed is constrained. The resulting LaTeX renderings of the four generated proofs are shown in Appendix 0.E.