QUAIL Question of the Day                                Friday, November 15
----------------------------------------------------------------------------

There's a lot of terminological underbrush in AI, and the hardest thing 
for me is making sure I don't get my concepts confused.  As a result, my 
first (rather simple) question checks a distinction in logic.

QUESTION:  Distinguish completeness of a theory and completeness of a
proof procedure; what is Godel talking about in his Completeness and
Incompleteness Theorems?  Please give examples for the first half of the 
question (both complete and incomplete).


PATRICK'S ANSWER:  

A complete theory is one contains, for every sentence in the language,
either that sentence or its negation.  A complete proof procedure for a
theory is one in which every sentence entailed by the axioms of the theory
can be proved.  The theory of the integers with successor is complete; the
theory of standard arithmetic is not.  Modus ponens is an example of an
incomplete proof procedure, and refutation resolution is an example of a
complete one. 

Godel's Completeness Theorem has to do with first-order logic.  It states
that there -is- a complete proof procedure for first-order logic, though
Godel did not provide one (Robinson was the first to present one --
resolution, which is refutation complete, though his rested on earlier
works; this was in the early 1960's).

Godel's Incompleteness Theorem says that the theory of standard (Peano) 
arithmetic is not complete; therefore there are true sentences about 
arithmetic that can't be proven.

 
EYAL'S ANSWER:

Completeness of a theory is the property that every sentence or its negation
is in the theory. Example: Take the model of natural numbers (any language);
Take the set of sentences that hold in that model. This is a complete theory.

Completeness of a proof procedure is the property that if a sentence is a valid
consequence of a set of axioms, then there is a proof using the proof procedure
that the sentence follows from the axioms.

Godel's Completeness Thm: Every consistent theory has a model (some people
say it differently: "\Gamma\models\varphi \implies \Gamma\proves\varphi".
These forms are equivalent). Here he talks about the completeness of the
procedure.

Godel's Incompleteness Thm: If T is a recursively enumerable axiomatization
of an extension of the theory of Natural Numbers, the T is not complete.
This one talks about the incompleteness of theories with recursively
enumerable axiomatization, given that they are rich enough in their
representation power.


LISE'S ANSWER:

good questions--this is the stuff I need to really 
memorize and get speedy on.  These answers are a mish-mash
from genesereth's logic notes and R&N and random guesses.

A theory is complete if for every s, either
s is in T or not s is in T.

A proof procedure is complete if for all s, either
T \proves s or T \proves not s.

Completeness theorem:  
If S logically entails s, then s is provable from S.

(It wasn't until 1965 that Robinson showed that Resolution is
such a procedure)

Incompleteness theorem:
There is no Finite Axiomatization of arithmetic.

If there were, then arithmetic would be decidable.

Arithmetic is not decidable, because you can construct
a mapping from sentences to numbers and represent logical
implication as a numerical condition.  Thus if the theory
of arithmetic were decidable, then logical implication would
be decidable.  We know that logical implication is undecidable
(this is halting problem)

examples:
incomplete theory:  
S = p => q
T = CN(S) 

then neither q or not q is in T.
(I don't think this is right..:-(... it says that theory
always have to be infinite... why?)

complete theory: primes

incomplete proof procedure: modus ponens
complete proof procedure: resolution refutation


PEDRITO'S ANSWER:

a theory is complete iff for every wff F in the language, either F or its
negation is in the theory, i.e. is logically entailed by the theory.  the
classical example of an incomplete theory is that of arithmetic; any
finite axiomatization is incomplete. this is the essence of godel's
incompleteness theorem. (question: is there some particular aspect of
arithmetic, such as equality, that makes any finite theory incomplete?) 
i'm not positive of a good complete theory example--maybe a simple one w/o
equality like the theory of equivalence relations which includes axioms
for transitivity, symmetry, and reflexivity. i need to get a hold of an
enderton. 

on the other hand, a proof procedure is complete iff every statement
entailed by a theory can be infered from the theory using the proof
procedure. godel's completeness theorem relates to this definition of
completeness, stating that there exists a complete proof procedure for
first-order logic. examples of incomplete proof procedures are abundant,
but the first that comes to mind is modus ponens for first-order logic.
the most well-known (resolution-)complete proof procedure for first-order
logic without equality is refutation-resolution. although this procedure
will not generate all the sentences in a theory, if a sentence is in the
theory then the procedure will generate a proof for it. (question: is
there no procedure for fol that is complete in the sense that it will
generate all the sentences in a theory?) 


AVI'S ANSWER:

A complete theory (over a language) is one in which for every sentence in
the language, either the sentence or its negation is in the theory
(remember that a theory is closed under implication).  For example, for FOL
with a single constant 'a', a single predicate R and a single function f,
the consequences of 
	f(a) = a
	R(a)
is complete.   If either sentence is removed the theory is incomplete. 
Godel's Incompleteness Theorem showed that no theory that includes number
theory is complete.  

An complete proof procedure is one that is guaranteed to find a proof of
every valid sentence.  Refutation resolution is complete; modus ponens
alone is incomplete.  Godel's Completeness Theorem showed that a complete
proof procedure exists for FOL.