Formal specification of Minimal Type Theory (updated)

[olcott]

Minimal Type Theory is intended to be its own Tarski Meta-language and
show exactly why logic expressions having pathological self-reference
meet the standard definition of incompleteness.

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

It would be incorrect to construe a formal system as incomplete on the
basis that this formal system can neither prove nor disprove infinitely
recursive logic expressions.

https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF



--
Copyright 2020 Pete Olcott

[André G. Isaak]

According to the syntax you give in that lank, the following would be a
well-formed expression of your system:

(A := B) → C

Do explain what that could possibly mean.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

[olcott]

Unless B is defined somewhere else the semantic phase of the parse would
fail.

This is an example of another sentence is that syntactically correct
nonsense:

https://en.wikipedia.org/wiki/Colorless_green_ideas_sleep_furiously

[André G. Isaak]

On 2020-09-28 15:36, olcott wrote:
> On 9/28/2020 4:29 PM, André G. Isaak wrote:
>> On 2020-09-28 15:22, olcott wrote:
>>> Minimal Type Theory is intended to be its own Tarski Meta-language
>>> and show exactly why logic expressions having pathological
>>> self-reference meet the standard definition of incompleteness.
>>>
>>> A theory T is incomplete if and only if there is some sentence φ such
>>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>>
>>> It would be incorrect to construe a formal system as incomplete on
>>> the basis that this formal system can neither prove nor disprove
>>> infinitely recursive logic expressions.
>>>
>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>
>>
>>
>> According to the syntax you give in that lank, the following would be
>> a well-formed expression of your system:
>>
>> (A := B) → C
>>
>> Do explain what that could possibly mean.
>>
>> André
>>
>
> Unless B is defined somewhere else the semantic phase of the parse would
> fail.

Assume B is defined. It is an atomic statement which is true. What would
the above mean?

Alternately, what would

¬(A := B)

mean?

You seem to not be getting the issue which I am raising. Your grammar
claims that (A := B) is a type of SENTENCE, and as such it should appear
wherever sentences appear, i.e. as one of the operands of a connective
like ∧, ∨, →, etc. But unlike every other type of sentence in your
grammar, which are things which have truth-values, definitions are
things which *don't* have truth values. You can't treat them as a type
of sentence en par with atomic sentences, conjunctions, disjunctions, etc.

There is a good reason why symbols used to form definitions are
relegated to the meta-language. They are fundamentally different from
the kinds of things which appear in the language.

[olcott]

On 9/28/2020 5:31 PM, André G. Isaak wrote:
> On 2020-09-28 15:36, olcott wrote:
>> On 9/28/2020 4:29 PM, André G. Isaak wrote:
>>> On 2020-09-28 15:22, olcott wrote:
>>>> Minimal Type Theory is intended to be its own Tarski Meta-language
>>>> and show exactly why logic expressions having pathological
>>>> self-reference meet the standard definition of incompleteness.
>>>>
>>>> A theory T is incomplete if and only if there is some sentence φ
>>>> such that (T ⊬ φ) and (T ⊬ ¬φ).
>>>>
>>>> It would be incorrect to construe a formal system as incomplete on
>>>> the basis that this formal system can neither prove nor disprove
>>>> infinitely recursive logic expressions.
>>>>
>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>
>>>
>>>
>>>
>>> According to the syntax you give in that lank, the following would be
>>> a well-formed expression of your system:
>>>
>>> (A := B) → C
>>>
>>> Do explain what that could possibly mean.
>>>
>>> André
>>>
>>
>> Unless B is defined somewhere else the semantic phase of the parse
>> would fail.
>
> Assume B is defined. It is an atomic statement which is true. What would
> the above mean?
>

T → c // Where T is the logic symbol for True

> Alternately, what would
>
> ¬(A := B)
>

¬(T) means ⊥ // Where ⊥ is the logic symbol for false.

> mean?
>
> You seem to not be getting the issue which I am raising. Your grammar
> claims that (A := B) is a type of SENTENCE, and as such it should appear
> wherever sentences appear, i.e. as one of the operands of a connective

%left ASSIGN_ALIAS
// := (definition operator) x := y means x is defined to be another
name for y

It is the exactly same macro substitution as C/C++ and is only used for
two things,

(1) To construct higher order logic expressions from layers of first
order logic expressions (see example in the updated paper).
Two layers creates second order logic.

(a) S1 := ∀x (Px ∨ ¬Px)
(b) ∀P(S1)
Every instance of the left-hand-side of a definition is to be expanded
into its right-hand-side. Thus the above two lines specify:
∀P(∀x (Px ∨ ¬Px))

(2) To accurately formalize actual self-reference to show its infinitely
recursive structure as this link explains:
https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html

> like ∧, ∨, →, etc. But unlike every other type of sentence in your
> grammar, which are things which have truth-values, definitions are
> things which *don't* have truth values. You can't treat them as a type
> of sentence en par with atomic sentences, conjunctions, disjunctions, etc.
>
> There is a good reason why symbols used to form definitions are
> relegated to the meta-language. They are fundamentally different from
> the kinds of things which appear in the language.
>
> André
>

Tarski's theory / metatheory hides the fact that the original expression
is ill-formed because it has pathological self-reference. It is not that
his metatheory has brilliant insights that his theory cannot see, it is
merely that his metatheory is defined with one level of indirection away
from his theory, thus no longer self-referential.

http://www.liarparadox.org/Tarski_275_276.pdf

[André G. Isaak]

If A := B means 'A is henceforth another name for B', in what possible
sense can that be evaluated as either true or false?

You avoid this question by simply NOT PROVIDING ANY SEMANTICS for your
MTT. If you want to claim that (A := B) is a sentence of the same sort
as A or as (A ∨ B), then you need to give it a truth table, which, of
course, makes utterly no sense since giving a definition isn't a
truth-functional operation. Were you to attempt to provide some actual
semantics, you would realize why this proposal is blatant nonsense.

>> mean?
>>
>> You seem to not be getting the issue which I am raising. Your grammar
>> claims that (A := B) is a type of SENTENCE, and as such it should
>> appear wherever sentences appear, i.e. as one of the operands of a
>> connective
>
> %left  ASSIGN_ALIAS
> //  := (definition operator) x := y means x is defined to be another
> name for y
>
> It is the exactly same macro substitution as C/C++ and is only used for
> two things,

And in C I can't write:

If #define A B {do something}
else {do something else}

It makes absolutely no sense.

> (1) To construct higher order logic expressions from layers of first
> order logic expressions (see example in the updated paper).
> Two layers creates second order logic.
>
> (a) S1 := ∀x (Px ∨ ¬Px)
> (b) ∀P(S1)

So what would

¬(S1 := ∀x (Px ∨ ¬Px))

mean?

Your grammar claims the above can be negated. If so, what would the
'negation' of the above definition mean?

> Every instance of the left-hand-side of a definition is to be expanded
> into its right-hand-side. Thus the above two lines specify:
> ∀P(∀x (Px ∨ ¬Px))

Which would not be well-formed first order logic. If you allow variables
to refer to predicates, you are not dealing with FOL. If you do allow
variables to refer to predicates, then what's the point of using the above?

> (2) To accurately formalize actual self-reference to show its infinitely
> recursive structure as this link explains:
> https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html
>
>> like ∧, ∨, →, etc. But unlike every other type of sentence in your
>> grammar, which are things which have truth-values, definitions are
>> things which *don't* have truth values. You can't treat them as a type
>> of sentence en par with atomic sentences, conjunctions, disjunctions,
>> etc.

Good of you to completely ignore the above paragraph.

André

>> There is a good reason why symbols used to form definitions are
>> relegated to the meta-language. They are fundamentally different from
>> the kinds of things which appear in the language.
>>
>> André
>>
>
> Tarski's theory / metatheory hides the fact that the original expression
> is ill-formed because it has pathological self-reference. It is not that
> his metatheory has brilliant insights that his theory cannot see, it is
> merely that his metatheory is defined with one level of indirection away
> from his theory, thus no longer self-referential.
>
> http://www.liarparadox.org/Tarski_275_276.pdf
>


--

[olcott]

You said that B had the value of True, therefore ¬B is false.

> You avoid this question by simply NOT PROVIDING ANY SEMANTICS for your

Not at all, not in the least. All of the semantics comes from the
conventional meaning of the logical operators.

> MTT. If you want to claim that (A := B) is a sentence of the same sort

No it is not a sentence of the same sort...
I know that what I am saying is unconventional and that must be the
reason that you are having difficulty with it.

As I said a few times now think of A := B as macro expansion.

X := blah blah blah
Now whenever you see X substitute blah blah blah just like the C/C++
#define would do.

In the case of self-reference the substitution is impossible proving
that ill-formed nature of self-referential expressions.

If you read the second page of this link you will see that Clocksin and
Mellish describe the same problem with Prolog expressions.

http://www.liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf

> as A or as (A ∨ B), then you need to give it a truth table, which, of
> course, makes utterly no sense since giving a definition isn't a
> truth-functional operation. Were you to attempt to provide some actual
> semantics, you would realize why this proposal is blatant nonsense.
>
>>> mean?
>>>
>>> You seem to not be getting the issue which I am raising. Your grammar
>>> claims that (A := B) is a type of SENTENCE, and as such it should
>>> appear wherever sentences appear, i.e. as one of the operands of a
>>> connective
>>
>> %left  ASSIGN_ALIAS
>> //  := (definition operator) x := y means x is defined to be another
>> name for y
>>
>> It is the exactly same macro substitution as C/C++ and is only used
>> for two things,
>
> And in C I can't write:
>
> If #define A B {do something}
> else {do something else}
>
> It makes absolutely no sense.
>

#define LP !True(LP) // is infinitely recursive.
https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html

>> (1) To construct higher order logic expressions from layers of first
>> order logic expressions (see example in the updated paper).
>> Two layers creates second order logic.
>>
>> (a) S1 := ∀x (Px ∨ ¬Px)
>> (b) ∀P(S1)
>
> So what would
>
> ¬(S1 := ∀x (Px ∨ ¬Px))

~(S1 := ∀x (P(x) ∨ ~P(x)))

<sentence_2 token="NOT">
<sentence_15 token="ASSIGN_ALIAS">
<sentence_15 token="IDENTIFIER" value="S1"/>
<sentence_4 token="FOR_ALL">
<sentence_4 token="IDENTIFIER" value="x"/>
<sentence_13 token="OR">
<atomic_sentence_1 token="IDENTIFIER" value="P">
<term_2 token="IDENTIFIER" value="x"/>
</atomic_sentence_1>
<sentence_2 token="NOT">
<atomic_sentence_1 token="IDENTIFIER" value="P">
<term_2 token="IDENTIFIER" value="x"/>
</atomic_sentence_1>
</sentence_2>
</sentence_13>
</sentence_4>
</sentence_15>
</sentence_2>

I should probably rewrite the syntax disallow that expression.

>
> mean?
>
> Your grammar claims the above can be negated. If so, what would the
> 'negation' of the above definition mean?
>

You found a bug in my grammar. Now that I found my fully operational
parser I can fix it and test the fix.

>> Every instance of the left-hand-side of a definition is to be expanded
>> into its right-hand-side. Thus the above two lines specify:
>> ∀P(∀x (Px ∨ ¬Px))
>
> Which would not be well-formed first order logic.

Of course the above is not a well-formed FOL expression as I have said
several times now.

You have to do much more than glance at a few of my words to understand
what I am saying. You also have to carefully read every word of my links.

The above is a second order logic expression that can be expressed using
first order logic syntax AND the ":=" assign alias operator. I have said
this and provided the example of how to do this three times times now.

> If you allow variables
> to refer to predicates, you are not dealing with FOL. If you do allow
> variables to refer to predicates, then what's the point of using the above?
>

The point is that with MTT you can write 187th order logic expressions
as FOL expressions nested 186 levels deep, all using the very simple
slightly augmented syntax of FOL.

