Re: This is how I overturn the Tarski Undefinability theorem

On 9/7/2024 8:19 AM, Richard Damon wrote:

On 9/7/24 9:06 AM, olcott wrote:

On 9/7/2024 3:35 AM, Mikko wrote:

On 2024-09-06 12:22:04 +0000, olcott said:
>

On 9/6/2024 6:55 AM, Mikko wrote:

On 2024-09-03 12:44:00 +0000, olcott said:
>

On 9/3/2024 5:38 AM, Mikko wrote:

On 2024-09-02 13:01:23 +0000, olcott said:
>

On 9/2/2024 2:54 AM, Mikko wrote:

On 2024-09-01 13:47:00 +0000, olcott said:
>

On 9/1/2024 7:52 AM, Mikko wrote:

On 2024-08-31 18:48:18 +0000, olcott said:
>

*This is how I overturn the Tarski Undefinability theorem*
An analytic expression of language is any expression of formal or natural language that can be proven true or false entirely on the basis of a connection to its semantic meaning in this same language.
>
This connection must be through a sequence of truth preserving operations from expression x of language L to meaning M in L. A lack of such connection from x or ~x in L is construed as x is not a truth bearer in L.
>
Tarski's Liar Paradox from page 248
    It would then be possible to reconstruct the antinomy of the liar
    in the metalanguage, by forming in the language itself a sentence
    x such that the sentence of the metalanguage which is correlated
    with x asserts that x is not a true sentence.
    https://liarparadox.org/Tarski_247_248.pdf
>
Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
>
*Formalized as Prolog*
?- LP = not(true(LP)).
LP = not(true(LP)).

>
According to Prolog semantics "false" would also be a correct
response.
>

?- unify_with_occurs_check(LP, not(true(LP))).
false.

>
To the extend Prolog formalizes anything, that only formalizes
the condept of self-reference. I does not say anything about
int.
>

When formalized as Prolog unify_with_occurs_check()
detects a cycle in the directed graph of the evaluation
sequence proving the LP is not a truth bearer.

>
Prolog does not say anything about truth-bearers.
>

>
It may seem that way if you have no idea what
(a) a directed is
(b) what cycles in a directed graph are
(c) What an evaluation sequence is

>
More relevanto would be what a "truth-maker" is.
Anyway, it seems that Prolog does not say anything about
truth-bearers because Prolog does not say anything about
truth-bearers.
>

>
When Prolog derives expression x from Facts and Rules
by applying the truth preserving operations of Rules to
Facts is the truthmaker for truth-bearer x.

>
A Prolog impementation applies Prolog operations.

>
Which are (like logic) for the most part truth preserving.
If (A & B) then A

>
Logic where the infoerence rules are for the most part truth prserving
is not useful. They all must be.
>

For some cases
Prolog offers several operations letting the implementation to
choose which one to apply.

>
I don't thing so. Once the Facts and Rules are specified
Prolog chooses whatever Facts and Rules to prove x or not.
It is back-chained inference.

>
Standard Prolog is what the Prolog standard says. Conforming implementations
may vary if the standard allows. If you think otherwise you are wrong.
There are also non-starndard Prlongs that vary even more.
>

>
The fundamental architectural overview of all Prolog implementations
is the same True(x) means X is derived by applying Rules (AKA truth preserving operations) to Facts.

>
The details are permitted to differ.
>

>
Instead of using any single order of logic we simultaneously
represent an arbitrary number of orders of logic in a type
hierarchy knowledge ontology.
>

 Doesn't work, and just shows that you don't understand what you are talking about.

This <is> already implemented in conventional type theory.
Objects of thought at differing orders of logic are different types.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer