From: torkel@sics.se (Torkel Franzen)
Subject: Re: ZFC etc. (was Re: Report on Philosophies of Physicists)
Organization: Swedish Institute of Computer Science, Kista
	<TORKEL.92Sep25094806@isis.sics.se>
	<1992Sep25.201622.40255@Cookie.secapl.com>
Date: Sat, 26 Sep 1992 09:33:51 GMT

In article <1992Sep25.201622.40255@Cookie.secapl.com> frank@Cookie.secapl.com
 (Frank Adams) writes:

   >The point is that in proving the consistency of propositional logic, we
   >are using reasoning techniques which include all the techniques built
   >in to propositional logic.  Now, the main concern I have seen with this
   >kind of statement is to wonder what the point is; we don't believe the
   >proof unless we already believe what we are trying to prove.

  Let us try to keep the two statements involved apart: the
combinatorial statement "logic is consistent", and a statement
expressing trust in our methods of reasoning. Very many people
"believe in" ordinary logic (and trust that it cannot lead them into
contradiction) without even being able to formulate the combinatorial
statement. Now the combinatorial statement, if we choose a suitable
formalization of logic, will be easily proved by using just those
rules of ordinary logic on which we normally rely and which are
formalized in the system. Your reflection above makes good sense if we
try to read into the proof a justification of our trust in our
ordinary modes of reasoning. It is then relevant to observe that the
proof is nothing of the kind. What it is is a simple proof of a simple
combinatorial result, as trustworthy as any other proof of comparable
complexity and level of abstraction. So what is the point of the
proof? It has as much of a point as any of thousands of routine
verifications of expected results in mathematics. It is only the
"mystique of consistency" that inspires people with the idea that
consistency proofs must be either non-trivial or pointless.

 >As for the other problem, let us step back for a moment to the point
 >where neither of the theorems in question had been proved.  In this
 >case, their status is very different.  If we were to have proved that
 >some formulae don't have a disjunctive normal form, this would have
 >been an interesting fact.  If we had proved that propositional logic
 >was inconsistent, it would have been a catastrophe -- there was
 >something wrong with our reasoning process.

  This is quite arbitrary, as so often in counterfactual reflections
of this kind. We may as well say that if we had proved that
propositional logic (i.e. some formal system so designated) was
inconsistent, it would have established the interesting fact that
"propositional logic" was not in fact a correct formalization of our
methods of reasoning.

 >(In fact, just this kind of catastrophe occurred with naive set theory
 >-- set theory with the axiom "for any property P, there is a set S of
 >all sets having property P.  This did invalidate all, or even very
 >much, of the reasoning process of mathematics up to that time; but it
 >was nevertheless probably the most event in the history of
 >mathematics.)

  The only person who stated an unrestricted comprehension axiom was
Frege, who did not do set theory, and whose system had had no impact
whatever on mathematics. Neither Cantor nor any other mathematician
took the view that the set-theoretic paradoxes invalidated even
set-theoretical reasoning. But this, of course, is a different topic.