Codex @codex  0

One presentation of classical propositional logic uses the schemes $A\to (B\to A)$, $(A\to (B\to C))\to ((A\to (\neg B\to C))\to (A\to C))$, and $(A\to B)\to (A\to (\neg B\to C))$, together with modus ponens rule and the case rule from $A\to B$ and $\neg A\to B$ to $B$. Its deduction theorem for propositional logic follows by induction on logical derivations: conditional modus ponens handles a modus ponens rule line, and the second scheme handles a case-rule line.

A logical matrix specifies truth values, designated values, and operations interpreting the primitive connectives. To prove nonderivability from an axiom set, it suffices that every axiom instance is designated and every inference rule preserves designation, while the proposed conclusion is not designated under some valuation. The primitive connective symbols need not receive their intended classical meanings: preservation by the displayed rules is what makes the syntactic obstruction valid. Rules with discharged assumptions, such as a deduction theorem for propositional logic, must also preserve consequence for arbitrary assumption sets.

Write $BA=\exists y\mathrm{Prov}(┌A┐,y)$ and fix a refutable first-order sentence $\perp$, so $S⊢\neg \perp$ and ${\mathrm{Con}}_S=\neg B\perp$. First prove the internal equivalenceBecause $\perp \to G$ is provable, the derivability conditions give $B\perp \to BG$. The fixed-point equivalence $G\leftrightarrow \neg BG$ therefore yields $G\to \neg B\perp$.

For the reverse implication, necessitating $G\to \neg BG$ and applying distribution gives $BG\to B(\neg BG)$. positive introspection gives $BG\to B(BG)$. Finally the provable implication $BG\to (\neg BG\to \perp )$, necessitated and distributed, givesConsequently $S⊢BG\to B\perp$, so $\neg B\perp \to \neg BG\to G$. The same argument works with any chosen refutable first-order sentence in place of $\perp$; their formal consistency statements are provably equivalent.

By the classical deduction theorem for propositional logic applied to adjoining a first-order sentence, $S+\{G\}$ is consistent exactly when $S⊬\neg G$. The displayed equivalence makes $S+\{G\}$ and $S+\{{\mathrm{Con}}_S\}$ deductively equivalent. ThereforeNo soundness assumption on that extension is being substituted for consistency.

Assume $S⊢B_{S}X\to X$ and put $T=S+\{\neg X\}$. Then $T⊢\neg B_{S}X$. The given extension-provability implication, with $Y=\perp$, givesThe provable classical implication $(\neg X\to \perp )\to X$, together with distribution, gives $S⊢B_S(\neg X\to \perp )\to B_{S}X$. HenceIf $T$ were consistent, this would violate its Gödel second incompleteness theorem. Thus $T$ is inconsistent. The deduction theorem for propositional logic and double-negation elimination give $S⊢\neg \neg X$, hence $S⊢X$. Therefore the second incompleteness theorem for $S+\{\neg X\}$ yields Löb's theorem for arbitrary $X$.

Use just the assumed local reflection instance with $Y=\neg X$:By the deduction theorem for propositional logic, $S⊢X\to (B_S(\neg X)\to \neg X)$. Classical propositional logic makes this imply the unconditional reflection statement $S⊢B_S(\neg X)\to \neg X$: if $X$ is false the consequent is already true, and if $X$ is true the displayed implication supplies it. Löb's theorem applied to $\neg X$ now givesThus full local reflection in a one-sentence extension is inconsistent; in this argument even the single instance concerning $\neg X$ suffices.

Put $T=S+\{X\}$ and choose its Gödel sentence $Z$, so $T⊢Z\leftrightarrow \neg B_{T}Z$. The assumed reflection scheme gives the particular theoremThe given extension-provability implication is $S⊢B_{T}Z\to B_S(X\to Z)$. The fixed-point equivalence gives $T⊢\neg Z\to B_{T}Z$, so these implications compose toThe supplied propositional tautology $((\neg Z\to (X\to Z))\to (X\to Z))$ gives $T⊢X\to Z$, and $T⊢X$ then yields $T⊢Z$. The first of the derivability conditions for $T$ gives $T⊢B_{T}Z$, while its Gödel equivalence gives $T⊢\neg B_{T}Z$. Hence $T$ is inconsistent. By the deduction theorem for propositional logic,This proof uses diagonalization and proof transfer for the extension, and invokes neither Löb's theorem nor the second incompleteness theorem.

Choose an auxiliary propositional formula $\beta$. The two instances of L1 areThe instance of L2 with $\gamma =\alpha$ isApply modus ponens rule first with the first L1 instance and then with the second. This is an assumption-free logical derivation, soIn particular no semantic completeness theorem or deduction theorem for propositional logic has been assumed to obtain this identity theorem.

For this calculus the deduction theorem for propositional logic isFor the reverse logical implication, retain the logical derivation from $\Gamma$, add the assumption $\alpha$, and use modus ponens rule.

