Discussion:
Final MTT syntax for Provability
(too old to reply)
Pete Olcott
2017-06-17 16:48:54 UTC
Permalink
Raw Message
"@" means the LHS is assigned as an alias for the RHS.

Thus the LHS nickname is to be considered one-and-the-same-thing as the expression on the RHS, as if macro substitution was to take place.

The primary purpose of this syntax is to provide the means for an expression to directly refer to itself. This is not at all the same convention that Tarski provided where a quoted expression is considered to be the name of the expression so that an expression can refer to its name.

With Tarski's convention the true nature of pathological self-reference cannot be expressed, it slips through the cracks of expressibility without ever being seen.

Provable(L, X) @ L ∈ Formal_Systems, ∃Γ ⊂ L (Γ ⊢ X)
~Provable(L, X) @ L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ X)
~Provable(L, X) @ L ∈ Formal_Systems, ∀Γ ⊂ L ~(Γ ⊢ X)
Refutable(L, X) @ L ∈ Formal_Systems, ∃Γ ⊂ L (Γ ⊢ ~X)

We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion, Formal_Systems is a predefined constant that is defined to have at least one element.

// Neither provable nor refutable in any formal system:
G @ ∀L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ G)

Copyright 2017 Pete Olcott
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Peter Percival
2017-06-17 16:55:15 UTC
Permalink
Raw Message
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as the
expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is considered
to be the name of the expression so that an expression can refer to its
name.
With Tarski's convention the true nature of pathological self-reference
cannot be expressed, it slips through the cracks of expressibility
without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at least
one element.
So how is "L ∈ Formal_Systems, ∃Γ ⊂ L (Γ ⊢ X)" to be read?
"L ∈ Formal_Systems and ∃Γ ⊂ L (Γ ⊢ X)"? I ask because I'm not
familiar with , in this context.

Also the three formulae with occurrences of ~ in them are meaningless by
your own admission.
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
DKleinecke
2017-06-17 18:07:15 UTC
Permalink
Raw Message
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an expression to directly refer to itself. This is not at all the same convention that Tarski provided where a quoted expression is considered to be the name of the expression so that an expression can refer to its name.
With Tarski's convention the true nature of pathological self-reference cannot be expressed, it slips through the cracks of expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion, Formal_Systems is a predefined constant that is defined to have at least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is

Provable(L, X) @ L ∈ Formal_Systems, L ⊢ X
~Provable(L, X) @ L ∈ Formal_Systems, ~ (L ⊢ X)
Refutable(L, X) @ L ∈ Formal_Systems, L ⊢ ~X

Not, I fear, very enlightening.
Pete Olcott
2017-06-17 18:41:35 UTC
Permalink
Raw Message
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an expression to directly refer to itself. This is not at all the same convention that Tarski provided where a quoted expression is considered to be the name of the expression so that an expression can refer to its name.
With Tarski's convention the true nature of pathological self-reference cannot be expressed, it slips through the cracks of expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion, Formal_Systems is a predefined constant that is defined to have at least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
--- G @ ∀L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ G)

The above expression named G is enormously simpler than the 1931 Incompleteness Theorem:
https://plato.stanford.edu/entries/goedel-incompleteness/

"The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F."

The above expression named G is neither provable nor refutable in any formal system what-so-ever.

If we stopped our analysis right there we would have an enormous simplification of the 1931 GIT that is much broader in scope than the 1931 GIT in that it simultaneously applies to every possible formal system of logic.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Peter Percival
2017-06-17 19:12:33 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?

Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
DKleinecke
2017-06-17 19:28:58 UTC
Permalink
Raw Message
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
Pete Olcott
2017-06-17 20:01:45 UTC
Permalink
Raw Message
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
DKleinecke
2017-06-17 22:39:15 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics". Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
Pete Olcott
2017-06-18 02:42:52 UTC
Permalink
Raw Message
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.

I will simply create a computer system that can totally understand what I am saying and then people can examine its source code. I just completed the YACC BNF specification for Minimal Type Theory today.

Here is the whole 75 page long 1931 Incompleteness Theorem simplified to a single line of Minimal Type Theory: G @ ∀L ∈ Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ G)

My version has a much broader scope because the 1931 Theorem only applied to Principia Mathematica.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
DKleinecke
2017-06-18 03:16:50 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code.
Please do just that.

What language do you propose to code this computer system in?
Pete Olcott
2017-06-18 03:54:26 UTC
Permalink
Raw Message
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code.
Please do just that.
What language do you propose to code this computer system in?
It is currently in C++, I am looking for a way to port it to C# so that my $8.00 per month website can directly run the code. I just updated to the most recent version of Bison and Flex.

