XPost: comp.theory, sci.math, sci.lang   
   From: polcott333@gmail.com   
      
   On 12/1/2025 7:39 PM, Tristan Wibberley wrote:   
   > On 01/12/2025 11:02, Mikko wrote:   
   >> olcott kirjoitti 29.11.2025 klo 23.59:   
   >>   
   >> G := (F ⊬ G) // G says of itself that it is unprovable in F   
   >>   
   >> With a reasonable type system that is a type error:   
   >> - the symbol ⊬ requires a sentence on the right side   
   >   
   > If we're using it in its normal epitheoretic meaning. I think Olcott is   
   > using it as a predicative object of a logistic F so it requires a   
   > formula on the right? That's not unreasonable since we take   
   >   
   > A |- B   
   >   
   > as a shorthand for   
   >   
   > |-A => |-B   
   >   
   > leaving us with "B is a formula" to which the unary predicate |- may be   
   > applied to make a statement.   
   >   
      
   The first incompleteness theorem states that in any   
   consistent formal system F within which a certain   
   amount of arithmetic can be carried out, there are   
   statements of the language of F which can neither   
   be proved nor disproved in F.   
   https://plato.stanford.edu/entries/goedel-incompleteness/   
      
   (G) F ⊢ GF ↔ ¬ProvF(┌GF┐)   
   https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom   
      
   G ↔ ¬Prov(⌜G⌝)   
   Directed Graph of evaluation sequence   
   00 ↔               01 02   
   01 G   
   02 ¬               03   
   03 Prov            04   
   04 Gödel_Number_of 01  // cycle thus stuck in infinite evaluation loop   
      
      
   *YACC Syntax of Olcott Minimal Type Theory*   
   https://philarchive.org/archive/PETMTT-4v2   
   I used the "defined as" operator to allow   
   direct self-reference.   
      
   > It's the epitheoretic "=>" that takes a statement on the right, but   
   > clearly it's more complex because systems and lists of statements can be   
   > used on the left. Olcott's use of |- as a predicative object of F is   
   > clearly awkwardly ambiguous, as tempting as it may be.   
   >   
   > The extra awkward thing here is that F is capable of using |- in its own   
   > formulae, making its (normal) use as a unary predicate redundant and   
   > perhaps obstructive leaving us with a system whose statements are   
   > exactly its formulas unless we have a unary predicative with no visible   
   > elements, if it's not nonsense for any other reasons.   
   >   
   > I wonder if that may not be done for some reason. There are lots of   
   > reasons to be concerned about it.   
   >   
   >> - the value of the ⊬ operation is a truth value   
   >   
   > /Should/ we take ⊬ to be an operation here? or just a predicative object   
   > of F?   
   >   
   >> - the symbol := requires the same type on both sides   
   >   
   > Unless it's an operation (as in, an action to be done to generate   
   > sentences/formulas of the system being analysed). When G is an   
   > epitheoretic object rather than an object of a definition extension of F   
   > then I think it /must/ be such an operation.   
   >   
   >   
      
      
   --   
   Copyright 2025 Olcott   
      
   My 28 year goal has been to make   
   "true on the basis of meaning" computable.   
      
   This required establishing a new foundation   
   for correct reasoning.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)