XPost: comp.theory, sci.math, sci.lang   
   XPost: comp.lang.prolog   
   From: polcott333@gmail.com   
      
   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.   
      
      
   --   
   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)