Prev: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent(EASY PROOF)
Next: prof. Charles N. Moore ?
From: herbzet on 2 Jul 2010 00:08


herbzet wrote:

> What we worry about is for an arbitrary metatheory and theory X
> and Y respectively we may have a pure existence proof in X of a
> contradiction in Y, without an actual contradiction to display.
>
> Or more generally, a derivation of some sort in X of the string
> "Y is inconsistent" that happens not to be sound.

No, my mind wandered.

What we're worried about in *this* thread is whether for an arbitrary
(consistent) metatheory and (inconsistent) theory X and Y respectively
there might occur a derivation of some sort in X of the string "Y is
consistent".

Aatu says, with certain mild(?) qualifications, no.

--
hz
From: Frederick Williams on 2 Jul 2010 06:13
Chris Menzel wrote:
>
> On Thu, 01 Jul 2010 17:16:35 +0100, Frederick Williams
> <frederick.williams2(a)tesco.net> said:
> > Charlie-Boo wrote:
> >>
> >> The next thing to actually do is to show how or why PA can't prove PA
> >> consistent in detail
> >
> > Hilbert & Bernays do that.
>
> Peter Smith's wonderfully lucid book _An Introduction to Gödel's
> Theorems_ highly recommended for this.

I've heard of it but never looked into it. Thank you for mentioning it.

--
I can't go on, I'll go on.
From: MoeBlee on 2 Jul 2010 17:11
On Jul 1, 5:50 pm, herbzet <herb...(a)gmail.com> wrote:
> MoeBlee wrote:
> > herbzet wrote:
> > > MoeBlee wrote:
> > > > herbzet wrote:

> I'm migrating to the terms "demonstration" or "derivation"
> for "formal proof".

Okay. By 'proof' in this context I had meant formal proof. But I'll
use 'derivation' instead in this context.


> What we worry about is for an arbitrary metatheory and theory X
> and Y respectively we may have a pure existence proof in X of a
> contradiction in Y, without an actual contradiction to display.

That is possible. But, as I understand, Aatu is talking about
metatheories (though he doesn't like the rubric 'metatheory') that DO
show the actual contradiction.

> > Z talks DIRECTLY (not even any "Godel coding" needed) about |-_PA.
> > I.e., Z can talk about provability in PA. In fact, in Z, we can DEFINE
> > PA itself (a certain set of sentences, as sentences themselves are
> > certain objects that Z may directly talks about)
>
> We'd have to use abbreviative definitions so that the Z strings
> in question are typographically identical to PA strings.  Or else rely
> on our ability to recognize that certain defined Z strings correspond
> to PA strings.

I don't see what why you're saying that. Let's take the formal theory
Z. In Z, we can define "is a symbol of the language of PA", "is a
formula of PA", etc.


I think the exercise to help here would be for you to do some of this
in formal Z. Let's say we've derived a bunch of theorems in formal Z
(I'll not say 'formal' anymore, since by 'Z' I mean the formal theory)
including a bunch of stuff about natural numbers, inductive sets,
definition-by-recursion theorems, etc. Then, still in Z, we can define
things like "is a first order language", "is a first order proof", "is
a first order theory", etc. Then, still in Z, we can specify a
particular set of objects (they will be sets themselves, since we're
in Z) to serve as the symbols for a certain language, and we specify a
set of formulas to be a certain set of axioms. Then we define a
constant symbol we nickname "PA" by "PA = the closure under first
order entailment (we will have already defined "closure under first
order entailment" in Z) from said axioms" (actually the formalization
of that is the definition in Z). Thus Z has defined 'PA' and we go on
to derive, in Z, things about PA

MoeBlee
From: MoeBlee on 2 Jul 2010 17:23
On Jul 1, 8:13 pm, herbzet <herb...(a)gmail.com> wrote:
> Aatu Koskensilta wrote:
> > herbzet writes:
>
> > > Yeh -- what *exactly* is being assumed has not been grindingly
> > > specified at a low level.  We're not there yet.  Hopefully, we won't
> > > have to go there.
>
> > We have to! Here goes: a consistent Sigma-1 complete formal theory T
> > can't prove for an inconsistent formal theory Q the claim "Q is
> > consistent". This is because "Q is inconsistent" is a Sigma-1 statement,
> > and so if true provable in T.
>
> Oy ...

Aatu is putting in technical and more rigorous and general form the
same thing I was saying in a loose way.

MoeBlee

From: Charlie-Boo on 2 Jul 2010 20:13
On Jul 2, 5:11 pm, MoeBlee <jazzm...(a)hotmail.com> wrote:
> On Jul 1, 5:50 pm, herbzet <herb...(a)gmail.com> wrote:
>
> > MoeBlee wrote:
> > > herbzet wrote:
> > > > MoeBlee wrote:
> > > > > herbzet wrote:
> > I'm migrating to the terms "demonstration" or "derivation"
> > for "formal proof".
>
> Okay. By 'proof' in this context I had meant formal proof. But I'll
> use 'derivation' instead in this context.
>
> > What we worry about is for an arbitrary metatheory and theory X
> > and Y respectively we may have a pure existence proof in X of a
> > contradiction in Y, without an actual contradiction to display.
>
> That is possible. But, as I understand, Aatu is talking about
> metatheories (though he doesn't like the rubric 'metatheory') that DO
> show the actual contradiction.
>
> > > Z talks DIRECTLY (not even any "Godel coding" needed) about |-_PA.
> > > I.e., Z can talk about provability in PA. In fact, in Z, we can DEFINE
> > > PA itself (a certain set of sentences, as sentences themselves are
> > > certain objects that Z may directly talks about)
>
> > We'd have to use abbreviative definitions so that the Z strings
> > in question are typographically identical to PA strings.  Or else rely
> > on our ability to recognize that certain defined Z strings correspond
> > to PA strings.
>
> I don't see what why you're saying that. Let's take the formal theory
> Z. In Z, we can define "is a symbol of the language of PA", "is a
> formula of PA", etc.
>
> I think the exercise to help here would be for you to do some of this
> in formal Z. Let's say we've derived a bunch of theorems in formal Z
> (I'll not say 'formal' anymore, since by 'Z' I mean the formal theory)
> including a bunch of stuff about natural numbers, inductive sets,
> definition-by-recursion theorems, etc. Then, still in Z, we can define
> things like "is a first order language", "is a first order proof", "is
> a first order theory", etc. Then, still in Z, we can specify a
> particular set of objects (they will be sets themselves, since we're
> in Z) to serve as the symbols for a certain language, and we specify a
> set of formulas to be a certain set of axioms. Then we define a
> constant symbol we nickname "PA" by "PA = the closure under first
> order entailment (we will have already defined "closure under first
> order entailment" in Z) from said axioms" (actually the formalization
> of that is the definition in Z). Thus Z has defined 'PA' and we go on
> to derive, in Z, things about PA

Why don't you do it here? At least start it - you know, the first few
lines of ZFC axioms and theorems derived from them as you go through
the steps. For a proof of PA consistency, I presume.

C-B

> MoeBlee

First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5
Prev: How Can ZFC/PA do much of Math - it Can't Even Prove PA is Consistent(EASY PROOF)
Next: prof. Charles N. Moore ?