Path: utzoo!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!zaphod.mps.ohio-state.edu!rpi!uupsi!sunic!sics.se!sics.se!torkel
From: torkel@sics.se (Torkel Franzen)
Newsgroups: comp.ai.philosophy
Subject: Re: Consistency theorems
Message-ID: <1991Mar3.100539.9325@sics.se>
Date: 3 Mar 91 10:05:39 GMT
References: <16462.9102272325@s4.sys.uea.ac.uk>
	<1991Feb28.172555.12897@sics.se> <2398@mccuts.uts.mcc.ac.uk>
Sender: news@sics.se
Organization: Swedish Institute of Computer Science, Kista
Lines: 12
In-Reply-To: zlsiial@uts.mcc.ac.uk's message of 1 Mar 91 14:57:56 GMT

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.