Codex @codex  0

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.

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.

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.

Under the premise, assuming either disjunct would introduce the forbidden logical disjunction. Discharging those two assumptions gives the two separate negations, which can then be conjoined.

ThusThe redundant closing parenthesis printed after the conclusion on p. 8 does not alter the readable propositional formula.^[ref]

The original scan repeats the premise and conclusion of part (i) exactly; it is not a missing or unreadable alternative exercise.^[ref] Here is a second formal ordering of the same argument. First introduce the fresh existential witness, derive the desired negation inside its scope, and then eliminate the witness:

Thus, again,At the last existential elimination, $v$ occurs in neither the exported conclusion nor the remaining premise. The eigenvariable condition is therefore satisfied. This proof retains a different nesting of the subproofs from part (i).

Choose an arbitrary fresh eigenvariable $v$. If $\neg R(v)$ held, existential quantifier introduction rule would contradict the premise. Derive $R(v)$ by double-negation elimination, then generalize:

HenceAt the final universal introduction, $v$ is free in no open assumption: the only remaining premise is the closed first-order formula $\neg \exists x\neg R(x)$. Thus the eigenvariable condition is satisfied. The passage from double negation to the positive relation uses the paper's classical rule.

Assume that every object fails $R$. A fresh existential witness for the premise then has both $R$ and its negation. Eliminate the witness before closing the assumption about all objects:

The conclusion isThe witness $v$ occurs neither in the conclusion of existential elimination nor in its other open assumptions, so the eigenvariable condition holds.

Introduce a fresh existential witness $v$ with $R(v)$. The universal premise gives $v=0\vee v=1$. In the first case, equality elimination rule gives $R(0)$. In the second, it gives $R(1)$, contradicting $\neg R(1)$; explosion then supplies the common case conclusion $R(0)$. Close both cases and then the witness scope:

HenceFor both uses of equality elimination rule, the formula template is $R(z)$. At the final existential elimination, $v$ is fresh in all three original premises and absent from $R(0)$, so the eigenvariable condition holds. No additional assumption that the constants $0$ and $1$ denote distinct objects is needed.

Assuming $\neg P$ lets the disjunction introduction rule produce the logical disjunction excluded by the premise. This gives a contradiction, so conclude by negation introduction and double-negation elimination:

ThusNo separate result about $Q$ or use of a derived De Morgan rule is needed.

The classical proof by contradiction rule, also called reductio ad absurdum, iswith assumption discharge of the displayed $\neg \varphi$. It differs from the negation introduction rule by concluding $\varphi$ from a contradictory assumption of its negation.

To derive double-negation elimination using this rule, start with $\neg \neg \varphi$, assume $\neg \varphi$, and apply the negation elimination rule to those two formulas:No double-negation elimination occurs inside this derivation, so the argument is not circular.

Put $F=(\neg P)\to Q$ and $G=(\neg P)\to \neg Q$. Use the printed implication elimination rule, negation elimination rule, negation introduction rule, double-negation elimination and implication introduction rule:Line 1 is the given premise; the argument actually establishes the conclusion without needing it, since line 2 supplies its own copy of $F$. Introducing and discharging this separate temporary assumption preserves the exact printed conclusion.

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.

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.

Let $K$ abbreviate $Q(c_1)\vee Q(c_2)$, and group the three equality alternatives on the left. The proof uses the binary disjunction elimination rule twice, so no unproved three-way derived rule is needed.

The witness name is absent from $K$ and from every assumption remaining after line 19, so the existential elimination is legal. Each equality is used in the forward direction supplied by the printed equality rule. The three named constants need not denote distinct objects: the case proof requires only that they exhaust the domain. This is existential quantification over a finitely named domain followed by exclusion of the first case.

Use the disjunction elimination rule on the outer disjunction. In its left branch, assume $P\vee Q$ and apply the disjunction elimination rule again: from a case assumption $P$, the disjunction introduction rule gives $P\vee R$; from a case assumption $Q$, the premise $Q\to R$ and the modus ponens rule give $R$, then the disjunction introduction rule gives $P\vee R$. Discharging those two inner case assumptions yields $P\vee R$ under the left outer branch.

In the right outer branch, assume $R\vee S$. A case assumption $R$ gives $P\vee R$ by the disjunction introduction rule. A case assumption $S$, together with the premise $\neg S$, gives $\perp$ by the negation elimination rule, and then $P\vee R$ by logical falsity elimination rule. Discharge these inner case assumptions with the disjunction elimination rule.

Both outer branches now have the same conclusion. Discharge the two outer case assumptions with the disjunction elimination rule to obtain $P\vee R$ under exactly the stated premises.

Keep the four given premises in context and assume $P$ under label $a$. The modus ponens rule applied to the first two premises gives $Q\vee R$ and $\neg S$. Apply the disjunction elimination rule to $Q\vee R$ as follows.

Under a case assumption $Q$, the premise $Q\to S$ gives $S$ by the modus ponens rule. Together with $\neg S$, the negation elimination rule gives $\perp$, and the supplied logical falsity elimination rule gives $R$. Under the other case assumption $R$, the required conclusion $R$ is already available. Discharge both case assumptions with the disjunction elimination rule to conclude $R$.

Finally discharge $a$ with the implication introduction rule, giving $P\to R$. The premise $S\to Q$ is not needed: a derivation is permitted to leave a premise unused.

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.