>> (2) To accurately formalize actual self-reference to show its
>> infinitely recursive structure as this link explains:
>> https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html
>>
>>> like ∧, ∨, →, etc. But unlike every other type of sentence in your
>>> grammar, which are things which have truth-values, definitions are
>>> things which *don't* have truth values. You can't treat them as a
>>> type of sentence en par with atomic sentences, conjunctions,
>>> disjunctions, etc.
>
> Good of you to completely ignore the above paragraph.
>

You are asking what is the semantics of a thing that has no semantics.
:= is only macro substitution it has no semantics.

> André
>
>>> There is a good reason why symbols used to form definitions are
>>> relegated to the meta-language. They are fundamentally different from
>>> the kinds of things which appear in the language.
>>>
>>> André
>>>
>>
>> Tarski's theory / metatheory hides the fact that the original
>> expression is ill-formed because it has pathological self-reference.
>> It is not that his metatheory has brilliant insights that his theory
>> cannot see, it is merely that his metatheory is defined with one level
>> of indirection away from his theory, thus no longer self-referential.
>>
>> http://www.liarparadox.org/Tarski_275_276.pdf
>>
>
>


--

Copyright 2020 Pete Olcott

[Jeff Barnett]

On 9/28/2020 3:22 PM, olcott wrote:

Ridiculous! Once again you recycle garbage and Andres feels he should
help you learn from your mistakes. You don't want to learn, you want to
troll. Andres should know better; he'd have a better chance of teaching
a skunk logic. The skunk is more pragmatic, smarter, and less a troll
than you are. (I know this from recent experience. My wife, as I type,
is trying to convince a skunk to get out of her greenhouse.)

Loop. Loop. Loop. I think you have not learned much in the last two
decades other than more words to use badly and more nonsense to goad
fools such as Andres and me as well as others. I must admit you are a
clever troll and that surprises me since the evidence showed you were
such a poor programmer - your patent and code showed you couldn't put
two consecutive thoughts together. On the other hand you can recycle
gibberish using technical terms from the high art with the best of them.
What is truly amazing is how you can sneak back to the same silly
arguments year after year using the same terms and avoid espousing a
single correct insight.

It's too bad USENET is not what it once was so we could give you awards
for Best in Class Troll, Longevity, Diversity, Double Talk as well as
other lesser categories. With the decline of USENET these awards are no
longer as meaningful as they once were. Let us all drink a toast to the
past and a PO who would be famous if he hit his stride earlier in life.

All together now: PO, HERE'S TO YOU!!!!
--
Jeff Barnett

[olcott]

"Great spirits have always encountered violent opposition from mediocre
minds. Albert Einstein.

[Jeff Barnett]

Great minds = Godel, et al
mediocre minds = PO

Do not have illusions about your mind or ideas; both are dysfunctional.
I think you would give Albert a chuckle and he would advise you not to
try to play the violin but get more exercise to clear your mind. It's
too bad he's not alive to tell you how flattering your quoting him is
even if misunderstood.
--
Jeff Barnett

[André G. Isaak]

But I didn't ask about the value of ¬B (or B or A or ¬A). I asked about
the value of ¬(A := B)

Since this isn't sinking in, let's use a pascal analogy.

In pascal, the following mean different things

A := B
A = B

The first is a variable assignment. The second is a comparison. The
first is a statement which describes an action and has no value. The
second is an expression which has a boolean value. The syntax of pascal
treats statements and expressions as fundamentally different units. The
first can stand alone; the second must be a part of some larger statement.

Your := is analogous to the first of these, but your grammar treats it
as the same type of object as the second. That's simply wrong. Which is
particularly ironic given that a language which you call 'minimal type
theory' fails to distinguish between different types of things.

>> You avoid this question by simply NOT PROVIDING ANY SEMANTICS for your
>
> Not at all, not in the least. All of the semantics comes from the
> conventional meaning of the logical operators.

Except := isn't a conventional operator. You can claim that your ¬, ∧,
→, etc. have conventional meanings. You can't state this for :=.

>> MTT. If you want to claim that (A := B) is a sentence of the same sort
>
> No it is not a sentence of the same sort...

According to your grammar it is, since your grammar only recognizes
SENTENCES. There is nothing in the grammar which mentions different
types of sentences.

> I know that what I am saying is unconventional and that must be the
> reason that you are having difficulty with it.

> As I said a few times now think of A := B as macro expansion.
>
> X := blah blah blah
> Now whenever you see X substitute blah blah blah just like the C/C++
> #define would do.

And is it possible to evaluate the following as true or false?

#define A B

No. It isn't. So why should it be possible to evaluate (A := B) as true
or false?

You really need to actually read that article. #define LP !True(LP) is
*not* infinitely recursive. From the article: "The self-reference rule
cuts this process short after one step, at (4 + foo)". You have a habit
of posting things which say exactly the opposite of what you claim they do.

André

[olcott]

If you would not be so damn sure pf your own opinion that I am wrong and
actually really earnestly tried to see what I am saying you would be
able to see that I am correct.

The only reason that some expressions of language are neither provable
nor disprovable is simply that they are not truth bearers.

[olcott]

A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more

A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more

I have said that so many times and you igored it so I said it ten more
times in a row.

> Since this isn't sinking in, let's use a pascal analogy.
>
> In pascal, the following mean different things
>
> A := B
> A = B
>

This is not Pascal it is Minimal Type Theory.

> The first is a variable assignment. The second is a comparison. The

Yes and neither one of those is macro substitution.
It seems that you might not believe that self reference can be
pathological. It seems that you must be ignoring the material on my
links. You can' do that and actually understand what I am saying.

Let me know when you have read the yellow highlighted material on the
second page of this link.
http://www.liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf

> first is a statement which describes an action and has no value. The
> second is an expression which has a boolean value. The syntax of pascal
> treats statements and expressions as fundamentally different units. The
> first can stand alone; the second must be a part of some larger statement.

A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more

>
> Your := is analogous to the first of these, but your grammar treats it
> as the same type of object as the second. That's simply wrong. Which is
> particularly ironic given that a language which you call 'minimal type
> theory' fails to distinguish between different types of things.

Yes the grammar has a bug.

>
>>> You avoid this question by simply NOT PROVIDING ANY SEMANTICS for your
>>
>> Not at all, not in the least. All of the semantics comes from the
>> conventional meaning of the logical operators.
>
> Except := isn't a conventional operator. You can claim that your ¬, ∧,
> →, etc. have conventional meanings. You can't state this for :=.

It is a conventional, macro substitution operator.
If is referred to as the definition operator.
Different variations of it have "def" as a subscript.

>
>>> MTT. If you want to claim that (A := B) is a sentence of the same sort
>>
>> No it is not a sentence of the same sort...
>
> According to your grammar it is, since your grammar only recognizes
> SENTENCES. There is nothing in the grammar which mentions different
> types of sentences.
>

A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more
A := B is only macro substitution nothing more

>> I know that what I am saying is unconventional and that must be the
>> reason that you are having difficulty with it.
>
>> As I said a few times now think of A := B as macro expansion.
>>
>> X := blah blah blah
>> Now whenever you see X substitute blah blah blah just like the C/C++
>> #define would do.
>
> And is it possible to evaluate the following as true or false?
>
> #define A B
>
> No. It isn't. So why should it be possible to evaluate (A := B) as true
> or false?
>

This can be construed two different ways:
(1) It is not possible to evaluate the expression as true or false.
(2) The LHS of the expression aquires the truth value of its RHS.
I am leaning towards your interpretation as more apt.

It specifies infinite recursion and this infinite recursion is ignored.

#define foo (4 + foo)
where foo is also a variable in your program.

Following the ordinary rules, each reference to foo will expand into (4
+ foo); then this will be rescanned and will expand into (4 + (4 +
foo)); and so on until the computer runs out of memory.

> cuts this process short after one step, at (4 + foo)". You have a habit
> of posting things which say exactly the opposite of what you claim they do.
>
> André
>

It recognizes the infinite recursion and intentionally fails to
interpret it correctly because interpreting it correctly has
dysfunctional results.

Prolog's unify_with_occurs_check/2 will report an error in this case.

None-the-less the point that you have been consistently dodging is that
infinitely recursive expressions are ill-formed expressions that cannot
be evaluated and because they cannot be evaluated they meet the standard
definition of incompleteness:

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

So error with the standard definition of Incompleteness is that it
allocates incompleteness to formal systems entirely on the basis that it
cannot evaluate infinitely recursive (thus ill-formed) expressions.

[olcott]

I rewrote my grammar to correct the error that you caught, now it simply
rejects the sample expressions that you provided as ill-formed.

https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF

[Jeff Barnett]

Or so they say. I wonder who has the best view of mathematical knowledge
in these forums? I'm sure it isn't you. You are the mediocrity providing
the violent opposition to those who know better. When you feel to quote
something snide, look in the mirror first.
--
Jeff Barnett

[olcott]

I do not claim to have mathematical knowledge and it is pretty obvious
to me and everyone else here that my mathematical knowledge is quite scant.

The only knowledge that I claim to have sufficiently demonstrated is the
one aspect of metamathematics pertaining to pathological self-reference.
It is only in this very specific and narrow focus that I have key insights.

> You are the mediocrity providing

My knowledge of mathematics as a whole is quite obviously far less than
mediocre. My knowledge of one single aspect of metamathematics is
self-evidently correct.

> the violent opposition to those who know better. When you feel to quote
> something snide, look in the mirror first.


--

Copyright 2020 Pete Olcott

[André G. Isaak]

snip 15 repetitions of the above

>> Your := is analogous to the first of these, but your grammar treats it
>> as the same type of object as the second. That's simply wrong. Which
>> is particularly ironic given that a language which you call 'minimal
>> type theory' fails to distinguish between different types of things.
>
> Yes the grammar has a bug.

Wouldn't it have been much easier to just acknowledge that without
repeating your assertion above 15 times? And yet you still go on to
repeat it an additional 5 times below (which I have also snipped).

>>> Not at all, not in the least. All of the semantics comes from the
>>> conventional meaning of the logical operators.
>>
>> Except := isn't a conventional operator. You can claim that your ¬, ∧,
>> →, etc. have conventional meanings. You can't state this for :=.
>
> It is a conventional, macro substitution operator.

No. It is used to indicate definitions in the meta language. Definitions
are not the same as macro expansion which is a simple text replacement
operation.

And I am not aware of *any* logic which defines the semantics of such a
symbol within the language itself. If you want to use it in the
language, you need to actually do so.

>> And is it possible to evaluate the following as true or false?
>>
>> #define A B
>>
>> No. It isn't. So why should it be possible to evaluate (A := B) as
>> true or false?
>>
>
> This can be construed two different ways:
> (1) It is not possible to evaluate the expression as true or false.

Right. That's because definitions aren't boolean expressions. But this
means that your definition isn't actually a translation of the Liar's
paradox which does present itself as a boolean expression.

>>> #define LP !True(LP) // is infinitely recursive.
>>> https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html
>>
>> You really need to actually read that article. #define LP !True(LP) is
>> *not* infinitely recursive. From the article: "The self-reference rule
>
> It specifies infinite recursion and this infinite recursion is ignored.
>
> #define foo (4 + foo)
> where foo is also a variable in your program.
>
> Following the ordinary rules, each reference to foo will expand into (4
> + foo); then this will be rescanned and will expand into (4 + (4 +
> foo)); and so on until the computer runs out of memory.
>
>> cuts this process short after one step, at (4 + foo)". You have a
>> habit of posting things which say exactly the opposite of what you
>> claim they do.
>>
>> André
>>
>
> It recognizes the infinite recursion and intentionally fails to
> interpret it correctly because interpreting it correctly has
> dysfunctional results.

No. It interprets it correctly, since that is the way #define is defined
to work for C.

