Re: Godel's Incompleteness and Nonmonotonic Logic

From: Stephan Lehmke (Stephan.Lehmke_at_ls1.cs.uni-dortmund.de)
Date: 08/26/04 

Date: 26 Aug 2004 12:13:55 GMT

In article <1b626f1.0408250900.6cd9d691@posting.google.com>,
        jagasian@mailinator.com (Student) writes:
>> > Godel's two famous theorems apply to first-order predicate logic.
>>
>> I'm not completely sure what two theorems you are referring to,
>> but if the theorem generally known as `the' "incompleteness theorem"
>> is among them then this statement is clearly false.
>
>
> Ok, lets settle this once and for all. There is no ambiguity as the
> original and its translations are readily available of Kurt Godel's
> "On Formally Undecidable Propositions of Principia Mathematica and
> Related Systems I". I am referring to the two incompleteness theorems
> presented there, the frist implying the second. Godel's first theorem
> shows that assuming consistency, there exists a formula in first-order
> predicate logic that is neither provable nor is its negation provable.

This is clearly false. Assuming that p is a unary predicate and x a
logical variable, then given the formula

F = (forall x) p(x)

obviously neither F nor -F is provable in first order logic.

No deep theorem of any kind is neccessary for this observation.

Goedel's incompleteness is neither about (un-augmented) first order
logic, nor does it state anything like what you describe above (note that
in the online ressource you gave, Flg stands for semantic consequence
and Bew for provability, so Proposition VI is _not_ (directly) a statement
about provability).

>
> Take classical logic, with one more rule: if "F" is not provable, then
> "not F" is provable, where F is any well formed formula in first-order
> predicate logic, i.e. negation commutes with provability, as is
> seemingly the case in these "Answer Set" logics such as AnsProlog and
> its varients.
>
> Finally, with regards to your comments on the importance of
> computability... my original question is not of computability, it is
> about consistency. The undecidability (lack of computability) of
> provability is not the same as provability, which is what is referred
> to in the aforementioned extension to classical logic.

But non-enumerability of provability is (in most accepted definitions)
the same as non-provability. Hence, in the "logic" you defined as
"Answer Set" logic above, if provability isn't decidable, then the
logic is not complete, full stop. No need to invoke inconsistency
here.

regards
Stephan

Relevant Pages

  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... I am referring to the two incompleteness theorems ... and Bew for provability, so Proposition VI is _not_ a statement ... my original question is not of computability, ...
    (sci.logic)
  • Re: Inside or Outside ?
    ... A numerical relation Ris said to be expressible in S ... I have noticed that, even tough the theorems should be in S, the ... provability path of P, ... a bit interesting at the formal level. ...
    (sci.logic)
  • Re: Godel, Rosser and Turing in 1 Easy Step - and Why would we want to?
    ... If "x proves y" is expressible, then provability does not coincide ... Note that we now have formal specifications for these theorems. ... Turing Machine a halts yes on input b. ... What has truth to do with arithmetic and logic? ...
    (sci.logic)
  • Re: My talk about Godel to the post-grads.
    ... This is not first order theorem where the syntactical Rules of Inference ... over that the proofs of the incompleteness theorems can be carried out ... whether the incompleteness theorems are PROVABLE in Z. Please! ... are the originating points of a proof, provability of a meta theorem flows ...
    (sci.logic)
  • Re: Deep Thoughts # 17: Liar Paradox is a Formal Metamathematical Theorem
    ... Truth and provability need not be defined with different systems. ... theorems is not r.e., any of these can be false if the other ... Formal Systems, ...
    (sci.logic)