Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

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.

share|improve this question
    
In your question, you haven't explained the motivation for why you are looking at this possible equivalence, nor what you have already tried (Kripke models? Weak counterexamples?). You could improve the question by explaining both your motivation and what you have already attempted. –  Carl Mummert Apr 26 '11 at 12:38
    
It seems from the BHK interpretation that the formula on the right side of the equals sign should not imply the formula on the left, so it would be more natural to be looking for a counterexample rather than a proof. –  Carl Mummert Apr 26 '11 at 13:07
    
maybe you could go into a bit of detail on what the question is actually asking? As I said I do not understand what P,U,V and Z are since you have not quantified them. –  quanta Apr 29 '11 at 11:08
    
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? –  quanta Apr 29 '11 at 21:15
add comment

2 Answers

up vote 3 down vote accepted

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

share|improve this answer
2  
When you substitute what you've put for $Z$ into (1), it doesn't appear that you get your (2). Rather, you get: $(P\rightarrow U \vee V) \rightarrow (P \rightarrow U) \vee (P \rightarrow V) $. And if I'm right about that, can't you then obtain (2) from (1) by a much simpler substitution: Let $Z = \top$. –  Amit Kumar Gupta Apr 26 '11 at 15:38
    
Sorry! That was a typo I messed up when correcting my earlier mistakes.. –  quanta Apr 26 '11 at 16:13
    
@Jan, I put in details for this part. –  quanta Apr 26 '11 at 16:20
add comment

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

share|improve this answer
    
+1 for the counter-model, that actually makes the proof self contained. –  quanta Apr 30 '11 at 0:34
    
$V=1$ should be $U=1$, also it is not usual to use the same name for different nodes of a Kripke model, so I think $w1$ should be $w2$. –  Kaveh Apr 30 '11 at 20:50
    
Just fixed U=1. –  Cookie Monster Mar 15 '12 at 0:09
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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