That's why you can't keep claiming that your := is the same as macro
replacement in C when clearly you don't intend it to be the same as in C.

You need to actually define how you want it to work.

And here you run into a serious problem. C is a computer language. C
programs are contained in a text file which is then run through a
compiler. Macro replacement is a *text replacement* operation, not
something which has any actual semantics associated with it (well,
that's not quite true, but the amount of interpretation which the
preprocessor applies to macros is extremely limited).

The language of logic isn't like that. Claiming to have 'macro
expansion' for FOL or some extension thereof makes no more sense than
claiming to have macro expansion for English.

[André G. Isaak]

On 2020-09-29 10:31, olcott wrote:

> I rewrote my grammar to correct the error that you caught, now it simply
> rejects the sample expressions that you provided as ill-formed.
>
> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF

Not quite. You added a new category, "definition", but you still list
your := under "sentence" as well. You want to remove it from that.

You now need to define what a 'definition' is in the semantics. By
placing it in a separate category you are clearly affirming that it
isn't something like a sentence, i.e. a boolean expression. So what
exactly is it?

Your grammar also claims that the following is well-formed:

(A, B, C) := (D ∨ E) → F

What might that mean?

André

[olcott]

Apparently not. I explained this all to you before in about five
different replies and you seemed to simply ignore the explanation.

> And yet you still go on to
> repeat it an additional 5 times below (which I have also snipped).
>
> >>> Not at all, not in the least. All of the semantics comes from the
> >>> conventional meaning of the logical operators.
> >>
> >> Except := isn't a conventional operator. You can claim that your ¬, ∧,
> >> →, etc. have conventional meanings. You can't state this for :=.
> >
> > It is a conventional, macro substitution operator.
>
> No. It is used to indicate definitions in the meta language. Definitions
> are not the same as macro expansion which is a simple text replacement
> operation.

I just proved that they are and you ignored my proof several times now.
Ignoring a proof is not at all the same thing as proving a correct
rebuttal.

Following the ordinary rules, each reference to foo will expand into (4
+ foo); then this will be rescanned and will expand into (4 + (4 +
foo)); and so on until the computer runs out of memory.

The self-reference rule cuts this process short after one step, at (4 +
foo). https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html

The macro does specify infinite recursion. The macro processor knows
this and overrides the specification.

> And I am not aware of *any* logic which defines the semantics of such a
> symbol within the language itself. If you want to use it in the
> language, you need to actually do so.
>

-- A := B is only macro substitution nothing more
-- A := B is only macro substitution nothing more
-- A := B is only macro substitution nothing more
-- A := B is only macro substitution nothing more
-- A := B is only macro substitution nothing more

It is a syntactic aspect of the language in the same way that #define is
a syntatic aspect of C/C++. It is not a sementic aspect of the language.

>>> And is it possible to evaluate the following as true or false?
>>>
>>> #define A B
>>>
>>> No. It isn't. So why should it be possible to evaluate (A := B) as
>>> true or false?
>>>
>>
>> This can be construed two different ways:
>> (1) It is not possible to evaluate the expression as true or false.
>
> Right. That's because definitions aren't boolean expressions.

> But this
> means that your definition isn't actually a translation of the Liar's
> paradox which does present itself as a boolean expression.
>

Sure it is:

#define LP !True(LP) // is infinitely recursive.

The macro preprocessor recognizes this and overrides it.

I show that the Liar Paradox must be rejected as a Boolean expression.
The Liar Paradox is not a truth bearer.

>>>> #define LP !True(LP) // is infinitely recursive.
>>>> https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html
>>>
>>> You really need to actually read that article. #define LP !True(LP)
>>> is *not* infinitely recursive. From the article: "The self-reference
>>> rule
>>
>> It specifies infinite recursion and this infinite recursion is ignored.
>>
>> #define foo (4 + foo)
>> where foo is also a variable in your program.
>>
>> Following the ordinary rules, each reference to foo will expand into
>> (4 + foo); then this will be rescanned and will expand into (4 + (4 +
>> foo)); and so on until the computer runs out of memory.
>>
>>> cuts this process short after one step, at (4 + foo)". You have a
>>> habit of posting things which say exactly the opposite of what you
>>> claim they do.
>>>
>>> André
>>>
>>
>> It recognizes the infinite recursion and intentionally fails to
>> interpret it correctly because interpreting it correctly has
>> dysfunctional results.
>
> No. It interprets it correctly, since that is the way #define is defined
> to work for C.
>

Following the ordinary rules, each reference to foo will expand into (4
+ foo); then this will be rescanned and will expand into (4 + (4 +
foo)); and so on until the computer runs out of memory.

The self-reference rule cuts this process short after one step, at (4 +
foo). https://gcc.gnu.org/onlinedocs/cpp/Self-Referential-Macros.html

The macro preprocessor recognizes infinite recursion and overrides it.
The macro preprocessor recognizes infinite recursion and overrides it.
The macro preprocessor recognizes infinite recursion and overrides it.
The macro preprocessor recognizes infinite recursion and overrides it.
The macro preprocessor recognizes infinite recursion and overrides it.

> That's why you can't keep claiming that your := is the same as macro
> replacement in C when clearly you don't intend it to be the same as in C.
>
> You need to actually define how you want it to work.

For pathological self-reference yt works the same way as other text that
you perpetually ignore.

http://www.liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf

It recognizes the infinite recursion the same way that Prolog's
unify_with_occurs_check/2 does and reports it as an error.

> And here you run into a serious problem. C is a computer language. C
> programs are contained in a text file which is then run through a
> compiler. Macro replacement is a *text replacement* operation, not
> something which has any actual semantics associated with it (well,
> that's not quite true, but the amount of interpretation which the
> preprocessor applies to macros is extremely limited).
>

I could have presented the whole thing the way that Prolog does it but
then mathematicians would say that my work has nothing to do with
mathematics it is computer science.

> The language of logic isn't like that. Claiming to have 'macro
> expansion' for FOL or some extension thereof makes no more sense than
> claiming to have macro expansion for English.
>
> André
>

Maybe there is a better way to do this mathematically, yet I can think
of none. The point is that pathological self-reference must be
accurately formalized so that is erroneous nature can be seen.

More properly pathological self-reference is infinite recursion in
computer science.

https://www.researchgate.net/publication/342503359_Defining_Godel_Incompleteness_Away


This: G ↔ (F ⊬ G) is the same sort of pathological self-reference that
Prolog would reject with its unify_with_occurs_check/2

When we say it this way:
G := (F ⊬ G)
Then even mathematicians can see its error.

[olcott]

On 9/29/2020 1:40 PM, André G. Isaak wrote:
> On 2020-09-29 10:31, olcott wrote:
>
>> I rewrote my grammar to correct the error that you caught, now it
>> simply rejects the sample expressions that you provided as ill-formed.
>>
>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>
>
> Not quite. You added a new category, "definition", but you still list
> your := under "sentence" as well. You want to remove it from that.
>

Clearly you do not understand YACC BNF.
definition is list OVER sentence not UNDER it.

The outermost part of a logical expression is either a definition or it
has no definition at all.

> You now need to define what a 'definition' is in the semantics. By

Unless it detects pathological self-reference it is only macro
substitution has zero semantics what-so-ever.

> placing it in a separate category you are clearly affirming that it
> isn't something like a sentence, i.e. a boolean expression. So what
> exactly is it?
>

It is a way for people to see that when pathological self-reference is
specified that an infinite expression cannot be evaluated. If we use
mathematical conventions we might consider pathological self-reference
as the same sort of thing as dividing by zero.

> Your grammar also claims that the following is well-formed:
>
> (A, B, C) := (D ∨ E) → F
>
> What might that mean?

I have a fully operational parser that rejects that expression.
The ONLY thing that can be in the left-hand-side (LHS) of a
ASSIGN_ALIAS / (definition operator) is a single identifier all by itself.

>
> André
>

That was a good catch. My YACC grammar was way off. I haven't looked at
it for a very long time. I must have stopped working on it before it was
finished.

[André G. Isaak]

On 2020-09-29 13:34, olcott wrote:
> On 9/29/2020 1:40 PM, André G. Isaak wrote:
>> On 2020-09-29 10:31, olcott wrote:
>>
>>> I rewrote my grammar to correct the error that you caught, now it
>>> simply rejects the sample expressions that you provided as ill-formed.
>>>
>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>
>>
>>
>> Not quite. You added a new category, "definition", but you still list
>> your := under "sentence" as well. You want to remove it from that.
>>
>
> Clearly you do not understand YACC BNF.
> definition is list OVER sentence not UNDER it.

IDENTIFIER ASSIGN_ALIAS sentence

appears in *both* lists.

> The outermost part of a logical expression is either a definition or it
> has no definition at all.
>
>> You now need to define what a 'definition' is in the semantics. By
>
> Unless it detects pathological self-reference it is only macro
> substitution has zero semantics what-so-ever.
>
>> placing it in a separate category you are clearly affirming that it
>> isn't something like a sentence, i.e. a boolean expression. So what
>> exactly is it?
>>
>
> It is a way for people to see that when pathological self-reference is
> specified that an infinite expression cannot be evaluated. If we use
> mathematical conventions we might consider pathological self-reference
> as the same sort of thing as dividing by zero.

Except that you are trying to claim that X := ¬X is a translation of
'this sentence is false'.

It isn't. It is a translation of 'X is defined as ¬X', which is not the
same thing.

'This sentence is false' is an assertion, not a definition. As such, it
would need to be categorized as a sentence rather than a definition in
your grammar. But your grammar lacks any way of translating "this
sentence". Definitions or "macro expansion" don't capture this.

>> Your grammar also claims that the following is well-formed:
>>
>> (A, B, C) := (D ∨ E) → F
>>
>> What might that mean?
>
> I have a fully operational parser that rejects that expression.

Yes, that was a misreading on my part.

[olcott]

On 9/29/2020 3:06 PM, André G. Isaak wrote:
> On 2020-09-29 13:34, olcott wrote:
>> On 9/29/2020 1:40 PM, André G. Isaak wrote:
>>> On 2020-09-29 10:31, olcott wrote:
>>>
>>>> I rewrote my grammar to correct the error that you caught, now it
>>>> simply rejects the sample expressions that you provided as ill-formed.
>>>>
>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>
>>>
>>>
>>>
>>> Not quite. You added a new category, "definition", but you still list
>>> your := under "sentence" as well. You want to remove it from that.
>>>
>>
>> Clearly you do not understand YACC BNF.
>> definition is list OVER sentence not UNDER it.
>
> IDENTIFIER ASSIGN_ALIAS sentence
>
> appears in *both* lists.
>

You are right again. I only changed the fully executable YACC that has
semantic actions. I did not change the one in my paper. It is fixed now.

>> The outermost part of a logical expression is either a definition or
>> it has no definition at all.
>>
>>> You now need to define what a 'definition' is in the semantics. By
>>
>> Unless it detects pathological self-reference it is only macro
>> substitution has zero semantics what-so-ever.
>>
>>> placing it in a separate category you are clearly affirming that it
>>> isn't something like a sentence, i.e. a boolean expression. So what
>>> exactly is it?
>>>
>>
>> It is a way for people to see that when pathological self-reference is
>> specified that an infinite expression cannot be evaluated. If we use
>> mathematical conventions we might consider pathological self-reference
>> as the same sort of thing as dividing by zero.
>
> Except that you are trying to claim that X := ¬X is a translation of
> 'this sentence is false'.
>

It is as close as I can get in mathematics. To get closer than this it
seems that we have to move to computer science.

> It isn't. It is a translation of 'X is defined as ¬X', which is not the
> same thing.

http://www.liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf

The fact that even as macro expansion it specifies an infinite term that
cannot be evaluated is as close as I can get to saying this in math.

>
> 'This sentence is false' is an assertion, not a definition. As such, it

