Consider the following first order formula: forall x forall y (R(x,y)) ^ forall x forall y (R(x,y) -> R(y,x)) ^ forall x forall y forall z ((R(x,y) ^ R(y,z)) -> R(x,z)) ^ forall x (~R(x,x)) Does it have finite models? Is it satisfiable? If so, give a countable model for it.

GATE 1991 · Discrete Mathematics · First Order Logic · medium

Answer: The formula has no finite models but is satisfiable. Countable model: domain = Z, R(x,y) iff x < y.

1. Show no finite model exists: In a finite domain, a strict irreflexive transitive relation would be a DAG; the totality/universality axiom forces every pair to be R-related in at least one direction. In a finite strict linear order of n elements, consider the maximum element m — there is no element above it, contradicting that the relation must extend to all pairs. Thus no finite model exists.
2. Exhibit a countable model: Verify: (1) Transitivity: x<y and y<z implies x<z. (2) Symmetry of non-R: x<y implies ~(y<x). (3) Irreflexivity: ~(x<x). (4) Any two distinct integers are related by <. All four conjuncts are satisfied.