XPost: comp.theory, sci.logic, sci.math   
   From: polcott333@gmail.com   
      
   On 1/20/2026 5:08 PM, Tristan Wibberley wrote:   
   > On 18/01/2026 23:41, olcott wrote:   
   >   
   >> I already just said that the proof and refutation of   
   >> Goldbach are outside the scope of PA axioms.   
   >   
   > So Richard is right that you need a truth value for not being covered:   
   >   
   > True(S, Goldbach) = OutOfScope   
   >   
   > or a type theory to give True(S, Goldbach) no content when Goldbach is   
   > out of scope, or keep it explicit with an InScope(S, P) family of   
   > propositions. Of course, the type theory approach is often easier to use   
   > with pencil and paper.   
   >   
      
   ∀x ∈ PA ((True(PA, x)  ≡ (PA ⊢ x))   
   ∀x ∈ PA ((False(PA, x) ≡ (PA ⊢ ~x))   
      
   In PA itself this requires pathological self-reference to   
   be computed in meta-math by detecting a cycle in the   
   directed graph of the evaluation sequence of the expression.   
   This seems to block all of the undecidability that would   
   otherwise be construed as incompleteness.   
      
   ∀x ∈ PA (~WellFounded(PA, x) ≡ (~True(PA, x) ∧ (~False(PA, x))   
      
   It is also best that an outer knowledge level resolve   
   Goldbach as outside of the domain of knowledge. If not   
   then PA might try brute force ans get stuck in a loop.   
   So within the domain of knowledge Goldbach is ~WellFounded.   
      
   > Is there a conventional alternative to implication for an explicit   
   > alternative of type theory?   
   >   
   > Unsatisfying: WhenInScope(S, P) -> (True(S, P) & Foo(P))   
   > More satisfying: WhenInScope(S,P,Q in (True(S,Q) & Foo(Q)))   
   >   
   > Hey, I see that in prolog often. Q is an indeterminate (unbound variable   
   > in prolog) bound by WhenInScope(S,P,Q in ...) within "...".   
   >   
   > or a lambda expression alternative:   
   >   
   > WhenInScope(S,P,λQ.True(S,Q) & Foo(Q))   
   >   
   > I prefer that over an implicit, semi-ad-hoc type theory.   
   >   
   > Are there conventional names for these ideas and an author and excellent   
   > exposition textbook?   
   >   
      
   Well-founded proof theoretic semantics.   
      
      
   --   
   Copyright 2026 Olcott

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

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