Email thread begun by Roger Jones, Sat, 14 Aug 2010 21:02:26 +0100
[The part of Roger's message above "Further Remarks" has been
incorported into the "Notes from final discussion," notes.txt.]

Here are some points of clarification about my contributions 
to the discussions at the TEITP workshop followed by some 
elaboration.

I raised the question of whether we should have degrees of 
trust, to which J responded with doubt about the feasibility 
of a numerical measure (which I had not intended).
I observed that I had in mind some other partial ordering.

Later there was a discussion about whether having multiple 
proofs gave greater trust.  I observed that having two 
proofs is dual to using two oracles in a single proof, and 
that in the natural ordering of sets of tags for oracles by 
inclusion (which probably corresponds to what is being done 
by isabelle and HOL4), the inequalities are non-strict.  If 
the degrees are augmented to take account of multiple proofs 
then having two proofs would also be in general better than 
or equal (in point of trust) to having either one  (better 
if the two originals are incomparable).

Further Remarks:

If sets of tags are used as degrees of trust, which is close 
to what is being done by Isabelle and HOL4, then the degrees 
form a semi-lattice.

I produced a small model in Isabelle HOL called X-Logic some 
years ago of heterogeneous distributed reasoning which 
encompassed degrees of assurance as sets of tags (slightly 
complicated by "endorsements") and this may be found at:

http://www.rbjones.com/rbjpub/isar/HOL/X-Logic.pdf
(now too old to work with Isabelle).

To take account of multiple proofs one can work in the 
distributive lattice generated by the set of tags.  Degrees 
can then be represented by sets of sets of tags (each set of 
tags is the set of oracles used in one of multiple 
alternative proofs).  The join operation (for the degree of 
a theorem with two proofs) is union, the meet (for the 
degree of a proof from the degrees of its parts) is a bit 
more complicated.

Whether this is worth the extra cost of maintaining the 
labels I don't is moot.

I am now working on lattices for degrees of trust (as well 
as other aspects of trust in heterogeneous distributed 
proof) in ProofPower but don't have anything to show for it 
yet.  There is a question about whether it is desirable to 
have uniformity between different tools in this area, or 
whether it would still be possible to exchange results 
between tools which had different notions of degree of trust.

Konrad's isolation of tagging from other aspects of the 
kernel and his desire to allow more general use of tags 
raises questions about whether trust in tagging is essential 
to overal trust.
It seems to me that these degrees of trust are concerned 
with integrity which is (informally) dual to security, and 
that one should expect to be able to show results analogous 
to security results, along the lines that theorems with low 
degrees do not contribute in any way to theorems with high 
degrees (this is an upside down way of saying that the tags 
are correctly propagated) and this should be taken into 
account when extending the tagging scheme.

Roger Jones