The mysterious sentence.

[Antonio Speltzu]

Let R (x, y, z ...) be a n-ary relation and suppose that there exists a formula r (x, y, z ...) of P that "expresses" this relation.
The existential quantification of r in one of its variables "expresses" the relation that results from projecting R onto the other components.
But what happens when there is only one variable left?
The projection of R (x) ceases to make sense and, therefore, what does the existential quantification of r (x) express in this case?
Miracle!!!. (exists x)r (x) goes from expressing a relation to expressing a mysterious sentence of an unknown formal system.

Example:
In proposition XI of Godel's theorem, the formula r(x) of P that "expresses" that x is an unprovable formula, when quantifying it, goes to express the sentence "Ex(x is a unprovable formula)", of no known what formal system.

Where and how this formula is obtained in each case is an absolute mystery.

[Antonio Speltzu]

Similarly, in the same proposition XI the formula of P that "expresses" that x is not a proof of 17 Gen r, when it is universally quantified,
it mysteriously goes on to express the sentence "(for all x) (x is not a proof of 17 Gen r".

Of which formal system it belongs and how it is obtained, Godel did not leave any clue.

[Rupert]

On Saturday, December 4, 2021 at 6:48:33 PM UTC+1, Antonio Speltzu wrote:
> Let R (x, y, z ...) be a n-ary relation and suppose that there exists a formula r (x, y, z ...) of P that "expresses" this relation.
> The existential quantification of r in one of its variables "expresses" the relation that results from projecting R onto the other components.
> But what happens when there is only one variable left?

Then if you project one more time, you get a 0-ary relation which is simply either the constant "true" or the constant "false".

> The projection of R (x) ceases to make sense

No it doesn't.

[Antonio Speltzu]

Curious definition. What would be the result of the projection, "true" or "false" or can you choose or, as in quantum mechanics, do the two states coexist simultaneously?
I begin to understand, quantum mechanics, quantification ...
But suppose you are right. Why does the quantification of r(x) not express in that case "true" or "false" but rather a mysterious sentence of an unknow formal system?

[Rupert]

On Sunday, December 5, 2021 at 9:45:18 AM UTC+1, Antonio Speltzu wrote:
> El domingo, 5 de diciembre de 2021 a las 8:46:07 UTC+1, Rupert escribió:
> > On Saturday, December 4, 2021 at 6:48:33 PM UTC+1, Antonio Speltzu wrote:
> > > Let R (x, y, z ...) be a n-ary relation and suppose that there exists a formula r (x, y, z ...) of P that "expresses" this relation.
> > > The existential quantification of r in one of its variables "expresses" the relation that results from projecting R onto the other components.
> > > But what happens when there is only one variable left?
> > Then if you project one more time, you get a 0-ary relation which is simply either the constant "true" or the constant "false".
> > > The projection of R (x) ceases to make sense
> > No it doesn't.
> Curious definition. What would be the result of the projection, "true" or "false" or can you choose or, as in quantum mechanics, do the two states coexist simultaneously?

We're just talking about the two truth-values of classical logic. If you have a 0-ary relation then either it contains the unique 0-tuple or it doesn't. Not as in quantum mechanics, no.

> I begin to understand, quantum mechanics, quantification ...
> But suppose you are right. Why does the quantification of r(x) not express in that case "true" or "false" but rather a mysterious sentence of an unknow formal system?

Well, you've got r(x) being a formula with one free variable in the language of P, haven't you, so in that case obviously if you precede it by an existential quantifier with the variable x then you'll end up with a sentence in the language of P. And it will be either true or false relative to the standard semantics.

[Antonio Speltzu]

El domingo, 5 de diciembre de 2021 a las 11:46:02 UTC+1, Rupert escribió:
> On Sunday, December 5, 2021 at 9:45:18 AM UTC+1, Antonio Speltzu wrote:
> > El domingo, 5 de diciembre de 2021 a las 8:46:07 UTC+1, Rupert escribió:
> > > On Saturday, December 4, 2021 at 6:48:33 PM UTC+1, Antonio Speltzu wrote:
> > > > Let R (x, y, z ...) be a n-ary relation and suppose that there exists a formula r (x, y, z ...) of P that "expresses" this relation.
> > > > The existential quantification of r in one of its variables "expresses" the relation that results from projecting R onto the other components.
> > > > But what happens when there is only one variable left?
> > > Then if you project one more time, you get a 0-ary relation which is simply either the constant "true" or the constant "false".
> > > > The projection of R (x) ceases to make sense
> > > No it doesn't.
> > Curious definition. What would be the result of the projection, "true" or "false" or can you choose or, as in quantum mechanics, do the two states coexist simultaneously?
> We're just talking about the two truth-values of classical logic. If you have a 0-ary relation then either it contains the unique 0-tuple or it doesn't. Not as in quantum mechanics, no.

What is a 0-tuple, the empty set?

> > I begin to understand, quantum mechanics, quantification ...
> > But suppose you are right. Why does the quantification of r(x) not express in that case "true" or "false" but rather a mysterious sentence of an unknow formal system?
> Well, you've got r(x) being a formula with one free variable in the language of P, haven't you, so in that case obviously if you precede it by an existential quantifier with the variable x then you'll end up with a sentence in the language of P. And it will be either true or false relative to the standard semantics.

Fine, but why do I say that said quantization "expresses" some strange sentence (like in the proposition XI)?
How is said sentence constructed in each case?. What formal system do they belong to?

[Rupert]

On Sunday, December 5, 2021 at 12:14:55 PM UTC+1, Antonio Speltzu wrote:
> El domingo, 5 de diciembre de 2021 a las 11:46:02 UTC+1, Rupert escribió:
> > On Sunday, December 5, 2021 at 9:45:18 AM UTC+1, Antonio Speltzu wrote:
> > > El domingo, 5 de diciembre de 2021 a las 8:46:07 UTC+1, Rupert escribió:
> > > > On Saturday, December 4, 2021 at 6:48:33 PM UTC+1, Antonio Speltzu wrote:
> > > > > Let R (x, y, z ...) be a n-ary relation and suppose that there exists a formula r (x, y, z ...) of P that "expresses" this relation.
> > > > > The existential quantification of r in one of its variables "expresses" the relation that results from projecting R onto the other components.
> > > > > But what happens when there is only one variable left?
> > > > Then if you project one more time, you get a 0-ary relation which is simply either the constant "true" or the constant "false".
> > > > > The projection of R (x) ceases to make sense
> > > > No it doesn't.
> > > Curious definition. What would be the result of the projection, "true" or "false" or can you choose or, as in quantum mechanics, do the two states coexist simultaneously?
> > We're just talking about the two truth-values of classical logic. If you have a 0-ary relation then either it contains the unique 0-tuple or it doesn't. Not as in quantum mechanics, no.
> What is a 0-tuple, the empty set?

