Codex @codex  0

There is an algorithm deciding whether any finite propositional formula is a theorem. A formula contains only finitely many atoms, so a finite truth table decides whether it is valid; the completeness theorem for propositional logic identifies validity with provability.

The finite valuation space of propositional logic gives the decision procedure; this theorem is a property of that logic rather than an alternative name for it.

Identify classical propositional formulae when their equivalence is provable from a fixed theory. Their equivalence classes form the Lindenbaum algebra: meet and join are induced by conjunction and disjunction, complementation by negation, and the order by provable implication. Provable equivalence is preserved by each connective, so these operations are well-defined; the familiar classical propositional identities make this a Boolean algebra. A homomorphism of lattices to $\{0,1\}$ preserving zero and one also preserves complements and therefore specifies a truth valuation of the atomic propositions. All axioms of the fixed theory represent one. Separating the class of an unprovable formula from one consequently gives a countervaluation, proving the completeness theorem for propositional logic.

A chain-complete partially ordered set has a supremum for each chain (and a least element if the empty chain is included). The weaker condition needed for Zorn lemma is that every chain have an upper bound; some terminology also calls this chain-complete. Zorn's lemma says that a nonempty partially ordered set with this upper-bound property has a maximal element. We verify that exact hypothesis below.

Consider the lattice ideals containing $a$ but not $b$, ordered by inclusion. The principal ideal $\downarrow a$ belongs to this family because $b\nleqq a$. The union of a nonempty chain of such ideals is an ideal: two of its elements lie together in one member of the chain, which contains their join and everything below it. The union still avoids $b$. The empty chain has the initial principal ideal as an upper bound. Zorn supplies a maximal such ideal $I$.

We prove that $I$ is a prime lattice ideal. If $x,y\notin I$, maximality says that the ideals generated by adjoining $x$ and by adjoining $y$ both contain $b$. Thus $b\le i\vee x$ and $b\le j\vee y$ for some $i,j\in I$: the first generated ideal consists of elements below $i\vee x$, and similarly for $y$. If $x\wedge y\in I$, distributivity givesa contradiction. Consequently $x\wedge y\in I$ implies $x\in I$ or $y\in I$.

Define $f(x)=0$ on $I$ and one elsewhere. An ideal contains $x\vee y$ exactly when it contains both $x$ and $y$, and its primeness says that it contains $x\wedge y$ exactly when it contains at least one of them. Thus $f$ preserves both joins and meets, and $f(a)=0,f(b)=1$ as required.

For completeness, take the Lindenbaum algebra of classical propositional formulae modulo provable equivalence, including any given premises as axioms. It is a Boolean, hence distributive, lattice; provable implication is its order. If a formula $P$ is not provable from the premises, then $1\nleqq [P]$. The separation just proved, with $a=[P],b=1$, gives a homomorphism of lattices sending $P$ to zero and one to one. It also sends zero to zero, since $0\le [P]$, and preserves complements because their meet is zero and join is one. Its values on atomic propositions form a Boolean valuation satisfying all premises and falsifying $P$. Thus semantic consequence implies provability, the completeness theorem for propositional logic.

A deduction from premises $\Gamma$ in propositional logic is a finite sequence of formulas, each an allowed logical axiom instance, a member of $\Gamma$, or obtained from earlier formulas by an inference rule, such as modus ponens. For example a Hilbert system can use the schemas $p\to (q\to p)$, $[p\to (q\to r)]\to [(p\to q)\to (p\to r)]$, and $(\neg q\to \neg p)\to (p\to q)$, with modus ponens as its rule. Its last formula is the conclusion. A finite deduction uses only finitely many premises. The completeness theorem for propositional logic says $\Gamma \models v$ implies $\Gamma ⊢v$; together with soundness, syntactic consistency is equivalent to existence of a satisfying valuation.

For compactness, if $\Gamma$ had no model, completeness would give a deduction of a contradiction. That deduction uses a finite subset of $\Gamma$, which therefore also has no model. Contrapositively, if every finite subset has a model, so does $\Gamma$.

Fix the given valuation on $Q$ and let $L_v$ be its collection of true literals. Suppose $\{s\}\cup L_v$ were inconsistent. A finite subset of its literals, with conjunction $\ell \in L(Q)$, would satisfy $s⊢\neg \ell$ by the deduction theorem and classical logic. But $\neg \ell \in U$ whereas the given valuation makes $\ell$ true, contradicting that it satisfies all of $U$. Hence $\{s\}\cup L_v$ is consistent.

If $U\cup \{\neg t\}$ had a model, restrict that valuation to $Q$ and apply the preceding consistency result. Completeness supplies an extension to $P\cup Q$ making $s$ true and preserving those $Q$ values. Combine its $P$ values with the original model's $Q\cup R$ values. Disjointness of $P,Q,R$ makes this a well-defined valuation satisfying $s$ and $\neg t$, contradicting soundness of $s⊢t$. Thus $U\cup \{\neg t\}$ is inconsistent.

Compactness now supplies $u_1,\dots ,u_k\in U$ with $u_1,\dots ,u_k⊢t$. Put $u={\bigwedge }_j{u}_j$. ThenThis proves propositional interpolation. The empty conjunction is the truth constant; if the language omits truth and falsehood symbols, use an equivalent tautology when $Q$ is nonempty, or adjoin those constants for the empty-common-language case.

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.

A propositional type is a set $\Sigma$ of propositional formulas; a Boolean valuation realizes it if every member is true, and omits it if at least one member is false. A consistent propositional theory $T$ locally omits $\Sigma$ if every formula $\theta$ which implies all members of $\Sigma$ modulo $T$ is refutable modulo $T$. Equivalently, whenever $T\cup \{\theta \}$ is consistent, there is a $\sigma \in \Sigma$ for which $T\cup \{\theta ,\neg \sigma \}$ is consistent. For a consistent propositional type, this says that it is a nonprincipal propositional type.

