torkel@sics.se (Torkel Franzen) (03/01/91)
In article <16462.9102272325@s4.sys.uea.ac.uk> jrk@information-systems.east- anglia.ac.uk (Richard Kennaway CMP RA) writes: >I'm not saying it's no evidence at all, but that it is only evidence >relative to the consistency of the system in which the proof is conducted. >If one accepts that consistency, the proof is perfectly good evidence; to >the extent that one doubts it, so is that evidence weakened. What you are saying is that the proof is evidence for the hypothetical statement "if S is consistent, then T is consistent". Thus, the proof in itself is no evidence at all for the consistency of T. Whether we have (empirical?) evidence apart from the proof for the consistency of S - and thereby, given the consistency proof, for the consistency of T - is a different matter. >What is special about consistency theorems is that they are consistency >theorems, and that they generally cannot be proved in systems weaker than >those whereof they speak. As a result, a proof of the consistency of a >system X conducted in a system Y containing X does not give one any reason >to believe in that consistency that one did not have already. There's an unwarranted step here from "not weaker" to "stronger". A theory T may well be proved consistent in a theory S that is not stronger than T. For example, the consistency of elementary arithmetic + "elementary arithmetic is inconsistent" is provable in elementary analysis. And I think you will agree that this consistency theorem is far from obvious. What you have in mind is a special class of consistency proofs: proofs by reflection, in which we prove that a theory T is consistent by noting, in a stronger theory S, that all theorems of T are true. These proofs are essentially trivial, granted. However, we must be careful in considering what is meant by saying that "the consistency proof is worthless as evidence to support one's belief in the consistency of T". Certainly it is true that if one has no confidence in the theory S, the proof gives one no reason whatever to believe in the consistency of T. But this applies to any theorem proved in S! A proof of a statement A in S is worthless as evidence to support one's belief in A unless there is evidence for the validity (in a stronger or weaker sense, depending on the logical form of A) of the axioms and rules of inference of S. What remains concerning consistency proofs by reflection is just this, that they're trivial.
zlsiial@uts.mcc.ac.uk (A.V. Le Blanc) (03/01/91)
It is not necessarily the case that all proofs of consistency of the type you mention are trivial. There is an interesting case of three theories A, B, and C, in which B and C contain all of the rules and axioms of A, C contains all of the rules and axioms of B, B contains rules and axioms which are not valid in A, and C contains axioms which are not valid in B. With the addition of a further axiom -- essentially a highly restrictive assumption about the domain of discourse, which is nevertheless consistent with the axioms and rules of A, B, and C, it is possible to construct a model of C, and hence of B, in the original A. Hence the consistency of B and of C is demonstrated relative to the much weaker system A. An article discussing this proof appeared in the Journal of Symbolic Logic, perhaps about 1967? entitled `The Consistency of Mereology' by Prof. Czeslaw Lejewski. The proof dates from about 1930. A. V. Le Blanc ZLSIIAL@uk.ac.mcc.cms
torkel@sics.se (Torkel Franzen) (03/03/91)
In article <2398@mccuts.uts.mcc.ac.uk> zlsiial@uts.mcc.ac.uk (A.V. Le Blanc) writes: >It is not necessarily the case that all proofs of consistency of the >type you mention are trivial. There are lots of non-trivial consistency proofs. The character of the proof you describe is not clear from your description, in view of the "addition of a further axiom". However, it seems plain that it is not of the kind that I characterized as trivial: proofs by reflection, in which a truth predicate for T is defined in an extension S of T, and it is proved in S that every theorem of T is true.