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?
$$\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{\mathcal D}{\Gamma\vdash A\uparrow B}}{\Gamma,\neg(A\uparrow B)\vdash\bot}}{\Gamma,\neg(A\uparrow B),\neg(A\uparrow B)\vdash\bot}}{\Gamma,\neg(A\uparrow B)\vdash A\uparrow B}\qquad\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{}{\Gamma,A\vdash A}}{\Gamma,\neg A,A\vdash \bot}}{\Gamma,\neg A\vdash A\uparrow B}{\uparrow}I_1}{\Gamma,\neg(A\uparrow B),\neg A\vdash\bot}}{\Gamma,\neg(A\uparrow B)\vdash A}\qquad\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{}{\Gamma,B\vdash B}}{\Gamma,\neg B,B\vdash \bot}}{\Gamma,\neg B\vdash A\uparrow B}{\uparrow}I_2}{\Gamma,\neg(A\uparrow B),\neg B\vdash\bot}}{\Gamma,\neg(A\uparrow B)\vdash B}}{\cfrac{\Gamma,\neg(A\uparrow B)\vdash\bot}{\Gamma\vdash A\uparrow B}\text{DNE}}{\uparrow}E$$
I'm using the derivable rule $\cfrac{\Gamma\vdash A}{\Gamma,\neg A\vdash\bot}$. This is probably not the most satisfying thing in the world. First, this wouldn't be doable in an intuitionistic logic. The elimination rule is not strong enough in that case. Next, your rules for $\uparrow$ are not pure, meaning they involve connectives other than $\uparrow$, namely $\bot$. This is a partial explanation of why things other than structural rules are needed. The single conclusion sequents are also not well-adapted to classical logic which is what I assume you are aiming for.
In the context of intuitionistic logic, your second elimination rule is too weak to recover the input of the introduction rules. The direct translation utilizing the elimination rule of disjunction would give $$\cfrac{\Gamma\vdash A\uparrow B\qquad\Gamma,\neg A\vdash C\qquad\Gamma,\neg B\vdash C}{\Gamma\vdash C}$$ (which is also not a pure rule). You are essentially choosing $C=\bot$. This produces the premises $\Gamma,\neg A\vdash\bot$ and $\Gamma,\neg B\vdash\bot$ which you are using proof by contradiction to turn into $\Gamma\vdash A$ and $\Gamma\vdash B$. But intuitionistically, $\Gamma\vdash A$ is stronger than $\Gamma,\neg A\vdash\bot$ which makes your proposed elimination rule weaker. The rule I gave above will work (given the usual intuitionistic rules for $\neg$) since it essentially defines $A\uparrow B$ as an intuitionistic $\neg A\lor\neg B$.
Local soundness and completeness are properties that are sensitive to the structural properties of the logic as a whole. It matters that you are (seemingly) using single conclusion sequents. Consider this set of rules (which are pure): $$\cfrac{\Gamma,A\vdash\Delta}{\Gamma\vdash A\uparrow B,\Delta}\qquad\cfrac{\Gamma,B\vdash\Delta}{\Gamma\vdash A\uparrow B,\Delta}\qquad\cfrac{\Gamma\vdash A\uparrow B,\Delta\qquad\Gamma\vdash A,\Delta\qquad\Gamma\vdash B,\Delta}{\Gamma\vdash\Delta}$$
Local soundness: $$\cfrac{\cfrac{\cfrac{\mathcal D}{\Gamma,A_i\vdash\Delta}}{\Gamma\vdash A_1\uparrow A_2,\Delta}\qquad\cfrac{\mathcal E_1}{\Gamma\vdash A_1,\Delta}\qquad\cfrac{\mathcal E_2}{\Gamma\vdash A_2,\Delta}}{\Gamma\vdash\Delta}\implies\llap{_R}\ \cfrac{\cfrac{\mathcal D}{\Gamma,A_i\vdash\Delta}\qquad\cfrac{\mathcal E_i}{\Gamma\vdash A_i,\Delta}}{\Gamma\vdash\Delta}\text{cut}$$
Local completeness: $$\cfrac{\mathcal D}{\Gamma\vdash A\uparrow B,\Delta}\implies\llap{_E}\ \cfrac{\cfrac{\cfrac{\mathcal D}{\Gamma\vdash A\uparrow B,\Delta}}{\Gamma\vdash A\uparrow B,A\uparrow B,\Delta}\qquad\cfrac{\cfrac{}{\Gamma,A\vdash A,\Delta}}{\Gamma\vdash A,A\uparrow B,\Delta}\qquad\cfrac{\cfrac{}{\Gamma,B\vdash B,\Delta}}{\Gamma\vdash B,A\uparrow B,\Delta}}{\Gamma\vdash A\uparrow B,\Delta}$$
I actually wrote this derivation first and then wrote the one at the top as a "translation" of this using negated hypothesis to stand for extra conclusions.
I would say there are some approaches to producing the appropriate rules. For example, many connectives can be related to inductive types for which the introduction and elimination rules are clearer. The computational interpretation (i.e. Curry-Howard) and categorical semantics also give perspectives that explain what local soundness/completeness means. For example, they are related to $\beta$-reduction and $\eta$-expansion in typed lambda calculi, and are related to the triangle identities of the adjunctions characterizing the semantic analogues of the connectives. However, as I alluded to before, the structural aspects of the logic impact all of these.