TITLE: Consequences of negating Russell's infinity axiom in FOL
QUESTION [2 upvotes]: Apologies in advance for another curious question.
From my research, it is clear that for any natural number we can construct a model that would entail a sentence such that there is the same number of elements in the domain of that model.
So, why not generalize this by using the negation of Russell's infinity axiom as a sufficient means to achieve the same ends (i.e. the entailment of any sentence in a finite domain)?

REPLY [1 votes]: It sounds like you're looking for a sentence which is satisfied in exactly the finite structures. By the compactness theorem$^1$, no such sentence exists in first-order logic. The crucial point is that a structure may be "wrong about itself." The classic example of this is the existence of nonstandard models of first-order Peano arithmetic: these are discrete ordered semirings which satisfy the first-order induction scheme, so "think" that all their initial segments are finite, yet "from the outside" have infinite elements. A first-order "axiom of finity" may rule out obvious infiniteness-es, but it won't be able to genuinely ensure that the structure in question is finite.
Of course this is a limitation of first-order logic specifically. In second-order logic for example we can indeed write down a sentence true in exactly the finite structures. But there are good technical reasons for wanting to stick to first-order logic; ultimately compactness (and its "cousin in limitation," the Lowenheim-Skolem theorem) is a good thing to have.

$^1$Specifically, suppose $\varphi$ is a first-order sentence true in structures of arbitrarily large cardinality. Then the theory $$\{\varphi\}\cup\{\exists x_1,...,x_n(\bigwedge_{1\le i<j\le n}x_i\not=x_j): n\in\mathbb{N}\}$$ is finitely satisfiable, hence by compactness has a model. But such a model must be infinite.
{"set_name": "stack_exchange", "score": 2, "question_id": 3930298}