Yet symbolic has no way to precisely specify actual self-reference so I
had to make one up.

> would need to be categorized as a sentence rather than a definition in
> your grammar. But your grammar lacks any way of translating "this
> sentence". Definitions or "macro expansion" don't capture this.
>

They capture it closer than anything else that I can think of.
LP := ~AnyPedicateAtALL(LP) // specifies an infinite term

All the other ideas that everyone else has is: "lets simply ignore
pathogical self-reference because there is no way to say it using
symbolic logic."

>>> Your grammar also claims that the following is well-formed:
>>>
>>> (A, B, C) := (D ∨ E) → F
>>>
>>> What might that mean?
>>
>> I have a fully operational parser that rejects that expression.
>
> Yes, that was a misreading on my part.
>
> André
>


--

Copyright 2020 Pete Olcott

[olcott]

Yet symbolic logic

[André G. Isaak]

On 2020-09-29 14:47, olcott wrote:
> On 9/29/2020 3:06 PM, André G. Isaak wrote:
>> On 2020-09-29 13:34, olcott wrote:
>>> On 9/29/2020 1:40 PM, André G. Isaak wrote:
>>>> On 2020-09-29 10:31, olcott wrote:
>>>>
>>>>> I rewrote my grammar to correct the error that you caught, now it
>>>>> simply rejects the sample expressions that you provided as ill-formed.
>>>>>
>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>
>>>>
>>>>
>>>>
>>>>
>>>> Not quite. You added a new category, "definition", but you still
>>>> list your := under "sentence" as well. You want to remove it from that.
>>>>
>>>
>>> Clearly you do not understand YACC BNF.
>>> definition is list OVER sentence not UNDER it.
>>
>> IDENTIFIER ASSIGN_ALIAS sentence
>>
>> appears in *both* lists.
>>
>
> You are right again. I only changed the fully executable YACC that has
> semantic actions. I did not change the one in my paper. It is fixed now.

Right, so when I pointed this out it might have been better for you to
have double-checked the paper rather than immediately claiming that I
didn't understand YACC.

>>> The outermost part of a logical expression is either a definition or
>>> it has no definition at all.
>>>
>>>> You now need to define what a 'definition' is in the semantics. By
>>>
>>> Unless it detects pathological self-reference it is only macro
>>> substitution has zero semantics what-so-ever.
>>>
>>>> placing it in a separate category you are clearly affirming that it
>>>> isn't something like a sentence, i.e. a boolean expression. So what
>>>> exactly is it?
>>>>
>>>
>>> It is a way for people to see that when pathological self-reference
>>> is specified that an infinite expression cannot be evaluated. If we
>>> use mathematical conventions we might consider pathological
>>> self-reference as the same sort of thing as dividing by zero.
>>
>> Except that you are trying to claim that X := ¬X is a translation of
>> 'this sentence is false'.
>>
>
> It is as close as I can get in mathematics. To get closer than this it
> seems that we have to move to computer science.
>
>> It isn't. It is a translation of 'X is defined as ¬X', which is not
>> the same thing.
>
>
> http://www.liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf
>
> The fact that even as macro expansion it specifies an infinite term that
> cannot be evaluated is as close as I can get to saying this in math.
>
>>
>> 'This sentence is false' is an assertion, not a definition. As such, it
>
> Yet symbolic has no way to precisely specify actual self-reference so I
> had to make one up.

Except your made up way doesn't actually capture this.

>> would need to be categorized as a sentence rather than a definition in
>> your grammar. But your grammar lacks any way of translating "this
>> sentence". Definitions or "macro expansion" don't capture this.
>>
>
> They capture it closer than anything else that I can think of.
> LP := ~AnyPedicateAtALL(LP) // specifies an infinite term
>
> All the other ideas that everyone else has is: "lets simply ignore
> pathogical self-reference because there is no way to say it using
> symbolic logic."

There is, of course, another, far more sensible alternative. Since the
liar's paradox is something that arises in natural language but not in
logic, discuss it in natural language rather than in the language of logic.

[olcott]

On 9/29/2020 5:26 PM, Ben Bacarisse wrote:
> olcott <No...@NoWhere.com> writes:
>
>> Yet symbolic [logic] has no way to precisely specify actual

>> self-reference so I had to make one up.
>

> Yet you claim that Gödel's proof uses self-reference. Will you now
> retract that claim? If not, why make up a way to do it when you think
> Gödel managed it nearly a century ago?
>

https://mavdisk.mnsu.edu/pj2943kt/Fall%202015/Promotion%20Application/Previous%20Years%20Article%2022%20Materials/godel-1931.pdf

14 Every epistemological antinomy can likewise be used for a similar
undecidability proof. (Gödel 1931)

Gödel 1931 ON FORMALLY UNDECIDABLE PROPOSITIONS OF PRINCIPIA MATHEMATICA
AND RELATED SYSTEMS I

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

Instead of going around and around about what the math says or what it
doesn't say Gödel himself said Every epistemological antinomy (including
the Liar Paradox) can likewise be used for a similar undecidability proof.

So all we have to do is formalize the natural language sentence:
"This sentence is not true."

Unlike the formalization of every other natural language sentence the
formalization of this sentence does not need to include any knowledge
about the world what-so-ever.

The Liar Paradox is merely an ordinary logical proposition that make an
assertion about its own truth value.

X := ¬(P ∨ Q) ↔ (¬P ∧ ¬Q)
In the above case we can simply say that X is true.

In the following cases we can say that the truth value is vacuous:
LP := ~True(LP)
G := ~Provable(G)

http://www.liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf
Prolog's unify_with_occurs_check/2 rejects such "infinite terms".

The same thing occurs when we examine the actual semantics of this C/C++
initialization.

int main()
{
bool LP = (LP != true);
}

When we actually pay attention to the semantics of this instead of
focusing on what compilers do or what C/C++ standards require then the
above expression would assign a Boolean value to LP on the basis of
comparing the Boolean value of true to an non-existent value.

This is exactly the same thing as recording the number of feet of length
of the car of a person that has no car.

--
Copyright 2020 Pete Olcott

.

[olcott]

On 9/29/2020 5:40 PM, André G. Isaak wrote:
> On 2020-09-29 14:47, olcott wrote:
>> On 9/29/2020 3:06 PM, André G. Isaak wrote:
>>> On 2020-09-29 13:34, olcott wrote:
>>>> On 9/29/2020 1:40 PM, André G. Isaak wrote:
>>>>> On 2020-09-29 10:31, olcott wrote:
>>>>>
>>>>>> I rewrote my grammar to correct the error that you caught, now it
>>>>>> simply rejects the sample expressions that you provided as
>>>>>> ill-formed.
>>>>>>
>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>>
>>>>> Not quite. You added a new category, "definition", but you still
>>>>> list your := under "sentence" as well. You want to remove it from
>>>>> that.
>>>>>
>>>>
>>>> Clearly you do not understand YACC BNF.
>>>> definition is list OVER sentence not UNDER it.
>>>
>>> IDENTIFIER ASSIGN_ALIAS sentence
>>>
>>> appears in *both* lists.
>>>
>>
>> You are right again. I only changed the fully executable YACC that has
>> semantic actions. I did not change the one in my paper. It is fixed now.
>
> Right, so when I pointed this out it might have been better for you to
> have double-checked the paper rather than immediately claiming that I
> didn't understand YACC.
>

In retrospect it would have been much better.

Sure it does.
In computer science
#define LP !True(LP)
would specify copying the string !True(!True(!True(...))) an infinite
number of times.

In Math
LP := ~True(LP)
we are only dealing with concepts not finite strings making the
expression infitely recursive.

>
>>> would need to be categorized as a sentence rather than a definition
>>> in your grammar. But your grammar lacks any way of translating "this
>>> sentence". Definitions or "macro expansion" don't capture this.
>>>
>>
>> They capture it closer than anything else that I can think of.
>> LP := ~AnyPedicateAtALL(LP) // specifies an infinite term
>>
>> All the other ideas that everyone else has is: "lets simply ignore
>> pathogical self-reference because there is no way to say it using
>> symbolic logic."
>
> There is, of course, another, far more sensible alternative. Since the
> liar's paradox is something that arises in natural language but not in
> logic,

The ONLY reason why it does no arise in logic is because nobody ever
bothered to translate it to logic. The Liar Paradox is merely a
proposition that makes an assertion about its own truth value. It need
not know anything about the world.

It was obvious to you that the truth teller paradox is vacuous.
"This sentence is true." True about what?
True about being true. True about being true about what?

The Liar Paradox also lack a truth object, it is vacuous.
Because it is vacuous it meets this definition:

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

Vacuous sentences can neither be proved nor disproved because they are
vacuous.

> discuss it in natural language rather than in the language of logic.
>
> André
>


--

Copyright 2020 Pete Olcott

[Jeff Barnett]

On 9/29/2020 1:34 PM, olcott wrote:

> I have a fully operational parser that rejects that expression.
> The ONLY thing that can be in the left-hand-side (LHS) of a
> ASSIGN_ALIAS / (definition operator) is a single identifier all by itself.

You could have a fully operational parser that blew your nose and that
wouldn't make any difference either. If the grammar allows it and the
parser rejects it, then two things are wrong: 1) the parser and 2) the
idiot that wrote it. Gee. I wonder who that might be? Oh I knew, it's
prePOsterous POppycock := (PO). Oh, you troll so well. My complements to
the act of the total nitwit on the trail of trivia. Once again you are
cheated out of recognition due you because of USENET contraction. Sigh.
--
Jeff Barnett

[André G. Isaak]

Which isn't self-reference. As I've pointed out, if a notation cannot
capture the general statement "This sentence has property P", then that
notation doesn't capture self-reference.

Until your notation provides a way for expressing 'this sentence is
written in German' in which it comes out as false rather than as
infinitely recursive, then your notation doesn't capture self-reference.

> In Math
> LP := ~True(LP)
> we are only dealing with concepts not finite strings making the
> expression infitely recursive.
>
>>
>>>> would need to be categorized as a sentence rather than a definition
>>>> in your grammar. But your grammar lacks any way of translating "this
>>>> sentence". Definitions or "macro expansion" don't capture this.
>>>>
>>>
>>> They capture it closer than anything else that I can think of.
>>> LP := ~AnyPedicateAtALL(LP) // specifies an infinite term
>>>
>>> All the other ideas that everyone else has is: "lets simply ignore
>>> pathogical self-reference because there is no way to say it using
>>> symbolic logic."
>>
>> There is, of course, another, far more sensible alternative. Since the
>> liar's paradox is something that arises in natural language but not in
>> logic,
>
> The ONLY reason why it does no arise in logic is because nobody ever
> bothered to translate it to logic. The Liar Paradox is merely a
> proposition that makes an assertion about its own truth value. It need
> not know anything about the world.

The reason it doesn't arise in logic is that the goal of logic is to
create systems which are *consistent*. Deliberately trying to find some
way to allow inconsistent propositions is an absurd goal.

And logic doesn't know anything about the world, nor should it need to.

André

> It was obvious to you that the truth teller paradox is vacuous.
> "This sentence is true."  True about what?
> True about being true. True about being true about what?
>
> The Liar Paradox also lack a truth object, it is vacuous.
> Because it is vacuous it meets this definition:
>
> A theory T is incomplete if and only if there is some sentence φ such
> that (T ⊬ φ) and (T ⊬ ¬φ).
>
> Vacuous sentences can neither be proved nor disproved because they are
> vacuous.
>
>> discuss it in natural language rather than in the language of logic.
>>
>> André
>>
>
>


--

[olcott]

You have sufficiently proven that you are not a fool, I wonder why you
continue acting like one?

[André G. Isaak]

