Admissibility of Harrop's rule, computationally

It is obvious that the following formula is not a theorem of intuitionistic propositional calculus (IPC).

$$(\neg A \; \to \; B \vee C) \;\; \to \;\; ((\neg A \; \to \; B) \vee (\neg A \; \to \; C))$$

It can be easily understood by considering Heyting semantics. Indeed, if you only have a function that maps any proof of $\neg A$ to either a proof of $B$ or a proof of $C$, you can neither build a function that maps any proof of $\neg A$ to a proof of $B$ nor a function that maps any proof of $\neg A$ to a proof of $C$.

The Harrop's rule below is however admissible in IPC.

$$\displaystyle \frac{ \neg A \; \to \; B \vee C}{ (\neg A \; \to \; B) \vee (\neg A \; \to \; C) }$$

How can it be understood from a computational (Heyting semantics) point of view?

• I'm not sure if this intuition is correct, but I see it as there is at most one proof of $A \to \bot$ since its codomain is empty, so it must be the empty function. So a proof o $\neg A \to B \lor C$ picks out one element of $B$ or one element of $C$. – fhyve Mar 31 '17 at 19:18

Suppose $IPC\vdash \neg A \to B\lor C$. Therefore by BHK interpretation there exists a function $f$ that converts a proof of $\neg A$ into pair $\left < a,b\right >$ where $a$ is 0 and $b$ is a proof of $B$ , or $a$ is 1 and $b$ is a proof of $C$. Therefore a proof of $(\neg A \to B) \vee (\neg A \to C)$ is a pair like

$$\left <a', b' \right >=\begin{cases}\left <0,0 \right >& \forall p\exists u (\vdash_u A \:\land\: \nvdash_{p(u)} \bot) \\ \left <i,\left < C_m \right > \right > & \exists p(\forall u(\vdash_u A \to \: \vdash_{p(u)} \bot)\land f(\left <p \right >)=\left < i, m \right >)\end{cases}$$

Where $\vdash_p \phi$ means $p$ is a proof of $\phi$, $C_m(x)=m$ is a constant function and $\left < p \right >$ is code of function $p$.

Also $\left <a',b' \right >$ is constructively well-defined because weak completeness of $IPC$ with respect to the finite Kripke models can be proved constructively, therefore all we need is checking a finite number of finite Kripke models to find whether $\exists u(\vdash_u \phi)$ or not.

• Your answer looks promising, but I cannot accept it because I do not understand it! Can you elaborate? – Bob Dec 9 '16 at 21:37
• @Bob: Which step is not clear? – Erfan Khaniki Dec 9 '16 at 22:12
• $P$ should be a function that takes as input a proof of $\neg A$ but your $P$ is a pair. I guess the domain of the function $p$ is $A$, but what is its codomain? In the second line of the definition of $P$, the variable $p$ is not binded; did you forget a quantifier or is it supposed to be a free variable? In the latter case, what does it represent? $f$ should take as input a proof of $\neg A$ but you give it the code $\left< p \right>$ of a function $p$. In my understanding of Heyting semantics, you do not need a notion of code because the meaning of a proof is a higner-order function. – Bob Dec 10 '16 at 9:26
• @Bob: when we want to proof something uniformly, we need code of function. As BHK interpretation said, proof of $A\lor B$ is a pair $\left < a,b \right >$ such that $a=0$ and $b$ is a proof of $A$ or $a=1$ and $b$ is a proof of $B$. I edited my post. – Erfan Khaniki Dec 10 '16 at 16:06
• @Bob: You can look at this paper (math.cas.cz/fichier/preprints/IM_20160728200958_81.pdf) which describes a general way of provability interpretation of intuitionistic logics. As a matter of fact, BPC is sound with respect to the primitive recursive realizability, but IPC is not sound with respect to this realizability. Therefore it is important what is the meaning of Heyting semantic. Because different formalizations lead to different intuitionistic logics. – Erfan Khaniki Dec 11 '16 at 14:54

The way I understand it is as follows. The most general formula

$(\neg A \; \to \; B \vee C) \;\; \to \;\; ((\neg A \; \to \; B) \vee (\neg A \; \to \; C))$

is not derivable in IPC, because it is not an intuitionistic truth, like you said.

In fact, we can find almost intuitionistic' Brouwerian counterexamples outside of IPC. For instance if we look at HA + MP and take

$R(n):= 1 \ \mbox{if the first block of 99 consecutive 9's}\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \mbox{in the decimal expansion of$\pi$ends at place$n$}$

$R(n):= 0\ \ \mbox{else}$

$A=\forall n [R(n)=0]$ $\ \ \ B= \exists n [R(2n)=1]$ $\ \ \ C= \exists n [R(2n+1)=1]$

Then we see that $\neg A\to B\vee C$ (using MP). But both $(\neg A \; \to \; B)$ and $(\neg A \; \to \; C)$ are elusive. The interesting thing here is, that if HA really proves $\neg A$, then without MP already HA proves there is $m$ with $R(m)=1$'. This since HA is closed under Markov's Rule, therefore proving $\neg\neg\exists n[P(n)]$ for decidable $P$ in HA allows one to deduce something about the structure of the proof, from which one can find a proof in HA of $\exists n [P(n)]$. This is a proof-theoretical property of the formal system HA.

Similarly, if in IPC we have formulas $A,B,C$ such that IPC proves $(\neg A \; \to \; B \vee C)$, then we know from the proof-theoretical properties of IPC that we can either find a proof in IPC of $(\neg A \; \to \; B)$ or of $(\neg A \; \to \; C)$.

So both computationally and semantically, this Harrop's Rule (also called Independence of Premise Rule, or IPR) being admissible for IPC should be seen as a statement about certain properties of the formal system IPC.

A nice reference is Rosalie Iemhoff's paper On the rules of intermediate logics.

Addendum: It just occurred to me that the question might be asking for an informal semantical/computational explanation why IPC has this property. In that case, consider that in general we cannot extract numerical existence from a negated formula $\neg A$. Therefore, if for a formula $A$ in IPC we deduce that $\neg A$ implies $\exists n\in\{0,1\} [(n=0\to B)\wedge (n=1\to C)]$, then we must have a means to pinpoint this $n$ without having to first prove $\neg A$. And that is precisely Harrop's rule IPR.

This is also why we need Markov's Principle (MP) in the counterexample above: to extract numerical existence from the negated formula $\neg\forall n[R(n)=0]$ which is equivalent to $\neg\neg\exists m [R(m)=1]$