4
$\begingroup$

I wonder whether the following holds in intuitionistic logic: $((P \to U \lor V) \to Z) \leftrightarrow ((P \to U) \to Z) \land ((P \to V) \to Z)$

For disjunction I assume the following two rules: $\begin{array}{lcl} \begin{array}{l} G\vdash U\\ \hline G\vdash U\lor V \end{array} &\quad& \text{(Rv1)}\\ &\\ \begin{array}{l} G\vdash V\\ \hline G\vdash U\lor V \end{array} &\quad& \text{(Rv2)}\\ &\\ \begin{array}{l} G,\ U\vdash A\\ G,\ V\vdash A\\ \hline G,\ U\lor V \vdash A \end{array} &\quad& \text{(Lv)}\end{array}$

I can easily proof the following direction: $((P \to U \lor V) \to Z) \to ((P \to U) \to Z) \land ((P \to V) \to Z)$

Namly we have: $\begin{array}{ll} U\vdash U\lor V\\ \hline P\to U\vdash P\to U\lor V\\ \hline (P\to U\lor V) \to Z\vdash (P\to U)\to Z \end{array}$

But I am not sure whether I can establish the other direction.

Bye

P.S.: I didn't try Kripke models or Weak conterexamples. I only tried proof theoretically to derive it, by the rules that I have given in my Question.

P.S.S.: It would give an alternative method to the Rip (Resolution for Intuitionistic Logic) found in Basic Proof Theory, Second Edition, Troelstra & Schwichtenberg, 2000, p.253.

  • 0
    I think that giving specific values for P,U,V,Z and showing this implies a (semi-)classical axiom proves that the formula cannot be proved in intuitionistic logic. You seemed to disagree, but why?2011-04-29

2 Answers 2

3

This is a very interesting question!

You have named the axiom (1) $((P \to U) \to Z) \land ((P \to V) \to Z) \to ((P \to U \lor V) \to Z).$

Let us throw away the $Z$ and switch it around though: (2) $(P \to U \lor V) \to (P \to U) \lor (P \to V),$


Details on the equivalence of (1) and (2):

To show that (1) implies (2) instantiate $Z := (P \to U) \lor (P \to V)$ and we have: $((P \to U) \to ((P \to U) \lor (P \to V))) \land ((P \to V) \to ((P \to U) \lor (P \to V))) \to ((P \to U \lor V) \to ((P \to U) \lor (P \to V)))$ the hypothesis both disappear and we are left with $(P \to U \lor V) \to ((P \to U) \lor (P \to V)).$

As for the other direction, we just apply the general theorem that $(A \to (B \lor C))$ implies $((B \to Z) \land (C \to Z)) \to (A \to Z)$.


Algorithmically, it is obvious that this axiom is not intuitionist. It is somehow guessing in advanced whether $P$ will imply $U$ or $V$ and taking that answer to build either a proof of $P \to U$ or $P \to V$. There is no way to perform this process without actually having $P$ already.


I claim this axiom is equivalent to the Godel-Dummett axiom there is a proof here on JSTOR but you can see the first page and get enough an idea how to do it. The Godel-Dummett axiom is $(P \to Q) \lor (Q \to P)$. If you have trouble proving this equivalent to (2) I can write it out in detail but it is not very difficult and quite fun.

It is a classical result that the Godel-Dummett implies weak excluded middle: $\neg P \lor \neg \neg P.$ That is not enough to get full classical logic but it is certainly not intuitionist logic! It's "half way" between excluded middle (classical) and the double negation embedding (which can be proved intuitionistically).

  • 0
    @Jan, I put in details for this part.2011-04-26
2

Picking up the idea of Quanta I get from:

((P -> U v V) -> Z) <- ((P -> U) -> Z) & ((P -> V) -> Z)

by setting Z = (P -> U) v (P -> V) we get:

((P -> U v V) -> (P -> U) v (P -> V)) <- ((P -> U) -> (P -> U) v (P -> V)) & ((P -> V) -> (P -> U) v (P -> V))

The parts of the conjunction do hold, so this should be equal to:

(P -> U v V) -> (P -> U) v (P -> V)

and now by setting P = U v V we get:

(U v V -> U v V) -> (U v V -> U) v (U v V -> V)

The left hand side holds, so this should be equal to:

(U v V -> U) v (U v V -> V)

Which is in turn equal to:

((U -> U) & (V -> U)) v ((U -> V) & (V -> V))

The identity implications do also hold, so that this should be equal to:

(V -> U) v (U -> V)

Now, although classically valid, this has a simple intuitionist counter model:

    w1 V=1, U=0    /   w0 V=0, U=0    \     w2 V=0, U=1 

Since the instantiated formula is not valid, the general original formula can also not be valid. Q.E.D.

Bye

  • 0
    Just fixed U=1.2012-03-15