All text I have read prove the Undecidability of first order logic a bit as an afterthought and after having proved the incompleteness and Undecidability of (Peano) Arithmetic.
This proof also hardly works in philosophy, I would like a proof that first order logic is undecidable, but without using arithmetic , Godels incompleteness theorems and all of that.
It is just such a tortuous route and get many will lost halfway, it is about first order logic why do we need to add arithmetic to proof undecidability?
My own first ideas of a proof:
(not sure even if it is correct, I posted this earlier in little different form at , Gödel's Completeness Theorem and satisfiability of a formula in first-order logic , in the hope of comments)
- There are some formula's where the answer about validity depends on the size of the domain.
$\exists x R(x) \to \forall x R(x) $ is true when the domain only contains one element, but false in any larger domain.
Suppose now we have a formula $\phi $ that is false in every finite domain but is true in an infinite domain.
- We cannot construct a model of $\phi $ just because it requires an infinite domain.
- Also we cannot proof $\lnot \phi $ because it is just not a true statement
So by soundness $ \not \vdash \lnot \phi $ and also $ \phi $ has no finite (constructable) model so $ \phi $ and $\lnot \phi $ are undecidable statements
And for $\phi $ we can just use $\lnot ( \forall x \forall y \forall z (((Rxy \land Ryz) \to Rxz ) \land \lnot Rxx) \land \forall y \exists x Rxy )$
I agree $\phi $ is a kind of (minimal) arithmetic in disguise, interprete Rxy as $ x > y $ , but it is not full arithmetic and the proof is much shorter.
But is this a correct line of reasoning?
Has a model to be constructive? ($ \phi $ is "obviously" satisfiable it is just not constructable)
Are there other and better ways to explain it? (references are very welcome)
Best Answer
But hold on! The proposition "first order logic is undecidable" is, when unpacked, just a proposition of the form "there is no computable function which does so-and-so". So of course a proof of this proposition is going to have to come from an application of the general theory of computable functions. (We might only need a naive ability to recognise a computation when we see it to establish the positive claim that some function can be computed: but to establish a negative, that there is no computable function which does so-and-so, we do need some general theory which can enable us to talk about the limits of the computable).
Now, the relevant computations here are over finite strings that constitute wffs and proofs, so the background theory we need in fact is or is tantamount to the theory of arithmetical computable functions (for you can code finite strings by numbers in familiar ways; or indeed we can go in the opposite direction and reconstruct arithmetic in the theory of finite strings). So the natural lines of proof that first order logic is undecidable will come from the theory of computable arithmetical functions (perhaps in slight disguise). In sum, broadly arithmetical considerations (far from being extraneous, a "tortuous" diversion) are exactly what we would expect to use here.
Added: What I wrote above was [at least intended to be] consistent with the sort of points Carl Mummert's makes in his typically elegant answer. It is the theory of computability that needs to be invoked: but the point at which it gets applied doesn't have to be to a formal arithmetic. As Carl very nicely points out, we could go instead via Tarksi's proof about groups. However, I was taking it that that sort of thing would seem to the OP even more "tortuous" a route to the undecidability result; and we are still applying the theory of computable numerical functions.
That's the main point to be made, but I can perhaps add a subsidiary comment on the remark
Well, by any ordinary constructive standards the wff you describe (losing the unintended negation) has a constructively acceptable model -- the natural numbers in their natural order! What is wrong with that?