Re: Cantor's circular "proof" that evens = integers

On May 24, 11:52 am, stevendaryl3...@xxxxxxxxx (Daryl McCullough)
wrote:
Aatu Koskensilta says...

Another point I wished to make was that people usually
obsess over consistency simply because they think a theory being consistent
or inconsistent is somehow more concrete or objective a state of affairs
than it being unsound for some class of sentences. We can counter this by
noting that a theory T proving "T is incosistent" is equally "objective".

What UTTER bull***. A theory T proving "T is inconsistent" IS JUST
BULL***. In that context, what you CALL "T is inconsistent"
SIMPLY DOES NOT MEAN that. You (and, for that matter, that
theory) are MISSING SOMETHING IMPORTANT here.

There is reply-target ambiguity here since I am replying to a message
in which AK is replying to DMC, but the point is, I am mad at both
of you, for the moment. Madder at Darryl, since it was AK who taught
me this lesson, but DMC should still have known it without needing
it explained to him, especially since HE UNDERTOOK to explain it
in this very message.

This might be obvious to most people, and so not worth saying,
but I want to point out that when someone says that for some
formula Con,

Con formalizes the metatheoretic claim that T is consistent

this claim must be relative to a particular *interpretation*
of the language in which Con is expressed.

Specifically, it must be in some interpretation in which
the truth value that the interpretaion assigns to Con(T)
MATCHES THE ACTUAL truth-value of Con(T), which must,
in fact, be TRUE, IF the enterprise is to be of any value at all.

To formalize consistency,
we concoct a formula along the lines of

forall y, forall z, forall w
Negation(y,z) & And(y,z,w)
-> ~ forall x, Proof(x,w)

where Negation(y,z) is a formula meaning
"z is the code of the negation of the
formula whose code is y", and And(y,z,w) is a formula meaning
"w is the code of the conjunction of the two formulas whose codes
are y and z" and Proof(x,w) is a formula meaning
"x is a code for a proof of a formula whose code is w".

But what forces Negation(y,z) and And(y,z,w) to be about formulas?

You deserve to be chastised because you asked this irrelevant
question. IT DOES NOT MATTER whether Negation and And are
or are not about formulas.

What forces Proof(x,w) to be about proofs?

The short answer is that at first-order, with a recursive
axiom-set, YOU CAN'T force this. But it MATTERS WHY!
WHAT GETS IN THE WAY of your being able to achieve
this theoretically sand syntactically? WHY do you have to
retreat to semantics.

You can't determine *syntactically* that a formula
is about proofs or is about formulas.

That's true, BUT IT IS ALSO IRRELEVANT. IF the notion
could be captured syntactically, it would hold FOR ALL MODELS
of the provability-theory in question, REGARDLESS of what they
were "about". Theorems Are NEVER *ABOUT* ANYthing --
unless you got lucky and got a first-order theory that was
categorical,
in which case it was ALSO TRIVIAL in the sense of NOT being rich
enough to be subject to Godelian incompleteness.

You have to establish, in some metatheoretic way, that for the
intended domain,

WHOA, HOSS!
IF this ESTABLISHED, IF this is any relevant sense PROVEN,
then by the completeness theorem, it will be true IN ALL
relevant domains. You don't YET need to invoke an "intended
domain" at all. Your claim of invocation of an intended domain
FOR THE GOAL of making the reasoning ABOUT FORMULAS
IS JUST WRONG. If the results are provable then it won't
matter what they are about.

The problem you face is that these results ARE NOT provable.
The problem you face is that ANY AND EVERY 1st-order
predicate you ATTEMPT to define as Prf(p,f) IS ABSOLUTELY
GUARANTEED TO GET IT *WRONG* in SOME model for SOME
statements and SOME proofs at least SOME of the time!
The question, therefore, is, WHY IS that?

I know the answer and I know AK knows since he told me.
WHAT SPECIFIC ATTRIBUTE of proofs (and of formulas, too;
it is an attribute they share) that makes this non-formalizable
at first-order?

.

Quantcast