XPost: comp.theory, sci.math   
   From: news.dead.person.stones@darjeeling.plus.com   
      
   On 03/01/2026 19:02, Tristan Wibberley wrote:   
   > On 03/01/2026 16:32, Mike Terry wrote:   
   >> On 03/01/2026 03:30, Richard Damon wrote:   
   >>> On 1/2/26 9:43 PM, André G. Isaak wrote:   
   >>>> On 2026-01-01 20:09, Richard Damon wrote:   
   >>>>> On 1/1/26 9:45 PM, André G. Isaak wrote:   
   >>>>>> On 2026-01-01 16:48, Richard Damon wrote:   
   >>>>>>> On 1/1/26 6:13 PM, Tristan Wibberley wrote:   
   >>>>>>>> On 01/01/2026 22:40, Richard Damon wrote:   
   >>>>>>>>   
   >>>>>>>>> But it IS a theorem of the base system, as it uses ONLY the   
   >>>>>>>>> mathematical   
   >>>>>>>>> operations definable in the base system. What makes you think it   
   >>>>>>>>> isn't a   
   >>>>>>>>> Theorem in the base system.   
   >>>>>>>>   
   >>>>>>>> It has no derivation in the base system, if it had you wouldn't   
   >>>>>>>> think   
   >>>>>>>> the base system were incomplete.   
   >>>>>>>>   
   >>>>>>>   
   >>>>>>> It has no PROOF in the base system.   
   >>>>>>   
   >>>>>> Which means it is not a theorem of the base system. A theorem is a   
   >>>>>> statement which can be proven in a particular system.   
   >>>>>   
   >>>>> I guess it depends on your definition of a "Theorem".   
   >>>>>   
   >>>>> I am using the one that goes:   
   >>>>>   
   >>>>> "A Theorem is a statement that has been proven."   
   >>>>   >   
   >>>>> note, no restriction that the proof was in the system the Theorem is   
   >>>>> stated in, as long as the proof shows that it is actually True in   
   >>>>> that system.   
   >>>>   
   >>>> A theorem is a statement that can be derived from the axioms of a   
   >>>> particular system. It may be true in other systems, but it is only a   
   >>>> theorem in systems in which it can be derived.   
   >>>   
   >>> Right, And the statement og Godel's G can be fully derived in the base   
   >>> system, as it is purely a mathematical relationship using the   
   >>> operations derivable in the system.   
   >>   
   >> Neither G nor ¬G has a derivation (in your terms, a "formal prooof")   
   >> within the base system.  That is what Godel proves, showing that the   
   >> base system is incomplete.   
   >   
   > That can't be what he meant can it? Lots of systems were known to have   
   > statements that had no derivation, all nonsense statements, for example.   
      
   Yes it was what he meant!  :/   
      
   His theorem was about formal systems of arithmetic.  Such systems don't   
   contain "nonsense   
   statements".  They have construction rules that define what constitues a well   
   formed formula (WFF),   
   and amongst those what so constitutes a "sentence".  The semantics for the   
   system define what every   
   sentence "means".  It is not possible to create "nonsense" sentences.   
      
   ok, we can put together nonsense strings of symbols like ∃∧=∧, but that   
   is not a WFF, let alone a   
   sentence.  Derivations (formal proofs using the system proof rules) produce   
   sentences as their   
   derived conclusion.  Incompleteness means that there is a /sentence/ s such   
   that neither s nor its   
   negation ¬s has a derivation.  (Of course the formulas "∃∧=∧" and   
   "¬∃∧=∧" and do not have a   
   derivation, but that's irrelevant.)   
      
   And yes, lots of theories are incomplete, for totally unremarkable reasons.    
   Godel wasn't claiming   
   to have discovered a new phenomenon!  :)  He was pointing out that a   
   /particular/ theory, which to   
   the best of anyone's knowledge at the time might well be complete [we would   
   certainly be pleased if   
   it were incomplete] /in fact/ was incomplete.   
      
   Look, imagine it turned out that P was in fact complete rather than   
   incomplete.  Obviously if we   
   chop out a few axioms, keeping same language etc., we can make the resulting   
   system incomplete,   
   right?  We may not even have enough derivation rules to prove very simple   
   arithmetic statements like   
   2+2=4 or their negations.  If Godel had announced that he had found this   
   incomplete system people   
   would have been puzzled at the joke, because nobody ever considered such a   
   system might be complete   
   in the first place.  This is just how some systems behave, no problem.   
      
   (Alternatively, it's totally trivial to give examples of FOL systems which are   
   obviously incomplete,   
   and we would be quite happy with that.  Such theories may well be worthy of   
   study in their own   
   right, although they are incomplete.  Um, example: the theory with equality   
   and no non-logical   
   symbols, and one single non-logical axiom:   
      
   Axiom:   ∀x∀y∀z (x=y ⋁ x=z ⋁ y=z)    // there are at most 2 objects   
   in our domain.   
      
   The resulting theory is obviously incomplete, and there's nothing "wrong" in   
   that.  Some theories   
   are just incomplete...  In our case we can't prove either of the following:   
      
   [a]     ∀x∀y (x=y)    // there's only one object in our domain   
   [b]    ¬∀x∀y (x=y)    // there's at least two objects in our domain   
      
   Looked at in terms of models of our Theory, models are those sets containing   
   at most 2 elements.   
   Once we fix on a particular model, one of [a] or [b] become TRUE in that   
   model, but which depends on   
   the model.   
      
   That's all incompleteness is saying (for FOL at least).  In GIT (FOL version)   
   neither the G   
   statement nor its negation is derivable, and in fact there are models of the   
   theory where G is TRUE,   
   and models where it is false.  G is TRUE in the model consisting of the   
   natural numbers with usual   
   arithmetic operations (sometimes called the "intended" model), i.e. G is true   
   when interpreted as an   
   arithmetic statement.   
      
   Hmmm, just for clarity, G is not a Theorem of the base system, although it is   
   TRUE in the particular   
   model we are most interested in.  If G were a Theorem of the base system, it   
   would be TRUE in every   
   model of that system, because FOL is sound and only proves true statements in   
   its models!   
   )   
      
   GIT was shocking because it showed that a system we /hoped/ might be complete,   
   in fact was not.  And   
   the method of proof for GIT basically shows that we can't fix such logical   
   systems in the nice we   
   we'd like by simply adding some "missing" axioms that we'd overlooked.  Either   
   the new system would   
   still be incomplete, or it would be inconsistent, or we would lose the ability   
   to effectively   
   recognise whether or not a statement is an axiom.  The world was not as simple   
   as people had hoped, sob.   
      
   >   
   > Did he really mean that there's some level of completeness in which   
   > there is meaninglessness (things that look like propositions but which   
   > are not? Well, duh. But arithmetic isn't required for that, merely   
   > self-references such as non-ranked definitions and fixed-point   
   > combinators (the meaning depends on a meaning that depends on a meaning   
   > that...).   
      
   No, I'm pretty sure he didn't mean that!   
      
      
   Mike.   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)