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: MoeBlee on 1 Jul 2010 11:40
On Jun 30, 5:01 pm, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:

> The two claims
>
>  T proves that Q is consistent.
>
> and
>
>  If T is consistent, so is Q.
>
> are not the same.

Right!

Thanks for saying this.

MoeBlee

MoeBlee



From: MoeBlee on 1 Jul 2010 17:49
On Jul 1, 3:24 pm, herbzet <herb...(a)gmail.com> wrote:

> If a consistent theory can prove a consistent theory inconsistent,

Which can happen, since a consistent theory might prove false (false
in the sense of arithmetic) theorems.

> why can't a consistent theory prove an inconsistent theory consistent?

Because if a theory T is inconsistent then there is derivation in T of
an inconsistency. So the metatheory witnesses that derivation, thus
the metatheory proves T is inconsistent.

MoeBlee

From: herbzet on 1 Jul 2010 19:19


MoeBlee wrote:
> herbzet wrote:
>
> > If a consistent theory can prove a consistent theory inconsistent,
>
> Which can happen, since a consistent theory might prove false (false
> in the sense of arithmetic) theorems.
>
> > why can't a consistent theory prove an inconsistent theory consistent?
>
> Because if a theory T is inconsistent then there is derivation in T of
> an inconsistency.

Yes ...

> So the metatheory witnesses that derivation, thus
> the metatheory proves T is inconsistent.

Surely, if the metatheory demonstrates "T is inconsistent",
and the metatheory is consistent, then the metatheory does
not also demonstrate "T is consistent".

But if T demonstrates an inconsistency (and is thus inconsistent),
then why must a consistent metatheory of T be able to witness
(demonstrate?) that?

(1) Not really sure what a "metatheory" is. If a theory X is capable
of expressing "theory Y is inconsistent", is that sufficient to
make theory X a metatheory of theory Y? (Because my question
quoted at the top of this post assumes only a little more than
that -- it assumes that X can not only express "Y is inconsistent"
but also provide that string with a derivation -- positing also,
of course, that X is consistent.)

(2) Not sure what "witness" means in this context, what it means
for some theory X to "witness" a feature of some theory Y.
Above, I just guessed at its meaning.

--
hz
From: MoeBlee on 1 Jul 2010 19:45
On Jul 1, 6:19 pm, herbzet <herb...(a)gmail.com> wrote:
> MoeBlee wrote:
> > herbzet wrote:
>
> > > If a consistent theory can prove a consistent theory inconsistent,
>
> > Which can happen, since a consistent theory might prove false (false
> > in the sense of arithmetic) theorems.
>
> > > why can't a consistent theory prove an inconsistent theory consistent?
>
> > Because if a theory T is inconsistent then there is derivation in T of
> > an inconsistency.
>
> Yes ...
>
> > So the metatheory witnesses that derivation, thus
> > the metatheory proves T is inconsistent.
>
> Surely, if the metatheory demonstrates "T is inconsistent",
> and the metatheory is consistent, then the metatheory does
> not also demonstrate "T is consistent".

Exactly.

> But if T demonstrates an inconsistency (and is thus inconsistent),
> then why must a consistent metatheory of T be able to witness
> (demonstrate?) that?

If I'm not mistaken, Aatu mentioned that we're talking about theories
of a certain kind. I surmised (am I not correct?) that certain things
about these theories here assumed, such as that the one theory is
adequate to talk about the other theory in such basic ways (for lack
of a more technical way of my putting it at this moment).

> (1) Not really sure what a "metatheory" is.

Doesn't matter. You were talking about theories proving things about
theories. I'm just using 'meta-theory' to refer to the theory that's
doing the proving about another theory (the object theory).

> (2) Not sure what "witness" means in this context, what it means
>     for some theory X to "witness" a feature of some theory Y.

For example, say Z set theory is "talking about" (is a meta-theory)
for PA. If PA is inconsistent, then we can prove that in Z, just by
displaying, in Z, the first proof (in an enumeration of PA proofs) of
a contradiction P & ~P. We display it in Z in the sense that that
proof (that sequence of formulas) is an OBJECT itself that Z talks
about. So if PA is inconsistent, then in Z we have a theorem that
"says", "there is a sequence of formulas that is a proof in PA such
that the last entry of that sequence is a formula "P & ~P" of PA".

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) and define
provability in PA and define truth in a given model for the language
of PA, and define the standard model for the language of PA, and all
kinds of things about PA. And one of these things is to talk about a
specific PA proof that happens to have as it's last entry a PA formula
"P&~P" (of course IF there is such a PA proof).

MoeBlee
From: herbzet on 1 Jul 2010 20:50


MoeBlee wrote:
> herbzet wrote:
> > MoeBlee wrote:
> > > herbzet wrote:
> >
> > > > If a consistent theory can prove a consistent theory inconsistent,
> >
> > > Which can happen, since a consistent theory might prove false (false
> > > in the sense of arithmetic) theorems.
> >
> > > > why can't a consistent theory prove an inconsistent theory consistent?
> >
> > > Because if a theory T is inconsistent then there is derivation in T of
> > > an inconsistency.
> >
> > Yes ...
> >
> > > So the metatheory witnesses that derivation, thus
> > > the metatheory proves T is inconsistent.
> >
> > Surely, if the metatheory demonstrates "T is inconsistent",
> > and the metatheory is consistent, then the metatheory does
> > not also demonstrate "T is consistent".
>
> Exactly.
>
> > But if T demonstrates an inconsistency (and is thus inconsistent),
> > then why must a consistent metatheory of T be able to witness
> > (demonstrate?) that?
>
> If I'm not mistaken, Aatu mentioned that we're talking about theories
> of a certain kind. I surmised (am I not correct?) that certain things
> about these theories here assumed, such as that the one theory is
> adequate to talk about the other theory in such basic ways (for lack
> of a more technical way of my putting it at this moment).

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.

> > (1) Not really sure what a "metatheory" is.
>
> Doesn't matter. You were talking about theories proving things about
> theories.

Right.

> I'm just using 'meta-theory' to refer to the theory that's
> doing the proving about another theory (the object theory).

Then we're about on the same page.

We're going to have to continue to be careful about saying
that X "proves" phi about Y, distinguishing formal proof
from, y'know, that other thing, *proof*.

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

> > (2) Not sure what "witness" means in this context, what it means
> > for some theory X to "witness" a feature of some theory Y.
>
> For example, say Z set theory is "talking about" (is a meta-theory)
> for PA. If PA is inconsistent, then we can prove that in Z, just by
> displaying, in Z, the first proof (in an enumeration of PA proofs) of
> a contradiction P & ~P. We display it in Z in the sense that that
> proof (that sequence of formulas) is an OBJECT itself that Z talks
> about. So if PA is inconsistent, then in Z we have a theorem that
> "says", "there is a sequence of formulas that is a proof in PA such
> that the last entry of that sequence is a formula "P & ~P" of PA".

Yes, we have a witness, in the sense that we can display the demonstration
in PA of a contradiction, and then reason by FOL to "There exists
a demonstration in PA of a contradiction" (I forget the name of
the rule of inference P(term) |- Ex (Px). )

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.

> 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.

> and define
> provability in PA and define truth in a given model for the language
> of PA, and define the standard model for the language of PA, and all
> kinds of things about PA. And one of these things is to talk about a
> specific PA proof that happens to have as it's last entry a PA formula
> "P&~P" (of course IF there is such a PA proof).

Yeh -- whew.

--
hz
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 ?