LARA

This is an old revision of the document!

Compactness for First-Order Logic

Let $S_0$ be a set of first-order formulas.

Suppose $S_0$ has no model. Then $expandProp(clauses(S_0))$ has no model. Some finite subset of it has no model. Some finite subset of $clauses(S_0)$ has no model. Some finite subset of $S_0$ has no model.