On 2020-09-29 18:40, olcott wrote:
> On 9/29/2020 5:26 PM, Ben Bacarisse wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> Yet symbolic [logic] has no way to precisely specify actual
>>> self-reference so I had to make one up.
>>
>> Yet you claim that Gödel's proof uses self-reference.  Will you now
>> retract that claim?  If not, why make up a way to do it when you think
>> Gödel managed it nearly a century ago?
>>
>
> https://mavdisk.mnsu.edu/pj2943kt/Fall%202015/Promotion%20Application/Previous%20Years%20Article%2022%20Materials/godel-1931.pdf
>
>
> 14 Every epistemological antinomy can likewise be used for a similar
> undecidability proof. (Gödel 1931)

Which is his way of saying the proof was loosely inspired by the
antinomy, not that it contains a formalization of that antinomy.

James Watson claims that his discovery of the double-helix structure of
DNA was inspired by a dream of two intertwined snakes. That doesn't mean
that there are snakes in DNA, or in his theory of DNA (Watson doesn't
specify whether these snakes tempted him into stealing Rosalind
Franklin's research which likely played a more significant role in "his"
discovery than the snakes did).

Gödel's math stands on its own. Coming up with contrived interpretations
of a footnote isn't going to change it.

[olcott]

You continue with the same mere unsupported assertion.
I explained several different ways to formalize pathological self
reference and it all boils down that you simply disbelieve them.

> if a notation cannot
> capture the general statement "This sentence has property P", then that
> notation doesn't capture self-reference.
>

The notion of (pathological) self reference in the case is that the
expression refers to a vacuous property that it does not have.

> Until your notation provides a way for expressing 'this sentence is
> written in German' in which it comes out as false rather than as
> infinitely recursive, then your notation doesn't capture self-reference.

That sentence is NOT referring to itself, it is refering to its natural
language encoding.

"This sentence is true."
is a proposition that refers to its own truth value.

>> In Math
>> LP := ~True(LP)
>> we are only dealing with concepts not finite strings making the
>> expression infitely recursive.
>>
>>>
>>>>> would need to be categorized as a sentence rather than a definition
>>>>> in your grammar. But your grammar lacks any way of translating
>>>>> "this sentence". Definitions or "macro expansion" don't capture this.
>>>>>
>>>>
>>>> They capture it closer than anything else that I can think of.
>>>> LP := ~AnyPedicateAtALL(LP) // specifies an infinite term
>>>>
>>>> All the other ideas that everyone else has is: "lets simply ignore
>>>> pathogical self-reference because there is no way to say it using
>>>> symbolic logic."
>>>
>>> There is, of course, another, far more sensible alternative. Since
>>> the liar's paradox is something that arises in natural language but
>>> not in logic,
>>
>> The ONLY reason why it does no arise in logic is because nobody ever
>> bothered to translate it to logic. The Liar Paradox is merely a
>> proposition that makes an assertion about its own truth value. It need
>> not know anything about the world.
>
> The reason it doesn't arise in logic is that the goal of logic is to
> create systems which are *consistent*. Deliberately trying to find some
> way to allow inconsistent propositions is an absurd goal.

Deliberately showing that the standard definition of incompleteness is
simply wrong-headed:

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

Because it reject whole formal system on the basis of ill-formed
expessions.

>
> And logic doesn't know anything about the world, nor should it need to.

The point is that we do not need to formalize natural language to
formalize the liar paradox because the liar paradox only requires the
ordinary attributes of propositions.

X := ¬(P ∨ Q) ↔ (¬P ∧ ¬Q)
In the above case we can simply say that X is true.

In the following cases we can say that the truth value is vacuous:
LP := ~True(LP)
G := ~Provable(G)

That you simply do not believe me counts as less than no rebuttal at
all. Instead of any sort of rebuttal it is merely an example of the
systematic error of bias.

>
> André
>
>> It was obvious to you that the truth teller paradox is vacuous.
>> "This sentence is true."  True about what?
>> True about being true. True about being true about what?
>>
>> The Liar Paradox also lack a truth object, it is vacuous.
>> Because it is vacuous it meets this definition:
>>
>> A theory T is incomplete if and only if there is some sentence φ such
>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>
>> Vacuous sentences can neither be proved nor disproved because they are
>> vacuous.
>>
>>> discuss it in natural language rather than in the language of logic.
>>>
>>> André
>>>
>>
>>
>
>


--

Copyright 2020 Pete Olcott

[olcott]

It is not and never has been the math that counts.
It is and always has been the meta math that counts.

The verifiable fact that the Liar Paradox meets this spec:
(Tarski based his whole proof on the liar Paradox)

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

And the only reason why the Liar Paradox cannot be proved or disproved
is that it is infinitely recursive proves that the foundational basis of
the definition of incompleteness is incorrect.

You already agreed that the truth teller paradox is vacuous what's up
with your position now?

[André G. Isaak]

On 2020-09-29 21:41, olcott wrote:
> On 9/29/2020 10:25 PM, André G. Isaak wrote:
>> On 2020-09-29 18:51, olcott wrote:
>>> On 9/29/2020 5:40 PM, André G. Isaak wrote:
>>>> On 2020-09-29 14:47, olcott wrote:

>>>>> Yet symbolic has no way to precisely specify actual self-reference
>>>>> so I had to make one up.
>>>>
>>>> Except your made up way doesn't actually capture this.
>>>
>>> Sure it does.
>>> In computer science
>>> #define LP !True(LP)
>>> would specify copying the string !True(!True(!True(...))) an infinite
>>> number of times.
>>
>> Which isn't self-reference. As I've pointed out,
>
> You continue with the same mere unsupported assertion.

It isn't unsupported. I support it directly below.

> I explained several different ways to formalize pathological self
> reference and it all boils down that you simply disbelieve them.

You can't formalize 'pathological' self-reference without first
formalizing self-reference.

>> if a notation cannot capture the general statement "This sentence has
>> property P", then that notation doesn't capture self-reference.
>>
>
> The notion of (pathological) self reference in the case is that the
> expression refers to a vacuous property that it does not have.
>
>> Until your notation provides a way for expressing 'this sentence is
>> written in German' in which it comes out as false rather than as
>> infinitely recursive, then your notation doesn't capture self-reference.
>
> That sentence is NOT referring to itself, it is refering to its natural
> language encoding.

Of course that sentence refers to itself. What the hell do you think
"this sentence" is referring to if not itself?

> "This sentence is true."
> is a proposition that refers to its own truth value.

That sentence is self-referential in exactly the same way that "this
sentence is in german" is self-referential.

The only difference is that the latter results in an undecidable
proposition whereas the former does not.

Claiming that a formal system is incomplete does *not* involved
rejecting that system. It involves claiming that it is incomplete. And
no one has argued that systems are incomplete based on 'ill-formed'
expressions.

>>
>> And logic doesn't know anything about the world, nor should it need to.
>
> The point is that we do not need to formalize natural language to
> formalize the liar paradox because the liar paradox only requires the
> ordinary attributes of propositions.
>
> X := ¬(P ∨ Q) ↔ (¬P ∧ ¬Q)
> In the above case we can simply say that X is true.

Except that isn't a proposition in any standard logic. Your MTT is not a
standard logic, and is far too ill-defined to be useful as one.

> In the following cases we can say that the truth value is vacuous:
> LP := ~True(LP)
>  G := ~Provable(G)
>
> That you simply do not believe me counts as less than no rebuttal at
> all. Instead of any sort of rebuttal it is merely an example of the
> systematic error of bias.

No. My point has always been that until you actually define a semantics
to go along with your syntax, you don't have a system at all. Saying you
are using the 'standard semantics' doesn't cut it. You can't mix
concepts from different languages and assume that the results will be
internally coherent.

>>
>> André
>>
>>> It was obvious to you that the truth teller paradox is vacuous.
>>> "This sentence is true."  True about what?
>>> True about being true. True about being true about what?
>>>
>>> The Liar Paradox also lack a truth object, it is vacuous.
>>> Because it is vacuous it meets this definition:
>>>
>>> A theory T is incomplete if and only if there is some sentence φ such
>>> that (T ⊬ φ) and (T ⊬ ¬φ).

No, the liar's paradox does not meet that definition. For starters, it
isn't a statement of logic. And even in natural language, it is not
undecidable, it is inconsistent.

>>> Vacuous sentences can neither be proved nor disproved because they
>>> are vacuous.

(A ∨ ¬A) is entirely vacuous until an interpretation is supplied, yet it
is perfectly provable.

[Keith Thompson]

André G. Isaak <agi...@gm.invalid> writes:
[...]

> James Watson claims that his discovery of the double-helix structure
> of DNA was inspired by a dream of two intertwined snakes. That doesn't
> mean that there are snakes in DNA, or in his theory of DNA (Watson
> doesn't specify whether these snakes tempted him into stealing
> Rosalind Franklin's research which likely played a more significant
> role in "his" discovery than the snakes did).

[...]

I haven't heard that. Are you thinking of Kekule's discovery of the
ring structure of benzene via a daydreame of a snake biting its own
tail?

--
Keith Thompson (The_Other_Keith) Keith.S.T...@gmail.com
Working, but not speaking, for Philips Healthcare
void Void(void) { Void(); } /* The recursive call of the void */

[André G. Isaak]

On 2020-09-29 22:29, Keith Thompson wrote:
> André G. Isaak <agi...@gm.invalid> writes:
> [...]
>> James Watson claims that his discovery of the double-helix structure
>> of DNA was inspired by a dream of two intertwined snakes. That doesn't
>> mean that there are snakes in DNA, or in his theory of DNA (Watson
>> doesn't specify whether these snakes tempted him into stealing
>> Rosalind Franklin's research which likely played a more significant
>> role in "his" discovery than the snakes did).
> [...]
>
> I haven't heard that. Are you thinking of Kekule's discovery of the
> ring structure of benzene via a daydreame of a snake biting its own
> tail?

No. I was aware of benzene anecdote, but was definitely thinking of
Watson. Whether the story is apocryphal is another matter.

A quick web search finds a variety of links but none which strike me as
particularly reputable. Here's one example.

https://uh.edu/engines/epi1868.htm

[Keith Thompson]

André G. Isaak <agi...@gm.invalid> writes:
> On 2020-09-29 22:29, Keith Thompson wrote:
>> André G. Isaak <agi...@gm.invalid> writes:
>> [...]
>>> James Watson claims that his discovery of the double-helix structure
>>> of DNA was inspired by a dream of two intertwined snakes. That doesn't
>>> mean that there are snakes in DNA, or in his theory of DNA (Watson
>>> doesn't specify whether these snakes tempted him into stealing
>>> Rosalind Franklin's research which likely played a more significant
>>> role in "his" discovery than the snakes did).
>> [...]
>>
>> I haven't heard that. Are you thinking of Kekule's discovery of the
>> ring structure of benzene via a daydreame of a snake biting its own
>> tail?
>
> No. I was aware of benzene anecdote, but was definitely thinking of
> Watson. Whether the story is apocryphal is another matter.
>
> A quick web search finds a variety of links but none which strike me
> as particularly reputable. Here's one example.
>
> https://uh.edu/engines/epi1868.htm

The Kekule story is fairly well known. I wonder if somebody (not you)
conflated the two.

https://en.wikipedia.org/wiki/List_of_dreams#Double_Helix_structure_of_DNA
refers to Watson giving a TED talk mentioning a dream of a spiral staircase.

Completely irrelevant, of course, but what the heck.

[olcott]

On 9/29/2020 11:22 PM, André G. Isaak wrote:
> On 2020-09-29 21:41, olcott wrote:
>> On 9/29/2020 10:25 PM, André G. Isaak wrote:
>>> On 2020-09-29 18:51, olcott wrote:
>>>> On 9/29/2020 5:40 PM, André G. Isaak wrote:
>>>>> On 2020-09-29 14:47, olcott wrote:
>
>>>>>> Yet symbolic has no way to precisely specify actual self-reference
>>>>>> so I had to make one up.
>>>>>
>>>>> Except your made up way doesn't actually capture this.
>>>>
>>>> Sure it does.
>>>> In computer science
>>>> #define LP !True(LP)
>>>> would specify copying the string !True(!True(!True(...))) an
>>>> infinite number of times.
>>>
>>> Which isn't self-reference. As I've pointed out,
>>
>> You continue with the same mere unsupported assertion.
>
> It isn't unsupported. I support it directly below.
>
>> I explained several different ways to formalize pathological self
>> reference and it all boils down that you simply disbelieve them.
>
> You can't formalize 'pathological' self-reference without first
> formalizing self-reference.

