XPost: comp.theory, sci.math, sci.lang   
   XPost: comp.lang.prolog   
   From: polcott333@gmail.com   
      
   On 2/5/2026 10:55 AM, olcott wrote:   
   > Changing the foundational basis to Proof Theoretic Semantics   
   > Tarski Undefinability is overcome   
   >   
   > x ∈ Provable ⇔ x ∈ True // proof theoretic semantics   
   >   
   > Changing the foundation to proof theoretic semantics where   
   > truth is well-founded provability blocks Tarski’s diagonal   
   > step most clearly seen on line (3)   
   >   
   > Here is the Tarski Undefinability Theorem proof   
   > (1) x ∉ Provable if and only if p   
   > (2) x ∈ True if and only if p   
   > (3) x ∉ Provable if and only if x ∈ True. // (1) and (2) combined   
   > (4) either x ∉ True or x̄ ∉ True;     // axiom: ~True(x) ∨   
   ~True(~x)   
   > (5) if x ∈ Provable, then x ∈ True;  // axiom: Provable(x) → True(x)   
   > (6) if x̄ ∈ Provable, then x̄ ∈ True;  // axiom: Provable(~x) →   
   True(~x)   
   > (7) x ∈ True   
   > (8) x ∉ Provable   
   > (9) x̄ ∉ Provable   
   >   
   > https://liarparadox.org/Tarski_275_276.pdf   
   >   
   > A proof theoretic prover rejects expressions that   
   > do not have "a well-founded justification tree within   
   > Proof theoretic semantics".   
   >   
   > The same way that Prolog does   
   >   
   > % This sentence is not true.   
   > ?- LP = not(true(LP)).   
   > LP = not(true(LP)).   
   > ?- unify_with_occurs_check(LP, not(true(LP))).   
   > false.   
   >   
   >   
      
   With actual competent human review   
   x ∈ Provable ⇔ x ∈ True // proof theoretic semantics   
   is changed to   
      
   x ∈ Provable ⇒ x ∈ True // proof theoretic semantics   
   This is Tarski's line (5)   
      
   This overrules anything that contradicts it because   
   it has now attained axiom status.   
      
   Below I show how this overrules Tarski line (3)   
   thus overcoming Tarski Undefinability when we   
   change its foundation from truth conditional semantics   
   to proof theoretic semantics. PTS was not available   
   at the time That he wrote   
   "The Concept of Truth in Formalized Languages"   
      
   (3) x ∉ Provable if and only if x ∈ True.   
   can be divided into   
   (3)(a) if x ∉ Provable, then x ∈ True   
   (3)(b) if x ∈ True, then x ∉ Provable   
   (5) if x ∈ Provable, then x ∈ True   
   (5) combined with (3)(b) becomes   
   if x ∈ Provable  then  x ∉ Provable   
      
      
   --   
   Copyright 2026 Olcott

   
      
   My 28 year goal has been to make 
   
   "true on the basis of meaning expressed in language"
   
   reliably computable for the entire body of knowledge.

   
      
   This required establishing a new foundation
   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)