Proof of compactness theorem in first order logic - clarification

Question

My question is about this question and the users's answer to it.

Here's the statement of the compactness theorem: If $T$ is a first order theory in some language $L$. The $T$ has a model if and only if every finite subset of $T$ has a model.

One direction $\implies$ is trivial. The user proves the other direction as follows

Assume $T$ does not have a model. Then every sentence $\varphi$ in $L$ is provable from $T$. Let $\varphi$ be any sentence in $T$. Then there is a proof of $\lnot \varphi$ from $T$, $\varphi_1' , \dots, \varphi_n' = \lnot \varphi$. Now let $S = T \cap \{ \varphi, \varphi_1' , \dots, \varphi_n' \}$. Then $S$ is a subset of $T$ and $\varphi$ and $\lnot \varphi$ are provable from it. To see that $\lnot \varphi$ is provable from $S$, observe that $\varphi_i'$ used in the proof are each either a sentence in $T$ or a consequence of such or a formula that is tautologically true. If $S$ is empty, that is, none of them are in $T$, then $\lnot \varphi$ is provable without $T$ and the claim holds. If there are any $\varphi_i' \in S$ then all of them are axioms of $T$ so that by definition, $\lnot \varphi$ is provable from $S$.

My questions are

1.) Why is it clear that $\varphi$ is provable from $S$?
2.) If there are any $\varphi'_i \in S$, then why are all of them axioms of $T$?

score 2 · Answer 1 · answered Oct 12 '13 at 04:52

2

$S\vdash\varphi$ simply because $\varphi\in S$.

The axioms of $T$ are by definition the sentences in $T$. $S\subseteq T$, so every $\varphi_k'\in S$ is a sentence in $T$, i.e., an axiom of $T$. The $\varphi_k'$ that are not in $T$ are either provable from sentences in $T$ or tautologies.

answered Oct 12 '13 at 04:52

Brian M. Scott

616,228

Thanks for the clarification. I misread it as a "If $\varphi'_i \in S$ for any $i$, then $\varphi'_1, \dots , \varphi'_n$ are all axioms of $T$." – user100367 Oct 12 '13 at 05:18
@user100367: You’re welcome. – Brian M. Scott Oct 12 '13 at 05:21

score 1 · Accepted Answer · edited Jun 12 '20 at 10:38

$\varphi$ is provable from $S$ since $\varphi$ is in $S$.
Perhaps it was not clearly written out. Since $T \vdash \neg \varphi$, we can consider a formal proof: $\varphi_1^\prime , \ldots , \varphi_n^\prime$ (where $\varphi_n^\prime$ is $\neg \varphi$). Now consider $S^\prime = T \cap \{ \varphi_1^\prime , \ldots , \varphi_n^\prime \}$: these are the axioms from $T$ which were used in the above proof. So it is really the definition of $\cap$ that ensure that each $\varphi_i^\prime$ belonging to $S$ (or in this write-up $S^\prime$) also belongs to $T$.

Note that the same formal proof gives us that $S^\prime \vdash \neg \varphi$. Taking $S = S \cup \{ \varphi \}$ we have that $S \subseteq T$, and $S$ proves both $\varphi$ and $\neg \varphi$.

Proof of compactness theorem in first order logic - clarification

2 Answers2