XPost: comp.theory, sci.math, comp.ai.philosophy   
   From: polcott333@gmail.com   
      
   On 1/22/2026 6:23 PM, Richard Damon wrote:   
   > On 1/20/26 6:33 PM, olcott wrote:   
   >> 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.   
   >   
   > Which just shows that you are a liar, as the relaitionship in PA doesn't   
   > refer to itself.   
   >   
   > You think you are allowed to equivocate on your use of looking into the   
   > meta-system.   
   >   
   >>   
   >> ∀x ∈ PA (~WellFounded(PA, x) ≡ (~True(PA, x) ∧ (~False(PA, x))   
   >   
   > For which there is no Proof-Theoretic resolution of, and thus no   
   > handling in Proof-Theoretic semantics.   
   >   
   >>   
   >> 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.   
   >   
   > But that isn't true, there is no knowledge of that fact, ax we don't   
   > know if it can be proven or refuted.   
   >   
   > In fact, it CAN'T be proved to be not-well-founded in PA, as proving   
   > that we can't disprove it ends up proving it.   
   >   
   > The problem is that some statements are inherently logically truth-   
   > beares, as there can be no middle to try to exclude, but they also might   
   > not be provable.   
   >   
   > Your Proof-Theoretic Semantics concept can't handle systems where that   
   > is a fact.   
   >   
   >>   
   >>> 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.   
   >>   
   >>   
   >   
   > So, have a reference that uses it the way you do, or are you admitting   
   > that it is you own cockamamie perversion of a system that works for the   
   > things it works for but not this sort of system.   
   >   
      
    From “Intuitionistic Type Theory” (1984), p. 7)   
   “To know a proposition is true is to know a proof of it.”   
      
   --   
   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)