Finite Domain of First Order Logic

768 Views Asked by At

Validity in first order logic is semidecidable, that's I would need infinite interpretation in order to prove the validity of a formula. Why this happens even if I use a finite domain for the interpretation? Is it possible to show it with an example?

1

There are 1 best solutions below

3
On

A consequence of Trakhtenbrot's theorem is that finite validity (or equivalently, finite unsatisfiability) in first-order logic is not semi-decidable (and in particular undecidable). By finite validity (resp. unsatisfability) I mean the fact that a first-order formula is true in every (resp. no) interpretation with finite domain.

It also implies that finite satisfiability (the fact that a first-order formula is true in some interpretation with finite domain) is semi-decidable but not decidable.

A nice (but technical) presentation of Trakhtenbrot's theorem and its cocnseqences is available here.