# Deducing the compactness theorem from the completeness theorem (in first order logic)

Given that $\Sigma\vdash\phi \Leftrightarrow \Sigma\vDash\phi$, I want to prove: $\Sigma \text{ satisfiable} \Leftrightarrow \text{ every finite subset of } \Sigma \text{ is satisfiable}$.

I will post my idea below, but I can't quite finish the $\Leftarrow$ direction. I would need that the set which I will call $\Delta$ is finite. Can someone point out what I'm missing please? Thank you very much.

Proof: The $\Rightarrow$ direction holds because if $\Sigma$ is satisfiable it has a model, which in turn is a model of every (especially every finite) subset of $\Sigma$.

$\Leftarrow$: Proof by contradiction. If $\Sigma$ is not satisfiable, then it isn't consistent. I.e. $\Sigma \vdash \bot$. This means that there is a subset $\Delta$ of $\Sigma$ from which $\bot$ is derivable. Correctness then gives $\Delta \vDash\bot$, i.e. for every model $\mathscr{A}$ one has that $\mathscr{A}\vDash\Delta$ gives $\mathscr{A}\vDash\bot$. But the last statement applies for no model, so we already have $\mathscr{A}\not\vDash\Delta$ for every $\mathscr{A}$, meaning that $\Delta$ has no model. If I knew that $\Delta$ was finite, then I would have a contradiction.

• Every proof uses only finitely many statements from $\Sigma$. Feb 3, 2016 at 19:32
• If $\Sigma\vdash\bot$ then there is a finite $\Delta\subseteq\Sigma$ such that $\Delta\vdash\bot$. Feb 3, 2016 at 19:32

Hint: call $n$ the length of a proof of $\bot$ from $\Sigma$. Then, at most $n$ formulas of $\Sigma$ appear in the proof. Set $\Delta=\{\gamma\in\Sigma: \text{$\gamma$appears in the given proof of$\bot$from$\Sigma$}\}$. Then $\Delta$ is finite and $\Delta\vdash\bot$.

• Is there an intuitive reason why a proof has to be finite? Feb 3, 2016 at 19:49
• I'm not sure what your definitions are, but in most cases, formulas are defined to be finite, if proofs could be infinitely long, then that'd contradict the finiteness of a formula (as you could construct infinite formulas from proofs). Feb 3, 2016 at 19:53
• It will be provable from the formal definition of a derivation/formal proof. For example, one book might say that a derivation is a finite sequence of formulas such that each formula is an axiom, an assumption, or derivable form previous formulas by modus ponens. Another book might define a derivation to be a finite tree of a particular kind. There are logics other than first-order logic where a proof may involve infinitely many formulas, but in those logics compactness does not generally hold. @see Feb 3, 2016 at 20:29
• @Carl Mummert Thank you for the elaboration. Feb 3, 2016 at 20:59