From: Charlie-Boo on
On Jun 29, 10:16 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Charlie-Boo <shymath...(a)gmail.com> writes:
> > Ok.  What is the reference to the proof in ZFC of PA consistency doing
> > it that way?
>
> It's in Shelah's _Cardinal Arithmetic_ p.3245 - 4325238532. Basically,
> you just do a triple-fold transfinite recursion over a coherent extender
> sequence to obtain a suitable premouse, and iterate the upward Mostowski
> collapsing lemma a few times. To remove the extendible cardinal
> introduce some Aronszjan trees using Sacks forcing.

Where's the part about how ZFC is used to do it?

C-B

> --
> Aatu Koskensilta (aatu.koskensi...(a)uta.fi)
>
> "Wovon man nicht sprechan kann, darüber muss man schweigen"
>  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

From: Charlie-Boo on
On Jun 29, 9:16 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> billh04 <h...(a)tulane.edu> writes:
> > Are you saying that it is a theorem of ZFC that PA is consistent?
>

> Sure. That is, the statement "PA is consistent" formalized in the
> language of set theory as usual is formally derivable in ZFC (and

No it isn't. PA can't do it and ZFC has nothing outside of PA
relevant to the proof.

Now, I refuted it - either prove it can be done, or refute my
refutation, or retract the statment, ok? Isn't that how Mathematics
works?

C-B

> already in much weaker theories).
>
> --
> Aatu Koskensilta (aatu.koskensi...(a)uta.fi)
>
> "Wovon man nicht sprechan kann, darüber muss man schweigen"
>  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

From: Charlie-Boo on
On Jun 29, 9:13 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Charlie-Boo <shymath...(a)gmail.com> writes:
> > ZFC was designed to avoid paradoxes by making explicit what can be a
> > set.  It doesn't do anything else except what the Peano Axioms give
> > it.
>
> Does PA give us Borel determinacy? Is Borel determinacy trivial?

Prove ZFC can prove it and PA can't.

C-B

> --
> Aatu Koskensilta (aatu.koskensi...(a)uta.fi)
>
> "Wovon man nicht sprechan kann, darüber muss man schweigen"
>  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

From: Charlie-Boo on
On Jun 29, 8:58 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Charlie-Boo <shymath...(a)gmail.com> writes:
> > How about when you said that Gentzen proved PA consistent using ZFC?
>
> No one ever proves anything using ZFC in the sense of producing formal
> derivations. Rather, they prove mathematical theorems using mathematical
> principles formalized in ZFC. By certain elementary considerations we
> know the formalizations of such theorems are formally derivable in ZFC.

How do you know that all of the logical argument can be formalized in
ZFC?

This is an example of what I call The Fallacy of the Famous Result.
People will attribute special status to a result (rather than other
similar results) whose only distinction is that it is famous. They
are often famous because they were the first (seminal) result in a
certain subject (e.g. a branch of Computer Science e.g. the Theory of
Computation or Incompleteness in Logic.) But why does that argument
not apply to the other results?

“Turing’s Halting Problem theorem proved for computers what Godel’s
First Incompleteness theorem proved for logic.” But these results
were simply the first theorems discovered in their respective areas.
It would be quite the coincidence if they were equivalent in some way
that distinguishes them from other theorems, especially more general
theorems discovered later (e.g. Rosser’s extension of Godel’s
results.)

Why is it Gödel’s theorem instead of Rosser’s theorem that is
equivalent to Turing’s result? Because Godel’s is more famous and the
author can’t figure out Rosser’s. It has no simple “This is
unprovable.” puzzle/joke/amusement to describe it that anyone can talk
about. Gregory Chaitin never mentions Rosser’s stronger results.
It’s too complicated for him to understand.

“The recursion theorem proves/explains/formalizes Godel’s
Incompleteness Theorem.” Why doesn’t it prove/explain/formalize
Rosser’s theorem? Or does it explain EVERY theorem?

And here we have the assertion that ZFC formalizes a proof of
consistency of PA. There are a good dozen axiomatizations of set
theory. Does ZFC2 (read: NF, NFU, CST, CZF, IZF etc.) formalize this
argument? How about ZFC3 that has only one short axiom!? How do you
know when an axiomatization of set theory has enough axioms to do the
job? Or the right axioms to do the job?

Without showing this specific proof being carried out in ZFC, how can
you show properties – capabilities – of ZFC that are sure to include
what is needed in this particular proof?

The answer is, you can’t. Unfortunately, even people like you who
know the names of lots of theorems also tow the party line despite the
fact that in all references given (Gentzen by Frederick Williams and
Hinman by MoeBlee) there is no mention of any of ZFC’s axioms anywhere
in their proofs (including earlier results on which it relies) at
all. Not just “not all” but “none at all”.

C-B

> --
> Aatu Koskensilta (aatu.koskensi...(a)uta.fi)
>
> "Wovon man nicht sprechan kann, darüber muss man schweigen"
>  - Ludwig Wittgenstein, Tractatus Logico-Philosophicus

From: Frederick Williams on
Charlie-Boo wrote:
>
> On Jun 29, 10:16 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> > Charlie-Boo <shymath...(a)gmail.com> writes:
> > > Ok. What is the reference to the proof in ZFC of PA consistency doing
> > > it that way?
> >
> > It's in Shelah's _Cardinal Arithmetic_ p.3245 - 4325238532. Basically,
> > you just do a triple-fold transfinite recursion over a coherent extender
> > sequence to obtain a suitable premouse, and iterate the upward Mostowski
> > collapsing lemma a few times. To remove the extendible cardinal
> > introduce some Aronszjan trees using Sacks forcing.
>
> Where's the part about how ZFC is used to do it?

Woosh.

--
I can't go on, I'll go on.