5
$\begingroup$

We have:

  1. $\varphi \lor \psi, \neg \varphi \vdash \psi$
  2. $\varphi \lor \psi, \varphi \to \chi, \psi \to \chi \vdash \chi$

Using $2$ and explosion (ex falso), one can prove $1$:

  1. $\varphi \lor \psi$ [premise]
  2. $\neg \varphi$ [premise]
    1. $\varphi$ [assumption]
    2. $\bot$ [contradiction 2 3.1]
    3. $\psi$ [explosion]
  3. $\varphi \to \psi$ [$\to$intro 3.1-3.3]
    1. $\psi$ [assumption]
  4. $\psi \to \psi$ [$\to$intro 5.1-5.1]
  5. $\psi$ [$\lor$elim 1 4 6]

However, can one prove $2$ from $1$ using other intuitionist rules?

$\endgroup$
  • $\begingroup$ I'm not sure that you can; with modus tollendo ponens: $\varphi \lor \psi, \lnot \varphi \vdash \psi$ we can derive (using $\to$-intro) ex falso: $\bot \vdash \varphi$. $\endgroup$ – Mauro ALLEGRANZA Sep 19 '17 at 15:33
1
$\begingroup$

You cannot constructively prove Proof By Cases from the suggestion Or-Elim rule. Consider the following valuations (found by my computer):

$$\begin{array} {cc|c} A & B & A \to B \\ \hline 1 & 1 & 1 \\ 2 & 1 & 1 \\ 3 & 1 & 1 \\ 1 & 2 & 2 \\ 2 & 2 & 1 \\ 3 & 2 & 1 \\ 1 & 3 & 3 \\ 2 & 3 & 3 \\ 3 & 3 & 1 \\ \end{array}$$

$$\begin{array} {c|c} A & \lnot A \\ \hline 1 & 3 \\ 2 & 3 \\ 3 & 1 \\ \end{array}$$

$$\begin{array} {cc|c} A & B & A \lor B \\ \hline 1 & 1 & 1 \\ 2 & 1 & 1 \\ 3 & 1 & 1 \\ 1 & 2 & 1 \\ 2 & 2 & 1 \\ 3 & 2 & 2 \\ 1 & 3 & 1 \\ 2 & 3 & 2 \\ 3 & 3 & 3 \\ \end{array}$$

And the following logic $L$:

$$\begin{array} {ll} \text{Axiom Schema:} & \\ \hline A \to B \to A & \text{Weakening} \\ (A \to B \to C) \to (A \to B) \to (A \to C) & \text{Conditional Modus Ponens} \\ \hline (A \to B) \to (A \to \lnot B) \to \lnot A & \text{Negation Propagation} \\ A \to \lnot A \to B & \text{Explosion} \\ \hline A \to (A \lor B) & \text{Or Intro 1} \\ A \to (B \lor A) & \text{Or Intro 2} \\ (A \lor B) \to \lnot A \to B & \text{Disjunctive Syllogism 1} \\ (A \lor B) \to \lnot B \to A & \text{Disjunctive Syllogism 2} \\ \hline \text{Inferences:} & \\ A, ~ (A \to B) \vdash B & \text{Modus Ponens} \\ \end{array}$$

Taking $1$ as the "true" value, each axiom schema is a tautology; and for modus ponens, implication has the property that if $A = 1$ and $(A \to B) = 1$ then $B = 1$. So every provable statement is also a tautology.

However, Proof By Cases, $P(A, B, C) = (A \lor B) \to (A \to C) \to (B \to C) \to C$, is not a tautology, specifically $P(2, 2, 2)\ne 1$. So it is not provable.

However, I suspect that replacing the negation schemas with the classical schemas $(\lnot A \to \lnot B) \to B \to A$ (or equivalent multiple rules for sanity's sake) leads to the Proof By Cases being provable since I've seen it in several logic publications.


KennyLau found the classical proof in a comment:

$$\begin{array} {rll} 1 & X \lor Y & \text{Premise} \\ 2 & X \to Z & \text{Premise} \\ 3 & Y \to Z & \text{Premise} \\ % 4 & \quad \quad \lnot Z & \text{Assumption} \\ 5 & \quad \quad \quad \quad Y & \text{Assumption} \\ 6 & \quad \quad \quad \quad Z & \text{Imp-Elim 3,5} \\ 7 & \quad \quad \lnot Y & \text{Contradiction of assumption 5, with 4 and 6} \\ 8 & \quad \quad X & \text{Needs a name, from 1 and 7} \\ 9 & \quad \quad Z & \text{Imp-Elim 2 and 8} \\ 10 & \lnot \lnot Z & \text{Contradiction of assumption 4, with 4 and 9} \\ 11 & Z & \text{Double negation elimination of 10} \\ \end{array}$$

$\endgroup$
  • $\begingroup$ Good lord. You actually set out building a model. Effort appreciated. $\endgroup$ – Kenny Lau Sep 20 '17 at 19:57
  • $\begingroup$ I like to think my computer did most of the work. Also your question interested me and I had to know for sure. $\endgroup$ – DanielV Sep 20 '17 at 19:59
  • $\begingroup$ Which software/program did you use? $\endgroup$ – Kenny Lau Sep 20 '17 at 19:59
  • $\begingroup$ @KennyLau C# for this one $\endgroup$ – DanielV Sep 20 '17 at 20:00
  • $\begingroup$ Shouldn't the arrows in "Proof By Cases" be conjunctions? $\endgroup$ – Kenny Lau Sep 20 '17 at 20:13
3
$\begingroup$

No. Write $\triangledown$ for our wannabe disjunction, so we have the rule $\varphi\triangledown\psi,\neg\varphi\vdash\psi$ (and presumably we have $\varphi_i\vdash\varphi_1\triangledown\varphi_2$ as well). Then, to make use of the $\varphi\triangledown\psi$ assumption in $\varphi\triangledown\psi,\varphi\to\chi,\psi\to\chi\vdash\chi$ we need to be able to prove $\neg\varphi$. There is simply no reason this would be provable.

This is even more evident with a computational interpretation. Here's what the beginning of a proof attempt would look like in Agda:

data ⊥ : Set where

¬_ : Set → Set
¬ A = A → ⊥

postulate WOr : Set → Set → Set
postulate Left : {φ ψ : Set} → φ → WOr φ ψ
postulate Right : {φ ψ : Set} → ψ → WOr φ ψ
postulate wOrElim : {φ ψ : Set} → WOr φ ψ → ¬ φ → ψ

orElim : {φ ψ χ : Set} → WOr φ ψ → (φ → χ) → (ψ → χ) → χ
orElim wor l r = r (wOrElim wor (λ x → ? (l x)))

There is no obvious choice of what to put for the ?. Computationally, there's no way to exfiltrate the $\chi$ l produces. In the computational interpretation of classical logic, Peirce's law gives us essentially a throw/catch mechanism so we could implement orElim in a made-up, classical version of Agda with something like:

orElim : {φ ψ χ : Set} → WOr φ ψ → (φ → χ) → (ψ → χ) → χ
orElim wor l r = try {r (wOrElim wor (λ x → throw (l x)))} catch(c) { c }    

This isn't a proof that it is impossible, of course. Maybe there's a clever program to do it that I didn't think of. In practice, though, programming experience combined with the computational interpretation of, particularly, intuitionistic logic makes it fairly easy to recognize that there are no data flow paths. As such, things which aren't intuitionistically provable become relatively self-evident.

If you did want to prove that you can't derive 2 from 1, you'd need to do something like an induction on the derivations, or you can make a counter-model, e.g. a topological model.

$\endgroup$
  • $\begingroup$ +1. I agree with your intuition; in order to use modus tollendo ponens we have to produce at a certain point in the derivation $\lnot \varphi$. Without Double Negation or some equivalent, the only way to "generate" the needed $\bot$ is through a contradiction. $\endgroup$ – Mauro ALLEGRANZA Sep 20 '17 at 9:33
  • $\begingroup$ But I do not see any way to produce a contradiction from the premises: $\varphi \lor \psi, \varphi \to \chi, \psi \to \chi$. The set of premises is clearly satisfiable. $\endgroup$ – Mauro ALLEGRANZA Sep 20 '17 at 9:34

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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