5
$\begingroup$

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))$
$\endgroup$
  • $\begingroup$ I don't know category theory. But I do have to wonder if it's easier to prove that ⊤→(a⊃c)→((b⊃c)⊃(((a⊃b)⊃b)⊃c)) than the formula you gave (or the "OR-3" formula of wikipedia). Also, do "→" and "⊃" differ here? $\endgroup$ – Doug Spoonwood Jun 30 '14 at 3:20
  • $\begingroup$ @DougSpoonwood Yes, $\to$ and $\supset$ are different. I'm using $\to$ to designate arrows, and $\supset$ to designate conditionals. A category has arrows, each of which has one source/domain and one target/codomain, so I'm afraid that "⊤→(a⊃c)→((b⊃c)⊃(((a⊃b)⊃b)⊃c))" isn't really intelligible here. That said, it did make me look at my question again and notice some nasty typos in the first two formulae (now fixed). $\endgroup$ – Joshua Taylor Jun 30 '14 at 3:56
  • $\begingroup$ @DougSpoonwood The short version of category theory as it relates here is that a category is a mathematical structure with objects and arrows. A logic can be a category when we take its formulae as objects and its proofs as arrows (where an arrow $f\colon A \to B$ is a proof of $B$ from $A$). E.g., $\pi\colon A \& B \to A$ and $\pi' \colon A \& B \to B$ are the canonical proofs of $A$ and $B$ from $A \& B$. For each proof $f\colon A \& B \to C$, there's a proof $\lambda f\colon A \to B \supset C$. I'm trying to find out whether there's a simpler proof of OR-3 than the one I've found. $\endgroup$ – Joshua Taylor Jun 30 '14 at 4:03
  • $\begingroup$ @DougSpoonwood Some of the claims in the previous comment (e.g., for each $f$ there's a $\lambda f$) actually depend on the particular structure that the category has (in this case, that the category is cartesian closed (which is implied by it being bicartesian closed)). So take them as true for this question, but not as general principles. $\endgroup$ – Joshua Taylor Jun 30 '14 at 4:05
  • 1
    $\begingroup$ @DougSpoonwood The only arrows that there are to work with are those that are specified by a bicartesian closed category. Have a look at an excellent overview: Bicartesian closed categories and logic. $\endgroup$ – Joshua Taylor Jul 1 '14 at 2:15
2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ I think I like this one better than the one in the question, but it still seems a bit more complicated than I'd like, so I'm going to hold off on accepting it for the time being; hopefully someone else will find a better solution. $\endgroup$ – Joshua Taylor Jun 30 '14 at 18:42
0
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Thank you for your input, although I'm afraid it doesn't help me all that much here. As I've mentioned, part of the problem I'm having is that this is a pretty simple natural deduction proof, but that the categorical construction is elusive. Lines 1–5 all have direct categorical equivalents. The disjunction elimination rule, though, is that "Given arrows $f\colon A \to C$ and $g\colon B \to C$, there is an arrow $[f,g]\colon A \lor B \to C$. The domains of the "cases" have to be the disjuncts exactly. That means that getting from 4 and 5 to 6 is much harder. From 4 and 5, what you get… $\endgroup$ – Joshua Taylor Jul 7 '14 at 11:35
  • $\begingroup$ …would be $(A\land(A\lif C))\lor (B\land(B\lif C)) \to C$. That doesn't end up being all that helpful, though, because conditional introduction (which works in both directions) has the form "Given $f\colon A \land B \to C$, there is an arrow $\lambda f\colon A \to B \lif C$." There's nothing in this case to apply it to, unfortunately. Each arrow is a "complete" proof that doesn't depend on any other assumptions; I think that means that we will always have either to use either $A \lor B \to ((A\lif C)\land(B\lif C))\lif C)$, where the conditionals are "baked into the codomain" or… $\endgroup$ – Joshua Taylor Jul 7 '14 at 11:47
  • $\begingroup$ $(A\land(A \lif C)\land(B\lif C))\lor(B\land(A\lif C)\land(B\lif C)) \to C$, where the conditionals are "baked into the domain". $\endgroup$ – Joshua Taylor Jul 7 '14 at 11:49
  • $\begingroup$ I did have a look at intuitionistic logic , looking how they deduce it, but in intuitionistic logic it (or an quite similar formula) is an axiom, also I was wondering is the problem really in getting from 4 and 5 to 6, (which is a rule as the pdf says that "+ is precisely the logical connective $\lor$" ,rephrased see chaper 4) Is the problem not in getting from 6 to 7? , also had a browse about catagory theory, but could not find a clear exposition on the coproduct (+) rules or axioms $\endgroup$ – Willemien Jul 7 '14 at 11:57
  • $\begingroup$ 6 to 7 is pretty easy actually. There's an arrow $\langle\langle\pi'\pi,\pi'\rangle,\pi\pi\rangle\colon (X\land Y)\land Z \to (Y\land Z)\land X$. $\endgroup$ – Joshua Taylor Jul 7 '14 at 15:14
-1
$\begingroup$

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
$\endgroup$
  • $\begingroup$ It doesn't help; there's no question about how to prove the result; there's a question about a shorter proof in what's essentially a specific proof system (the categorical presentation). By the time a problem is clausified, almost all of the structural issues (commutativity) have been wiped away. The question is essentially, what's the easiest way to prove $(A \lif C) \lif ((B\lif C)\lif ((A\lor B)\lif C)))$ in a natural deduction system where constructive dilemma/disjunction elimination can't be used within the scope of assumptions. This doesn't (attempt to) help with that. $\endgroup$ – Joshua Taylor Jul 14 '14 at 15:25
  • $\begingroup$ Thank you for the attention (and the suggestion to encode the categorical structure and use an automated reasoner was helpful, though hasn't found a solution yet), but -1 as "This answer is not useful" and that's explicitly acknowledged in the answer. $\endgroup$ – Joshua Taylor Jul 14 '14 at 15:27
  • $\begingroup$ @JoshuaTaylor How did you encode the assumptions of category theory into the automated reasoner? Did you use any hints or weight any formulas? Did you have any resonators or weight any subformulas? Did you have any demodulators? What rule(s) of inference did you let the automated reasoner use? $\endgroup$ – Doug Spoonwood Jul 14 '14 at 16:26
  • 1
    $\begingroup$ Here's a gist of the latest Prover9 input, proof.in. It's just configured with set(auto) at the moment. I tried some various term weightings, but that's really sort of black magic to me, especially when the proofs I've found by hand require so much currying and uncurrying. The comments have some notes about some lemmas that can help, and the sometimes utility of having uncurry as a function. If you can get any better results from this than I can, that'd almost certainly be a helpful result. $\endgroup$ – Joshua Taylor Jul 14 '14 at 16:44
  • $\begingroup$ @JoshuaTaylor You've used "arrow" as a trinary predicate. I don't know if that's better or worse than using arrow as a binary predicate and including a product function more often. Also, when I ran Prover9 it used UR resolution. I don't know if linked UR resolution would work better or not. $\endgroup$ – Doug Spoonwood Jul 14 '14 at 17: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.