1
$\begingroup$

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:

  1. Is my understanding correct?
  2. Does the second system (as is) have local completeness, and if not, what qualities does the elimination rule lack?
  3. If it doesn't have local completeness, is there a way of expanding/rewriting the elimination rule(s) to get local completeness?
  4. Is there a systematic way to get locally sound & complete elimination rules just knowing the introduction rules, and vice versa?
$\endgroup$
1
$\begingroup$

$$\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.

$\endgroup$
  • $\begingroup$ Lovely answer.Yes, I was being cheeky using $\bot$ instead of introducing an arbitrary proposition. $\endgroup$ – V. Jackson Jun 8 '18 at 5:01
  • $\begingroup$ (edit timed out on me :/) To continue, I should have also mentioned I also include the usual rules for $\bot$E. I'm not really assuming any desired logic, more adding rules, and seeing what logic I get. I was looking for a pure elimination rule for the second system, but it's interesting that it seems to be impossible without resorting to multiple conclusions. Do you know of any more in depth resources/papers on what is possible under different structural properties? $\endgroup$ – V. Jackson Jun 8 '18 at 5:09
  • $\begingroup$ Are you quite sure your single conclusion elimination rule satisfies the local soundness property? I don't think you can get $\Gamma \vdash C$ from only proofs $\Gamma, \neg A \vdash C$ and $\Gamma, \neg B \vdash C$ without multiple conclusions. $\endgroup$ – V. Jackson Jun 8 '18 at 5:28
  • 1
    $\begingroup$ You also have a derivation ending in $\Gamma,A\vdash\bot$ (or $B$). You derive $\Gamma\vdash\neg A$ via $\neg I$ and then use Cut. I don't know a resource that directly targets what you want. Negri's and von Plato's "Structural Proof Theory" goes into proof theoretic sensibilities, i.e. why harmony is good. There's a large literature the computational and categorical perspectives. Sørensen's and Urzyczyn's "Lectures on the Curry-Howard Isomorphism" and Jacob's "Categorical Logic and Type Theory" are decent resources for each of those respectively. Linear logic is another useful perspective. $\endgroup$ – Derek Elkins Jun 8 '18 at 6:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.