From: Nam Nguyen on
Frederick Williams wrote:
> Nam Nguyen wrote:
>> Frederick Williams wrote:
>>> Nam Nguyen wrote:
>>>> [...] And what does your definition have
>>>> to do with GIT, it being dependent on the naturals as a model of some
>>>> formal system?
>>> What exactly is GIT here? As I remarked elsewhere [1], Theorem VI [2]
>>> is entirely syntactic in its statement and proof.
>> "entirely in its ... proof"? Really? So which formal system is that
>> "syntactic proof" in? What are the axioms of that particular formal
>> system?
>
> A good answer would be: read all about in my reference [2]. I call that
> a good answer because then you'll get precisely what G\"odel had to say,
> well not _precisely_ because [2] is an English translation of a German
> work.
>
> On the other hand it's not _that_ good an answer because it seems
> impolite, so here's a quotation from [2, p599] (P is the system in
> question):
>
> P is essentially the system obtained when the logic of PM is
> superposed upon the Peano axioms^{16} (with the numbers as
> individuals and the successor relation as primitive notion).
>
> G\"odel's footnote 16 reads:
>
> The addition of the Peano axioms, as well as all other
> modifications introduced in the system PM, merely serve to
> simplify the proof and is dispensable in principle.
>
> I do not intend to list the axioms and rules but I will remark that the
> ramified theory of types is not used.

As AK has alluded to, as well your mentioning above "(P is the system in
question), as well as what Godel himself wrote:

We proceed now to the rigorous development of the proof sketched above,
and begin by giving an exact description of the formal system P,
for which we seek to demonstrate the existence of undecidable propositions.

then P is just *a* T under investigation. Without loss of generality,
we could take ZF as P. Now, you've asked me above "What exactly is GIT
here?". My answer is that typically when we say GIT we'd refer to GIT1
which would be, according to Godel's paper (and for all practical
purposes), the following meta statement:

(1) "Bew_c[(17 Gen r)]" is true _and_ "Bew_c[Neg(17 Gen r)]" is true.