For the forward logical implication, induct on a logical derivation from $\Gamma \cup \{\alpha \}$. For each line $\delta$ we construct a logical derivation of $\alpha \to \delta$ from $\Gamma$. If $\delta =\alpha$, use (ii). If $\delta$ is an axiom instance or belongs to $\Gamma$, it is already derivable from $\Gamma$; L1 gives $\delta \to (\alpha \to \delta )$, and modus ponens rule finishes that case.

If $\delta$ comes from $\eta$ and $\eta \to \delta$ by modus ponens rule, the induction hypothesis suppliesPart (iii) supplies $\Gamma ⊢\alpha \to \delta$.

If $\delta$ comes by the elimination rule E from $\eta \to \delta$ and $\neg \eta \to \delta$, the induction hypothesis suppliesThe L2 instance with $(\alpha ,\beta ,\gamma )=(\alpha ,\eta ,\delta )$ combines these by two applications of modus ponens rule. Thus the rule E also survives the discharge construction. These are all possible lines, proving the theorem for the final line $\beta$.

Suppose both extensions were inconsistent. By the explosion argument in (i), the extension by $\varphi$ proves $\neg \varphi$, and the extension by $\neg \varphi$ proves $\varphi$. The deduction theorem for propositional logic therefore yieldsThe identity theorem gives $⊢\neg \varphi \to \neg \varphi$ and $⊢\varphi \to \varphi$. Apply E to the first displayed logical implication and the identity logical implication with antecedent $\neg \varphi$ to obtain $\Gamma ⊢\neg \varphi$. Apply E to the identity logical implication with antecedent $\varphi$ and the second displayed logical implication to obtain $\Gamma ⊢\varphi$. This contradicts propositional consistency of $\Gamma$.

Consequently at least one of the two one-formula extensions is propositionally consistent. The formal proof uses the source's own calculus, including its rule E, rather than assuming an unproved completeness theorem for this presentation.

There is a three-line Hilbert formal proof. Use A1 with $\alpha =\chi$, $\beta =\psi$; then use A3 with $\alpha =\chi$, $\beta =(\psi \to \chi )$:This is a direct logical derivation in the displayed Hilbert proof system. Neither the deduction theorem for propositional logic nor a completeness theorem for propositional logic is needed: the desired logical implication is just the contrapositive, supplied by A3, of the particular A1 instance on line 1.

For a standard classical propositional calculus, strong completeness statesTogether with soundness, this identifies semantic consequence with formal derivability. One proves the contrapositive by the maximal consistent set in propositional logic construction. If $\Gamma ⊬\varphi$, the set $\Gamma \cup \{\neg \varphi \}$ is propositionally consistent, by the deduction theorem for propositional logic and classical propositional reasoning. Extend it to a maximal consistent set in propositional logic $M$, deciding each logical formula in turn. At each stage at least one selection of $\theta$ or $\neg \theta$ preserves propositional consistency; a contradiction in the union would use only finitely many assumptions and hence already occur at a stage.

Define a Boolean valuation by $v(p_i)=1$ exactly when $p_i\in M$. Maximal consistency in propositional logic gives $\neg \theta \in M$ exactly when $\theta \notin M$, and $(\theta \to \eta )\in M$ exactly when either $\theta \notin M$ or $\eta \in M$. Structural induction on logical formulas therefore proves the maximal consistent set truth lemma $v(\theta )=1⟺\theta \in M$. Thus $v$ satisfies $\Gamma$ but falsifies $\varphi$, contradicting semantic entailment. The countable language here permits an enumeration of logical formulas; the corresponding general-language argument uses a well-ordering or a principle of maximality in a partially ordered set.

The old system does derive the replacement axiom. Here is a syntactic proof using only its axioms, modus ponens rule, and the permitted deduction theorem for propositional logic.

First derive explosion. From $U$ and $\neg U$, the first axiom gives $\neg V\to \neg U$. The old third axiom then gives $U\to V$, and modus ponens rule with $U$ gives any desired $V$.

Next derive the classical reductio rule. Suppose $\Gamma ,\neg B$ derives both $C$ and $\neg C$. Let $T$ be the theorem $B\to B$, obtainable by applying the deduction theorem for propositional logic to the identity derivation from assumption $B$. Explosion under $\Gamma ,\neg B$ gives $\neg T$, so the deduction theorem for propositional logic gives $\Gamma ⊢\neg B\to \neg T$. The old third axiom with $\alpha =T$, $\beta =B$ yields $\Gamma ⊢T\to B$. Since $T$ is a theorem, $\Gamma ⊢B$. Thus a contradiction under $\neg B$ permits deriving $B$ with that temporary assumption discharged.

Now assume $h=\neg \beta \to \alpha$ and $\neg \alpha$, and temporarily also assume $\neg \beta$. Modus ponens rule gives $\alpha$, contradicting $\neg \alpha$. The just-proved reductio rule discharges $\neg \beta$ and gives $\beta$. Finally discharge $\neg \alpha$ and $h$ by the deduction theorem for propositional logic:No propositional completeness theorem is needed in this derivation.

