How to prove |– (U → V ) → ((¬U → V ) → V)? Or how to deduce V from (U → V ), (¬U→V) using Deduction theorem? This is what I need to ultimately prove: |– (U → V ) → ((¬U → V ) → V)
We have these axioms and modus ponens:
Axiom 1 is: P→(Q→P)
Axiom 2 is: (P→(Q→R))→((P→Q)→(P→R))
Axiom 3 is: (¬Q→¬P)→ (P→Q)
Modus ponens is: from P and P→Q infer Q
A proof in this manner means a sequence of lines where each line is an axiom, or a formula from your "base" set ({α,¬α} below), or an inference (using modus ponens), with the last line being the formula being proved.
I used the deduction theorem to say that a finding a proof from the empty set of that formula is equivalent to finding a proof:
(U → V ), (¬U→V) |– V
Using these axioms and modus penons I want to infer V from (U → V ), (¬U→V)
I'm a bit stuck here. Any help please?
 A: The proof that I know of is fairly tricky, and consists on bootstrapping up several results from axiom 3 in turn, using the Deduction Theorem.
Lemma schema 1: $\vdash \lnot A\rightarrow(A \rightarrow B)$.
Proof: By the Deduction Theorem, it suffices to show $\lnot A \vdash A \rightarrow B$.  Then, using axiom 3 and a modus ponens, we reduce to showing that $\lnot A \vdash \lnot B \rightarrow \lnot A$.  This is now easy. $\square$
Lemma schema 2: $\vdash (\lnot A\rightarrow A)\rightarrow A$.
Proof: By the Deduction Theorem, it suffices to show that $\lnot A\rightarrow A\vdash A$.  Now, in general, for any propositional formula $P$, we have that $\lnot A\rightarrow A, \lnot A \vdash P$ through concluding $A$ as well, and then applying lemma schema 1.  But then, by the Deduction Theorem, we conclude that $\lnot A\rightarrow A \vdash \lnot A \rightarrow P$.  In particular, $\lnot A\rightarrow A \vdash \lnot A \rightarrow \lnot(\lnot A \rightarrow A)$; and now, combining this fact with axiom 3 and an application of modus ponens, we then see that $\lnot A\rightarrow A \vdash (\lnot A\rightarrow A)\rightarrow A$.  Since $\lnot A\rightarrow A \vdash \lnot A\rightarrow A$ also, a modus ponens gives the required conclusion $\lnot A \rightarrow A \vdash A$. $\square$
Lemma schema 3: $\vdash \lnot\lnot A \rightarrow A$.
Proof: By the Deduction Theorem, it suffices to show that $\lnot\lnot A \vdash A$.  Now, $\lnot\lnot A \vdash \lnot A\rightarrow A$ using lemma schema 1 and a modus ponens.  Now, from lemma schema 2 (and extension of context) we also have $\lnot\lnot A \vdash (\lnot A\rightarrow A)\rightarrow A$, and a modus ponens gives the desired conclusino $\lnot\lnot A \vdash A$. $\square$
Lemma schema 4: $\vdash A \rightarrow \lnot\lnot A$.
Proof: Using axiom 3 and a modus ponens, it suffices to show $\vdash \lnot\lnot\lnot A \rightarrow \lnot A$.  This is then a specialization of lemma schema 3. $\square$
Lemma schema 5: $\vdash (A\rightarrow B)\rightarrow(\lnot B\rightarrow \lnot A)$.
Proof: By the Deduction Theorem, it suffices to show $A\rightarrow B \vdash \lnot B\rightarrow \lnot A$.  Using axiom 3 and a modus ponens, we reduce to showing $A \rightarrow B \vdash \lnot\lnot A \rightarrow \lnot\lnot B$.  By another application of the Deduction Theorem, it suffices to show $A\rightarrow B, \lnot\lnot A \vdash \lnot\lnot B$.  But then, lemma schema 3 and a modus ponens gives $A \rightarrow B, \lnot\lnot A \vdash A$; a modus ponens gives $A \rightarrow B, \lnot \lnot A \vdash B$; and finally, lemma schema 4 and a modus ponens gives from this that $A\rightarrow B, \lnot\lnot A \vdash \lnot\lnot B$. $\square$
Final result: $\vdash (U\rightarrow V) \rightarrow [(\lnot U\rightarrow V)\rightarrow V]$.
Proof: By two applications of the Deduction Theorem, it suffices to show $U\rightarrow V, \lnot U\rightarrow V \vdash V$.  But by lemma schema 5, $U\rightarrow V, \lnot U\rightarrow V \vdash \lnot V\rightarrow \lnot U$; and combining with the assumption $\lnot U \rightarrow V$, an easy argument gives $\lnot V\rightarrow V$.  But now by lemma schema 2, $U\rightarrow V, \lnot U\rightarrow V \vdash (\lnot V\rightarrow V)\rightarrow V$ also; and a final modus ponens gives what we wanted. $\square$
