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
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é
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.
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.
André
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
On 2020-09-28 18:00, olcott wrote:
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.
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
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!!!!
On 9/29/2020 12:29 AM, Jeff Barnett wrote:
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!!!!
"Great spirits have always encountered violent opposition from mediocre minds. Albert Einstein.
On 9/28/2020 8:04 PM, André G. Isaak wrote:
On 2020-09-28 18:00, olcott wrote:
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.
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 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
On 2020-09-28 21:00, olcott wrote:
On 9/28/2020 8:04 PM, André G. Isaak wrote:
On 2020-09-28 18:00, olcott wrote:
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.
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 said that B had the value of True, therefore ¬B is false.
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?
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
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é
On 9/29/2020 12:02 AM, olcott wrote:
On 9/29/2020 12:29 AM, Jeff Barnett wrote:
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!!!!
"Great spirits have always encountered violent opposition from
mediocre minds. Albert Einstein.
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.
On 2020-09-28 18:00, olcott wrote:
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.
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.
On 9/29/2020 2:01 AM, Jeff Barnett wrote:
On 9/29/2020 12:02 AM, olcott wrote:
On 9/29/2020 12:29 AM, Jeff Barnett wrote:
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!!!!
"Great spirits have always encountered violent opposition from
mediocre minds. Albert Einstein.
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.
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.
On 9/29/2020 2:48 AM, André G. Isaak wrote:
On 2020-09-28 21:00, olcott wrote:
On 9/28/2020 8:04 PM, André G. Isaak wrote:
On 2020-09-28 18:00, olcott wrote:
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.
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 said that B had the value of True, therefore ¬B is false.
But I didn't ask about the value of ¬B (or B or A or ¬A). I asked
about the value of ¬(A := B)
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.
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.
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.
#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.
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
On 9/29/2020 9:20 AM, olcott wrote:
On 9/29/2020 2:01 AM, Jeff Barnett wrote:
On 9/29/2020 12:02 AM, olcott wrote:
On 9/29/2020 12:29 AM, Jeff Barnett wrote:
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!!!!
"Great spirits have always encountered violent opposition from
mediocre minds. Albert Einstein.
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.
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.
"Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein.
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.
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é
On 2020-09-29 09:49, olcott wrote:
On 9/29/2020 2:48 AM, André G. Isaak wrote:
On 2020-09-28 21:00, olcott wrote:
On 9/28/2020 8:04 PM, André G. Isaak wrote:
On 2020-09-28 18:00, olcott wrote:
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.
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 said that B had the value of True, therefore ¬B is false.
But I didn't ask about the value of ¬B (or B or A or ¬A). I asked
about the value of ¬(A := B)
A := B is only macro substitution nothing more
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é
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.
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.
André
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.pdfYet symbolic logic
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é
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."
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.
André
olcott <NoOne@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?
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.
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.
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.
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.
Yet symbolic has no way to precisely specify actual self-reference so
'This sentence is false' is an assertion, not a definition. As such, it >>>
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.
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é
On 9/29/2020 5:26 PM, Ben Bacarisse wrote:
olcott <NoOne@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)
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:
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.
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.
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,
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é
On 2020-09-29 18:40, olcott wrote:
On 9/29/2020 5:26 PM, Ben Bacarisse wrote:
olcott <NoOne@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.
André
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.
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.
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).
André G. Isaak <agisaak@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?
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.
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.
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.
André
On 2020-09-29 22:29, Keith Thompson wrote:
André G. Isaak <agisaak@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.
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.
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 <NoOne@NoWhere.com> writes:
On 9/29/2020 8:12 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:
On 9/29/2020 5:26 PM, Ben Bacarisse wrote:
olcott <NoOne@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.
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é
olcott <NoOne@NoWhere.com> writes:
On 9/30/2020 6:43 AM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:
On 9/29/2020 8:12 PM, Ben Bacarisse wrote:
olcott <NoOne@NoWhere.com> writes:
On 9/29/2020 5:26 PM, Ben Bacarisse wrote:
olcott <NoOne@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.
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.
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.
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.
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é
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.
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.
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.
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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é
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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".
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
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.
André
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems regardless
of your attempts to redefine terms.
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.
On 2020-10-12 00:24, olcott wrote:
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems regardless
of your attempts to redefine terms.
If my definition is correct and his is incorrect then his whole proof
has been refuted.
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.
André
On 10/12/2020 4:18 AM, André G. Isaak wrote:
On 2020-10-12 00:24, olcott wrote:
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems
regardless of your attempts to redefine terms.
If my definition is correct and his is incorrect then his whole proof
has been refuted.
His definition is correct.
It doesn't even make sense to call an accepted definition 'incorrect'.
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 ⊬ ¬φ).
On 2020-10-12 08:41, olcott wrote:
On 10/12/2020 4:18 AM, André G. Isaak wrote:
On 2020-10-12 00:24, olcott wrote:
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems
regardless of your attempts to redefine terms.
If my definition is correct and his is incorrect then his whole
proof has been refuted.
His definition is correct.
It doesn't even make sense to call an accepted definition 'incorrect'.
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.
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.
André
On 10/12/2020 9:56 AM, André G. Isaak wrote:
On 2020-10-12 08:41, olcott wrote:
On 10/12/2020 4:18 AM, André G. Isaak wrote:
On 2020-10-12 00:24, olcott wrote:
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems
regardless of your attempts to redefine terms.
If my definition is correct and his is incorrect then his whole
proof has been refuted.
His definition is correct.
It doesn't even make sense to call an accepted definition 'incorrect'.
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.
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.
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:
On 10/12/2020 4:18 AM, André G. Isaak wrote:Self-contradictory sentences exist in NATURAL language. They don't
On 2020-10-12 00:24, olcott wrote:It is certainly the case that self-contradictory expression of
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems
regardless of your attempts to redefine terms.
If my definition is correct and his is incorrect then his whole
proof has been refuted.
His definition is correct.
It doesn't even make sense to call an accepted definition 'incorrect'. >>>>
language exist and these non-truth bearers prove that a formal system
is "incomplete" entirely on that basis that they are not truth bearers. >>>
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?
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:
On 10/12/2020 4:18 AM, André G. Isaak wrote:
On 2020-10-12 00:24, olcott wrote:
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems
regardless of your attempts to redefine terms.
If my definition is correct and his is incorrect then his whole
proof has been refuted.
His definition is correct.
It doesn't even make sense to call an accepted definition
'incorrect'.
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.
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:
On 10/12/2020 4:18 AM, André G. Isaak wrote:
On 2020-10-12 00:24, olcott wrote:
On 10/12/2020 12:14 AM, André G. Isaak wrote:
On 2020-10-11 23:07, olcott wrote:
On 10/11/2020 11:45 PM, André G. Isaak wrote:
On 2020-10-11 22:07, olcott wrote:
On 10/11/2020 10:56 PM, André G. Isaak wrote:
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é
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".
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.
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.
No. Gödel's Incompleteness Theorems remain proven theorems
regardless of your attempts to redefine terms.
If my definition is correct and his is incorrect then his whole >>>>>>>> proof has been refuted.
His definition is correct.
It doesn't even make sense to call an accepted definition
'incorrect'.
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.
On 14/10/2020 01:42, olcott wrote:
On 10/13/2020 7:37 PM, Mike Terry wrote:[snip]
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:
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 >>>>>>> Gdel'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.
On 10/13/2020 7:37 PM, Mike Terry wrote:[snip]
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:
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 >>>>>> Gdel'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.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 293 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 221:00:24 |
| Calls: | 6,623 |
| Calls today: | 5 |
| Files: | 12,171 |
| Messages: | 5,318,040 |