FOM: Satisfiable formulas are not r.e.

[Jeffrey Ketland]

Replying to Roger Bishop Jones: "Reduction of 2nd Order Logic to 1st Order"
(August 29th)
----------------------

Dear Roger

In replying to Matt Insall, you wrote:

>If others had thought so presumably the rules of inference for first order
>logic would have been engineered to demonstrate all satisfiable sentences
>and Godel's completeness result would then have been quite a different
>theorem.
>I don't myself think this would have been an improvement, but I suspect it
>would have in any case have made no difference to my point, since I would
>guess that the satisfiable sentences are also recursively enumerable.


Let S be the set of satisfiable formulas (in, say, L: the lang of 1st order
arithmetic). I think there's proof (using Church's Theorem) that this set is
not r.e.

Let V be the set of valid formulas in L. From Church's Theorem, we know that
V is renotrec (r.e. but not recursive).
So, there is a list {v_n} such that a formula is valid iff it appears on the
list (where v : N --> N is a recursive function; V is its range).
Suppose for reductio that S is r.e.. Then, there would be a list {s_n} such
that a formula is satisfiable iff it appears on the list. (i.e., s : N --> N
is a recursive function and S is its range).
But, this would give a decision procedure for validity!
For let A be a formula. If A is valid, then it appears on the V-list (as
say, v_n). If A is not valid, then ~A is satisfiable, so ~A appears on the
S-list (as say s_m). Hence, we can decide if A is valid, by systematically
checking both these lists. But this is impossible, by Church's Theorem.
Hence, S is not r.e.

(Richard C. Jeffrey 1991 "Formal Logic: Its Scope and Limits" (Chapter 8,
Undecidability) discusses this and other soluble/insoluble cases of the
decision problem).

Best wishes - Jeff


~~~~~~~~~~~ Jeffrey Ketland ~~~~~~~~~
Dept of Philosophy, University of Nottingham
Nottingham NG7 2RD United Kingdom
Tel: 0115 951 5843
Home: 0115 922 3978
E-mail: jeffrey.ketland at nottingham.ac.uk
Home: ketland at ketland.fsnet.co.uk
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~