From: Aatu Koskensilta on
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
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
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
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
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