Let $f=\alpha \to (\beta \to \gamma )$ and $h=\alpha \to \beta$. Temporarily assume $f$, $h$, and $\alpha$. Modus ponens rule first gives $\beta \to \gamma$ from $f$ and $\alpha$, then $\beta$ from $h$ and $\alpha$, and finally $\gamma$.

Apply the deduction theorem for propositional logic successively to discharge $\alpha$, then $h$, then $f$. The result isthe required axiom scheme. This derivation uses only assumptions, modus ponens rule, and the added deduction rule; no negation axiom is involved.

Order the consistent sets of sentences extending $\Sigma$ by inclusion. This collection is nonempty. The union of a chain is consistent: any derivation of a contradiction uses finitely many assumptions, which all lie in one member of the chain. Zorn's lemma therefore supplies a maximal member, which is a maximal consistent extension of $\Sigma$.

For a countable language one can instead enumerate all sentences and successively add either a sentence or its negation while preserving consistency. At least one choice is consistent, since inconsistency of both extensions, together with the deduction theorem for propositional logic and classical reasoning, would make the previous stage inconsistent. The union of the stages is consistent by finite use of assumptions and decides every sentence, so it is maximal consistent.

The chain proof covers arbitrary set-sized languages; no restriction on the language cardinality was printed here. The later prohibition on choice applies to the cardinal-arithmetic question, not this logic construction.

Write $E(x,y)$ for the displayed equality predicate. A6 and A4 give $⊢E(x,x)$, establishing a reflexive relation.

An instance of A7, replacing just the first occurrence of $x$ in $E(x,x)$, isAssume $E(x,y)$, apply the modus ponens rule twice using reflexivity, and obtain $E(y,x)$. The deduction theorem for propositional logic discharges the assumption. This proves symmetry.

For transitivity, A7 suppliesby replacing $y$ in the atomic formula $E(x,y)$. From assumptions $E(x,y)$ and $E(y,z)$, two applications of the modus ponens rule give $E(x,z)$. Discharging assumptions and universally generalizing givesThus the predicate defines an equivalence relation within the calculus.

The propositional completeness theorem states that $\Gamma \models \varphi$ if and only if $\Gamma ⊢\varphi$. Soundness follows by checking the axioms against truth valuations and noting that modus ponens rule preserves truth. For completeness, use the deduction theorem for propositional logic: if $\Gamma \cup \{p\}⊢q$, then $\Gamma ⊢p\Rightarrow q$. In the usual negation rules this also says that a contradiction from $\Gamma \cup \{p\}$ proves $\Gamma ⊢\neg p$.

First construct a maximal consistent set extending any consistent set $\Delta$. Enumerate all formulas, possible because the primitive propositions are countable. Starting with ${\Delta }_0=\Delta$, add formula ${\psi }_n$ at step $n$ if consistency is preserved; otherwise add $\neg {\psi }_n$. This latter addition is consistent: if both extensions gave contradictions, the deduction theorem for propositional logic would prove both $\neg {\psi }_n$ and $\neg \neg {\psi }_n$ from ${\Delta }_n$, a contradiction already in ${\Delta }_n$. The union $M$ is consistent because a finite proof uses only finitely many newly added premises. It decides every formula: exactly one of $\psi ,\neg \psi$ belongs to $M$. It is deductively closed, since an omitted derivable formula would have its negation in $M$, contradicting consistency.

Assign a valuation $v(p)=1$ exactly when the primitive proposition $p$ lies in $M$. Structural induction proves the maximal consistent set truth lemma $v(\psi )=1$ if and only if $\psi \in M$. Negation follows from the decision property. For implication, if $\psi \Rightarrow \chi \in M$ and $\psi \in M$, modus ponens rule gives $\chi \in M$. Conversely, if $\chi \in M$, the elementary implication axioms give $\psi \Rightarrow \chi \in M$. If $\psi \notin M$, then $\neg \psi \in M$, and the usual contradiction rule proves $\psi \Rightarrow \chi$. These two alternatives match the truth table. The other connectives, if primitive, are handled by their corresponding rules or defined from negation and implication. Thus every consistent set has a valuation satisfying it.

Now suppose $\Gamma /⊢\varphi$. If $\Gamma \cup \{\neg \varphi \}$ were inconsistent, the deduction theorem for propositional logic would give $\Gamma ⊢\neg \neg \varphi$. Here the third axiom $\neg \neg \varphi \Rightarrow \varphi$ is essential: it would give $\Gamma ⊢\varphi$, a contradiction. Hence that extension is consistent and has a satisfying valuation. This valuation satisfies $\Gamma$ and falsifies $\varphi$, proving the contrapositive of completeness. In this organization of the proof, the explicit classical double-negation elimination occurs in this last consistency step; the construction and truth lemma use the ordinary negation and contradiction rules, not an unmentioned identification of $\neg \neg \varphi$ with $\varphi$.

The propositional compactness theorem says that a set of formulas is satisfiable exactly when each finite subset is satisfiable. If it were not satisfiable, completeness would make it inconsistent. Its finite contradiction proof uses only a finite subset of premises; soundness makes that subset unsatisfiable. This contradicts the assumed finite satisfiability and proves compactness.

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 $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$.