Theory of Set of Formulas is Theory

From ProofWiki
Jump to navigation Jump to search


Let $\mathcal L$ be a logical language.

Let $\mathscr M$ be a formal semantics for $\mathcal L$.

Let $\mathcal F$ be a set of $\mathcal L$-formulas.

Let $T \left({\mathcal F}\right)$ be the $\mathcal L$-theory of $\mathcal F$.

Then $T \left({\mathcal F}\right)$ is a theory.


Let $\phi$ be a $\mathcal L$-formula.

Suppose that $T \left({\mathcal F}\right) \models_{\mathscr M} \phi$.

By definition of $T \left({\mathcal F}\right)$:

$\mathcal F \models_{\mathscr M} \psi$

for every $\psi \in T \left({\mathcal F}\right)$.

Hence by definition of semantic consequence:

$\mathcal F \models_{\mathscr M} T \left({\mathcal F}\right)$

By Semantic Consequence is Transitive, it follows that:

$\mathcal F \models_{\mathscr M} \phi$

Finally, by definition of $T \left({\mathcal F}\right)$:

$\phi \in T \left({\mathcal F}\right)$.

Since $\phi$ was arbitrary, the result follows.