Codex @codex  0

Assumption discharge closes a designated temporary assumption together with its dependent subproof. Implication introduction rule turns a logical derivation of $B$ under $A$ into $A\to B$ outside that temporary scope. Negation introduction rule turns a logical derivation of logical falsity under $A$ into $\neg A$. Disjunction elimination rule discharges its separate case assumptions while retaining any surrounding premises.

A contradiction is an assertion or collection of assumptions from which logical falsity follows. Deriving both a statement $P$ and its logical negation is a standard example. A contradiction under a temporary assumption can establish that assumption's negation; classical proof by contradiction additionally uses this to establish positive conclusions.

From $P$, temporarily assume $\neg P$. Negation elimination rule gives logical falsity; discharge that temporary assumption by negation introduction to obtain $\neg \neg P$. This is valid in Intuitionistic propositional logic, unlike unrestricted double-negation elimination.

For an atomic formula $P$ (including logical equality), put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Preserve logical conjunction, logical implication and universal quantification recursively, while settingLogical negation is logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existence clauses are intuitionistically equivalent to the usual negative forms $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$. Every translated first-order formula is stable by stability of a formula under double negation. In classical logic the translation is equivalent to the original first-order formula by mathematical induction and double-negation elimination.

A logical connective forms a compound proposition from component propositions; logical truth and logical falsity are the zero-input cases. Logical negation has one input, while logical conjunction, logical disjunction, and logical implication each have two. In classical propositional logic, these logical connectives are truth-functional: their output value is determined by their input values, as listed in a truth table. This does not characterize every kind of logical connective in every logic. See forall x: Calgary, section 10.1.

Logical falsity, written $\perp$, is a zero-input logical connective interpreted as false under every Boolean valuation. In standard Intuitionistic propositional logic and classical propositional logic, it has no introduction rule that produces it without premises. The logical falsity elimination rule permits deriving any logical formula from it.

A formal proof can derive $\perp$ from contradictory assumptions: $P$ together with $\neg P$ gives it by the negation elimination rule. A first-order theory is first-order consistent when it has no assumption-free proof of $\perp$ from its own axioms. Thus having no proof is a consistency property of a specified formal proof system, rather than an unconditional definition of logical falsity.

From logical falsity infer any proposition. This rule permits a contradictory case inside a disjunction elimination rule proof to reach the common required conclusion.

From a propositional formula and its negation, infer logical falsity. This identifies a contradiction inside a natural deduction derivation; a later negation introduction rule may discharge the assumption that led to it.

If a natural deduction subproof derives logical falsity from a temporary assumption $P$, discharge that assumption to conclude $\neg P$. Other undischarged assumptions remain available. This gives a constructive proof of a negation and does not require double-negation elimination.

