Relation between the monadic and two-variable fragment of first order logic

102 Views Asked by At

My question is whether there are any inclusions or relations with respect to decidability between the monadic and two-variable fragment of classical first-order logic.

1

There are 1 best solutions below

1
On

Monadic classical first-order logic (where all the relation symbols are unary and there are no functions symbols) is decidable, even in the case with identity. This result is known as the Lowenheim–Behmann theorem. An intuition of the proof can be found here.

Having a single binary relation symbol different from identity in a first-order language results in a undecidable logic. This result is known as the Church–Herbrand theorem.

More details can be found in Chapter 21 of Computability and Logic by George S. Boolos, John P. Burgess, Richard C. Jeffrey, 4th edition.