Re: The key undecidable instance that I know about

On 3/14/25 11:54 PM, olcott wrote:

On 3/14/2025 8:57 PM, Richard Damon wrote:

On 3/14/25 3:01 PM, olcott wrote:

On 3/14/2025 1:42 PM, Richard Damon wrote:

On 3/14/25 10:27 AM, olcott wrote:

On 3/13/2025 6:08 AM, Mikko wrote:

On 2025-03-11 23:26:28 +0000, olcott said:
>

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:
>

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

>
Have you pbulished that "Minimal Type Theory" or put it to a web page?
Without a pointer to it there is no point to mention it. Of course one
can create a language that can express a self reference but why would
one?

>
https://www.researchgate.net/ publication/315367846_Minimal_Type_Theory_MTT

>
Does not define any theory.
>

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

>
The article 315367846_Minimal_Type_Theory_MTT says that "Types must be
expressly stated in Minimal Type Theory" but the syntax allows untyped
quantification.
>

https://www.researchgate.net/ publication/317953772_Provability_with_Minimal_Type_Theory

>
This article uses @ as definition article but a comment in the syntax
says that := is used.
>
None of the articles defines what is a valid proof in Minimal Type Theory.
>

We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.
>
Until we do this we get confused into believing
that such expressions are in any way undecidable.
>

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

>
A self reference cannot be expressed in an uninterpreted formal language.
Sometimes some symbols and expressions are interpreted to represent
themselves or other symbols or expressions. For example, the symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

>
LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

>
Without decoding no semantics can be extracted from the syntax.
>

>
LP := ~True(LP) obtains its entire semantics from the expression.

>
But none of your arguments have talked about an expression that derives itself from that expression
>

>
Because of the cycle in the directed graph of its evaluation
sequence LP cannot derive its semantic meaning from anything
else: ~True(~True(~True(~True(~True(~True(...))))))

>
But the p that can be developed as a statement in the languaged, based on the idea in the metalanguge that must be true if and only if it is false, doesn't.
>

>
Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)

>
Right, like Godel's expression G specifically derives its semantics from the natured of the system F and the mathematics the system F creates. And, in the meta we can construct a mathematical statement in F, whose truth is the direct opposite of its provability, and thus must be True and Unprovable, as it can't be False but Provably True.
>
This language seems to be beyond what you can understand, so you just make up lies to cover your ignorance.
>

>
of the set of general knowledge of the world encoded as
Rudolf Carnap meaning postulates using something like Montague
Grammar. Each unique sense meaning has its own GUID.
>

>
WHich is irrelevent here, as Formal systems don't have that problem.
>
Your problem

>
In my type theory based system there is no need for
any separate language and meta-language.
>
Rudolf Carnap meaning postulates are arranged in an
inheritance hierarchy where each unique sense meaning
is assigned its own GUID.
>
The language is something like Montague Grammar.
LP := ~True(LP) is rejected as semantically incorrect.
>

>
but the existing systens aren't built on your "Type Theory" so you need to show that it works in THOSE systems to use it,
>

 Discard all inferior systems.

NOT A VALID OPERATION.
Sorry, but you are just proving you don't understand what you are talkig about.
"Inferior" can't be precisely defined in this context.

 

I guess you are just admitting that you don't understand what you are talking about, and your "logic" assumes you can just make up crap and call it true,
>

 We axiomatize all the basic facts of the world (facts
that cannot be derived on the basis of other facts).
Then we plug everything else into an inheritance hierarchy
knowledge ontology.

But what about contradictory "facts"? Things that define differents systems of current logic, thinks like two parrallel lines will never meet (Plane Gemoetry) vs Two non-conincident lines will allways have two points of intersection (Spherical Geometry).

 Anything that cannot be derived by applying Truth preserving
operations to these basic facts is either untrue or unknown.

And what about things we can't know if we can know?

 This gives us a True() predicate that always works except
for unknowns. It certainty does not get totally confused
by self-contradictory expressions. These simply cannot be
derived by applying truth preserving operations to basic facts.

No, it doesn't give one, as it has been shown by Godel and Tarski and many others, that if you system of logic has enough axioms to create a system which has the full power of Natural Numbers, which by your description, yours will, it is possible to derive via the use of a meta-system, (which is created by a set of valid assumption of possiblities, a major part of which is assigning a number to every one of the finite number of axioms and basic symbols of the system) we can construct a statement whose truth value is the opposite of its provability, and thus must be true but unprovable in the basic system.
You can not bring all these axiom numbering axioms into the original system, as then you end you with an infinite number of axioms, as for every axiom you number, you created a new axiom to assign that value.
Under this condition, there are statements that the Truth Predicate can not answer, as they are truth predicate contradictory.
The only way out is to make the system not able to handle all the properties of the Natural Numbers, which thus makes it clearly inferior to the existing system.
Sorry, you are just showing yourself to not really understand what you are talking about, and that you are too stupid to realize this.

 

Sorry, you are just proving you don't understand how logic work, and nobody should take anything you say seriously.