Note in his meta theorem (1) the 2 expressions inside the 2 pairs of
double quotes (") are FOL formulas written in the language of arithmetic,
which in modern day consideration is L(PA) but which is _not_ L(ZF)!

The long and short of it is no matter how much syntactical characteristic
of P (ZF in this example) Godel utilized in his proof of GIT, his proof
would be done in a formal system, say the "proving" system, that would be
in general different from the P "in question". Now, let's rephrase (1)
a bit further:

(2) "Bew_c[(17 Gen r)] /\ Bew_c[Neg(17 Gen r)]" is true.

where if the 1st order formula in L(PA), say, GIT1, is defined:

GIT1 <-> Bew_c[(17 Gen r)] /\ Bew_c[Neg(17 Gen r)]

then finally the condensed but technical form of GIT is:

(3) "GIT1" is true

Now, I claim that (3) is a meta statement whose proof of which will
have to depend on the _non-syntactical notion of *truth* of the naturals_.
But you seem to believe otherwise that in (3) 'true' can be discarded
and the proof of (3) can be casted as an "entirely syntactic" one,
just as any FOL proof which is syntactical (and finite).

But so far, you still fail to demonstrate how the casting is done, or
how we could demonstrate the "proving" formal system is syntactically
consistent. [Let's remember that we don't need Godel to syntactically
prove difficult theorems: any of us can prove any formula by _assuming_
[intentionally or not] inconsistent axioms!]
From: Newberry on
On Feb 27, 11:55 am, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote:
> Newberry <newberr...(a)gmail.com> writes:
> > On Feb 27, 10:00 am, "Jesse F. Hughes" <je...(a)phiwumbda.org> wrote:
> >> Even if I do accept that certain sentences involving definite
> >> descriptions without referent are neither true nor false (and I'm not
> >> saying that I accept this), it does not follow that sentences of the
> >> form
>
> >>   (Ax)(Px -> Qx)
>
> >> are meaningless unless (Ex)Px and (Ex)~Qx are true.
>
> > Clarification. The theory of presuppositions teaches that the above
> > sentences are neither true nor false. That a proper subset of such
> > sentences are meaningless is my addition. In fact Strawson's main
> > problem was to explain why an apparently meaningful sentence "All
> > Jonh's children are asleep" is neither true nor false. I would be
> > happy to supply you my paper on this topic.
>
> > Strawson also did NOT include the secong condition  (Ex)~Qx.
>
> But (Ax)(Px -> Qx) is equivalent to (Ax)(~Qx -> ~Px) -- right?

That's what I said. We are thinking remarkably alike.

>  Let's
> call those formulas (1) and (2), resp.
>
> Suppose (Ex)Px and ~(Ex)~Qx, i.e., (Ax)Qx.  Then (2) is (according to
> what you've told me) neither true nor false.  I surely assumed that
> (1) is similarly neither true nor false under the same conditions.
>
> (I also thought that you'd said something similar previously.)

That is my position but apparently not Strawson's.

>
> --
> Jesse F. Hughes
>   "And I will dream that I live underground and people will say, 'How
> did you get there?'  
>   "'I just live there,' I will tell them." -- Quincy P. Hughes, Age 4- Hide quoted text -
>
> - Show quoted text -

From: Nam Nguyen on
Nam Nguyen wrote:
> Frederick Williams wrote:
>> Nam Nguyen wrote:
>>> Frederick Williams wrote:
>>>> Nam Nguyen wrote:
>>>>> [...] And what does your definition have
>>>>> to do with GIT, it being dependent on the naturals as a model of some
>>>>> formal system?
>>>> What exactly is GIT here? As I remarked elsewhere [1], Theorem VI [2]
>>>> is entirely syntactic in its statement and proof.
>>> "entirely in its ... proof"? Really? So which formal system is that
>>> "syntactic proof" in? What are the axioms of that particular formal
>>> system?
>>
>> A good answer would be: read all about in my reference [2]. I call that
>> a good answer because then you'll get precisely what G\"odel had to say,
>> well not _precisely_ because [2] is an English translation of a German
>> work.
>>
>> On the other hand it's not _that_ good an answer because it seems
>> impolite, so here's a quotation from [2, p599] (P is the system in
>> question):
>>
>> P is essentially the system obtained when the logic of PM is
>> superposed upon the Peano axioms^{16} (with the numbers as
>> individuals and the successor relation as primitive notion).
>>
>> G\"odel's footnote 16 reads:
>>
>> The addition of the Peano axioms, as well as all other
>> modifications introduced in the system PM, merely serve to simplify
>> the proof and is dispensable in principle.
>>
>> I do not intend to list the axioms and rules but I will remark that the
>> ramified theory of types is not used.
>
> As AK has alluded to, as well your mentioning above "(P is the system in
> question), as well as what Godel himself wrote:
>
> We proceed now to the rigorous development of the proof sketched above,
> and begin by giving an exact description of the formal system P,
> for which we seek to demonstrate the existence of undecidable
> propositions.
>
> then P is just *a* T under investigation. Without loss of generality,
> we could take ZF as P. Now, you've asked me above "What exactly is GIT
> here?". My answer is that typically when we say GIT we'd refer to GIT1
> which would be, according to Godel's paper (and for all practical
> purposes), the following meta statement:
>
> (1) "Bew_c[(17 Gen r)]" is true _and_ "Bew_c[Neg(17 Gen r)]" is true.
>
> Note in his meta theorem (1) the 2 expressions inside the 2 pairs of
> double quotes (") are FOL formulas written in the language of arithmetic,
> which in modern day consideration is L(PA) but which is _not_ L(ZF)!
>
> The long and short of it is no matter how much syntactical characteristic
> of P (ZF in this example) Godel utilized in his proof of GIT, his proof
> would be done in a formal system, say the "proving" system, that would be
> in general different from the P "in question". Now, let's rephrase (1)
> a bit further:
>
> (2) "Bew_c[(17 Gen r)] /\ Bew_c[Neg(17 Gen r)]" is true.
>
> where if the 1st order formula in L(PA), say, GIT1, is defined:
>
> GIT1 <-> Bew_c[(17 Gen r)] /\ Bew_c[Neg(17 Gen r)]
>
> then finally the condensed but technical form of GIT is:
>
> (3) "GIT1" is true

Between (1) and (3) I had a mistake: it's the negations of Bew_c[(17 Gen r)]
and Bew_c[Neg(17 Gen r)] I meant to use. But my argument is unchanged.
In fact the (genuine) mistake incidentally would serve my purpose here: if
the "proving" system is inconsistent, then it would prove what Godel
intended as well as my unindented mistake!

But how do we demonstrate by _pure syntactical mean_ this "proving" system
is consistent? The answer is we can't, and neither could Godel possible have.

Welcome to the circularity in GIT:

The lone "proving" system is doing no more magic than the "has-to-be-
proven" ones, in so far as the concept of arithmetics of the natural
numbers is concerned!

>
> Now, I claim that (3) is a meta statement whose proof of which will
> have to depend on the _non-syntactical notion of *truth* of the naturals_.
> But you seem to believe otherwise that in (3) 'true' can be discarded
> and the proof of (3) can be casted as an "entirely syntactic" one,
> just as any FOL proof which is syntactical (and finite).
>
> But so far, you still fail to demonstrate how the casting is done, or
> how we could demonstrate the "proving" formal system is syntactically
> consistent. [Let's remember that we don't need Godel to syntactically
> prove difficult theorems: any of us can prove any formula by _assuming_
> [intentionally or not] inconsistent axioms!]
From: Frederick Williams on
Nam Nguyen wrote:

>
> But how do we demonstrate by _pure syntactical mean_ this "proving" system
> is consistent? The answer is we can't, and neither could Godel possible have.

As I remarked, G\"odel had no need to: he assumed omega consistency
which is defined syntactically.

I'll say it again Theorem VI (it's that which I'm talking about and
nothing else) is stated and proved in purely syntactic terms.
Furthermore the proof is carried out in the system P, that's G\"odel's
P. You seem to say in your news:P_fin.119$QL4.116(a)newsfe24.iad that
there are other possible P's. But I was taking about G\"odel's P.
From: Nam Nguyen on
Frederick Williams wrote:
> Nam Nguyen wrote:
>
>> But how do we demonstrate by _pure syntactical mean_ this "proving" system
>> is consistent? The answer is we can't, and neither could Godel possible have.
>
> As I remarked, G\"odel had no need to: he assumed omega consistency
> which is defined syntactically.

