The Conditions Under Which a Sentence of Predicate Logic Can Have a Model but No Finite Model

In predicate logic, a sentence can have a model but no finite model under certain conditions, particularly involving the structure of the predicates and the domain of discourse. This article explores these conditions and provides examples to clarify the concepts.

Key Points to Consider

Infinite Domains: A sentence is satisfied in some infinite domain but not in any finite domain may have a model in an infinite domain but no finite model. This often occurs if the sentence asserts properties that can only be true for infinitely many elements.

Expressing Infinite Properties: Sentences that require an infinite number of distinct elements, such as the existence of infinite sequences or the ability to define certain functions, can have models in infinite structures but not in finite structures. One example is a sentence stating the existence of infinite sequences.

Non-Finite Axioms: If the axioms or sentences involve quantifiers that imply infinite structures, like the existence of infinitely many distinct elements, a theory might not have a finite model even if it has models in general.

Compactness Theorem: This theorem in model theory states that a set of sentences has a model if every finite subset of the set has a model. Thus, a theory requiring infinite structures by implication might not have a finite model.

Example of a Predicate Logic Sentence with No Finite Model

Consider the following logical sentences:

forall x(Exx)forall xforall y(Exy Leftrightarrow Eyx)forall xforall yforall z((Exy wedge Eyz) Rightarrow Exz)forall xforall y(xy Leftrightarrow forall z((Sxz Leftrightarrow Syz) wedge (Szx Leftrightarrow Szy)))forall xexists y(Sxy)forall xforall yforall z((Sxy wedge Sxz) Rightarrow Eyz)forall xforall yforall z((Sxz wedge Syz) Rightarrow Exy)exists y(
egexists xSxy)

This complex sentence can be simplified by interpreting the predicate (Exy) as (xy) and the predicate (Sxy) as “(y) is a successor of (x).”

Understanding the Sentence

The first three sentences essentially state that (Exy) is an equivalence relation:

(forall x(xx)) (forall xforall y(xy Leftrightarrow yx)) (forall xforall yforall z((xy wedge yz) Rightarrow xz))

However, the next sentence implies that (Exy) must be the equality on the nose, i.e., (xy Leftrightarrow forall z((Sxz Leftrightarrow Syz) wedge (Szx Leftrightarrow Szy))). This justifies our understanding that (Exy) can be interpreted as (xy).

Defining the Successor Function

The next two sentences define a unique successor function (N) on the domain, such that:

(forall xforall yforall z((z Nx wedge z Ny) Rightarrow x y)) (Injectivity) (exists y( egexists x(Sxy))) (Non-surjectivity)

This means that (N) is an injective function that is not surjective. Take the natural numbers as a model and interpret (N(x) mapsto x 1). This satisfies the conditions and proves the sentence has at least one model—namely the natural numbers.

No Finite Model

To prove it has no finite model, choose any (x) that is not the successor of anything. Then (Nx) cannot be equal to (x), contradicting the definition of (x). Also, (NNx) cannot be equal to (x) or (Nx). Proceeding by induction, all elements corresponding to (x) are distinct, implying there are infinitely many.

Implications and Insights

This example shows that proving whether a logical sentence has models but only finite models is equivalent to number theory problems. It also highlights how equality and functions can be sneakily included in the language of predicate logic, even if the intentions are to work with predicates.

The von Neumann–Bernays–G?del set theory axioms (NBG) have finite axioms, making them a single logical sentence in predicate logic. Incompleteness theorems apply to NBG, implying there's no algorithm to determine whether a given logical sentence has a model or only finite models.

Tractability

Given the complexity and undecidability, even if you have an oracle for determining the existence of models, determining whether a sentence has a finite model remains undecidable without imposing further constraints.