That seems reasonable except that at the level of logical propositions
there may not be any kind of self-reference that is not pathological.

>>> if a notation cannot capture the general statement "This sentence has
>>> property P", then that notation doesn't capture self-reference.
>>>
>>
>> The notion of (pathological) self reference in the case is that the
>> expression refers to a vacuous property that it does not have.
>>
>>> Until your notation provides a way for expressing 'this sentence is
>>> written in German' in which it comes out as false rather than as
>>> infinitely recursive, then your notation doesn't capture self-reference.
>>
>> That sentence is NOT referring to itself, it is refering to its
>> natural language encoding.
>
> Of course that sentence refers to itself. What the hell do you think
> "this sentence" is referring to if not itself?

I always thought that the sentence:
"This sentence has five words". referred to itself, except that when it
is translated into symbolic logic it ceases to have any words.

>> "This sentence is true."
>> is a proposition that refers to its own truth value.
>
> That sentence is self-referential in exactly the same way that "this
> sentence is in german" is self-referential.

int main()
{
bool LP = !(LP == true);
}

Taken literally means to compare a non-exsitent truth value to true and
then negate the result.

>
> The only difference is that the latter results in an undecidable
> proposition whereas the former does not.

It is not really undecidable at all. It has no truth value at all.

I am doing that right now. I am not no one.

>>>
>>> And logic doesn't know anything about the world, nor should it need to.
>>
>> The point is that we do not need to formalize natural language to
>> formalize the liar paradox because the liar paradox only requires the
>> ordinary attributes of propositions.
>>
>> X := ¬(P ∨ Q) ↔ (¬P ∧ ¬Q)
>> In the above case we can simply say that X is true.
>
> Except that isn't a proposition in any standard logic. Your MTT is not a
> standard logic, and is far too ill-defined to be useful as one.

So then you say that all new ideas must be wrong because they are new
ideas.

>> In the following cases we can say that the truth value is vacuous:
>> LP := ~True(LP)
>>   G := ~Provable(G)
>>
>> That you simply do not believe me counts as less than no rebuttal at
>> all. Instead of any sort of rebuttal it is merely an example of the
>> systematic error of bias.
>
> No. My point has always been that until you actually define a semantics
> to go along with your syntax, you don't have a system at all. Saying you
> are using the 'standard semantics' doesn't cut it. You can't mix
> concepts from different languages and assume that the results will be
> internally coherent.

They work consistently and you can't show otherwise.

>>>
>>> André
>>>
>>>> It was obvious to you that the truth teller paradox is vacuous.
>>>> "This sentence is true."  True about what?
>>>> True about being true. True about being true about what?
>>>>
>>>> The Liar Paradox also lack a truth object, it is vacuous.
>>>> Because it is vacuous it meets this definition:
>>>>
>>>> A theory T is incomplete if and only if there is some sentence φ
>>>> such that (T ⊬ φ) and (T ⊬ ¬φ).
>
> No, the liar's paradox does not meet that definition. For starters, it
> isn't a statement of logic. And even in natural language, it is not
> undecidable, it is inconsistent.

Because it cannot be proved or disproved IT DOES MEET THAT DEFINITION.

>>>> Vacuous sentences can neither be proved nor disproved because they
>>>> are vacuous.
>
> (A ∨ ¬A) is entirely vacuous until an interpretation is supplied, yet it
> is perfectly provable.
>
> André

Yeah who knows maybe some people will interpret this: (A ∨ ¬A)
as a demand for an ice cream cone right now!!!

[André G. Isaak]

On 2020-09-29 23:47, Keith Thompson wrote:

> The Kekule story is fairly well known. I wonder if somebody (not you)
> conflated the two.

That sounds like a reasonable hypothesis. I don't recall where I first
encountered this claim, and none of the sites which I found that mention
it seem particularly scholarly so it may well simply be a mistake that
has propagated.

[Richard Damon]

On 9/29/20 11:41 PM, olcott wrote:
>
> A theory T is incomplete if and only if there is some sentence φ such
> that (T ⊬ φ) and (T ⊬ ¬φ).
>
> Because it reject whole formal system on the basis of ill-formed
> expessions.