I was looking into Coco/R and ALTLR
Coco/R takes 70 KB versus 108 MB for the same parser. 1600-fold less memory.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
DKleinecke
2017-06-18 06:32:46 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code.
Please do just that.
What language do you propose to code this computer system in?
It is currently in C++, I am looking for a way to port it to C# so that my $8.00 per month website can directly run the code. I just updated to the most recent version of Bison and Flex.
I was looking into Coco/R and ALTLR
Coco/R takes 70 KB versus 108 MB for the same parser. 1600-fold less memory.
Thank You. I will be waiting.
Peter Percival
2017-06-18 12:21:27 UTC
Permalink
Raw Message
Post by Pete Olcott
Here is the whole 75 page long 1931 Incompleteness Theorem simplified
⊂ L (Γ ⊢ G)
GIT doesn't apply to "formal systems" without qualification (plenty are
complete).
Post by Pete Olcott
My version has a much broader scope because the 1931 Theorem only
applied to Principia Mathematica.
No it doesn't.
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Peter Percival
2017-06-18 14:52:38 UTC
Permalink
Raw Message
Post by Peter Percival
Post by Pete Olcott
Here is the whole 75 page long 1931 Incompleteness Theorem
Formal_Systems, ~∃Γ ⊂ L (Γ ⊢ G)
GIT doesn't apply to "formal systems" without qualification (plenty
are complete).
Post by Pete Olcott
My version has a much broader scope because the 1931 Theorem only
applied to Principia Mathematica.
No it doesn't.
I know that such niceties as proving what one claims are of no interest
to you, but nevertheless I refer you to Gödel's theorem VI. After all
the many posts of yours about (supposedly) Gödel's incompleteness
theorem you still don't know what it says.
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Pete Olcott
2017-06-18 13:54:50 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code. I just completed the YACC BNF specification for Minimal Type Theory today.
My version has a much broader scope because the 1931 Theorem only applied to Principia Mathematica.
It is impossible to encode the above semantic meaning in any formal system and either prove or refute the above expression within that formal system.

Many formal systems will not be able to prove or refute the above expression simply because they are not sufficiently expressive to encode its semantic meaning.

Therefore the above expression is neither provable nor refutable within any formal system of the set of all formal system of logic.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Arnaud Fournet
2017-06-18 14:19:20 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code. I just completed the YACC BNF specification for Minimal Type Theory today.
My version has a much broader scope because the 1931 Theorem only applied to Principia Mathematica.
It is impossible to encode the above semantic meaning in any formal system and either prove or refute the above expression within that formal system.
Many formal systems will not be able to prove or refute the above expression simply because they are not sufficiently expressive to encode its semantic meaning.
Therefore the above expression is neither provable nor refutable within any formal system of the set of all formal system of logic.
Nice,
so maybe it's time to fuck off and keep your garbage theories for yourselves somewhere else.
A.
Pete Olcott
2017-06-18 15:38:13 UTC
Permalink
Raw Message
Post by Arnaud Fournet
Post by Pete Olcott
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code. I just completed the YACC BNF specification for Minimal Type Theory today.
My version has a much broader scope because the 1931 Theorem only applied to Principia Mathematica.
It is impossible to encode the above semantic meaning in any formal system and either prove or refute the above expression within that formal system.
Many formal systems will not be able to prove or refute the above expression simply because they are not sufficiently expressive to encode its semantic meaning.
Therefore the above expression is neither provable nor refutable within any formal system of the set of all formal system of logic.
Nice,
so maybe it's time to fuck off and keep your garbage theories for yourselves somewhere else.
A.
https://www.brainyquote.com/quotes/quotes/a/alberteins129798.html
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Peter Percival
2017-06-18 14:41:42 UTC
Permalink
Raw Message
Post by Pete Olcott
Many formal systems will not be able to prove or refute the above
expression simply because they are not sufficiently expressive to
encode its semantic meaning.
If "the above expression simply" means "G @ ∀L ∈ Formal_Systems, ~∃Γ ⊂ L
(Γ ⊢ G)", then so what? It is an expression of your devising and
therefore of interest only to you.
Post by Pete Olcott
Therefore the above expression is neither provable nor refutable
within any formal system of the set of all formal system of logic.
--
Do, as a concession to my poor wits, Lord Darlington, just explain
to me what you really mean.
I think I had better not, Duchess. Nowadays to be intelligible is
to be found out. -- Oscar Wilde, Lady Windermere's Fan
Pete Olcott
2017-06-18 15:37:05 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code. I just completed the YACC BNF specification for Minimal Type Theory today.
My version has a much broader scope because the 1931 Theorem only applied to Principia Mathematica.
MTT is the universal meta-language that can encode the semantic meaning of every object language (including itself).

