Let $\mathcal{L}$ be a languange and let $F\left(\mathcal{L}\right)$
be the corresponding set of formulas in F.O.L.
I encountered a concise script on logics/structure with a nice deduction system on base of the connectives $\wedge$,
$\to$, $\bot$ and $\forall$ where derivations are presented as binary trees by means
of identity axioms and the following rules:
-
$\wedge$ elimination
-
$\wedge$ introduction
-
Modus Ponens
-
Deduction-rule
-
Reductio ad Absurdum
-
Generalization
-
Instantiation
The system deals with all elements of $F(\mathcal L)$ (i.e. formulas) and the script contains a proof of soundness.
Also there is a proof of the following statement:
If $\Sigma$ is
a set of sentences that is (syntactically) consistent (i.e. $\Sigma\nvdash\bot$)
then $\Sigma$ has a model.
However, what I am really after (as counterpart of soundness) is actually a proof of:
If $\Sigma$ is
a set of formulas that is (syntactically) consistent (i.e. $\Sigma\nvdash\bot$)
then $\Sigma$ has a model.
The fact that only sentences are dealt with makes me suspect that there is some obvious extension from sentences to formulas (and I hope that is true), but unfortunately I cannot find it.
Thank you in advance for taking notice of my question.
Best Answer
First prove a lemma: Let $L'$ be a language which includes constant symbols $\{c_i\mid i\in I\}$ (and possibly other constant symbols too), and let $L = L'\setminus \{c_i\mid i\in I\}$. Let $\Delta'\vdash \varphi'$ be a derivation in the language $L'$. Let $\Delta$ and $\varphi$ be obtained from $\Delta'$ and $\varphi'$ by replacing all instances of each constant symbol $c_i$ by a fresh variable $x_i$. Then $\Delta\vdash \varphi$ is a derivation in the language $L$.
This should be an easy induction on the structure of the proof.
Now suppose $\Sigma$ is a consistent set of $L$-formulas. Enumerate the free variables appearing in the formulas in $\Sigma$ as $\{x_i\mid i\in I\}$. For each variable $x_i$, let $c_i$ be new constant symbol, and let $L' = L\cup \{c_i\mid i\in I\}$. Let $\Sigma'$ be the set of $L'$-sentences obtained by substituting $c_i$ for each free instance of $x_i$ in $\Sigma$. By the lemma, $\Sigma'$ is consistent: if $\Sigma'\vdash \bot$ is a derivation in the language $L'$, then $\Sigma\vdash \bot$ is a derivation in the language $L$, since $\Sigma$ is obtained from $\Sigma'$ (up to possibly renaming variables) by replacing each constant $c_i$ with the variable $x_i$.
Now you can use your theorem about consistent sets of sentences to see that there is an $L'$-structure $M'$ which is a model of $\Sigma'$. Letting $M$ be the reduct of $M'$ to $L$, we have that $(M;(c_i^{M'})_{i\in I})$ is a model of $\Sigma$.