"Incomplete" doesn't reject whole formal systems, it states that such a
consistant system of axioms that can be enumerated by some algorithm,
will have some propositions that they can not prove or disprove, or
stated another way, some true statements they can not prove just by the
axiom of the system (if it is just a false statement that can not be
disproven, then you can convert it to its negation and that isn't provable)

The statement also fully allows systems that are 'complete', but also
points out that such systems are limited in the sense that they can not
express all truths about the arithmetic of natural numbers.

You having an axiom that Truth is defined by ability to be proven, is an
acceptable axiom, but Godel proof just shows that the system you derive
from that axiom will be incapable of expressing all the truths about the
arithmetic of natural numbers.

I suppose you could conclude from this that to properly show all the
truths about the arithmetic of natural numbers, we need to be able to
employ the recursion that you are rejecting by your axioms.

[olcott]

On 9/30/2020 8:08 AM, Richard Damon wrote:
> On 9/29/20 11:41 PM, olcott wrote:
>>
>> A theory T is incomplete if and only if there is some sentence φ such
>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>
>> Because it reject whole formal system on the basis of ill-formed
>> expessions.
>
> "Incomplete" doesn't reject whole formal systems, it states that such a
> consistant system of axioms that can be enumerated by some algorithm,
> will have some propositions that they can not prove or disprove, or
> stated another way, some true statements they can not prove just by the
> axiom of the system (if it is just a false statement that can not be
> disproven, then you can convert it to its negation and that isn't provable)

The problem is that the inability of a formal system to prove or
disprove ill-formed propositions makes this formal system incomplete.

> The statement also fully allows systems that are 'complete', but also
> points out that such systems are limited in the sense that they can not
> express all truths about the arithmetic of natural numbers.

When we cut out the purely extraneous complexity of natural numbers
See the bottom of the first page:
https://www.researchgate.net/publication/342503359_Defining_Godel_Incompleteness_Away

And perform this same proof on the basis of its meta-mathematics alone,
then we can see that any logical expression that asserts that it is
logically equivalent to its own unprovability would fail Prolog's
unify_with_occurs_check/2 because it specifies an "infinite term".

http://www.liarparadox.org/Prolog_Detects_Pathological_Self_Reference.pdf

>
> You having an axiom that Truth is defined by ability to be proven, is an
> acceptable axiom, but Godel proof just shows that the system you derive
> from that axiom will be incapable of expressing all the truths about the
> arithmetic of natural numbers.
>
> I suppose you could conclude from this that to properly show all the
> truths about the arithmetic of natural numbers, we need to be able to
> employ the recursion that you are rejecting by your axioms.
>

[olcott]

On 9/30/2020 6:43 AM, Ben Bacarisse wrote:
> olcott <No...@NoWhere.com> writes:
>

>> On 9/29/2020 8:12 PM, Ben Bacarisse wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> On 9/29/2020 5:26 PM, Ben Bacarisse wrote:
>>>>> olcott <No...@NoWhere.com> writes:
>>>>>
>>>>>> Yet symbolic [logic] has no way to precisely specify actual
>>>>>> self-reference so I had to make one up.
>>>>>
>>>>> Yet you claim that Gödel's proof uses self-reference. Will you now
>>>>> retract that claim? If not, why make up a way to do it when you think
>>>>> Gödel managed it nearly a century ago?
>>>>
>>>> https://mavdisk.mnsu.edu/pj2943kt/Fall%202015/Promotion%20Application/Previous%20Years%20Article%2022%20Materials/godel-1931.pdf
>>>>
>>>> 14 Every epistemological antinomy can likewise be used for a similar
>>>> undecidability proof. (Gödel 1931)
>>>>
>>>> Gödel 1931 ON FORMALLY UNDECIDABLE PROPOSITIONS OF PRINCIPIA
>>>> MATHEMATICA AND RELATED SYSTEMS I
>>>>
>>>> A theory T is incomplete if and only if there is some sentence φ such
>>>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>>>

>>>> Instead of going around and around about what the math says...
>>>
>>> By which you mean you can see the problem (you can't be right about both
>>> your claims) so you'd rather not talk about it. OK. Fine by me.
>>
>> Instead of going around and around about what the math says we go
>> straight to the actual crux of the issue which is the meta-math.
>
> I'm asking about what you said. Did Gödel find a way to do what you say
> is not possible in "symbolic logic", or were you wrong to say that his
> proof involves self-reference? You can't be right about both.
>

see page 41
https://mavdisk.mnsu.edu/pj2943kt/Fall%202015/Promotion%20Application/Previous%20Years%20Article%2022%20Materials/godel-1931.pdf

Gödel both denies the circular nature of his proof and explains the
precise details of this circular nature in the same footnote.

15 In spite of appearances, there is nothing circular about such a
proposition, since it begins by asserting the unprovability of a wholly
determinate formula (namely the q-th in the alphabetical arrangement
with a definite substitution), and only subsequently (and in some way by
accident) does it emerge that this formula is precisely that by which
the proposition was itself expressed.

... proposition X, ... begins by asserting the unprovability of ...
formula Y ... and only subsequently ... does it emerge that this formula
Y is precisely that by which the proposition X was itself expressed.
(formula Y expresses proposition X).

proposition X asserts the unprovability of formula Y which expresses
proposition X

Gödel found an enormously convoluted way to express pathological
self-reference that is much simpler with the metalanguage of MTT.

X := (F ⊬ Y)
Y := X
becomes
X := (F ⊬ X)

Gödel's way of expressing pathological self-reference was so convoluted
that in the same footnote that he denies circular reference he explains
all of the details of exactly how the reference is indeed circular.

We have to untangle his convoluted natural language grammar to most
clearly see this:

(see above analysis).
proposition X asserts the unprovability of formula Y which expresses
proposition X

[olcott]

On 9/30/2020 9:57 AM, André G. Isaak wrote:
> On 2020-09-29 19:38, Ben Bacarisse wrote:
>
>> The maths/CS distinction you make is an artificial one.
>
> I'm not actually convinced that Olcott knows what CS is. There's been
> many instances where he seems to use it as a synonym for 'computer
> programming'.
>
> André
>

Compared to the average PhD mathematician I know hardly any of the whole
body of mathematics at all. Compared to the average PhD computer
scientist my knowledge of the whole body of computer science is a little
better yet still far far less.

My whole focus since 2004 is the single issue of how pathological
self-reference creates what appears to be undecidable expressions of
language. From the perspective of mathematics I simply ignore most of
mathematics and only examine the portion of meta-mathematics that most
directly applies to pathological self-reference.

So I may be an expert on the meta-mathematics of pathological
self-reference and mostly clueless about the rest of the body of
mathematics.

Everyone here has been judging my credibility on the meta-mathematics of
pathological self-reference entirely on the basis of my lack of
credibility in mathematics.

That turns out to be an incorrect basis, firstly because the notion of
credibility itself is sometimes a very poor proxy for validity. Some
people lacking the proper credentials to show that they should know what
they are talking about indeed still do know what they are talking about.

[olcott]

> You are having a lot of trouble with this. I don't know how to be more
> clear. I am asking about what /you/ said, not what Gödel said.

> You
> said that something what impossible despite having claimed for years
> that it was exactly what certain proofs do.

Garbled grammar. I can't make it out.

> It makes no difference if
> the authors of those proofs deny or affirm it. Heck, it makes no
> different if the proofs are junk written by madmen. I just want to know
> which of your contradictory claim you now hold to be true.

>
>> Gödel found an enormously convoluted way to express pathological
>> self-reference
>

> Well, there's the answer! You were wrong to say that it is not possible
> to do it in symbolic logic. It is possible.
>

He did not do it in symbolic logic. It can't be done in symbolic logic.
He cobbled together a convoluted mess of arithmetic that seems to meet
the standard definition of incompleteness:

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

> Here "enormously convoluted" just means that you don't understand it.
> If you did, you would see why it can't be expressed in your
> semantics-free logic grammar.
>

The above definition of incompleteness is the simplest way to express
incompleteness anything added on top of that definition is extraneous
and thus inessential details.

When we use Minimal Type Theory to express the same incompleteness proof
there is no need to artificially contrive a provability predicate from
very many arithmetic expressions.

We simply use the provability operator directly: ⊢. Once we eliminate
the extraneous Gödel numbers from the incompleteness proof we can begin
to to see why G is neither provable nor disprovable. Gödel's proof only
showed that G is neither provable nor disprovable he never showed why.

As soon as we see why the whole conclusion of incompleteness is refuted
on the basis that its definition does not exclude ill-formed sentences.

[olcott]

On 10/11/2020 6:55 PM, André G. Isaak wrote:
> On 2020-10-11 08:05, olcott wrote:
>> On 10/11/2020 7:52 AM, Andy Walker wrote:
>>> On 11/10/2020 03:29, olcott wrote:
>>>> Undecidable propositions are decided to not be propositions at all.
>>>
>>>      Unfortunately for this idea, whether or not a proposition is
>>> decidable is itself undecidable.  So you have no algorithm which
>>> shows whether a proto-proposition is an actual proposition [because
>>> it is decidable] or one that you have decided is not a proposition
>>> [because it is undecidable].  Of course, there is then a simple
>>> proof that all the ones you can't decide are undecidable, but you
>>> don't know which they are.
>>>
>>
>> ∀x (Proposition(x) ↔ (⊢x ∨ ⊢¬x))
>
> There are thousands of outstanding mathematical problems for which no
> proof is know. It's possible that some of those problems have no proof.
> It's also possible that they have a proof that no one has stumbled upon
> yet. How do you propose to deal with these?
>
> André
>

Unless and until they are provable or disprovable they do not count as
valid propositions.

All that I have done is take the standard definition of incompleteness
and switch the "blame".

A theory T is incomplete if and only if there is some sentence φ such
that (T ⊬ φ) and (T ⊬ ¬φ).

with the blame switched from theory T to expression φ:

Expression φ is a proposition of theory T if and only if (T ⊢ φ) or (T ⊢
¬φ).

// DeMorgan's theorem applied so that I can specify what <is>
// a proposition instead of what is not a proposition.

This one tiny little change makes Gödel's 1931 theorem impossible to
prove because it loses its entire basis.

[André G. Isaak]

On 2020-10-11 21:45, olcott wrote:
> On 10/11/2020 6:55 PM, André G. Isaak wrote:
>> On 2020-10-11 08:05, olcott wrote:
>>> On 10/11/2020 7:52 AM, Andy Walker wrote:
>>>> On 11/10/2020 03:29, olcott wrote:
>>>>> Undecidable propositions are decided to not be propositions at all.
>>>>
>>>>      Unfortunately for this idea, whether or not a proposition is
>>>> decidable is itself undecidable.  So you have no algorithm which
>>>> shows whether a proto-proposition is an actual proposition [because
>>>> it is decidable] or one that you have decided is not a proposition
>>>> [because it is undecidable].  Of course, there is then a simple
>>>> proof that all the ones you can't decide are undecidable, but you
>>>> don't know which they are.
>>>>
>>>
>>> ∀x (Proposition(x) ↔ (⊢x ∨ ⊢¬x))
>>
>> There are thousands of outstanding mathematical problems for which no
>> proof is know. It's possible that some of those problems have no
>> proof. It's also possible that they have a proof that no one has
>> stumbled upon yet. How do you propose to deal with these?
>>
>> André
>>
>
> Unless and until they are provable or disprovable they do not count as
> valid propositions.

Now this position is entirely ridiculous, since it would imply that the
only things that count as propositions are axioms.

After all, everything else is initially unproven until someone proves
it. But if you declare such things to 'not be valid propositions' based
on the fact they have yet to be proved, then presumably your system will
not allow any attempts at proving them since you have already declared
them to be ill-formed.

And how exactly is your system supposed to know which propositions have
been proven? Does it maintain a list of all proven propositions? In that
case, your system isn't used to form proofs at all. People working in
*other* systems prove theorems, and then you add them to your list.

André

> All that I have done is take the standard definition of incompleteness
> and switch the "blame".
>
> A theory T is incomplete if and only if there is some sentence φ such
> that (T ⊬ φ) and (T ⊬ ¬φ).
>
> with the blame switched from theory T to expression φ:
>
> Expression φ is a proposition of theory T if and only if (T ⊢ φ) or (T ⊢
> ¬φ).
>
> // DeMorgan's theorem applied so that I can specify what <is>
> // a proposition instead of what is not a proposition.
>
> This one tiny little change makes Gödel's 1931 theorem impossible to
> prove because it loses its entire basis.
>
>


--

[olcott]

That is all explained in the part that you ignored:

-- All that I have done is take the standard definition
-- of incompleteness and switch the "blame".

-- All that I have done is take the standard definition
-- of incompleteness and switch the "blame".

-- All that I have done is take the standard definition
-- of incompleteness and switch the "blame".

-- All that I have done is take the standard definition
-- of incompleteness and switch the "blame".

>
>> All that I have done is take the standard definition of incompleteness
>> and switch the "blame".
>>
>> A theory T is incomplete if and only if there is some sentence φ such
>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>
>> with the blame switched from theory T to expression φ:
>>
>> Expression φ is a proposition of theory T if and only if (T ⊢ φ) or (T
>> ⊢ ¬φ).
>>
>> // DeMorgan's theorem applied so that I can specify what <is>
>> // a proposition instead of what is not a proposition.
>>
>> This one tiny little change makes Gödel's 1931 theorem impossible to
>> prove because it loses its entire basis.
>>
>>
>
>


--

Copyright 2020 Pete Olcott

[olcott]

-- All that I have done is take the standard definition
-- of incompleteness and switch the "blame".

-- This one tiny little change makes Gödel's 1931 theorem
-- impossible to prove because it loses its entire basis.

-- This one tiny little change makes Gödel's 1931 theorem
-- impossible to prove because it loses its entire basis.

-- This one tiny little change makes Gödel's 1931 theorem
-- impossible to prove because it loses its entire basis.

>
>> All that I have done is take the standard definition of incompleteness
>> and switch the "blame".
>>
>> A theory T is incomplete if and only if there is some sentence φ such
>> that (T ⊬ φ) and (T ⊬ ¬φ).
>>
>> with the blame switched from theory T to expression φ:
>>
>> Expression φ is a proposition of theory T if and only if (T ⊢ φ) or (T
>> ⊢ ¬φ).
>>
>> // DeMorgan's theorem applied so that I can specify what <is>
>> // a proposition instead of what is not a proposition.
>>
>> This one tiny little change makes Gödel's 1931 theorem impossible to
>> prove because it loses its entire basis.
>>
>>
>
>


--

Copyright 2020 Pete Olcott

[André G. Isaak]

Whether you say that once, or eight different times in two separate
posts, doesn't change the fact that it doesn't address any of the points
I made at all.

How do you distinguish an undecidable proposition from one which you
simply have been unable to prove or disprove. You can't simply dismiss
any unproven propositions as 'non-propositions' based on your inability
to prove or disprove them.

And a formal system has no knowledge whatsoever of which theorems have
been proven in the past.

André

[olcott]

By simply shifting the blame incompleteness is abolished and Gödel's
1931 proof loses its entire basis, making everything else abut his proof
moot.

> How do you distinguish an undecidable proposition from one which you
> simply have been unable to prove or disprove. You can't simply dismiss
> any unproven propositions as 'non-propositions' based on your inability
> to prove or disprove them.
>

If a proposition is impossible to prove or disprove it is decided to be
incorrect thus eliminating undecidable expressions of language from
being construed as propositions.

This is a revision of my idea that addresses your objection.

> And a formal system has no knowledge whatsoever of which theorems have
> been proven in the past.
>

All that I am doing is abolishing the term: "undecidable proposition"
and replacing it with: "incorrect expression of language".

A formal system cannot be construed to be incomplete on the basis of its
inability to prove or disprove: "incorrect expressions of language".

> André

[André G. Isaak]

No. Gödel's Incompleteness Theorems remain proven theorems regardless of
your attempts to redefine terms.

>> How do you distinguish an undecidable proposition from one which you
>> simply have been unable to prove or disprove. You can't simply dismiss
>> any unproven propositions as 'non-propositions' based on your
>> inability to prove or disprove them.
>>
>
> If a proposition is impossible to prove or disprove it is decided to be
> incorrect thus eliminating undecidable expressions of language from
> being construed as propositions.

But how do you determine whether a proposition is impossible to prove or
disprove as opposed to simply being one that you have been unable to
prove or disprove?

> This is a revision of my idea that addresses your objection.

It doesn't address them at all.

>> And a formal system has no knowledge whatsoever of which theorems have
>> been proven in the past.
>>
>
> All that I am doing is abolishing the term: "undecidable proposition"
> and replacing it with: "incorrect expression of language".

You are not in a position to abolish a widely accepted term and replace
it with something else. Mathematics uses terminology as it is defined
within mathematics, not as it is defined by you.

[olcott]

If my definition is correct and his is incorrect then his whole proof
has been refuted.

>
>>> How do you distinguish an undecidable proposition from one which you
>>> simply have been unable to prove or disprove. You can't simply
>>> dismiss any unproven propositions as 'non-propositions' based on your
>>> inability to prove or disprove them.
>>>
>>
>> If a proposition is impossible to prove or disprove it is decided to
>> be incorrect thus eliminating undecidable expressions of language from
>> being construed as propositions.
>
> But how do you determine whether a proposition is impossible to prove or
> disprove as opposed to simply being one that you have been unable to
> prove or disprove?

All that I am doing is taking the already existing set of undecidable
propositions and reclassifying this exact same set as incorrect
expressions of language.

>
>> This is a revision of my idea that addresses your objection.
>
> It doesn't address them at all.

Only because you seem to not be paying close enough attention.
With my more narrowly defined terms your objections become out-of-scope.

>
>>> And a formal system has no knowledge whatsoever of which theorems
>>> have been proven in the past.
>>>
>>
>> All that I am doing is abolishing the term: "undecidable proposition"
>> and replacing it with: "incorrect expression of language".
>
> You are not in a position to abolish a widely accepted term and replace
> it with something else. Mathematics uses terminology as it is defined
> within mathematics, not as it is defined by you.
>
> André

If my definition is correct and the one that Gödel used is incorrect
then his whole proof fails.

[André G. Isaak]

His definition is correct.

It doesn't even make sense to call an accepted definition 'incorrect'.

>>
>>>> How do you distinguish an undecidable proposition from one which you
>>>> simply have been unable to prove or disprove. You can't simply
>>>> dismiss any unproven propositions as 'non-propositions' based on
>>>> your inability to prove or disprove them.
>>>>
>>>
>>> If a proposition is impossible to prove or disprove it is decided to
>>> be incorrect thus eliminating undecidable expressions of language
>>> from being construed as propositions.
>>
>> But how do you determine whether a proposition is impossible to prove
>> or disprove as opposed to simply being one that you have been unable
>> to prove or disprove?
>
>
> All that I am doing is taking the already existing set of undecidable
> propositions and reclassifying this exact same set as incorrect
> expressions of language.

And what exactly do you mean by 'the existing set of undecidable
propositions'? How do you determine membership in that set? You can't
declare some set of propositions to be 'nonpropositions' unless you can
actually describe that set.

[olcott]

It is certainly the case that self-contradictory expression of language
exist and these non-truth bearers prove that a formal system is
"incomplete" entirely on that basis that they are not truth bearers.

It is like saying that natural language is an incomplete formal system
because natural language cannot correctly answer the question: What time
is it (yes or no)?

>
>>>
>>>>> How do you distinguish an undecidable proposition from one which
>>>>> you simply have been unable to prove or disprove. You can't simply
>>>>> dismiss any unproven propositions as 'non-propositions' based on
>>>>> your inability to prove or disprove them.
>>>>>
>>>>
>>>> If a proposition is impossible to prove or disprove it is decided to
>>>> be incorrect thus eliminating undecidable expressions of language
>>>> from being construed as propositions.
>>>
>>> But how do you determine whether a proposition is impossible to prove
>>> or disprove as opposed to simply being one that you have been unable
>>> to prove or disprove?
>>
>>
>> All that I am doing is taking the already existing set of undecidable
>> propositions and reclassifying this exact same set as incorrect
>> expressions of language.
>
> And what exactly do you mean by 'the existing set of undecidable
> propositions'? How do you determine membership in that set? You can't
> declare some set of propositions to be 'nonpropositions' unless you can
> actually describe that set.
>
> André
>

An expression φ is undecidable in theory T if and only if
(T ⊬ φ) and (T ⊬ ¬φ).

[André G. Isaak]

Self-contradictory sentences exist in NATURAL language. They don't exist
in the standard languages of logic including the one used in Gödel's
proof, and play no role in proving incompleteness.

> It is like saying that natural language is an incomplete formal system
> because natural language cannot correctly answer the question: What time
> is it (yes or no)?

Natural language isn't a formal system at all. And I have no idea why
you always insist on using interrogatives as examples. Interrogatives
don't exist in logic, and only declarative sentences have truth values
in natural language.

>>
>>>>
>>>>>> How do you distinguish an undecidable proposition from one which
>>>>>> you simply have been unable to prove or disprove. You can't simply
>>>>>> dismiss any unproven propositions as 'non-propositions' based on
>>>>>> your inability to prove or disprove them.
>>>>>>
>>>>>
>>>>> If a proposition is impossible to prove or disprove it is decided
>>>>> to be incorrect thus eliminating undecidable expressions of
>>>>> language from being construed as propositions.
>>>>
>>>> But how do you determine whether a proposition is impossible to
>>>> prove or disprove as opposed to simply being one that you have been
>>>> unable to prove or disprove?
>>>
>>>
>>> All that I am doing is taking the already existing set of undecidable
>>> propositions and reclassifying this exact same set as incorrect
>>> expressions of language.
>>
>> And what exactly do you mean by 'the existing set of undecidable
>> propositions'? How do you determine membership in that set? You can't
>> declare some set of propositions to be 'nonpropositions' unless you
>> can actually describe that set.
>>
>> André
>>
>
> An expression φ is undecidable in theory T if and only if
> (T ⊬ φ) and (T ⊬ ¬φ).

I didn't ask you to define 'undecidable'. I asked you how you would
*determine* whether a given sentence was decidable or not.

[olcott]

Notice that Tarski explicitly refers to:

two mutually contradictory sentences (i.e. such
that one is the negation of the other) neither of
which is provable

And he goes on to make the existence of such sentence his basis
for ignoring: "the principle of the excluded middle."

Here Tarski says that true can diverge from provable because the law
excluded middle does not apply to provable sentences because
self-contradictory sentences (that are obviously true) cannot be proven.

It might appear at first sight … that 'true sentence'
with respect to the language of a formalized
deductive science means nothing other than
'provable theorem'...

Closer reflection shows, however, that this view
must be rejected for the following reason:

no definition of true sentence which is in
agreement with the ordinary usage of language
should have any consequences which contradict
the principle of the excluded middle.

This principle, however, is not valid in the domain
of provable sentences. A simple example of two
mutually contradictory sentences (i.e. such that one
is the negation of the other) neither of which is
provable...

Thus the definition of true sentence which we are
seeking must also cover sentences which are not
provable. http://www.liarparadox.org/tarski_186.pdf

Tarski, Alfred 1983. “The concept of truth in formalized languages” in
Logic Semantics, Metamathematics. Indianapolis: Hacket Publishing
Company, 186.

Copyright 2020 Pete Olcott

[Mike Terry]

Note that André is talking about /self-contradictory/ sentences (which
indeed don't exist in FOL)...

>
> Notice that Tarski explicitly refers to:
>
> two mutually contradictory sentences (i.e. such
> that one is the negation of the other) neither of
> which is provable

ok, so Tarski isn't talking about /self/ contradictory sentences?

Why then are you quoting this here? Could it be that you don't
understand the first thing about what Tarski says?

>
> And he goes on to make the existence of such sentence his basis
> for ignoring: "the principle of the excluded middle."

The text you quote below does not show Tarski "ignoring" the principle.
It shows him explaining why the principle is "not valid in the domain of
provable sentences". I.e. we can have two sentences P and ¬P such that
neither are *provable*. He is saying that /if/ we equated true with
provable, this would actually contradict the principle of excluded
middle, in that the previous example would have 'P v ¬P' as "true",
whereas neither P nor ¬P would be "true".

So far from "ignoring" the principle, it is the basis of his argument!

(I don't expect you would follow any of that though...)

>
> Here Tarski says that true can diverge from provable because the law
> excluded middle does not apply to provable sentences because
> self-contradictory sentences (that are obviously true) cannot be proven.

And where below does Tarski refer to self-contradictory sentences?
Really your summing up of what Tarski is about to say is nonsense...

>
> It might appear at first sight … that 'true sentence'
> with respect to the language of a formalized
> deductive science means nothing other than
> 'provable theorem'...
>
> Closer reflection shows, however, that this view
> must be rejected for the following reason:
>
> no definition of true sentence which is in
> agreement with the ordinary usage of language
> should have any consequences which contradict
> the principle of the excluded middle.
>
> This principle, however, is not valid in the domain
> of provable sentences. A simple example of two
> mutually contradictory sentences (i.e. such that one
> is the negation of the other) neither of which is
> provable...
>
> Thus the definition of true sentence which we are
> seeking must also cover sentences which are not
> provable. http://www.liarparadox.org/tarski_186.pdf
>
> Tarski, Alfred 1983. “The concept of truth in formalized languages” in
> Logic Semantics, Metamathematics. Indianapolis: Hacket Publishing
> Company, 186.
>
>

Look, there's no point quote-mining for quotes you think support your
views when in fact you can't follow even the overall pattern of argument
being employed, let alone the details. Just answer André's questions in
your own words, and if you don't understand his point, ask for help.
(If you did understand his point, you might respond with something
relevant to his point. Making long responses with quotes unrelated to
the specific point is a kind of giveaway...)

Regards,
Mike.

[olcott]

He is merely phrasing a self-contradictory sentence differently.

We could say that the liar paradox and its negation form a pair of
mutually contradictory sentences.

Instead we say that the Liar Paradox is a single sentence that is
neither provable nor disprovable (meaning that its negation is not
provable).

[Mike Terry]

No he isn't. OK, so what do you think is the self-contradictory
sentence that he is phrasing differently?

Mike.

[olcott]

He is using arbitrary self-contradictory sentences to show that true and
diverge from provable.

Here is uses the Liar paradox itself:
http://www.liarparadox.org/247_248.pdf

It would
then be possible to reconstruct the antinomy of the liar in the
metalanguage, by forming in the language itself a sentence x
such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.

[Mike Terry]

On 14/10/2020 01:42, olcott wrote:
> On 10/13/2020 7:37 PM, Mike Terry wrote:
>> On 14/10/2020 01:01, olcott wrote:
>>> On 10/13/2020 5:36 PM, Mike Terry wrote:
>>>> On 13/10/2020 21:01, olcott wrote:
>>>>> On 10/12/2020 9:56 AM, André G. Isaak wrote:
>>>>>> On 2020-10-12 08:41, olcott wrote:

[snip]

>>>>>>>
>>>>>>> It is certainly the case that self-contradictory expression of
>>>>>>> language exist and these non-truth bearers prove that a formal
>>>>>>> system
>>>>>>> is "incomplete" entirely on that basis that they are not truth
>>>>>>> bearers.
>>>>>>
>>>>>> Self-contradictory sentences exist in NATURAL language. They don't
>>>>>> exist in the standard languages of logic including the one used in
>>>>>> Gödel's proof, and play no role in proving incompleteness.
>>>>>>
>>>>
>>>> Note that André is talking about /self-contradictory/ sentences (which
>>>> indeed don't exist in FOL)...
>>>>
>>>>>
>>>>> Notice that Tarski explicitly refers to:
>>>>>
>>>>> two mutually contradictory sentences (i.e. such
>>>>> that one is the negation of the other) neither of
>>>>> which is provable
>>>>
>>>> ok, so Tarski isn't talking about /self/ contradictory sentences?
>>>
>>> He is merely phrasing a self-contradictory sentence differently.
>>>
>>
>> No he isn't. OK, so what do you think is the self-contradictory
>> sentence that he is phrasing differently?
>>
>> Mike.
>>
>
> He is using arbitrary self-contradictory sentences to show that true and
> diverge from provable.

What do you mean exactly by "self-contradictory sentences"? It looks
like you just mean "a pair of sentences which together imply a
contradiction", such as {ExAy x=y, ¬ExAy x=y}?

That's a possible interpretation for the phrase, but it's totally banal.
Obviously if this is your interpretation, then FOL contains self
contradictory statements (duh!), but:

1) That wasn't what André was talking about. He should speak
for himself of course, but I guess he intended the phrase to
mean a sentence which if true would imply it is false, and
vice versa. (Like LP in english language.)

2) That wasn't what YOU were talking about above, since you
talked about them being non-truth bearers. But both
ExAy x=y and ¬ExAy x=y are truth bearers, assuming we have
fixed an interpretation, such as "the natural numbers" [in
which case the first is FALSE and the second TRUE]

If in fact you did mean LP-like statements [which if true it would imply
they are false and vice versa], then none of those appeared in your
quoted Tarski text which you've clipped, and it's still the case that
your description of what was being said in that text was rubbish, and
not relevent to what you were replying to.

Mike.

[olcott]

You are simply ignoring what I said and then asking me what I said?

> That's a possible interpretation for the phrase, but it's totally banal.
>  Obviously if this is your interpretation, then FOL contains self
> contradictory statements (duh!), but:
>
> 1)  That wasn't what André was talking about.  He should speak
>     for himself of course, but I guess he intended the phrase to
>     mean a sentence which if true would imply it is false, and
>     vice versa.  (Like LP in english language.)
>
> 2)  That wasn't what YOU were talking about above, since you
>     talked about them being non-truth bearers.  But both
>     ExAy x=y and ¬ExAy x=y are truth bearers, assuming we have
>     fixed an interpretation, such as "the natural numbers" [in
>     which case the first is FALSE and the second TRUE]
>

Some of the brightest people in the world can't seem to understand that
when an expression of language (because of its structure) cannot
possibly be resolved to true or false that this proves that is it not a
truth bearer.

> If in fact you did mean LP-like statements [which if true it would imply
> they are false and vice versa], then none of those appeared in your
> quoted Tarski text which you've clipped, and it's still the case that
> your description of what was being said in that text was rubbish, and
> not relevent to what you were replying to.
>
> Mike.
>

I meant exactly what I quoted:
A simple example of two mutually contradictory sentences

(i.e. such that one is the negation of the other) neither
of which is provable

http://www.liarparadox.org/tarski_186.pdf

The Liar Paradox fits this bill.