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)