https://plato.stanford.edu/entries/tarski-truth/#ObjLanMet

That MTT is a universal meta-language that can even encode its own semantic meaning extends Tarki's ideas significantly. No need for Tarski's infinite hierarchy of languages, the semantic formalization "buck" stops at MTT.

This advance is only made possible because MTT encodes the meanings of its target objects using the smallest possible unit of meaning. Not a Jerry Fodor semantic atom:
https://plato.stanford.edu/entries/language-thought/

MTT uses semantic subatomic compositionality subatomic particles:
{Things} and {Relations} between {Things}.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Pete Olcott
2017-06-18 16:42:35 UTC
Permalink
Raw Message
Post by Pete Olcott
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Post by DKleinecke
Post by Peter Percival
Post by Pete Olcott
Post by DKleinecke
Post by Pete Olcott
Thus the LHS nickname is to be considered one-and-the-same-thing as
the expression on the RHS, as if macro substitution was to take place.
The primary purpose of this syntax is to provide the means for an
expression to directly refer to itself. This is not at all the same
convention that Tarski provided where a quoted expression is
considered to be the name of the expression so that an expression can
refer to its name.
With Tarski's convention the true nature of pathological
self-reference cannot be expressed, it slips through the cracks of
expressibility without ever being seen.
We use: L ∈ Formal_Systems
instead of: ∃L ∈ Formal_Systems
because L ∈ Formal_Systems is an axiom and not an assertion,
Formal_Systems is a predefined constant that is defined to have at
least one element.
Why do you introduce Γ? Isn't it true that if Γ ⊢ X then, for
any G such that Γ ⊂ G, G ⊢ X? It appears all you need is
Not, I fear, very enlightening.
The above expression named G is enormously simpler than the 1931
So is, let's say, 2+3=5. "So what?" people will ask "since 2+3=5 has
nothing to do with GIT." And your G is just the same. If you ever want
to know what GIT says, how it's proved, and what the
neither-provable-nor-refutable statement really is, read Mendelson.
Post by Pete Olcott
https://plato.stanford.edu/entries/goedel-incompleteness/
"The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F."
The above expression named G is neither provable nor refutable in any
formal system what-so-ever.
If we stopped our analysis right there we would have an enormous
simplification of the 1931 GIT that is much broader in scope than the
1931 GIT in that it simultaneously applies to every possible formal
system of logic.
What are you saying, that you have an incompleteness theorem that is
applicable to every possible formal system of logic? Even those which
are complete?
Can you ask yourself whether the readers of sci.lang want to read your
posts? If you think the answer may be "no", perhaps you'd like to stop
posting there?
This part of his stuff does not apply to sci.lang but he keeps
asserting his theory reflects, or is based on, natural language.
The formalization of the entire set of all semantic meaning equally applies to formal languages and natural languages, thus it is both the formal semantics of linguistics as well as the semantics of logical inference.
But so far you haven't presented even a plausible formal
"semantics".
The whole idea of credibility and thus plausibility is complete crap.
Credibility is a cheap hooker stand-in for measuring actual validity.
Post by DKleinecke
Even if you do it does not follow that you
have said anything meaningful about the semantics of
human speech. If anything is clear about this issue it is
that the human mind does not work like a computer.
It would take up more than the rest of my life to sufficiently explain how this applies to natural language to anyone that does not already have Doug Lenat's level of understanding of these things.
I will simply create a computer system that can totally understand what I am saying and then people can examine its source code. I just completed the YACC BNF specification for Minimal Type Theory today.
My version has a much broader scope because the 1931 Theorem only applied to Principia Mathematica.
MTT is the universal meta-language that can encode the semantic meaning of every object language (including itself).
https://plato.stanford.edu/entries/tarski-truth/#ObjLanMet
That MTT is a universal meta-language that can even encode its own semantic meaning extends Tarki's ideas significantly. No need for Tarski's infinite hierarchy of languages, the semantic formalization "buck" stops at MTT.
https://plato.stanford.edu/entries/language-thought/
{Things} and {Relations} between {Things}.
To describe the above more completely I will have to formulate an axiomatic set theory that is entirely logically coherent. In the mean time one can think of {Things} as the proper class that has everything besides itself as a member and {Relations} as a proper subset of {Things}.

{Things} will contain some elements that are logically incoherent. These will exist within the category of {Misconceptions}.
--
(Γ ⊨ _FS A) ≡ (Γ ⊢ _FS A)
Loading...