1
$\begingroup$

I am reading Awodey's book on Category Theory, and I'm not sure if this is a typo:

  1. $p \vdash r$ and $q \vdash r$ iff $p \vee q \vdash r$

Shouldn't the rule instead be

  1. $p \vdash r$ or $q \vdash r$ iff $p \vee q \vdash r$

My main disagreement is with the reverse direction: if $p \vee q \vdash r$, then it is not necessarily true that $p \vdash r$ and $q \vdash r$.

$\endgroup$

1 Answer 1

1
$\begingroup$

Rule 5. is simply a re-statement of the "usual" Natural Deduction rules for $\lor$-elimination and -introduction (intuitionistically valid) :

$$\frac{\Gamma, \vdash \varphi }{\Gamma \vdash \varphi \lor \psi} \quad (\lor-i_1)$$

$$\frac{\Gamma \vdash \psi }{\Gamma \vdash \varphi \lor \psi} \quad (\lor-i_2)$$

$$\frac{\Gamma, \varphi \vdash \tau \quad \Gamma, \psi \vdash \tau \quad \Gamma \vdash \varphi \lor \psi}{\Gamma \vdash \tau} \quad (\lor-e)$$

For :

if $p∨q⊢r$, then $p⊢r$ and $q⊢r$

we have that both $p$ and $q$ "separately" imply $p \lor q$.

For :

if $p⊢r$ and $q⊢r$, then $p∨q⊢r$

we clearly need that $r$ be derivable from both $p$ and $q$, in order (applying $\lor$-elimination, or proof by cases) to conclude with $r$.

$\endgroup$
2
  • $\begingroup$ I still don't really understand the "introduction" rule part -- that is if r follows from p v q, then r follows from p and r follows from q. Do both of those necessarily need to be true -- why not just one? $\endgroup$
    – pyrrhic
    Commented Nov 10, 2014 at 2:43
  • 1
    $\begingroup$ @pyrrhic - because we can prove it as follows : (i) assume $p$; then by $\lor$-intro : $p \vdash p \lor q$; but by hupotheses : $p∨q⊢r$. Thus, by "transitivity" of $\vdash$ : $p⊢r$. Now : (ii) assume $q$ ... and proceed in the same way. $\endgroup$ Commented Nov 10, 2014 at 7:27

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .