Simplifying a categorical proof of constructive dilemma

Question

In axiomatic propositional calculus the following axiom schema captures constructive dilemma: $\newcommand{\lif}{\supset} \renewcommand{\land}{\&}$

\begin{equation} (a \lif c) \lif ((b \lif c) \lif ((a \lor b) \lif c)) \tag{1} \end{equation}

In a bicartesian closed category representing a logic, disjunctions are coproducts, and this simple form of the constructive dilemma is captured by the coproduct arrow, such that given arrows $f\colon A \to C$ and $g\colon B \to C$, there is a unique arrow $[f,g]\colon A \lor B \to C$. Now, since $(1)$ is a theorem of the propositional calculus, we expect there to be an arrow of the following form in the bicartesian closed category:

\begin{equation} \top \to (a \lif c) \lif ((b \lif c) \lif ((a \lor b) \lif c)) \tag{2} \end{equation}

I've got a derivation of this arrow, but it seems much more complicated than it needs to be. In fact, of all the axioms in one of the axiom systems shown on Wikipedia, this is the most complicated to derive an arrow for. I'm wondering if this can be simplified in some way that I'm missing. Here's the derivation that I've got. We start with:

$$ A \land ((A \lif C) \land (B\lif C)) \xrightarrow{\langle{\pi\pi',\pi\rangle}} (A\lif C)\land A \xrightarrow{\mathrm{eval}} C $$

Currying this, we get

$$ A \xrightarrow{\lambda(\mathrm{eval}\langle{\pi\pi',\pi\rangle})} ((A \lif C) \land (B\lif C)) \lif C \tag{3} $$

Similarly for $B$:

$$ B \land ((A \lif C) \land (B\lif C)) \xrightarrow{\langle{\pi'\pi',\pi\rangle}} (B \lif C)\land B \xrightarrow{\mathrm{eval}} C $$

Currying this, we get

$$ B \xrightarrow{\lambda(\mathrm{eval}\langle{\pi'\pi',\pi\rangle})} ((A \lif C) \land (B\lif C)) \lif C \tag{4} $$

With $(3)$ and $(4)$ we can get a coproduct arrow:

$$ A \lor B \xrightarrow{[(3),(4)]} ((A \lif C) \land (B\lif C)) \lif C \tag{5} $$

To bring $\top$ into the picture, we can compose $(5)$ with a projection:

$$ \top \land (A \lor B) \xrightarrow{(5)\pi'} ((A \lif C) \land (B\lif C)) \lif C \tag{6} $$

Now, since this is a (bi)cartesian closed category, we can uncurry $(6)$ to get:

$$ (\top \land (A \lor B)) \land ((A \lif C) \land (B\lif C)) \xrightarrow{\lambda^{-1}((5)\pi')} C \tag{7} $$

Now, products are commutative, so it's not hard to get

\begin{multline} ((\top \land (A \lif C)) \land (B\lif C)) \land (A \lor B) \to \\ (\top \land (A \lor B)) \land ((A \lif C) \land (B\lif C)) \tag{8} \end{multline}

which through composition gives us:

$$ ((\top \land (A \lif C)) \land (B\lif C)) \land (A \lor B) \xrightarrow{(\lambda^{-1}((5)\pi'))(8)} C \tag{9} $$

We can curry $(9)$ three times to get the desired theorem arrow:

\begin{equation} \top \xrightarrow{\lambda\lambda\lambda(9)} (a \lif c) \lif ((b \lif c) \lif ((a \lor b) \lif c)) \tag{10} \end{equation}

Phew! This all seems rather convoluted, given how trivial some of the theorem arrows are to derive. E.g., the projects and injections are trivial:

\begin{gather*} \lambda\pi\colon \top \to (p \land q) \lif p \qquad \lambda\pi'\colon \top \to (p \land q) \lif q \\ \lambda\iota\colon \top \to p \lif (p \lor q) \qquad \lambda\iota'\colon \top \to q \lif (p \lor q) \end{gather*}

Some of the arrows for the other connectives are a bit trickier, but this one is by far the most complicated, and I wonder if I've missed some easier way to do this. Is there some more canonical, simpler way?

This is a pretty simple proof in natural deduction systems, along the lines of:

• 1. Assume $a \lif c$.
  • 2. Assume $b \lif c$.
    • 3. Assume $a \lor b$.
    • 4. $c$ by $\lor$-elimination with 1, 2, 3.
    • 5. $(a\lor b) \lif c$ by $\lif$-introduction 3–4.
  • 6. $(b\lif c) \lif ((a \lor b) \lif c)$ by $\lif$ introduction 2–5.
• 7. $(a\lif c) \lif ((b\lif c) \lif ((a \lor b) \lif c))$ by $\lif$ introduction 1–6.

The difficulty in the categorical treatment seems that there's no way to do $\lor$-elimination (i.e., to construct a coproduct arrow) in a context where there are other assumptions. So the arrow derivation I've given above actually makes the $\lor$-elimination one of the last steps, analogous to:

• Assume $a$
  • Assume $a \lif c$
    • Assume $b \lif c$
      • $c$ by modus ponens
• $\vdots$
• $a \lif ((a \lif c) \lif ((b \lif c) \lif c))$ by …
• $\vdots$ (similarly for $b$)
• $b \lif ((a \lif c) \lif ((b \lif c) \lif c))$ by …
• Assume $a \lor b$
  • $((a \lif c) \lif ((b \lif c) \lif c))$ by $\lor$-elimination
• $(a \lor b) \lif ((a \lif c) \lif ((b \lif c) \lif c))$ yb $\lif$-introduction
• $\vdots$ rearranging antecedents
• $(a \lif c) \lif ((b \lif c) \lif ((a \lor b) \lif c))$

Answer 1

$\newcommand{\lif}{\supset} \renewcommand{\land}{\&}$After chugging away on this for a while, I do think that the difficulty comes in keeping any “in-scope assumptions” available in each of the cases. The proof I outlined in the question does this by making the codomain of the coproduct arrow an exponential. That is, in trying to show $C$ from the assumptions $A \lor B$, $A \lif C$, and $B \lif C$, I ended up deriving arrows of the form

\begin{gather} f\colon A \to ((A \lif C) \land (B \lif C)) \lif C \\ g\colon B \to ((A \lif C) \land (B \lif C)) \lif C \end{gather}

in order to get a coproduct arrow

$$ [f,g]\colon A \lor B \to ((A \lif C) \land (B \lif C)) \lif C $$

It seems like the an (the?) alternative to this is to embed the assumptions in each of the alternatives. That is, getting $f$ and $g$ like:

\begin{gather} f\colon A \land (A \lif C) \land (B \lif C) \to C \\ g\colon B \land (A \lif C) \land (B \lif C) \to C \\ \end{gather}

to get a coproduct arrow:

$$ [f,g]\colon (A \land (A \lif C) \land (B \lif C)) \lor (B \land (A \lif C) \land (B \lif C)) \to C $$

The disjunction has much more complicated disjuncts, but it's not all that hard to derive the arrow that distributes conjunction over disjunction. (In fact, I asked a question about this about a year ago, probably when working on a similar problem, distribution of categorical product (conjunction) over coproduct (disjunction).)

\begin{multline} \top \land (A \lif C) \land (B \lif C) \land (A \lor B) \to \\ (A \land (A \lif C) \land (B \lif C)) \lor (B \land (A \lif C) \land (B \lif C)) \tag{11} \end{multline}

and with composition we get:

$$\top \land (A \lif C) \land (B \lif C) \land (A \lor B) \to C$$

Currying twice, we get

$$\top \to (A \lif C) \lif ((B \lif C) \lif ((A\lor B) \lif C))$$

I'm not sure whether this is simpler or not, especially since it does some hand waving with regard to $(11)$. It does avoid the need for "uncurrying" from the most interesting parts of the proof, which I find appealing, though there's still one case of it in the justification of $(11)$.

Answer 2

You can prove it in Sequent Calculus as described in the pdf mentioned in the comments (http://zll22.user.srcf.net/talks/2011-12-01-CategoricalLogic.pdf )

1  A                     |- A                               Identity
2  B                     |- B                               Identity
3  C                     |- C                               Identity
4  A, A -> C             |- C                               1,3 Modus ponens
5  B, B -> C             |- C                               2,3 Modus ponens
6  A v B, A -> C, B -> C |- C                               4,5 Disjunction elimination
7  A -> C, B -> C, A v B |- C                               6 reshuffeling antecedents
8  A -> C, B -> C,       |- (A v B) -> C                    7 Conditional proof
9  A -> C                |- (B->C)->((A v B) -> C)          8 Conditional proof
10                       |- (A->C)->((B->C)->((A v B)->C))  9 Conditional Proof 

So if you can replace every line with its categorical equivalent you are done :)

(Ps line 3 is used twice, and i do take some liberties with the structural rules , but these rules aren't mentioned in the pdf)

Good luck

ADDED later:

I made a maybe a better proof:

1  A                     |- A                               Identity
2  B                     |- B                               Identity
3  C                     |- C                               Identity
4  A, A -> C             |- C                               1,3 Modus ponens
5  A                     |- (A -> C) -> C                   4  Conditional proof
6  A, B -> C             |- (A -> C) -> C                   5  weakening
7  A                     |- (B -> C) -> ((A -> C) -> C)     6  Conditional proof  
8  B, B -> C             |- C                               2,3 Modus ponens
9  B, B -> C, A -> C     |- C                               8  weakening
10 B, B -> C             |- (A -> C) -> C                   9  Conditional proof
11 B                     |- (B -> C) -> ((A -> C) -> C)     10 Conditional proof
12 A v B                 |- (B -> C) -> ((A -> C) -> C)     7,11 Disjunction elimination
13 B -> C                |- B -> C                          Identity
14 A v B, B -> C         |- (A -> C) -> C                   12,13 Modus ponens
15 A -> C                |- A -> C                          Identity
16 A v B, B -> C, A -> C |- C                               14,15 Modus ponens
17 A -> C, B -> C, A v B |- C                               16 reshuffeling antecedents
18 A -> C, B -> C        |- (A v B) -> C                    17 Conditional proof
19 A -> C                |- (B->C)->((A v B) -> C)          18 Conditional proof
20                       |- (A->C)->((B->C)->((A v B)->C))  19 Conditional Proof 

Not sure if the rule of weakening (line 6 and 9) is allowed again this is a structural rule.

Ps if you refer to this proof refer to it as proof 2

Answer 3

I'll put up a resolution proof here. It probably doesn't help.

assumption 1 ANac
assumption 2 ANbc
assumption 3 Aab
R 1, 3     4 Abc
R 2, 4     5 c