From: george on
On Nov 8, 11:59 pm, Newberry <newberr...(a)gmail.com> wrote:
> He clearly believes that the we know PA/ZFC

There is no such thing as PA/ZFC.
PA is one thing. ZFC is another.

> to be consistent with the
> same certainty as any mathematical theorem

The theorem that PA is consistent is provable in ZFC.
It is NOT provable from/in PA. That ZFC is consistent has never
been proven. It is certainly not provable from ZFC. Bothering to
try to prove it in anything stronger is pointless; you would just have
the same question about whether that stronger theory was vs. wasn't
consistent.

> i.e. we can prove G.

"G" is NOT *one* thing. There is a DIFFERENT G for every
(sufficiently
rich) recursive axiom-set. You canNOT prove G(PA) in PA.
You canNOT prove G(ZFC) in ZFC.

> So the question arises how we can construct a machine that can do the same.
> obviously not by emulating PA/ZFC.

First-order logic is complete. It has inference rules. You just
construct a machine
that applies the inference rules repeatedly. There are some
treatments with as few as
one rule. And there *is* a way of doing this that you could think of
as "emulating ZFC".
Or emulating anything else for that matter. The point being that the
axioms from which
you are going to derive this theory are just one more INPUT to the
machine.

From: george on
On Nov 9, 7:17 am, aatu.koskensi...(a)xortec.fi wrote:
> Yes, PA is obviously consistent.

Come on.
The Gentzen proof is not obviously understandable.
N doesn't obviously exist at all.

From: george on
AK > >
> > Yes, PA is obviously consistent.

On Nov 9, 8:00 am, abo <dkfjd...(a)yahoo.com> wrote:
> Conclusive! Obvious! Who could doubt what one learned as a young boy
> in Sunday school?

I rated that 5 stars.
Which I really don't like having to do for people with whom I've had
bitter arguments.

From: george on
On Nov 9, 8:20 am, Herman Jurjus <hjur...(a)hetnet.nl> wrote:
> aatu.koskensi...(a)xortec.fi wrote:
> > Yes, PA is obviously consistent.
>
> So what?

So N is a model of it, so G is true, so a whole buncha stuff.
Pick one. I don't think AK will care as much as Newberry will.

From: Daryl McCullough on
Newberry says...

>He clearly believes that the we know PA/ZFC to be consistent with the
>same certainty as any mathematical theorem i.e. we can prove G. So the
>question arises how we can construct a machine that can do the same.
>obviously not by emulating PA/ZFC.

Well, here's an attempt at describing an informal metatheory that
captures a lot of human metatheoretic reasoning:

1. Every axiom of ZFC is true.

2. For every statement Phi in the language of ZFC,
Phi <-> Phi is true.

3. If T is any theory in the language of ZFC, and every
axiom of T is true, then every theorem of T is true.

This informal theory can prove Con(ZFC) and
Con(ZFC + Con(ZFC)), etc. And it's all perfectly
mechanical; you can write a program to work out
all the consequences of rules 1-3.

Of course, we can give a name to this new theory:

Let ZFC_1 = the collection of all statements in
the language of ZFC that follow from rules 1-3.

Then we can come up with yet another theory by
modifying rule1:

1'. Every axiom of ZFC_1 is true.

Then we could let ZFC_2 be the set of all consequences
of rules 1', 2, and 3. etc.

--
Daryl McCullough
Ithaca, NY