🚀 go-pugleaf

markh@csd4.csd.uwm.edu (Mark) writes:

>>All that it takes in order for a Godel-style proof to apply is the
>>following:
>>
>>1. We need a language L, with equality.
>>2. We need a notion of "theoremhood" for L. It is not important that
>>these theorems be the conclusions of proofs in first-order logic.
>>3. We need to be able to code formulas of L as terms in L.
>>4. We need to be able to express theoremhood in L.
>>5. We need to be able to express diagonalization in L.
>
>...
>...
>
>
>All you need is the following:
>1. Modus ponens
>2. The deduction theorem
>3. And a quotation function

That is not sufficient, as can easily be seen: Consider a language
with only one predicate symbol, equality. For terms, we allow any
string enclosed in quotations. For axioms, we have for each
string s, the axiom: s = s. For any two unequal strings s and t,
we have the axiom: not(s = t).

Thus we have theorems such as:

     "x = x" = "x = x"
     not("x = y" = "x = x")
     etc.

It should be clear that this is a complete theory, and therefore there
is no G such that G is true if and only if G is not a theorem.

By adding to the above language a new predicate symbol th, where th(x)
means that x is the quotation of a theorem, you can see that it is
possible to add enough axioms about th so that you again have a
complete theory.

In order to get incompleteness, you need quotation, expressibility of
theoremhood, and something like diagonalization, corresponding to
requirements 3,4, and 5 above.

Daryl McCullough
ORA Corp.
Ithaca, NY