I have been following Frank Pfenning's Notes on natural deduction, and I have a few questions on how to write rules with the local soundness and local completeness properties.
Consider these rules for NAND, which I'll denote by $A \uparrow B$. I'm also assuming the usual structural rules (premise, cut, weakening, contraction, and exchange).
If we consider NAND as $A \uparrow B \equiv \neg (A \wedge B)$, we get rules like
$$\frac{\Gamma,A,B \vdash \bot}{\Gamma \vdash A\mathrel{\uparrow}B}\text{$\mathord{\uparrow}\text{I}$} \qquad \frac{\Gamma \vdash A \uparrow B \quad\; \Gamma \vdash A \quad\; \Gamma \vdash B}{\Gamma \vdash \bot}\text{$\mathord{\uparrow}\text{E}$}$$
The local soundness property (as far as I can tell, given I'm using a slightly different formalisation) is that you can rewrite all introductions followed directly by eliminations (of the same connective) as a series of cuts.
$$ \frac{ \dfrac{\Gamma,A,B \vdash \bot}{\Gamma \vdash A \mathrel{\uparrow} B} \text{$\mathord{\uparrow}\text{I}$} \quad\; \lower{1.4ex}{\Gamma \vdash A} \quad\; \lower{1.4ex}{\Gamma \vdash B} }{\Gamma \vdash \bot}\text{$\mathord{\uparrow}\text{E}$} \quad \Longrightarrow_R \quad \dfrac{ \lower{1.4ex}{\Gamma \vdash B} \quad\; \dfrac{\Gamma \vdash A \quad\; \Gamma,A,B \vdash \bot}{\Gamma,B \vdash\bot}\text{cut} }{\Gamma \vdash \bot}\text{cut} $$
The local completeness property is that, given a proof of the connective, we can eliminate and then reintroduce the connective.
$$ \Gamma \vdash A \mathrel{\uparrow} B \quad \Longrightarrow_E \quad \dfrac{ \dfrac{\Gamma \vdash A \mathrel{\uparrow} B} {\Gamma,A,B \vdash A \mathrel{\uparrow} B}\text{weaken} \quad\; \dfrac{}{\Gamma,A,B \vdash A}\text{prem} \quad\; \dfrac{}{\Gamma,A,B \vdash B}\text{prem} }{ \dfrac{\Gamma,A,B \vdash \bot} {\Gamma \vdash A \mathrel{\uparrow} B}\text{$\mathord{\uparrow}$I} }\text{$\mathord{\uparrow}$E} $$
On the other hand, if we consider $A \uparrow B \equiv \neg A \vee \neg B$, we get rules something like
$$\frac{\Gamma,A \vdash \bot}{\Gamma \vdash A\mathrel{\uparrow}B}\text{$\mathord{\uparrow}\text{I}_1$} \qquad \frac{\Gamma,B \vdash \bot}{\Gamma \vdash A\mathrel{\uparrow}B}\text{$\mathord{\uparrow}\text{I}_2$} \qquad \frac{\Gamma \vdash A \uparrow B \quad\; \Gamma \vdash A \quad\; \Gamma \vdash B}{\Gamma \vdash \bot}\text{$\mathord{\uparrow}\text{E (?)}$}$$
I believe this captures most of what it means to be NAND. The local soundness properties are easy to show; however, I can't derive the local completeness properties, and suspect that the elimination rule is not enough.
My questions:
- Is my understanding correct?
- Does the second system (as is) have local completeness, and if not, what qualities does the elimination rule lack?
- If it doesn't have local completeness, is there a way of expanding/rewriting the elimination rule(s) to get local completeness?
- Is there a systematic way to get locally sound & complete elimination rules just knowing the introduction rules, and vice versa?