Yeah sure. Like an ordered n-tuple, only in the case n=0. It would usually be defined to be the empty set, yes.

> > > I begin to understand, quantum mechanics, quantification ...
> > > But suppose you are right. Why does the quantification of r(x) not express in that case "true" or "false" but rather a mysterious sentence of an unknow formal system?
> > Well, you've got r(x) being a formula with one free variable in the language of P, haven't you, so in that case obviously if you precede it by an existential quantifier with the variable x then you'll end up with a sentence in the language of P. And it will be either true or false relative to the standard semantics.
> Fine, but why do I say that said quantization "expresses" some strange sentence (like in the proposition XI)?
> How is said sentence constructed in each case?. What formal system do they belong to?

Well, you've been given the details of how the sentence is constructed (or at least I've done my very best to explain).

[Antonio Speltzu]

El domingo, 5 de diciembre de 2021 a las 17:00:30 UTC+1, Rupert escribió:
> On Sunday, December 5, 2021 at 12:14:55 PM UTC+1, Antonio Speltzu wrote:
> > El domingo, 5 de diciembre de 2021 a las 11:46:02 UTC+1, Rupert escribió:
> > > On Sunday, December 5, 2021 at 9:45:18 AM UTC+1, Antonio Speltzu wrote:
> > > > El domingo, 5 de diciembre de 2021 a las 8:46:07 UTC+1, Rupert escribió:
> > > > > On Saturday, December 4, 2021 at 6:48:33 PM UTC+1, Antonio Speltzu wrote:
> > > > > > Let R (x, y, z ...) be a n-ary relation and suppose that there exists a formula r (x, y, z ...) of P that "expresses" this relation.
> > > > > > The existential quantification of r in one of its variables "expresses" the relation that results from projecting R onto the other components.
> > > > > > But what happens when there is only one variable left?
> > > > > Then if you project one more time, you get a 0-ary relation which is simply either the constant "true" or the constant "false".
> > > > > > The projection of R (x) ceases to make sense
> > > > > No it doesn't.
> > > > Curious definition. What would be the result of the projection, "true" or "false" or can you choose or, as in quantum mechanics, do the two states coexist simultaneously?
> > > We're just talking about the two truth-values of classical logic. If you have a 0-ary relation then either it contains the unique 0-tuple or it doesn't. Not as in quantum mechanics, no.
> > What is a 0-tuple, the empty set?
> Yeah sure. Like an ordered n-tuple, only in the case n=0. It would usually be defined to be the empty set, yes.

So as you say above a 0-ary relation is either {} (the empty set) or {{}} (the set that contains the empty set).
But you also say above that a 0-ary relation is the constant "true" or "false".
So I deduce that either {} = "true" and {{}} = "false" or vice versa.

> > > > I begin to understand, quantum mechanics, quantification ...
> > > > But suppose you are right. Why does the quantification of r(x) not express in that case "true" or "false" but rather a mysterious sentence of an unknow formal system?
> > > Well, you've got r(x) being a formula with one free variable in the language of P, haven't you, so in that case obviously if you precede it by an existential quantifier with the variable x then you'll end up with a sentence in the language of P. And it will be either true or false relative to the standard semantics.
> > Fine, but why do I say that said quantization "expresses" some strange sentence (like in the proposition XI)?
> > How is said sentence constructed in each case?. What formal system do they belong to?
> Well, you've been given the details of how the sentence is constructed (or at least I've done my very best to explain).

Yes, but not how the sentence that it "expresses" is constructed.
You refuse to accept the obvious.

[Rupert]

Well, I was telling you that if it's a sentence (that is, a 0-ary predicate), then it "expresses" a 0-ary relation, and there are only two of those, and you can think of them as the truth-values True and False, and of course in the event that P is consistent it would be True.

[Khong Dong]

So consider the FOL _syntactical_ axiom:

(*) ~("There is zero prime" \/ "There are finitely many primes" \/ "There are infinitely many primes").

What does (*) _semantically_ "express"? And is (*) "true" of a model M (and if so which M)?

[Khong Dong]

Just in case, the relevant definition is:

𝑝𝑟𝑖𝑚𝑒(𝑝) ↔ ∃𝑧∃𝑜∀𝑥∀𝑢∀𝑣[(𝑧∗𝑥=𝑧) ⋀ (𝑜∗𝑥=𝑥) ⋀ ¬(𝑧=𝑜) ⋀ ¬(𝑧=𝑝) ⋀ ¬(𝑜=𝑝) ⋀ ((𝑝=𝑢∗𝑣) → (𝑢=𝑜 ⋁ 𝑣=𝑜))].

[Khong Dong]

And just to go deeper into Gödel's semantical-truth failure, suppose we have (can define) some unary predicate symbol 'abcPrime(n)' solely as a definable expression written in L({(*)}), and as a function of the definition 𝑝𝑟𝑖𝑚𝑒(𝑝), would you be able to scratch out a proof-design for

(***) ({(*)} |- (**))

where

(**) "There are finitely many primes p which are abcPrime(p)"

?

Or isn't it true that

undecide({(*)} |- (**))

while you'd (Rupert) acknowledge that Gödel's Completeness thesis still fails in this case for {(*)}?

[Khong Dong]

> And just to go deeper into Gödel's semantical-truth failure, suppose we have (can define) some unary predicate symbol 'abcPrime(n)' solely as a definable expression written in L({(*)}), and as a function of the definition 𝑝𝑟𝑖𝑚𝑒(𝑝), would you be able to sketch out a proof-design for

>
> (***) ({(*)} |- (**))
>
> where
>
> (**) "There are finitely many primes p which are abcPrime(p)"
>
> ?

It goes without saying that L({(*)}) = L(<,*).

[Antonio Speltzu]

You do not find out. That's not the problem.
The problem is how you go, in proposition XI, from a relation to a sentence, by quantifying the formula of P that represents the relation:
From the relation "x is a non-demonstrable formula" to the sentence "there is a non-demonstrable formula"
From the relation "x is not a proof of 17 Gen r" to the sentence "17 Gen r is not provable"
How are those sentences constructed?

What formal system do they belong to?

What is the link with relations?

[Rupert]

