'When Are Relations Neither True Nor False?
in [Math]
|
From: Aatu Koskensilta on 26 Feb 2010 12:43 Frederick Williams <frederick.williams2(a)tesco.net> writes: > On the other hand it's not _that_ good an answer because it seems > impolite, so here's a quotation from [2, p599] (P is the system in > question): > > P is essentially the system obtained when the logic of PM is > superposed upon the Peano axioms^{16} (with the numbers as > individuals and the successor relation as primitive notion). > > G\"odel's footnote 16 reads: > > The addition of the Peano axioms, as well as all other > modifications introduced in the system PM, merely serve to > simplify the proof and is dispensable in principle. > > I do not intend to list the axioms and rules but I will remark that the > ramified theory of types is not used. System P is what G�del proves this and that about -- although later in the paper he observes the only properties of P he uses in the proof are that it is primitive recursively axiomatized and capable of representing the primitive recursive functions -- but his mathematical reasoning is, as he explains, perfectly constructive. Indeed, by inspecting G�del's reasoning (in excruciatingly tedious detail) we find that there are primitive recursive functions f and g such that for every e, if e is a (p.r) code for a set of axioms of a theory T containing elementary arithmetic, and x is a code of a proof of the (Pi-1) formula with code g(e), then f(x) is a code of a proof of contradiction in T can be proved by nothing but computation on open terms (involving functions defined by primitive recursion), propositional logic, and the induction rule: A(0) A(n) --> A(n+1) ---------------------- (x)A(x) In logical jargon, the proof of the incompleteness theorem is essentially "logic free". > PS: I have a vague feeling that I M Copi proved (in ZF) that type > theory is consistent, but I cannot find a reference. If anyone knows > what I'm talking about I'd be pleased to be told. That type theory is consistent has a trivial proof in set theory. Just observe that all the axioms are true in V_omega+omega. (A more complex argument shows that the consistency of type theory is provable even in Zermelo set theory.) > PS the second: One can prove a "theorem VI" for far weaker systems such > as Robinson's. Sure. But Robinson arithmetic is too weak to prove (either of) the incompleteness theorems. -- Aatu Koskensilta (aatu.koskensilta(a)uta.fi) "Wovon man nicht sprechan kann, dar�ber muss man schweigen" - Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Frederick Williams on 26 Feb 2010 12:45 Newberry wrote: > > On Feb 25, 8:18 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) > wrote: > > Newberry says... > > > > >[...] Frege also believed that the > > >axioms in his system were manifestly true. > > > > Well, he was mistaken. The belief that a system is consistent > > can be mistaken. > > Which of his axioms was not manifestly true? You state[1] that a function, too, can act as the indeterminate element. This I formerly believed, but now this view seems doubtful to me because of the following contradiction. Let w be the predicate: to be a predicate that cannot be predicated of itself. Can w be predicated of itself? From each answer the opposite follows. [1] I'm quoting Russell from van Heijenoort, the "you" is Frege. At the point "[1]" Russell refers to a passage in Begriffsschrift which is also in van Heijenoort in English translation.
From: MoeBlee on 26 Feb 2010 15:28 On Feb 25, 7:39 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: > MoeBlee wrote: > > On Feb 25, 11:22 am, Newberry <newberr...(a)gmail.com> wrote: > > >> And we believe that PA is consistent because all its axioms are > >> manifestly true? > > > They're clearly true to a lot of people. They seem clearly true to me. > > Which axiom of PA doesn't strike you as true? > > How about the very first axiom listed in Shoenfield's book: > > N1. Sx =/= 0 > > which is _clearly false_ to me at this moment, when I'm thinking of > the (rather "natural") integers! I made it clear in my posts that by 'true' I mean as to the natural numbers (not as to 'the natural integers', whatever you may mean by that other than the natural numbers), which are 0 and successors of other natural numbers. > The moral of the story: "clearly true" is very subjective and has > no firm basis for deciding what's true or false. But model/relation > definition conformance would decide what's true or false. Naturally. It's clearly true that by the model theoretic definition of 'true' we have axiom N1 true in the standard model for the language of PA. Aside from that, it's clearly true that when we're talking about the everyday notion of natural numbers, zero is not the successor of any natural number. MoeBlee
From: MoeBlee on 26 Feb 2010 15:34 On Feb 25, 8:17 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: > Frederick Williams wrote: > > Nam Nguyen wrote: > >> [...] And what does your definition have > >> to do with GIT, it being dependent on the naturals as a model of some > >> formal system? > > > What exactly is GIT here? As I remarked elsewhere [1], Theorem VI [2] > > is entirely syntactic in its statement and proof. > > "entirely in its ... proof"? Really? So which formal system is that > "syntactic proof" in? I'd be surprised to find myself mistaken that it can be formalized in a number of formal systems. >What are the axioms of that particular formal > system? Is that formal system consistent by any chance? How did Godel > "know" that formal system is consistent? Godel may not have had PRA specifically in mind at the time (I think PRA was only subsequently stated as an explicit theory?), but at least we do know how to formalize PRA. And if we cannot be confident that PRA is consistent then I don't know what substantive mathematical theory we could be confident as to consistency. In any case, PRA may serve as a formal embodiment of what Godel referred to as finitistic and intuitionistically unobjectionable (or whatever exact phrase he used). MoeBlee
From: MoeBlee on 26 Feb 2010 15:41
On Feb 25, 8:33 pm, Nam Nguyen <namducngu...(a)shaw.ca> wrote: > MoeBlee wrote: > > On Feb 25, 8:52 am, Newberry <newberr...(a)gmail.com> wrote: > >> When we are making logical inferences we are preserving the > >> truth and we are able to formalize the steps syntactically. So when we > >> arrive at the conclusion that G is true how did we fathom it without > >> being able to formalize it? > > > If you demand formalization, then we can formalize in a meta-theory > > such as Z set theory. > I'm assuming you meant Z set theory is a FOL formal system. (Would my > assumption be correct?) Of course. If I had meant second order (or even higher order) Z then I would have specified that. > > That is, e.g., Z set theory proves that the > > Godel sentence for PA is true in the standard model for the language > > of PA, as we also may formally prove (and we can do it in even weaker > > meta-theories than Z set theory) that the the Godel sentence for PA is > > not a theorem of PA. > > One perhaps could prove a lot of interesting theorems in the formal system > Z. But the more crucial question here is how would we know Z is consistent > so that the negations of those theorems aren't provable, syntactically > speaking? And that has been discussed to death on various threads. We should all be familiar with various takes on that subject, as well as in the literature, as Maddy's famous JSL articles have been mentioned many times also (also, e.g. Boolos's 'Logic Logic Logic'). Notice, that in certain posts I have myself said that if one has grave doubts as to the consistency of PA, then a Z proof of consistency of PA would not help. However, that does not vitiate my answer to the poster that we can indeed formalize our reasoning that G is true. MoeBlee |