Final MTT syntax for Provability

[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.

[Peter Percival]

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?

[Pete Olcott]

Post by Peter Percival

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.