How do you express "there are finitely many" and "there are infinitely many"? (Those can not in fact be expressed in first-order languages, but if you're working in the standard model, you could do it, sure.)

[Rupert]

Well, we've been through it quite a few times, I don't get which bit you don't yet understand.

> What formal system do they belong to?

Our object theory is P.

[Antonio Speltzu]

The one who doesn't understand is me.
If "P is consistent" or "17 Gen r is not provable" are formulas of P, why does Godel speak in proposition XI of the formulas of P that "express" them?

[Rupert]

Well, of course the string of symbols "P is consistent" is not a formula of P, but there is a sentence in the language of P (and I thought I'd *finally* got you to understand which one it was) which "says" that P is consistent. In the sense that it says that there exists at least one sentence in the language of P which is not provable in P.

[Antonio Speltzu]

It seems that we are understanding each other.
There is a formula of P that says, expresses "P is consistent", right.
What I ask is what is the expression "P is consistent".
Is it a sentence? From what formal system? How is built? Where does it come from?
You yourself say that it does not belong to P.

[Rupert]

Well, that's a sentence in English with a symbol P that denotes a particular formal system.

[Antonio Speltzu]

Then the formula of P, let's call it r(x), which expresses, represents the relation "x is a non-demonstrable formula of P",
when quantifying it goes on to express the sentence in English "P is consistent" or
"there is a non-demonstrable formula in P "if you want. Is this right?
Magical transformation !!.
How do you get the sentence in English from the relation?
Is there some logical-mathematical function, that I do not know, that performs such a transformation?

[Rupert]

Consider the formula with one free variable Bew(x) which expresses "x is the Gödel number of a formula which is provable in P". And consider the formula with one free variable Form(x) which expresses "x is the Gödel number of a formula in the language of P".

Now consider the sentence (Ex)(Form(x) & ~Bew(x)). This is the sentence of which Gödel says, loosely speaking, that it is the sentence which "says" that P is consistent.

You've been told this often enough, of course. It is explained in the paper.

[Julio Di Egidio]

On Monday, 6 December 2021 at 14:08:48 UTC+1, Rupert wrote:
> On Monday, December 6, 2021 at 1:56:00 PM UTC+1, Antonio Speltzu wrote:
> > El lunes, 6 de diciembre de 2021 a las 13:18:21 UTC+1, Rupert escribió:
> > > On Monday, December 6, 2021 at 1:16:25 PM UTC+1, Antonio Speltzu wrote:

<snip>

> > Is there some logical-mathematical function, that I do not know, that performs such a transformation?

You have been explained the relationship of the semantics (PM) to the syntax (P) few times already by
now: it's in the paper.

> Consider the formula with one free variable Bew(x) which expresses "x is the Gödel number of a formula
> which is provable in P". And consider the formula with one free variable Form(x) which expresses "x is the
> Gödel number of a formula in the language of P".
>
> Now consider the sentence (Ex)(Form(x) & ~Bew(x)). This is the sentence of which Gödel says, loosely
> speaking, that it is the sentence which "says" that P is consistent.

Informally, it rather says <exists x s.t. ("the formula whose G-number is x") is not "provable"> which is
incompleteness: consistency is a consequence.

> You've been told this often enough, of course. It is explained in the paper.

Yes, and, crucially, since I think this is another point easily missed: 'Bew', of all those definitions, is the
one that is *not* recursive: indeed, if system P could prove its own incompleteness/consistency...

Julio

[Khong Dong]

Apparently you're unable to literally write down the _syntactical_ axiom (*). (I did inform before you *multiple times* how to spell out the three sentences in quotes of (*).)

> (Those can not in fact be expressed in first-order languages,

Again I did write down the three sentences of (*) for you before.

> but if you're working in the standard model, you could do it, sure.)

You seem to have failed to notice my " _syntactical_ axiom". Why?

[Rupert]

I recall reading your definitions before, yes, I'd have to refresh my memory. What I said was correct, and I made a conjecture about what you have in mind. Why don't you just say once again what you have in mind?

[Khong Dong]

OK. Here they are:

Assuming a syntactical unary predicate symbol P:

- "There exists no 𝑥 which 𝑃(𝑥)", denoted by '(0)𝑃(∗)', is defined as:
(0)𝑃(∗) ↔ ∀𝑥[¬𝑃(𝑥)].
- "There exist infinitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑎𝐼)𝑃(∗)', is defined in an anti induction form as:
(𝑎𝐼)𝑃(∗) ↔ ∃𝑥[𝑃(𝑥)] ⋀ ∀𝑥∃𝑦[𝑃(𝑥) → (𝑃(𝑦) /\ (𝑥 < 𝑦))].
- "There exist finitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗)', is defined as:
(𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗) ↔ ¬(0)𝑃(∗) ⋀ ~(𝑎𝐼)𝑃(∗).

I've also given the definition for the syntactical unary predicate symbol 'prime'. So now you have the full wff (*) written. Would you now be able to answer my questions:

What does (*) _semantically_ "express"? And is (*) "true" of a model M (and if so which M)? [Note again the underlying language is L(<,*)].

[Rupert]

Well, I can't be bothered typing out an English version of what it says, that's a waste of time. Since it's a tautology in propositional logic it's true in all models.

[Khong Dong]

So you've failed to write out in English a _correct_ short sentence (one or no more than two lines) semantically expressing (*).

> Since it's a tautology in propositional logic it's true in all models.

Again, you've also failed to understand the *genuine difference* between "semantics" and "truth" of a sentence: the formal *on its own* has nothing to do with the later.

Let me point out what (*) would express, would be interpreted: There exists _no_ language structure -- hence model -- for (*).

Hope that has helped.

[Nam Nguyen]

I don't think, Rupert, one in the right mind is able to understand why you had to refuse acknowledging the obvious (as it seems to have been the case).

It's just a matter of wording but (*) clearly expresses/states (clearly can be interpreted as) that the subset -- containing primes -- of the underlying _nonempty_ domain of discourse U is neither empty, nor finite, nor infinite!

What kind of _nonempty_ universe U would _you_ think could have such kind of subset?

[Julio Di Egidio]

On Monday, 6 December 2021 at 17:38:13 UTC+1, khongdo...@gmail.com wrote:
> On Monday, 6 December 2021 at 03:12:51 UTC-7, Rupert wrote:
> > On Sunday, December 5, 2021 at 10:10:56 PM UTC+1, khongdo...@gmail.com wrote:
> > > On Sunday, 5 December 2021 at 11:31:13 UTC-7, Rupert wrote:
> > > > On Sunday, December 5, 2021 at 5:33:28 PM UTC+1, Antonio Speltzu wrote:

> > > So consider the FOL _syntactical_ axiom:

The *FOL* *statement*: it's neither an axiom nor saying "syntactical" adds anything there.

> > > (*) ~("There is zero prime" \/ "There are finitely many primes" \/ "There are infinitely many primes").
> > >
> > > What does (*) _semantically_ "express"? And is (*) "true" of a model M (and if so which M)?
>
> > How do you express "there are finitely many" and "there are infinitely many"?
>
> Apparently you're unable to literally write down the _syntactical_ axiom (*).

Either there are no primes, or there are finitely many, or there are infinitely many: so, either you know of a forth case out of this world, or that statement is identically *false* in any possible and conceivable model.

Julio

[Antonio Speltzu]

What a mess!
Godel doesn't say that because (Ex)(Form(x) & ~Bew(x)) is precisely the definition of the consistency of P.
What Godel says is that there is a statement of P, which he calls w, which expresses "(Ex)(Form(x) & ~Bew(x))" or "P is consistent".

[Khong Dong]

Well then you and Rupert must admit the consistent theory {(*)} has zero model since, as you and he basically have said, its lone axiom (*) is "*false* in any possible and conceivable model". No?

>
> Julio

[Julio Di Egidio]

On Monday, 6 December 2021 at 20:51:07 UTC+1, khongdo...@gmail.com wrote:
> On Monday, 6 December 2021 at 11:45:36 UTC-7, Rupert wrote:
> > On Monday, December 6, 2021 at 7:09:08 PM UTC+1, khongdo...@gmail.com wrote:

<snipped>

> > > OK. Here they are:
> > > Assuming a syntactical unary predicate symbol P:
> > > - "There exists no 𝑥 which 𝑃(𝑥)", denoted by '(0)𝑃(∗)', is defined as:
> > > (0)𝑃(∗) ↔ ∀𝑥[¬𝑃(𝑥)].
> > > - "There exist infinitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑎𝐼)𝑃(∗)', is defined in an anti induction form as:
> > > (𝑎𝐼)𝑃(∗) ↔ ∃𝑥[𝑃(𝑥)] ⋀ ∀𝑥∃𝑦[𝑃(𝑥) → (𝑃(𝑦) /\ (𝑥 < 𝑦))].
> > > - "There exist finitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗)', is defined as:
> > > (𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗) ↔ ¬(0)𝑃(∗) ⋀ ~(𝑎𝐼)𝑃(∗).
> > > I've also given the definition for the syntactical unary predicate symbol 'prime'.
> > > So now you have the full wff (*) written. Would you now be able to answer my questions:
> > > What does (*) _semantically_ "express"?

> > Well, I can't be bothered typing out an English version of what it says, that's a waste of time.
> So you've failed to write out in English a _correct_ short sentence (one or no more than two lines) semantically expressing (*).

Since you have actually already presented it in English (along with some hints at a FOL rendition), it's not even clear why you would then make such demands for translation into English, and even less clear is why Rupert would have any trouble with it, unless he has completely misread the whole thing, which is plausible given he said your statement is true, which of course it isn't.

> > Since it's a tautology in propositional logic it's true in all models.

(Eh?? You sure?)

> Again, you've also failed to understand the *genuine difference* between "semantics" and "truth" of a sentence: the formal *on its own* has nothing to do with the later.

Please explain: how is now semantics, formal or not, *not* defining what is "truth" for an object theory?

> Let me point out what (*) would express, would be interpreted: There exists _no_ language structure -- hence model -- for (*).

That's not an interpretation, I have given the/an interpretation in my other post, that's only its evaluation. And yeah, it's plan false, so what??

Julio

[Antonio Speltzu]

What a mess!
Godel doesn't say that because (Ex) (Form (x) & ~ Bew (x)) (there is a non-demonstrable formula) is precisely the definition of the consistency of P.
What Godel says is that there is a sentence of P, which he calls w, which expresses "(Ex) (Form (x) & ~ Bew (x))" or "P is consistent".

[Khong Dong]

Semantically, (*) would express that the set of primes -- being a subset of the *non*empty domain of discourse U -- is neither empty, nor finite, nor infinite.

What _kind of subset_ would _you_ think that be?

[Julio Di Egidio]

(You reply to yourself now?) No: what kind of "axiom" would that be! And if you add it to, or make out of it, an *arithmetic* theory (not just "FOL", which is just the language) it is a *false* arithmetic statement and axiom and you get a false theory (not correct), even if consistent...

Julio

[Khong Dong]

Well then according to you, (*) is also true in a model in which its _negation_ ~(*) is true. That's a contradiction, Rupert.

[Julio Di Egidio]

On Tuesday, 7 December 2021 at 04:36:42 UTC+1, khongdo...@gmail.com wrote:

> Well then according to you, (*) is also true in a model in which its _negation_ ~(*) is true. That's a contradiction, Rupert.

Of course you'll just keep going ad nauseam---

*Plonk*

Julio

[Rupert]

I chose not to bother, yes, because it was a boring and pointless task.

> > Since it's a tautology in propositional logic it's true in all models.
> Again, you've also failed to understand the *genuine difference* between "semantics" and "truth" of a sentence: the formal *on its own* has nothing to do with the later.
>
> Let me point out what (*) would express, would be interpreted: There exists _no_ language structure -- hence model -- for (*).
>
> Hope that has helped.

Yes, okay, thank you, so I missed the negation sign out the front, all right then it's a negation of a tautology and it's not true in any model.

[Rupert]

Yes, but the point is he's telling you exactly which sentence he means, isn't he? He's assuming that you'll agree that it's self-evident that, philosophically and somewhat vaguely speaking, it states that P is consistent, but whether you agree with that part of it doesn't matter, because that's not part of the mathematical part of the argument, as I tell you over and over again.

[Antonio Speltzu]

What is the mathematical part of the argument, then?
That 17 Gen r "expresses" its own indemonstrability? Sure?

[Rupert]

I went through this a number of times before. I'm over it now.

[Antonio Speltzu]

I know some of us go when you come back. But I thought you could help a neophyte.

[Khong Dong]

So the theory {(*)} has no model even if it's _syntactically_ consistent, still invalidating Gödel's Completeness thesis, you'd acknowledge. Agree?

[Rupert]

Why would you get the idea that it's syntactically consistent? I would say that I can derive a contradiction from (*) even just in classical propositional logic.

[Khong Dong]

Note my "even if ".

> Why would you get the idea that it's syntactically consistent?

Why would you get the idea that it's _syntactically_ inconsistent?

> I would say that I can derive a contradiction from (*) even just in classical propositional logic.

I'd say that you can't produce the syntactical proof ({(*)} |- ~(n=n)) without relying on non syntactical-proof theoretical knowledge (e.g. propositional logic) then you're not making sense at all.

Syntactical inconsistency requires syntactical proof strictly via rules of inference.

Btw, why do you believe, as you seem to have, that ~(*) _syntactically_ is a logical axiom/theorem?

[Rupert]

It's obvious.

> > I would say that I can derive a contradiction from (*) even just in classical propositional logic.
> I'd say that you can't produce the syntactical proof ({(*)} |- ~(n=n)) without relying on non syntactical-proof theoretical knowledge (e.g. propositional logic) then you're not making sense at all.

Of course I can produce a "syntactical proof". We've been through all this before and I'm quite sure Jim Burns gave you one.

>
> Syntactical inconsistency requires syntactical proof strictly via rules of inference.
>
> Btw, why do you believe, as you seem to have, that ~(*) _syntactically_ is a logical axiom/theorem?

Because it's obvious. (*) is clearly the negation of a tautology.

[Khong Dong]

That's your technical shortcoming.

In FOL syntactical paradigm, we don't have semantical/truth-value-theoretical "tautology": we have instead syntactical Propositional axioms (Shoenfield's pg. 21).

Syntactical proof definition has no tautology, syntactical proof definition needs no tautology. If you know how syntactical proof is defined.

You might want to go and read Shoenfield's pg. 204 to see how he _syntactically_ proves theorem N9 in his PA (P) -- _without_ the word "truth"/"truth-table"/"tautology"/"propositional logic" or the like of "semantic".

(Isn't it true in sci.logic a mathematician [CM, iirc] once mentioned something to the effect that you can use rules of inference to produce a theorem without caring whether or not the theorem has any semantics or truth value?)

[Khong Dong]

If you notice there on pg. 21, you'll see Shoenfield using multiple times "of the form" -- syntactical form mind you -- and not "of the truth value or tautology".

Please don't fight for a loosing "war"/cause, Rupert. There's the ABC war facing you and others ... (Just saying out loud).

[Rupert]

What I mean by "tautology" is that if you treat all quantified subformulas as propositional atoms, then you get a propositional formula which is tautologous, that is, the standard semantics assigns it the truth value "true" under any truth valuation.

> Syntactical proof definition has no tautology, syntactical proof definition needs no tautology. If you know how syntactical proof is defined.
>
> You might want to go and read Shoenfield's pg. 204 to see how he _syntactically_ proves theorem N9 in his PA (P) -- _without_ the word "truth"/"truth-table"/"tautology"/"propositional logic" or the like of "semantic".

I'm fine.

[Khong Dong]

People know what you irrelevantly meant: "truth valuation" instead of proof-proving.

> > Syntactical proof definition has no tautology, syntactical proof definition needs no tautology. If you know how syntactical proof is defined.
> >
> > You might want to go and read Shoenfield's pg. 204 to see how he _syntactically_ proves theorem N9 in his PA (P) -- _without_ the word "truth"/"truth-table"/"tautology"/"propositional logic" or the like of "semantic".

> I'm fine.

You're not. You're confused between proof and truth.

[Julio Di Egidio]

On Wednesday, 8 December 2021 at 07:27:26 UTC+1, Rupert wrote:
> On Tuesday, December 7, 2021 at 9:00:31 PM UTC+1, khongdo...@gmail.com wrote:
> > On Tuesday, 7 December 2021 at 11:51:07 UTC-7, Rupert wrote:

<snip>

> What I mean by "tautology" is that if you treat all quantified subformulas as propositional atoms, then you get a propositional formula which is tautologous, that is, the standard semantics assigns it the truth value "true" under any truth valuation.
> > Syntactical proof definition has no tautology, syntactical proof definition needs no tautology. If you know how syntactical proof is defined.
> >
> > You might want to go and read Shoenfield's pg. 204 to see how he _syntactically_ proves theorem N9 in his PA (P) -- _without_ the word "truth"/"truth-table"/"tautology"/"propositional logic" or the like of "semantic".
>
> I'm fine.

Your reply to Antonio is even more and truly *ridiculous*...

You are an incompetent asshole and a nasty spammer selling the usual broken products for the masses. And the rest of the time you flood the channel with ignoble polemics ad nauseam with the local nut cases, lest any significant post not go unnoticed...you retarded cunt and yet another fucking disgrace.

*Plonk*

Julio

[Julio Di Egidio]

For once I agree with you, he is a total fucking disgrace.

Julio

[Rupert]

You seem to have somehow got the idea that my contributions to this newsgroup are substantially lower quality or more pointless than yours. This is incorrect.

[Rupert]

All tautologies are provable in both classical propositional calculus and also classical first-order logic. Because classical propositional calculus is semantically complete and is a sublogic of first-order logic. This most definitely would be covered in Shoenfield.

[Julio Di Egidio]

A totally gratuitous retort as usual: indeed, I know more logic and everything than you retarded cunt can even guess!! ESAD.

*Plonk*

Julio

[Julio Di Egidio]

I has said ridiculous, I should be clearer around here: you are TOTALLY WRONG on everything that in fact counts, from the role of semantics in GIT that you keep misguidedly and eventually plainly wrong downplaying, to what first-order even means...

You fucking twisted asshole, here is a suggestion for you: first, get the fuck out of Usenet, it's not good for you and even less for the planet; second, stop taking those pills and eating that shit for a change, that stuff is *not* good for your health, your health is, indeed and contra the brain-washing and plain nazism, in *your* hands...

And now get the fuck out of here, the hotel for the retarded cunts is round the corner, and it's never full...

*Plonk*

Julio

[Rupert]

I think it's, on the whole, pretty fair to say that you have not been specific about what shortcomings you see in my posts.

[Julio Di Egidio]

> I think it's, on the whole, pretty fair to say that you have not been specific about what shortcomings you see in my posts.

Translation: you are pretty confident the casual reader won't be able to discern, and will have to trust your pedigree against my spitting on any pedigree... you fucking fraud proper.

Fuck you Rupert and the whole insane nazi brigade.

(EOD.)

*Plonk*

Julio

[Jim Burns]

Your (JDE's) end of this "debate", which you now are
alleging you are ending, could be replaced by a
simple script that randomly selects insults from
some sort of collection.

It would probably be worth your while to write such
a script. It couldn't take more than a few minutes.
I'm not sure, at this moment, where to get a collection
of insults, but I have confidence in you, in this regard.

Then you could go off and pursue some more satisfying
goal, secure in the knowledge that we fiends of sci.logic
will not be left uninsulted.

> *Plonk*

I'm assuming you haven't already done this.

[Julio Di Egidio]

On Wednesday, 8 December 2021 at 09:27:28 UTC+1, Jim Burns wrote:
> On 12/8/2021 2:57 AM, Julio Di Egidio wrote:

> > Fuck you Rupert and the whole insane nazi brigade.
> >
> > (EOD.)
>
> Your (JDE's) end of this "debate", which you now are
> alleging you are ending, could be replaced by a
> simple script that randomly selects insults from
> some sort of collection.

Of course just some more gratuitous libel and the systematic
rewriting of history: as you too won't but keep confirming
yourself yet another resident disgrace and retarded agent of
enemy.

*Troll Alert*

Julio

[Khong Dong]

On Wednesday, 8 December 2021 at 01:27:28 UTC-7, Jim Burns wrote:
> On 12/8/2021 2:57 AM, Julio Di Egidio wrote:
> > On Wednesday, 8 December 2021 at 08:08:51 UTC+1,
> > Rupert wrote:

> > (EOD.)

> Your (JDE's) end of this "debate", which you now are
> alleging you are ending, could be replaced by a
> simple script that randomly selects insults from
> some sort of collection.

Not sure if I'd use every words JDE has but Rupert has brought insults to himself.

It appears Rupert wasn't honest when refused to acknowledge ~(*) isn't a logical theorem _syntactically_ provable from the few logical axioms on Shoenfield's pg. 21. All Rupert had was disingenuously repeating the buzzword "obvious" (or the like of semantical truth). Ditto for his failure in his alleged {(*)} being _syntactically_ inconsistent (he couldn't _syntactically_ prove it).

He's not competent in mathematical logic (FOL), so he should stop being disingenuous with his "obvious" day in day out.

[Rupert]

We're having one of these moments where you're demanding that someone to do a tedious and pointless exercise for you (which has actually already been done anyway), without you paying them any money, and if they won't do it for free you'll say they're being dishonest in claiming that they can do it.

[Khong Dong]

Just more piling of disingenuous utterances.

[Khong Dong]

Can I cite your name, Rupert, in other fora in informing them (asking them about) that you can, from the few logical axioms on Shoenfield's pg. 21, _syntactically_ prove ~(*) is a logical theorem?

[Rupert]

I'm not hugely keen, but if you absolutely have to, then yeah sure, as long as you also clarify that that's where we're working with these definitions (quoted from you above):

- "There exists no 𝑥 which 𝑃(𝑥)", denoted by '(0)𝑃(∗)', is defined as:
(0)𝑃(∗) ↔ ∀𝑥[¬𝑃(𝑥)].
- "There exist infinitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑎𝐼)𝑃(∗)', is defined in an anti induction form as:
(𝑎𝐼)𝑃(∗) ↔ ∃𝑥[𝑃(𝑥)] ⋀ ∀𝑥∃𝑦[𝑃(𝑥) → (𝑃(𝑦) /\ (𝑥 < 𝑦))].
- "There exist finitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗)', is defined as:
(𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗) ↔ ¬(0)𝑃(∗) ⋀ ~(𝑎𝐼)𝑃(∗).

Because it's trivial, isn't it. Let me prove it for you right now.

~(*) is ~~((0)P(*) or (aI)P(*) or (~(0)P(*) and ~(aI)P(*)))

and we're using Shoenfield's definition of "and" which is on page 17, he says "A and B" abbreviates "not (A implies not B)", and "A implies not B" abbreviates "(not-A or B)", so we get "A and B" abbreviates "not (not A or not B)".

So I have "not p or p" is always a logical axiom, and I can infer "q or p" from p, and I can infer p from "p or p", I can infer "(p or q) or r" from "p or (q or r)", and I can infer "q or r" from "p or q" and "nor p or r", and I have to show you that "not not (p or q or (~p and ~q))", that's "not not (p or q or ~(~~p or ~~q))" when you disabbreviate it, is always a theorem, because the one you want me to show is a theorem is an instance of that one. Okay, is that all right? I've stated the axiom schema and all the inference rules going from Shoenfield on p. 21, and I've given you the propositional schema which I have to prove is such that every instance is a theorem. Now then. Go to Lemma 2 on p. 28 of Shoenfield, a complete proof of that lemma is given there, it says that if a propositional formula is a tautology then it's a theorem. This propositional formula is clearly a tautology, it's clear that it's true under every possible assignment of truth values to p and q, using the standard semantics. So it must be a theorem. Good. Now we're done. Happy now?

[Khong Dong]

No I don't see it, perhaps because I read too much into:

<quote>
We emphasize that defined symbols are _not_ symbols of the language, and that defined formulas are _not_ formulas of the language. Moreover, when we say anything about a defined formula, we are really talking the formula of then language which it abbreviates (provided that it makes any difference).
</quote>

(https://www2.karlin.mff.cuni.cz/~krajicek/shoenfield.pdf, pg. 6)

Again, "defined formulas are _not_ formulas of the language".

> I've stated the axiom schema and all the inference rules going from Shoenfield on p. 21, and I've given you the propositional schema which I have to prove is such that every instance is a theorem.

Shoenfield's _nonlogical_ axiom N8

(N8) (𝑥 < 𝑆𝑦) ↔ (𝑥 < 𝑦) ⋁ (𝑥 = 𝑦)

comprises of two independent _nonlogical_ axioms one of which is, say, N8a

(N8a) ¬(𝑥<𝑆𝑦) ⋁ (𝑥<𝑦) ⋁ (𝑥=𝑦)

which of course is a full formula -- not a defined one -- in the underlying language. But in form, (N8a) is a disjunction of three disjuncts, just like my ~(*).

You're not saying Shoenfield's N8a (or even N8) is a logical theorem, are you?

> Now then. Go to Lemma 2 on p. 28 of Shoenfield, a complete proof of that lemma is given there, it says that if a propositional formula is a tautology then it's a theorem. This propositional formula is clearly a tautology, it's clear that it's true under every possible assignment of truth values to p and q, using the standard semantics. So it must be a theorem. Good. Now we're done. Happy now?

No, we're not there yet, because you haven't been able to show ~(*) -- as a formal-language formula (NOT a defined one) of L(<,*) -- is a logical theorem.

Very ... very far from it.

[Khong Dong]

> We emphasize that defined symbols are _not_ symbols of the language, and that defined formulas are _not_ formulas of the language. Moreover, when we say anything about a defined formula, we are really talking the formula of the language which it abbreviates (provided that it makes any difference).
> </quote>

(Minor typo correction in the above.)

[Rupert]

But for your ~(*), as we've noted, the third disjunct has a particular relationship to the first two.

[Khong Dong]

Then again "defined formulas are _not_ formulas of the language" and non-logicality (or not) would rest only on formulas of the language. So you haven't shown any logical theorem yet.

The point of showing N8, N8a is to alert you in this case the non-logical theorem-hood doesn't come from the form of the formula, but from the fact that a function (e.g. 'S') can always logically connote/induces a relation (e.g. '<') but not necessarily the other way around, hence ↔ signifies a non-logicality relationship among all three formulas involved.

The case of ~(*) is similar: it's not the form of the defined formula that causes the non-logicality, but the actual formal language symbols '<', '*' viz-a-viz the definition of 'prime' given that are the culprits.

[Rupert]

My reading of Shoenfield in the bit you quote is that if you have a meta-language expression with abbreviations, it should be taken to refer to an unabbreviated formula in the object language. Nothing I said is inconsistent with that.

> The point of showing N8, N8a is to alert you in this case the non-logical theorem-hood doesn't come from the form of the formula, but from the fact that a function (e.g. 'S') can always logically connote/induces a relation (e.g. '<') but not necessarily the other way around, hence ↔ signifies a non-logicality relationship among all three formulas involved.
>
> The case of ~(*) is similar: it's not the form of the defined formula that causes the non-logicality, but the actual formal language symbols '<', '*' viz-a-viz the definition of 'prime' given that are the culprits.

Well, I've explained the issue to you.

[Khong Dong]

Do you now concede/acknowledge that you haven't been able to syntactically prove ~(*), as written in L(<,*), is a logical theorem?

[Rupert]

Of course not, why on earth would I concede that? I've given you a perfectly good proof if you're willing to use a lemma from Shoenfield. I could also give you a more direct proof without too much trouble if I could be bothered. It comes from the way you've defined your notation. I agree that you could easily enough offer different definitions so that then we'd be able to say that as you've defined it it's not a logical theorem. But given the definitions of the notation that you've actually given, it is a logical theorem, definitely, and I've explained to you why that is clearly enough.

[Khong Dong]

Apparently you're being disingenuous again. The last time you "could be bothered" with the expected _syntactical proof_ from Shoenfield's logical axioms (pg. 21) you had this "proof":

https://groups.google.com/g/sci.logic/c/FgfGh9FinYc/m/YAS6r2rGAAAJ

which is invalid and that has been clearly explained to you.

In fine, you've repeatedly failed to syntactically prove ~(*), as written in L(<,*), to be a logical theorem.

[Again, forget about Shoenfield's Lemma 2 on p. 28: We're not there yet, until you successfully syntactically prove ~(*), as written in L(<,*), is a logical theorem].

[Rupert]

No, it hasn't. There's nothing wrong with that proof. The only thing I recall you saying is something about a convention that Shoenfield makes about using abbreviations in meta-linguistic expressions. That's neither here nor there. That proof is fine.

> In fine, you've repeatedly failed to syntactically prove ~(*), as written in L(<,*), to be a logical theorem.
>
> [Again, forget about Shoenfield's Lemma 2 on p. 28: We're not there yet, until you successfully syntactically prove ~(*), as written in L(<,*), is a logical theorem].

You can recover a complete so-called "syntactical" proof from working through the proof of that Lemma 2 together with what I gave you. I could do that easily enough. But I am not your slave. There is no good reason why I should do monkey tricks for you on demand for free.

If you had any mathematical ability at all, and if you have a copy of Shoenfield, then you yourself could follow through the proof of Lemma 2 and re-construct the "syntactical" proof for yourself. It is a trivial exercise in classical propositional logic.

[Khong Dong]

"monkey"? "any mathematical ability at all"? What a dishonest, incompetent monkey-retort you've uttered.

Listen. In this analogy (to Shoenfield's passage about _defined formula_ being _not_ a formula of the language)

"prime(n) \/ ~prime(n)".replaceAll("prime(n) \/ ~prime(n)", "n=n" /\ "~n=n")

the defined expression

"prime(n) \/ ~prime(n)"

is just a _subjective_ alias for (replaceable by) the actual formal language formula

"n=n" /\ "~n=n"

which in no way on earth or in heaven is a logical theorem. Duh!

You have to replace ~(*) by _formal symbols_ of L(<,*) before you even have a (zero) chance to prove via syntactical logical axioms (pg. 21) that it is a logical theorem. Which for the record you've so far literally failed to accomplish. So honestly admit your failure and stop your "monkey" (your word) disingenuous B.S.

[Rupert]

The meta-linguistic expression stands for an un-abbreviated formula of the object language, is what he means. The un-abbreviated formula of the object language, of course, can still be a logical theorem.

[Khong Dong]

You've been told what he meant: "defined formulas are _not_ formulas of the language". And what "are _not_ formulas of the language" (Shoenfield's words) obviously can't be validly taken to be a logical formula of the language.

> The un-abbreviated formula of the object language, of course, can still be a logical theorem.

Trust but verify. (You once had a failed "obvious" proof.)

So now prove it (your "can still be a logical theorem"): successfully syntactically prove ~(*), as written in L(<,*), is a logical theorem. You haven't proved that.

[Khong Dong]

And you're supposed to (only) strictly use the logical axioms on pg. 21, not Lemma 2 pg .28 (or wherever else).

[Rupert]

This idea of yours that I am "supposed" to perform for you on demand, for free, you need to re-think.

[Khong Dong]

No. You're just being incompetent and dishonest.

[Khong Dong]

Everyone in the right mind would know: {"There is zero prime"} |- ~(*).

Since you (wrongly) believed ~(*) is a logical formula, you must have believed one of:

- "There is zero prime" is a logical formula
- a nonlogical axiom in a consistent theory can prove a logical theorem
- {"There is zero prime"} is inconsistent.

Any which way is of ignorance, which is your knowledge of the matter.

[Khong Dong]

Issues having been clearly explained, do you now, Rupert, concede/acknowledge it's impossible for you to syntactically prove ~(*), as written in L(<,*), is a logical theorem?

[Rupert]

Of course not. The proof I gave you is fine.

[Khong Dong]

What you gave is just a delusional incompetence, dishonesty.

[Rupert]

All right. Since I'm so incredibly bored, let's have another go at this.

So first of all, we quote from you. Let's scroll up.

To quote from you:

- "There exists no 𝑥 which 𝑃(𝑥)", denoted by '(0)𝑃(∗)', is defined as:
(0)𝑃(∗) ↔ ∀𝑥[¬𝑃(𝑥)].
- "There exist infinitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑎𝐼)𝑃(∗)', is defined in an anti induction form as:
(𝑎𝐼)𝑃(∗) ↔ ∃𝑥[𝑃(𝑥)] ⋀ ∀𝑥∃𝑦[𝑃(𝑥) → (𝑃(𝑦) /\ (𝑥 < 𝑦))].
- "There exist finitely many 𝑥′𝑠 each of which 𝑃(𝑥)", denoted by '(𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗)', is defined as:
(𝑓𝑖𝑛𝑖𝑡𝑒)𝑃(∗) ↔ ¬(0)𝑃(∗) ⋀ ~(𝑎𝐼)𝑃(∗).

Now also to quote from you:

(*) ~("There is zero prime" \/ "There are finitely many primes" \/ "There are infinitely many primes").

Where I made the assumption, perhaps rather bold I admit, that I should take this to be another way of saying

~((0)P(*) \/ (finite)P(*) \/ (aI)P(*)) where all of these should be taken to be abbreviations as given above and where P(x) should be taken to abbreviate some formula or other which expresses "x is prime" if only we took the trouble to get rid of all the abbreviations (I'm not going to go to all the trouble of chasing up your original document and disentangling all the abbreviations).

So, when you say ~(*), that's a meta-linguistic expression whose referent is a formula in the object language L(<,*), which we could in principle write out in full if we went to the trouble of dis-entangling all the abbreviations, and which is of the form ~~(p \/ (~p /\ ~q) \/ q) where p and q are subformulas, and I looked up Shoenfield's abbreviations and dis-abbreviated that as ~~(p \/ ~(~~p \/ ~~q) \/ q). So if you're willing to accept that your meta-linguistic expression ~(*) has a referent which is a formula in the object language L(<,*) of that form, then if I prove for you that every formula of that form is provable from Shoenfield's axiom schemas and modus ponens, then I'm done. And I did in fact prove that *if* you're willing to accept the lemma which I cited, I could of course always waste more time by making the proof even more explicit, but if you're just going to try to wriggle out of it by saying that the meta-linguistic expression is not a formula of the object language, then you're wasting my time, aren't you, because I couldn't reasonably have known that that was how you meant the original question. Meta-linguistic expressions that have abbreviations in them are not formulas of L(<,*), no, but that is a triviality. But if you're willing to agree that proving that every formula of the form ~~(p \/ ~(~~p \/ ~~q) \/ q) is provable in Shoenfield's axiomatization of first-order logic should be enough, because the formula of the object language L(<,*) to which the meta-linguistic expression *refers according to your conventions plus Shoenfield's conventions* is of that form, and if for some bizarre reason I'm willing to waste even more time and give you a direct proof of that from the axiom schemata rather than just citing the lemma I cited, well yeah I do claim it most definitely can be done, and shouldn't be too much work, although of course there's no particular reason why I should jump through that particular hoop for you for free. But there's certainly no point in bothering if you're just going to use the get-out that you meant the meta-linguistic expression itself and not the formula of the object language to which it refers according to the conventions you've set up. So... let me know, and when we've got past that hurdle I'll let you know whether I still feel like I can be bothered. But yeah, it is trivial to point out that meta-linguistic expressions with abbreviations in them are not formulas of L(<,*).

[Khong Dong]

""? ""? You're good at being disingenuous, aren't you? In this very thread I specifically gave you this definition so you know what ~(*) is *IN THE FULL LANGUAGE L(<,*)*:

<quote>

Just in case, the relevant definition is:

𝑝𝑟𝑖𝑚𝑒(𝑝) ↔ ∃𝑧∃𝑜∀𝑥∀𝑢∀𝑣[(𝑧∗𝑥=𝑧) ⋀ (𝑜∗𝑥=𝑥) ⋀ ¬(𝑧=𝑜) ⋀ ¬(𝑧=𝑝) ⋀ ¬(𝑜=𝑝) ⋀ ((𝑝=𝑢∗𝑣) → (𝑢=𝑜 ⋁ 𝑣=𝑜))].

</quote>

So what's up with ~(*) being a defined formula for this full language formula? And please, don't half-bake, coin your private term "meta-linguistic expression" (below) when I and Shoenfield already pointed to you it's a *defined formula*.

>
> So, when you say ~(*), that's a meta-linguistic expression whose referent is a formula in the object language L(<,*), which we could in principle write out in full if we went to the trouble of dis-entangling all the abbreviations, and which is of the form ~~(p \/ (~p /\ ~q) \/ q) where p and q are subformulas, and I looked up Shoenfield's abbreviations and dis-abbreviated that as ~~(p \/ ~(~~p \/ ~~q) \/ q). So if you're willing to accept that your meta-linguistic expression ~(*) has a referent which is a formula in the object language L(<,*) of that form, then if I prove for you that every formula of that form is provable from Shoenfield's axiom schemas and modus ponens, then I'm done.

No you're not. Please review what Shoenfield wrote: "defined formulas are _not_ formulas of the language". And your "~~(p \/ ~(~~p \/ ~~q) \/ q)" here is not a formula of the language.

I know you don't want to expand ~(*) by replacing "𝑝𝑟𝑖𝑚𝑒" with its full definiens above, but that doesn't rob the fact that ~(*) and your "~~(p \/ ~(~~p \/ ~~q) \/ q)" are just defined formulas, inadequate for mathematicians to evaluate whether or not it's a logical theorem.

> And I did in fact prove that *if* you're willing to accept the lemma which I cited,

Again, that shows your lack of sufficient knowledge in mathematical logic (FOL). You don't need that lemma or PL or truth table or tautology, if you fail -- and you have failed -- to recognize ~(*) and your "~~(p \/ ~(~~p \/ ~~q) \/ q)" are just defined formulas -- _not_ formulas of L(<,*).

[Khong Dong]

That is:

"rather bold I admit"? "chasing up your original document"? You're good at being disingenuous, aren't you? In this very thread I specifically gave you this definition so you know what ~(*) is *IN THE FULL LANGUAGE L(<,*)*:

[Rupert]

So why the hell do you have a problem with me saying I've proved it to be a logical theorem? It's an instance of the propositional schema " "~~(p \/ ~(~~p \/ ~~q) \/ q)". And no, I'm not going to waste my time writing out which instance it is. All of Shoenfield's axiom schemas are given as rules of inference applied to propositional schemata. If you're happy to accept the lemma I cited, you should now agree that
~(*) has been proved to be a logical theorem.

[Khong Dong]

Why the hell have you kept failing to understand the textbook simple knowledge that "defined formulas are _not_ formulas of the language" [Shoenfield]?

> It's an instance of the propositional schema " "~~(p \/ ~(~~p \/ ~~q) \/ q)". And no, I'm not going to waste my time writing out which instance it is.

That's your shortcoming: we're not talking about a general instance! We're talking about a specific defined formula which Shoenfield insisted "defined formulas are _not_ formulas of the language". Got it now?

[Rupert]

I know that perfectly well. Why the hell should I bother to write it out? Am I some kind of performing monkey who is required to jump through hoops for you on demand without you paying me any money? I've proved for you that ~(*) is a logical theorem. There is no good reason why I should have to write out the full formula.

[Khong Dong]

Stop idiotic "monkey" whining.

> I've proved for you that ~(*) is a logical theorem.

More dishonest utterance.

> There is no good reason why I should have to write out the full formula.

There is: it'd help you to overcome your ignorance of mathematical logic. (Though it was pointed out to you that there's a short-cut way to know ~(*) *IN THE FULL LANGUAGE L(<,*)* isn't logical theorem -- but you're too incompetent to understand).