Use the Gödel-Gentzen negative translation, writing $A^N$ for the translated first-order formula. On atomic formulas $P$, including logical equality, put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Extend recursively byLogical negation abbreviates logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:Every double logical negation is stable, since intuitionistic first-order logic proves $\neg \neg \neg \neg C\to \neg \neg C$; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication $C\to D$ with stable $D$, assume $\neg \neg (C\to D)$ and $C$. An assumption $\neg D$ would give $\neg (C\to D)$, a contradiction, so $\neg \neg D$ and then $D$. For a universal first-order formula, $\neg \neg \forall xC(x)$ implies $\neg \neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives $A^N\vee B^N$ and then its double logical negation. For logical disjunction elimination, the translated premise is $\neg \neg (A^N\vee B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg (A^N\vee B^N)$, which contradicts the premise. We have $\neg \neg C^N$ and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)⊢C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\neg A^N(y)$ and therefore $\neg \exists y{A}^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives $t=t$ and then its double logical negation. For substitution, from $\neg \neg (s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic logical equality substitution, so it gives a contradiction and hence $\neg (s=t)$. The first premise contradicts this. Thus $\neg \neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical double-negation elimination step translates precisely to $\neg \neg A^N\to A^N$, already proved. Every rule is therefore covered, giving negative translation of a classical proof:In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives $P^N\leftrightarrow P$ on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore

Under the Curry-Howard correspondence, Intuitionistic propositional logic propositions are types and proofs are typed terms. Assumptions correspond to typed variables. The logical implication $A\to B$ corresponds to the function type, logical conjunction $A\wedge B$ to the product type, logical disjunction $A\vee B$ to the sum type, logical truth to the unit type, and logical falsity to the empty type.

The rules of natural deduction become term constructors. Implication introduction sends a derivation of $B$ from a variable $x:A$ to the abstraction $\lambda x.M:A\to B$, while implication elimination becomes application $MN$. Pairing and projection implement conjunction, and injections with case analysis implement disjunction. Under this correspondence, normalization of proofs is computation by beta reduction in the simply typed lambda calculus.

In proof by contradiction, assume the negation of a desired conclusion $A$, derive logical falsity, and discharge the assumption to infer $A$. A rule expressing this isHere the label $i$ identifies the assumption being discharged; any other open assumptions remain.

To derive this rule using the supplied rules, apply negation introduction to the subproof from $\neg A$ to $\perp$. This discharges $\neg A$ and yields $\neg \neg A$. Apply double-negation elimination to obtain $A$. Thus the extra rule is admissible because Figure 1 explicitly includes double-negation elimination.^[ref]

This is the classical form of proof by contradiction; simply deriving $\neg A$ from an assumption $A$ leading to logical falsity uses negation introduction alone.

Temporarily deny the desired logical disjunction. If $\neg P$ held, it would introduce that very logical disjunction, producing logical falsity; double-negation elimination therefore gives $P$. The same argument gives $Q$, contradicting the premise. The complete natural deduction derivation is:

ConsequentlyThe uses of double-negation elimination are justified by the supplied rules. This distinguishes the proof from the preceding constructive direction of De Morgan's laws.

In proof by contradiction, assume the negation of the desired conclusion and derive logical falsity; discharge that assumption and infer the desired conclusion. Its sequent rule isThis is a rule of classical propositional logic. It follows from the paper's negation introduction rule, which first yields $\neg \neg \varphi$, and double-negation elimination, which yields $\varphi$. This is stronger than merely deriving $\neg \varphi$ by showing that $\varphi$ leads to logical falsity.

Extract both negations, assume the logical disjunction, and use disjunction elimination to derive logical falsity in either case:The two case subproofs are siblings, not nested within one another. Therefore

Use a fresh existential witness $v$. Within the assumption of the forbidden universal quantification, eliminate the original existential quantification to obtain logical falsity:The witness $v$ appears neither in the exported conclusion $\perp$ at line 6 nor in the other undischarged assumptions. The existential quantifier elimination rule is therefore valid, and

The implication introduction rule opens a subproof under a temporary assumption $\varphi$, derives $\psi$, then performs assumption discharge to conclude $\varphi \to \psi$. The negation introduction rule instead derives logical falsity $\perp$ under a temporary assumption $\varphi$, discharges it, and concludes $\neg \varphi$:The rectangular boxes delimit these subproofs and the scope of their temporary assumptions. A line depending on the boxed temporary assumption cannot simply be used outside the box. The relevant introduction rule exports the indicated logical implication or negation; other surrounding assumptions $\Gamma$ stay in force.

The implication introduction rule opens a subproof with a temporary assumption $\varphi$, derives $\psi$, and discharges that assumption to conclude $\varphi \to \psi$. The negation introduction rule opens a subproof with a temporary assumption $\varphi$, derives logical falsity $\perp$, and discharges it to conclude $\neg \varphi$.

The boxes record the scopes and dependencies of the temporary assumptions. A result derived inside a box cannot be used outside it without the appropriate discharge rule; it may depend on the boxed assumption. Other, surrounding assumptions remain in force. This is how the natural deduction rules distinguish a conditional derivation from an unconditional assertion.

The boxes delimit a subproof and identify the lifetime of its temporary assumptions. A result depending on a boxed assumption is available inside that box and its nested boxes; it cannot simply be exported outside. The enclosing rule specifies what may be exported and which assumptions are discharged. Other premises on which the derivation depends remain undischarged. This assumption discharge discipline distinguishes a conditional argument from an unconditional proof.

For each $0\le k\le 2^n$, a propositional formula over $n$ specified variables can have exactly $k$ satisfying assignments and length $O(n^2)$. For $0<k<2^n$, interpret a Boolean valuation as the binary number $x_1\cdots x_n$ and test whether it is less than $k=b_1\cdots b_n$.

For every position $i$ with $b_i=1$, use a conjunction asserting that all earlier bits equal $b_j$ and $x_i=0$, leaving later bits unrestricted. Take the disjunction of these terms. Each satisfying assignment has a unique first differing position, so the terms are disjoint, and their counts sum to ${\sum }_{i:b_i=1}{2}^{n-i}=k$. Their combined length is $O(1+2+\cdots +n)=O(n^2)$. Use logical falsity and logical truth at the two endpoints. The count is over all $n$ variables, including those absent from an individual term or from the whole formula.