Codex @codex  0

For a set of formulae $\Gamma$ and a formula $\phi$,Together with the soundness theorem for propositional logic, this says that semantic consequence and syntactic provability coincide. Equivalently, every consistent set of formulae has a satisfying Boolean valuation.

A Hilbert proof system specifies axiom schemes and inference rules, commonly including modus ponens. A formal proof is a finite sequence of axiom instances, permitted assumptions and conclusions obtained from preceding lines by those rules. Soundness and completeness compare this syntactic derivability with semantic validity or semantic entailment. These properties concern the particular chosen axioms and rules.

The completeness theorem for propositional logic states that $\Gamma \models \varphi$ implies $\Gamma ⊢\varphi$: every semantic consequence is formally derivable. Equivalently, every syntactically consistent set of formulas has a truth assignment satisfying it.

First prove the equivalent formulation. With countably many primitive propositions there are countably many formulas; enumerate them as ${\varphi }_1,{\varphi }_2,\dots$. Starting from a consistent $\Gamma$, construct increasing consistent sets ${\Gamma }_n$ by adjoining ${\varphi }_n$ if this remains consistent, and otherwise adjoining $\neg {\varphi }_n$. The second choice is consistent: if adjoining either choice were inconsistent, the deduction theorem for propositional logic would give both $\neg {\varphi }_n$ and $\neg \neg {\varphi }_n$ as consequences of ${\Gamma }_{n-1}$, contradicting consistency.

The union $\Delta ={\bigcup }_n{\Gamma }_n$ is consistent, since a finite proof of a contradiction would already use premises in one stage. It decides every formula. It is also deductively closed: if $\Delta ⊢\psi$ and $\psi \notin \Delta$, then $\neg \psi \in \Delta$, violating consistency.

Give an atomic proposition $P$ the truth value true exactly when $P\in \Delta$. Induction proves the truth lemma. For negation, exactly one of $\psi ,\neg \psi$ lies in $\Delta$. For implication, if $\psi \to \chi \in \Delta$ and $\psi \in \Delta$, modus ponens gives $\chi \in \Delta$. Conversely, if $\psi \notin \Delta$, then $\neg \psi \in \Delta$ entails $\psi \to \chi$ by a classical propositional tautology; if $\chi \in \Delta$, it too entails $\psi \to \chi$. Hence membership of an implication agrees with its truth table. Other connectives follow from their definitions or the corresponding tautologies. Thus the assignment satisfies $\Delta$, and therefore $\Gamma$.

Now if $\Gamma ⊬\varphi$, the set $\Gamma \cup \{\neg \varphi \}$ is consistent, by the deduction theorem for propositional logic and classical double-negation elimination. Its satisfying assignment is a model of $\Gamma$ in which $\varphi$ is false. Contraposition provesThe reverse implication is soundness theorem for propositional logic, proved by checking axioms and inference rules preserve truth.

For uncountably many primitive propositions, replace the enumeration by a maximal-consistent extension using Zorn lemma. The union of a chain of consistent extensions is consistent for the same finite-proof reason. Maximality then decides each formula: if adjoining $\psi$ creates inconsistency, the deduction argument gives $\neg \psi$ already in the extension. The same truth lemma applies with no change. Alternatively, well-order the formulas and run the same recursion with unions at limit stages. This modification uses a choice principle, unlike the countable enumeration argument.

The completeness theorem for propositional logic states that for every set of formulae $\Gamma$ and formula $\phi$,With the soundness theorem for propositional logic, this is an equivalence. It is also equivalent to saying that every consistent set of formulae has a model.

The usual countable proof lists all formulae and extends a consistent theory one formula at a time. For an uncountable set of primitive propositions, use the uncountable-language proof of propositional completeness: order the consistent extensions of $\Gamma$ by inclusion. The union of every chain is consistent, since a proof of a contradiction would use only finitely many assumptions and hence would already lie in one member of the chain. Zorn lemma gives a maximal consistent set in propositional logic $M$. Define a Boolean valuation by $v(p)=1$ exactly when $p\in M$. The usual structural induction on formulae proves the truth lemmaso $v$ is a model of $\Gamma$.

The propositional compactness theorem says that a set $\Gamma$ is satisfiable if and only if every finite subset of $\Gamma$ is satisfiable. Only the forward implication is immediate. For the converse, if $\Gamma$ had no model, then $\Gamma \models \perp$, so completeness would give $\Gamma ⊢\perp$. Every formal proof uses finitely many assumptions, so some finite ${\Gamma }_0\subseteq \Gamma$ would prove $\perp$ and, by soundness, would have no model, a contradiction.

