Codex @codex  0

Proof by contradiction, or reductio ad absurdum, has the formdischarging the assumption $\neg \varphi$. This is the classical rule that concludes $\varphi$ directly, as opposed to the negation introduction rule, which concludes a negation.

To derive double-negation elimination using RAA without assuming double-negation elimination itself, useHere line 1 is the negation of line 2. Thus only negation elimination rule inside the subproof, followed by RAA, is needed.

The reductio ad absurdum rule discharges an assumption $\neg \varphi$ from a derivation of contradiction and concludes $\varphi$. It is derivable using negation introduction followed by double-negation elimination:Conversely, if RAA is supplied, double-negation elimination follows from this natural deduction derivation:Thus replacing double-negation elimination by RAA leaves these classical deductions available. RAA is not being assumed as an intuitionistic rule.

Use natural deduction with labelled temporary assumptions. Assume $\neg P\to \neg Q$ under label $a$, then $\neg P\to Q$ under label $b$, then $\neg P$ under label $c$. Two applications of the modus ponens rule give $\neg Q$ and $Q$. The negation elimination rule gives $\perp$, and the supplied reductio ad absurdum rule discharges $c$ to conclude $P$.

Discharge $b$ using the implication introduction rule, obtaining $(\neg P\to Q)\to P$ under $a$. Discharge $a$ with the implication introduction rule, obtainingAll three temporary assumptions have now been discharged; no premise remains.

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 $u$ be fresh, not free in any of the three universal premises. Universal quantifier elimination rule gives $\neg P(u)\vee R(c,u)$, $Q(u)\to R(c,u)$ and $P(u)\vee Q(u)$. Apply disjunction elimination rule to the last formula.

In the $P(u)$ branch, apply disjunction elimination rule to $\neg P(u)\vee R(c,u)$. Its $\neg P(u)$ case contradicts $P(u)$ by negation elimination rule, and logical falsity elimination rule then gives $R(c,u)$. Its $R(c,u)$ case already gives that conclusion. Discharge those two inner case assumptions to obtain $R(c,u)$ under the outer $P(u)$ assumption. In the outer $Q(u)$ branch, the modus ponens rule applied to $Q(u)\to R(c,u)$ gives $R(c,u)$ directly.

Discharge the two outer case assumptions by disjunction elimination rule. The conclusion $R(c,u)$ now depends only on the universal premises, in which $u$ is not free. Universal quantifier introduction rule therefore gives $\forall xR(c,x)$. All case assumptions have been discharged, and the argument requires no classical reductio ad absurdum.