Re: Godel's Incompleteness and Nonmonotonic Logic

From: Jamie Andrews; real address _at_ bottom of message (me_at_privacy.net)
Date: 08/25/04 

Date: 25 Aug 2004 19:27:11 GMT

In comp.lang.prolog Student <jagasian@mailinator.com> wrote:
>> > Godel's two famous theorems apply to first-order predicate logic....
> 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.

     No, it shows that, assuming consistency, there exists a
formula in first-order *arithmetic* that is neither provable nor
is its negation provable. The proof depends crucially on the
ability to use arithmetic operations (to encode proofs). The
reference to Russell & Whitehead's "Principia Mathematica" in
the title is intended to point this out.

     Goedel's *completeness* theorem of the same year (and other
similar completeness theorems) do show that if any given formula
of first order logic is true in all models, then it is provable.
This can be extended (trivially) to say that if a given formula
F is true in all models of a finite set {A1, A2, ..., An} of
axioms, then F is provable from A1, ..., An. This is trivially
true because (A1 & ... & An) -> F is true in all models and
therefore provable.

     This *completeness* result does not extend to arithmetic
because no *finite* set of axioms characterizes arithmetic.
Induction on the integers is an axiom *schema*, not a single axiom.

--Jamie. (a Dover edition designed for years of use!)
  andrews .uwo } Merge these two lines to obtain my e-mail address.
         @csd .ca } (Unsolicited "bulk" e-mail costs everyone.)

Relevant Pages

  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... you are using them in a standard way in CBL. ... assertion that the set of theorems is ... Any system where PR being the set of theorems satisfies the axioms. ... theorems or truths of any given system besides your say so. ...
    (sci.logic)
  • Re: primitive recursive: obsolete?
    ... we have to add more axioms. ... all true sentences of arithmetic in the language of PA. ... logic we define the set of sentences true in the standard model of PA ... theorems" or not has no bearing on the fact that what I said is ...
    (sci.logic)
  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... I am referring to the two incompleteness theorems ... ability to use arithmetic operations (to encode proofs). ... F is true in all models of a finite set of ... because no *finite* set of axioms characterizes arithmetic. ...
    (comp.lang.prolog)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ...  It's the *axioms* ... If no more theorems to generate, ... bastardizing the notion of an axiomatic system to the point that it ... The program was to be able to rewrite all mathematics starting using ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... It's the *axioms* ... If no more theorems to generate, ... Otherwise it's not an axiomatic system. ... The program was to be able to rewrite all mathematics starting using ...
    (sci.logic)