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.

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.

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.

Derive each negated component in its own subproof, then combine them. Assumption lines below begin local scopes; the listed discharge ranges close those scopes.

Only the original premise remains open. No classical principle is needed for this direction of De Morgan's laws.

Assume the conjunction and obtain a contradiction in each of the two cases supplied by the premise:

The two case assumptions disappear at line 9, while the conjunction assumption remains available until line 10. The proof uses only the primitive rules printed in the paper.

The supplied double-negation elimination rule provides the classical step needed to recover each positive component:

Both local negated assumptions have been discharged. The proof establishes the positive conjunction without assuming an unproved derived version of De Morgan's laws.

Write $H$ for $(\varphi \to \psi )\to \varphi$. The following derives Peirce's law directly from the printed primitive rules, including double-negation elimination:

Every assumption is discharged, so the last formula is a theorem. In particular, no unproved appeal to the derived RAA rule is hidden in the argument.

Write $D(\varphi ,\psi )=\neg (\neg \varphi \wedge \neg \psi )$. We derive the two disjunction introduction rules and the disjunction elimination rule without using any disjunction rule inside the derivations.

For left introduction, start with $\varphi$ and temporarily assume $\neg \varphi \wedge \neg \psi$. The conjunction elimination rule gives $\neg \varphi$, and the negation elimination rule gives $\perp$. Discharge the temporary conjunction by the negation introduction rule, concluding $D(\varphi ,\psi )$. For right introduction, start with $\psi$ and use the right conjunction elimination rule to obtain $\neg \psi$ instead. Thus either input derives the required encoded disjunction.

For elimination, suppose $D(\varphi ,\psi )$ is available, together with a derivation of $\kappa$ from an additional assumption $\varphi$ and a derivation of $\kappa$ from an additional assumption $\psi$. Keep their common external context fixed. Temporarily assume $\neg \kappa$ under label $a$. Temporarily assume $\varphi$ under label $b$ and insert the supplied first branch derivation to obtain $\kappa$. Negation elimination rule gives $\perp$, so negation introduction rule discharges $b$ and gives $\neg \varphi$. Repeat with a temporary assumption $\psi$ under label $c$ and the supplied second branch derivation, discharging $c$ to obtain $\neg \psi$.

Conjunction introduction rule now gives $\neg \varphi \wedge \neg \psi$. Its negation $D(\varphi ,\psi )$ gives $\perp$ by negation elimination rule. The supplied reductio ad absurdum rule discharges $a$ and yields $\kappa$. This discharges the two branch assumptions as required and proves the encoded elimination rule. Its last step uses classical propositional logic; the same encoded elimination principle is not generally available in Intuitionistic propositional logic.

Let $N(\varphi ,\psi )$ abbreviate $\neg \varphi \wedge \neg \psi$. Suitable rules areTheir derivations require no new axiom. For introduction, apply the conjunction introduction rule to the two premises, obtaining $\neg \varphi \wedge \neg \psi$, which is exactly the abbreviation. For left and right elimination, unfold the abbreviation and apply the corresponding conjunction elimination rule. These are therefore derived rules for the NOR connective.

An equivalent subproof presentation of introduction permits one subproof from assumption $\varphi$ to $\perp$ and another from assumption $\psi$ to $\perp$: use the negation introduction rule to discharge each assumption, then apply the conjunction introduction rule. If elimination is desired in contradiction form, combine the left projection with $\varphi$, or the right projection with $\psi$, using the negation elimination rule. All these presentations reduce directly to the permitted rules.

Temporarily assume $Q(c)$ under label $a$. The implication premise and the modus ponens rule yield $\forall x(P(x)\leftrightarrow P(c))$. Instantiate it at $c^{\prime }$ using the universal quantifier elimination rule, obtaining $P(c^{\prime })\leftrightarrow P(c)$. Its right biconditional elimination rule gives $P(c)\to P(c^{\prime })$.

Apply the modus ponens rule with the premise $P(c)$ to obtain $P(c^{\prime })$. Together with $\neg P(c^{\prime })$, negation elimination rule gives $\perp$. Discharge $a$ using the negation introduction rule to conclude $\neg Q(c)$. Nothing assumes that the two constant symbols denote different objects; if they denoted the same object, the stated premises would themselves already be inconsistent.

Keep the premise $P\to Q$ open. Assume $Q\to \neg P$, then temporarily assume $P$. Two applications of the implication elimination rule produce $Q$ and then $\neg P$, contradicting the temporary $P$. Discharge $P$ using the negation introduction rule, then discharge $Q\to \neg P$ using the implication introduction rule.This natural deduction proof uses only the supplied introduction and elimination rules. Line 6 is an application of the negation elimination rule; no classical contradiction principle is needed.