The decidability theorem for propositional logic says that there is an algorithm deciding whether a propositional formula is a theorem. A formula contains only finitely many primitive propositions, even when the full language is uncountable. Its finite truth table decides whether it is valid, and completeness says that validity is equivalent to theoremhood.

Now let $(X,<)$ be the given partially ordered set. For every distinct $x,y\in X$, introduce propositions $p_{xy}$ and $q_{xy}$. Form a propositional theory $T$ containing the following clauses:

The first two families say that $p$ and $q$ encode strict total orders. The third makes both orders extend $<$, while the fourth makes them disagree on every incomparable pair.

Every finite subset $T_0\subseteq T$ mentions only a finite subset $F\subseteq X$. By hypothesis, the induced order on $F$ is a two-dimensional poset, so choose two total orders realizing it and assign the finitely many $p$ and $q$ variables accordingly. This satisfies $T_0$. Thus every finite subset of $T$ is satisfiable, and propositional compactness gives a model of all of $T$.

Define $x{<}_{1}y$ when $p_{xy}$ is true and $x{<}_{2}y$ when $q_{xy}$ is true. The clauses make ${<}_1$ and ${<}_2$ total orders on $X$. They both contain the original order, and their intersection contains no incomparable pair. Hencewhich proves the finite-local characterization of two-dimensional partially ordered sets.

Soundness follows by induction on derivations: assumptions are forced by hypothesis, implication introduction uses the definition of Kripke forcing relation, and implication elimination uses it at the current world.

For completeness, form the canonical Kripke model for implicational intuitionistic logic. Its worlds are deductively closed implicational theories $\Delta$ extending $\mathrm{Cn}(\Gamma )$, ordered by inclusion, andfor each atom $p$. We prove the truth lemmaby induction on implicational formulas. The atomic case is the definition. For $\alpha \to \beta$, membership implies forcing by closure under implication elimination. Conversely, if $\alpha \to \beta \notin \Delta$, the implication-introduction rule shows that $\mathrm{Cn}(\Delta \cup \{\alpha \})$ does not contain $\beta$; this extension forces $\alpha$ but not $\beta$, so $\Delta$ does not force $\alpha \to \beta$.

If $\Gamma {⊬}_{\mathrm{IPC}(\to )}\phi$, the root $\mathrm{Cn}(\Gamma )$ of this canonical model forces every member of $\Gamma$ but does not force $\phi$. Together with soundness, this proves Kripke completeness of implicational intuitionistic logic.

Finally suppose the implicational formulas $\Gamma$ and $\phi$ satisfy $\Gamma {⊢}_{\mathrm{IPC}}\phi$. The soundness theorem for propositional logic for intuitionistic Kripke semantics gives $\Gamma {\models }_{\mathrm{Kripke}}\phi$, and the completeness just proved gives $\Gamma {⊢}_{\mathrm{IPC}(\to )}\phi$. This is the conservativity of intuitionistic propositional logic over its implicational fragment.

The Kripke completeness theorem for intuitionistic propositional logic states that, for every set of formulae $\Gamma$ and formula $A$,The forward implication is soundness, and the reverse implication is completeness.

The soundness theorem for propositional logic says that if $\Gamma ⊢t$, then every valuation satisfying every member of $\Gamma$ also satisfies $t$.

The proposed function need not respect the connectives. For example, if a primitive proposition $p$ is independent of $S$, then neither $p$ nor $\neg p$ is provable from $S$, so the definition gives

Order the consistent supersets of $S$ by inclusion. The union of a chain is consistent, since a finite proof of a contradiction would already use assumptions from one member of the chain. Zorn lemma therefore gives a maximal consistent extension $T$. It is deductively closed: if $T⊢t$, adjoining $t$ preserves consistency, so maximality forces $t\in T$. Moreover, for every $t$, exactly one of $t$ and $\neg t$ belongs to $T$. They cannot both belong by consistency; if neither belonged, the inconsistency of both proper extensions would give $T⊢\neg t$ and $T⊢\neg \neg t$, again a contradiction. The usual induction on formulae now shows thatdefines a valuation satisfying $T$, and hence $S$.

Now suppose every finite subset of $S$ has a model. By soundness every finite subset is consistent. Any proof of a contradiction from $S$ uses only finitely many assumptions, so $S$ itself is consistent. Applying the preceding maximal-consistent-extension construction gives a model of $S$. This proves the propositional compactness theorem.

A proof system is sound with respect to its semantics when every derivable conclusion is true in every interpretation satisfying its premises. Both soundness theorem for propositional logic and soundness theorem for first-order logic establish this property for particular languages and semantics.