finitely satisfiable

(Robinson's Non-standard analysis)

Definition.

Let Φ(x) be a set of formulae, each in the variables x=(x₁,...,x_n). Φ is called finitely satisfiable if for every finite subset Ψ⊆Φ there exists c=(c₁,...,c_n) such that ψ(c) holds for all ψ∈Ψ.

Examples.

1. In the language of real numbers with the standard model of the real numbers, the set of formulae "x<a", for every constant a∈R: Φ = {x:x<a: a∈R}. Φ is finitely satisfiable: if we are given the formulae indexed by a₁,...,a_n, then x=0.5*min{a₁,...,a_n} satisfies x<a₁,...,x<a_n. Thus Φ is finitely satisfiable.
2. In the language of natural numbers with the standard model of natural numbers, the set Φ = {x:x>n: n∈N}. Again, it is easy to see that Φ is finitely satisfiable -- e.g. take x=n₁+...+n_k to satisfy the formulae indexed by these k n's.
3. In the language of set theory, let Φ be the set of formulae "x has at least n different elements", for all n. That is, Φ={φ_n: n≥ 0}, where

   φ_n(x) = ∃t₁...∃t_n: (t₁∈x & ... & t_n∈x) & (t₁≠t₂ & ... & t₁≠t_n & ... & t_n-1≠t_n

   Then Φ is finitely satisfiable, even if our model includes only finite sets, as long as it includes arbitrarily large finite sets.