Skip to content

Soundness and Completeness

Suppose that \(\Gamma\) is a set of qf formulas of \(LR(\sigma)\) and \(\psi\) is a qf formula of \(LR(\sigma)\).

\(\Gamma\vdash_\sigma \psi\) means that there is a derivation of natural deduction of \(\psi\) where all undischarged assumptions are elements of \(\Gamma\).

\(\Gamma\models_\sigma\psi\) means that for all \(\sigma\)-structures \(A\), if for all \(\chi\in\Gamma\), \(\models_A\chi\), then \(\models_A\psi\).

Soundness of Natural Deduction with qf Sentences

Let \(\sigma\) be a signature, \(\Gamma\) a set of qf sentences of \(LR(\sigma)\) and \(\psi\) a qf sentence of \(LR(\sigma)\). Then:

\[\text{If } \Gamma\vdash_\sigma\psi \text{ then } \Gamma\models_\sigma\psi\]

Completeness of Natural Deduction with qf Sentences

Let \(\sigma\) be a signature, \(\Gamma\) a set of qf sentences of \(LR(\sigma)\) and \(\psi\) a qf sentence of \(LR(\sigma)\). Then:

\[\text{If } \Gamma\models_\sigma\psi \text{ then } \Gamma\vdash_\sigma\psi\]

Hintikka Set

Let \(\sigma\) be a signature and let \(\Gamma\) be a set of qf sentences of \(LR(\sigma)\) (with only \(\wedge\) and \(\neg\) in the language). We say that \(\Gamma\) is a Hintikka set if it meets the following conditions:

  1. If \((\varphi\wedge\psi)\in\Gamma\), then \(\varphi\in\Gamma\) and \(\psi\in\Gamma\),
  2. If \(\neg(\varphi\wedge\psi)\in\Gamma\), then either \(\neg\varphi\in\Gamma\) or \(\neg\psi\in\Gamma\),
  3. If \((\neg(\neg\varphi)) \in\Gamma\), then \(\varphi \in\Gamma\).
  4. \(\bot\not\in\Gamma\).
  5. There is no atomic sentence \(\varphi\) such that both \(\varphi\) and \((\neg \varphi)\) are in \(\Gamma\).
  6. For every closed term \(t\), \((t=t)\) is in \(\Gamma\).
  7. If \(\varphi\) is atomic and \(s,t\) are closed terms such that both \((s=t)\in\Gamma\) and \(\varphi[s/x]\in\Gamma\), then \(\varphi[t/x]\in\Gamma\).

Lemma

If \(\Gamma\) is a Hintikka set for \(LR(\sigma)\), then there is some \(\sigma\)-structure \(A\) that is a model of \(\Gamma\).

Lemma

If \(\Gamma\) is a consistent set of qf sentences, then there is a Hintikka set \(\Delta\) such that \(\Gamma\subseteq \Delta\).

Decidability Theorem for qf Sentences

There is an algorithm which, given a finite set of qf sentences, will decide whether or not the set has a model.