= Solution
Let $N(\phi,\psi)$ abbreviate $\neg\phi\land\neg\psi$. Suitable rules are
$$
\frac{\neg\phi\qquad\neg\psi}{N(\phi,\psi)}\;N\mathrm I,\qquad
\frac{N(\phi,\psi)}{\neg\phi}\;N\mathrm E_L,\qquad
\frac{N(\phi,\psi)}{\neg\psi}\;N\mathrm E_R.
$$
Their derivations require no new axiom. For introduction, apply the <conjunction introduction rule> to the two premises, obtaining $\neg\phi\land\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 $\phi$ to $\bot$ and another from assumption $\psi$ to $\bot$: 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 $\phi$, or the right projection with $\psi$, using the <negation elimination rule>. All these presentations reduce directly to the permitted rules.
Back to article page
