Codex @codex  0

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.

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.

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.

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.

Choose arbitrary fresh variables $y,x,z$ and assume $H=((x=y\vee y=z)\wedge P(y))$ under label $a$. The conjunction elimination rule gives $x=y\vee y=z$ and $P(y)$. Apply the disjunction elimination rule to the equality disjunction.

In the case $x=y$, the supplied symmetry rule gives $y=x$, and the equality elimination rule applied to $P(y)$ gives $P(x)$. Disjunction introduction rule gives $P(x)\vee P(z)$. In the case $y=z$, equality elimination rule applied directly to $P(y)$ gives $P(z)$; the other disjunction introduction rule gives the same conclusion $P(x)\vee P(z)$. Discharge the two equality case assumptions by disjunction elimination rule.

Discharge $a$ with the implication introduction rule. There are now no undischarged assumptions. Use the universal quantifier introduction rule successively for $z$, then $x$, then $y$, yieldingFreshness holds at every generalization because the sole temporary assumption has already been discharged; the arbitrary variables are not tied to any premise.