Right: that's what you said (and I didn't have a chance to make comment
the last time).

OK syntactical proof means the entire proof is a _finite sequence_
of _finite formulas_. So how did Godel manage to bring _infinitely_
many constant-terms (i.e. numerals), which would be required for
encoding the concept of w-consistency, his "finite" proof?

>
> I'll say it again Theorem VI (it's that which I'm talking about and
> nothing else) is stated and proved in purely syntactic terms.

You just _said_ that but you've not proven it. Anybody could "say"
anything!

> Furthermore the proof is carried out in the system P, that's G\"odel's
> P. You seem to say in your news:P_fin.119$QL4.116(a)newsfe24.iad that
> there are other possible P's. But I was taking about G\"odel's P.

You should really read my recent post again where I said something
about ZF as an example of a P, about "proving" system, and about
what Godel himself said:

>> We proceed now to the rigorous development of the proof sketched above,
>> and _begin by giving an exact description of the formal system P_,
>> _for which_ we seek to demonstrate the _existence of undecidable propositions_.

(The highlight is mine). Do you understand now P is just _a_ system under
investigation, and not in general written in the language where he'd express
the formula such as "~Bew_c[(17 Gen r)] /\ ~Bew_c[Neg(17 Gen r)]"?

Why is so hard for you to understand the distinction between _a_ P and his
alleged "proving" formal system?