Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP Posting-Version: version B 2.10.1 6/24/83 (MC840302); site boring.UUCP Path: utzoo!linus!philabs!cmcl2!seismo!mcvax!boring!lambert From: lambert@boring.UUCP Newsgroups: net.math Subject: Re: Re: Nova's Mathematical Mystery Tour (truth of CH) Message-ID: <6355@boring.UUCP> Date: Thu, 14-Mar-85 06:56:19 EST Article-I.D.: boring.6355 Posted: Thu Mar 14 06:56:19 1985 Date-Received: Sun, 17-Mar-85 21:09:21 EST References: <143@ihlpa.UUCP> <460@petsd.UUCP> <6353@boring.UUCP> <350@talcott.UUCP> <529@mcvax.UUCP> Reply-To: lambert@boring.UUCP (Lambert Meertens) Organization: CWI, Amsterdam Lines: 92 Summary: Apparently-To: rnews@mcvax.LOCAL >>> The same must apply to classical mathematicians. Even though CH is in- >>> dependent of the axioms of ZF Set Theory, it is conceivable (although high- >>> ly implausible) that someone will some day come up with new methods of >>> mathematical reasoning that are *obviously* valid, using which CH can be >>> decided. [...] >>> Lambert Meertens >> Really? I had always thought that there were two kinds of universe: >> in one class, the CH is true, and in the other it is false. [...] >> If this duality is valid, how can one possibly come up with new methods by >> which CH can be decided? Or is this duality valid in the first place? >> Greg Kuperberg > In a mathematical theory you use axioms and inference rules to arrive > at theorems. The axioms are usually made explicit; they are not considered > obvious, but are assumed as a starting point. The rules of inference are > seldom made explicit - it is assumed that mathematicians can recognise > valid reasoning. What Lambert says (I think) is that it is conceivable > (but unlikely) that somebody comes up with an obviously valid inference > rule that would enable us to decide CH from the ZFC axioms. > I do not agree, since the current inference rules already allow you to > construct models in which CH holds and models in which it doesnt hold. > Stronger inference rules deciding CH would thus lead to a contradiction. > Something that is conceivable to me is that one might come up with new > axioms for Set Theory that are *obviously* valid and would decide CH. > Andries Brouwer To me, there is an essential difference between (i) mathematical *reasoning*, in which propositions, natural numbers, sets, etc. are used as *tools*, and (ii) mathematical *theories*, in which abstract objects with certain properties are studied (using mathematical reasoning), such as algebra or set theory, or (mathematical formal) logic. In the latter, for instance, a mathematician uses mathematical reasoning, including propositions and inferences, to study properties of gottloboids (which are abstract objects intended to formalize mathematical theories and mathematical reasoning, and which are often called--somewhat confusing-- `theories'). In set theory, zermeloids are studied. These are supposed to formalize sets. But they cannot form the *foundation* for the use of sets in mathematical reasoning, if only since it is impossible to discuss the meaning of a theory without using the notion of `set'. To make the issue more complicated, set theory is formalized in one particular gottloboid, such as ZFC. For the same reason, it is impossible to found mathematics using gottloboids as a basis. If the axioms and inference rules of a gottloboid are correct, in the sense that they are valid for the part of mathematics the gottloboid is supposed to formalize, then we may translate the string of symbols obtained by applying the rules of the formal game into a mathematical proposition that we know to be valid: a theorem. This is such a common operation that we are usually not aware of the fact that there are two levels here, the `normal' mathematical level and a metamathematical level. In fact, the excursion to the metalevel is never necessary to reach a conclusion on the normal level, only possibly convenient. It is, of course, essential for metatheorems (such as Goedel's and Cohen's results). So I reject an approach in which sets are defined as `whatever objects satisfy the axioms of ZF Set Theory' as unsound and viciously circular. (Stronger, I have no reason to assume or believe that these zermeloids faithfully formalize sets, since I cannot think of a reasoning that makes the Axiom of Choice plausible, let alone of a justification for it--but that is beside the issue; assume for simplicity's sake that I believe in it.) Given any set of axioms, there may be other systems satisfying the axioms (called `models' in mathematical logic) than the particular one it was supposed to formalize. This means that some propositions may exist whose formal expression is formally undecidable from the set of formal axioms. But in no way does this imply that they are not possibly plain right or wrong. For example, for any acceptable gottloboid formalizing natural numbers, say FOL+PA, Goedel's Incompleteness Theorem can be translated into a formal proposition GIT that is formally undecidable, meaning that there exists a model for FOL+PA in which GIT is `false'. But the mathematical proposition formalized by GIT is true, valid, right, correct. (It is a red herring to call these models `universes' as though they all have equal status: there is the original system that we tried to formalize, and there are bogus, non-standard models that are an artefact of the inherent limitations of formalization.) Similarly, the formal undecidability of CH does not imply anything about the status of CH; it still might be plain right, or plain wrong. (In case you are interested in my position, I actually think that CH is devoid of meaning.) I do not see an essential difference between axioms and inference rules; an axiom is simply an inference rule with an empty set of antecedents. I think Andries is wrong when he says that adding inference rules to ZFC that make CH decidable would lead to a contradiction. In particular, if adding CH itself as an axiom leads to a contradiction, then one can formally infer `not CH'. (In case ZFC+CH is only omega-inconsistent, standard metamathematical reasoning would still lead to the conclusion that CH is false.) -- Lambert Meertens ...!{seismo,philabs,decvax}!lambert@mcvax.UUCP CWI (Centre for Mathematics and Computer Science), Amsterdam