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.

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.