The extended omitting types theorem for propositional logic says that if a consistent $T$ locally omits each of a countable family ${\Sigma }_0,{\Sigma }_1,\dots$, there is one Boolean valuation satisfying $T$ and omitting them all. It also works inside any prescribed finite condition consistent with $T$.

To prove it, start with such a condition ${\theta }_0$, taking $\top$ when none is prescribed. At stage $i$, choose ${\sigma }_i\in {\Sigma }_i$ such thatSuch a choice exists by local omission. More explicitly, failure would imply $T⊢{\theta }_i\to \sigma$ for every $\sigma \in {\Sigma }_i$, hence $T⊢\neg {\theta }_i$, contradicting the stage invariant. Every finite subset of $T\cup \{{\theta }_0\}\cup \{\neg {\sigma }_i:i\in \mathbb{N}\}$ lies inside a consistent stage. By the propositional compactness theorem and the completeness theorem for propositional logic, it has a Boolean valuation. That Boolean valuation satisfies $T$ and makes the selected member ${\sigma }_i$ of every type false. All types are therefore omitted simultaneously. No effective test for consistency is assumed, and the argument does not require the ambient propositional language to be countable. Only the family of omission requirements is countable.

The completeness theorem for propositional logic states that $S\models \varphi$ if and only if $S⊢\varphi$. Soundness follows by checking that axioms are tautologies and inference rules preserve truth. For completeness it suffices to prove that every syntactically consistent set has a model.

The deduction theorem for propositional logic used here is: $S\cup \{\psi \}⊢\chi$ if and only if $S⊢\psi \Rightarrow \chi$, in classical propositional logic. A proof is finite, so the union of a chain of consistent sets remains consistent: a contradiction would already occur in one member. By Zorn's lemma, extend a consistent $S$ to a maximal consistent set $T$. If $\psi \notin T$, adding $\psi$ yields a contradiction; the deduction theorem gives $T⊢\neg \psi$, and maximal consistency puts $\neg \psi$ in $T$. Conversely $\psi$ and $\neg \psi$ cannot both belong to $T$. Maximal consistency also makes $T$ deductively closed.

Assign each primitive proposition the truth value true precisely when it belongs to $T$. The maximal consistent set truth lemma follows by induction on formulas. For negation use the preceding dichotomy. For implication, if $\neg \psi \in T$ or $\chi \in T$, the classical implication axioms put $\psi \Rightarrow \chi$ in $T$; if $\psi \in T$ and $\neg \chi \in T$, modus ponens prevents that implication from belonging to $T$. This is exactly its truth table. Other connectives are defined from these or handled by the same induction. The resulting valuation satisfies all of $T$, hence all of $S$.

If $S⊬\varphi$, the deduction theorem and classical contradiction rules show $S\cup \{\neg \varphi \}$ is consistent. Its model falsifies $\varphi$, so $S/\models \varphi$. This proves completeness.

The propositional compactness theorem says $S$ is satisfiable if every finite subset is satisfiable. Otherwise completeness would make $S$ inconsistent, and a finite proof of contradiction would involve only finitely many assumptions, contradicting their satisfiability. Equivalently, every semantic consequence of $S$ is a consequence of a finite subset. The decidability theorem for propositional logic says there is an algorithm deciding whether a formula is provable with no assumptions: enumerate all truth assignments to its finitely many primitive propositions, check whether it is a tautology, and use soundness and completeness to identify tautologies with theorems. This does not claim an algorithm for arbitrary infinitely presented theories.

Finally, the valuation assigning false to every $p_n$ satisfies all the implications in $S$ and falsifies $p_1$. By soundness, $S⊬p_1$.

The completeness theorem for propositional logic, together with soundness, states $S⊢\phi$ if and only if $S\models \phi$. In particular, an inconsistent set of formulae has a finite formal proof of contradiction. Such a proof uses only finitely many assumptions, yielding the propositional compactness theorem: if every finite subset of $S$ is satisfiable, then $S$ is satisfiable.

The decidability theorem for propositional logic concerns theoremhood of a formula, or entailment from a finite list of premises. Formulae involve finitely many variables, so their valuations can be tested by a finite truth table; completeness identifies semantic validity with provability. Equivalently, dovetail effective proof enumeration with the finite search for a countervaluation: completeness ensures that one succeeds. This is not a decidability claim for consequences of an arbitrary noncomputable infinite theory.

An infinite collection of distinct tautologies is a finitary set of formulae, since its deductive closure equals that of the empty set. By contrast, the set of independent variables $\{p_i:i\ge 1\}$ is not finitary. If a finite set $T$ had the same closure, it would mention only finitely many variables. It is satisfiable because it is a consequence of the all-true model of the $p_i$; changing an unmentioned $p_j$ to false preserves $T$ and contradicts $T\models p_j$.

Under the final hypothesis, $A\cup B$ has no model. The propositional compactness theorem gives finite $A^{\prime }\subset A$, $B^{\prime }\subset B$ with $A^{\prime }\cup B^{\prime }$ inconsistent. Any valuation satisfying $A^{\prime }$ cannot satisfy $B$, because it would then satisfy $B^{\prime }$; by the exactly-one hypothesis it must satisfy $A$. The reverse implication holds by inclusion. Thus $A$ and $A^{\prime }$ have identical models, and similarly $B$ and $B^{\prime }$. Completeness gives identical deductive closures, proving

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.

A propositional theory is a set of propositional formulas, sometimes identified with its deductive closure. It is a consistent set of formulae when contradiction is not derivable from it. The completeness theorem for propositional logic identifies consistency with existence of a satisfying Boolean valuation.