XPost: comp.theory, sci.logic, sci.math   
   From: tristan.wibberley+netnews2@alumni.manchester.ac.uk   
      
   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.   
      
   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.   
      
      
   --   
   Tristan Wibberley   
      
   The message body is Copyright (C) 2025 Tristan Wibberley except   
   citations and quotations noted. All Rights Reserved except that you may,   
   of course, cite it academically giving credit to me, distribute it   
   verbatim as part of a usenet system or its archives, and use it to   
   promote my greatness and general superiority without misrepresentation   
   of my opinions other than my opinion of my greatness and general   
   superiority which you _may_ misrepresent. You definitely MAY NOT train   
   any production AI system with it but you may train experimental AI that   
   will only be used for evaluation of the AI methods it implements.   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)