A sentence valid in all finite structures

Question

Consider a first order language $L$. Let $S$ be an $L$-sentence true in all finite $L$-structures but false in some infinite $L$-structure. The completeness theorem implies $S$ can not be proven by usual means. Yet, is there another way to establish $S$ is true in all finite models? Another question is whether we can write down $S$ at all. Are there some examples, say, from graph or set theory?

Answer 1

Another question is whether we can write down S at all.

Consider the language $\mathcal{L} = \{ \leq \}$, and the sentence $S$ saying that if

1. $\leq$ is transitive ($\forall x,y,z. x \leq y \wedge y \leq z \rightarrow x \leq z$),
2. $\leq$ is antisymmetric ($\forall x,y. x \leq y \wedge y \leq x \rightarrow x = x$,
3. $\leq$ is reflexive ($\forall x. x \leq x$), and
4. $\leq$ is total ($\forall x,y. x \leq y \vee y \leq x$)

then there is a $\leq$-maximum element ($\exists x. \forall y. y \leq x$).

This sentence is true in every finite $\mathcal{L}$-structure, but of course false in $\langle \mathbb{N}, \leq \rangle$ where $\leq$ denotes the standard ordering of $\mathbb{N}$.

The completeness theorem implies S can not be proven by usual means. Yet, is there another way to establish S is true in all finite models?

As you note, as long as we allow arbitrary (finite or infinite) structures, Gödel's completeness theorem provides a strong correspondence between semantic validity and deductive (syntactic) provability.

Of course, the $S$ written down above is not provable in first-order logic, since it fails in some (infinite) structure.

Unfortunately, it is not possible to find similar, complete deductive rules that would allow us to prove precisely those sentences that hold in all finite structures: this follows from a well-known result in recursion theory, known as Trakhtenbroth's theorem.