From: Aatu Koskensilta on
Charlie-Boo <shymathguy(a)gmail.com> writes:

> If so, what is the formal expression in ZFC that PA is consistent?

On any scheme for expressing such statements in the unextended language
of set theory it's a virtually incomprehensible string of symbols. If
you really want to have a look, go through a set theory text and write a
computer program to output it for you. Why would you want to see it in
the first place?

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on
Charlie-Boo <shymathguy(a)gmail.com> writes:

> To see it means to have actually created it, and its actual creation
> would answer the very interesting question of whether ZFC can prove
> that PA is consistent even though PA can't.

We already know the answer. The axioms used in the proof are a
restricted form of comprehension, infinity, union and pairing. Spelling
out the formalization of "PA is consistent" in the language of set
theory would be a tedious, trivial and pointless undertaking, of no
apparent mathematical interest whatsoever.

> It would substantiate your assertions. Is that of value?

Well, no. I can't think of any pressing reason I should want to convince
you of anything.

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Aatu Koskensilta on
Ki Song <kiwisquash(a)gmail.com> writes:

> Perhaps an analogy is in order!
>
> I feel like what Charlie-Boo is asking people to do is analogous to
> asking someone to perform the addition:
>
> Sqrt{2}+Sqrt{3}, with a decimal precision of 10^(10^(10^100)) place.

The analogy is apt, but it's not really quite that bad. Based on nothing
at all I'd estimate that a formalization of "PA is consistent", fully
spelled-out in the language of set theory, fits in less than ten
pages. But perhaps you were thinking of Bourbaki, whose term for the
number 1 already consists of 4,523,659,424,929 symbols and
1,179,618,517,981 disambiguatory links?

--
Aatu Koskensilta (aatu.koskensilta(a)uta.fi)

"Wovon man nicht sprechan kann, dar�ber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
From: Jesse F. Hughes on
billh04 <hale(a)tulane.edu> writes:

>> > Theorem. (all x in N)(all y in N)(if S x = S y then x = y)
>>
>> > Here N is a set (defined as mentioned before).
>> > Here x and y are sets since everything in ZFC is a set.
>> > Here S is a set (the successor function).
>> > Thus, the theorem is a statement about sets.
>> > ZFC can proves statements about sets using the ZFC axioms.
>>
>> > Why do you think this theorem cannot be proved using the ZFC axioms?
>>
>> If it could be done without the axiom of infinity, then the axiom of
>> infinity wouldn't be needed in ZFC.  Maybe it is, but I doubt that.
>
> But the axiom of infinity is a ZFC axiom. So, I am allowed to use it
> in proving a theorem in ZFC.

In fact, the use of infinity for this particular theorem is trivial
indeed.

ZFC proves

(Ax)(Ay)( Sx = Sy -> x = y ).

To prove

(Ax in N)(Ay in N)( Sx = Sy -> x = y ),

we need merely add a definition of N to ZFC. The axiom of infinity is
used to show that there is a unique set satisfying certain conditions
and we define N to be that set[1]. But the properties of that set are
literally irrelevant to this particular proof.

Footnotes:
[1] Yes, Charlie, by *adding* an axiom to ZFC, resulting in a
conservative extension, but this is only a nicety. We could prove a
theorem with the same content without adding the definition. Suppose
our defining axiom is P(x), so that our definition of N is the axiom

P(N).

Now, ZFC proves (Ex)(Px & (Ay)(Py -> y=x)). So, the statement

(Ax in N)(Ay in N)( Sx = Sy -> x = y )

means the same thing as

(Ew)(Pw & (Ax in w)(Ay in w)( Sx = Sy -> x = y )).
--
Jesse F. Hughes

"How lucky we are to be able to hear how miserable Willie Nelson could
imagine himself to be." -- Ken Tucker on Fresh Air
From: Alan Smaill on
Charlie-Boo <shymathguy(a)gmail.com> writes:

> On Jun 29, 5:28�pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
>> On Jun 29, 4:23�pm, Transfer Principle <lwal...(a)lausd.net> wrote:
>>
>> > I'm not skeptical (in the way that Charlie-Boo is skeptical) about
>> > the provability of Con(PA) in either ZFC or PRA+epsilon_0. But I
>> > am suspicious of the fact that the induction needs only to be
>> > taken up to epsilon_0,
>>
>> As to ZFC, you don't need such fancy stuff as epsilon_0. Just do the
>> routine proof that with the system of omega with 0, successor,
>> addition, and multiplication we get a model of all the PA axioms.
>
> The problem isn't to conclude that a model exists, using ZFC. The
> problem is to prove that PA is consistent, using ZFC.

If you admit that ZF can express "structure S is a model for theory T",
then have a go at working out how the provable existence of a model
shows consistency.

Hint: a semantic definition of consistency of T is that there is
no formula P such that P and ~P are logical consequences of T.

Hint: recall the definition of satisfaction of a negated formula
in a structure.

Hint: try using FOL.

Is that enough hints?

> C-B
>
>> MoeBlee
>

--
Alan Smaill