Hopefully this is just about on topic enough..
(Oh and it's not home work, I just can't bring myself to let it go!) Taken from "Simon Thompson: Type Theory and Functional Programming" Section 1.1 Exercise 1.3 Question: Give a proof of (A => (B => C)) => ((A /\ B) => C). Now I can easily perform (and verify, it's given earlier in the section) the proof of implication with the terms flipped around: ((A /\ B) => C) => (A => (B => C)) Thus: [A]2 [B]1 ----------- (/\ I) [(A /\ B) => C]3 A /\ B ---------------------------------------- (=> E) C --------- (=> I) 1 B => C ------------------ (=> I) 2 A => (B => C) --------------------------- (=> I) 3 ((A /\ B) => C) => (A => (B => C)) My problem arrives finding a solution to the exercise question, my approach is to basically run the above proof backwards. Thus: A => (B => C) A --------------------- (=> E) B B => C --------------------- (=> E) C Now at this point I thought "aha, I can use (=> I) to introduce (A /\ B)" and get: --------------------- (=> I) 1 (A /\ B) => C But here I am only entitled to discharge (A /\ B) in the preceding proof and not A and B on their own. What proof which would allow me to discharge my assumptions A and B? I can see in my head how it makes perfect sense, but can't jiggle a way to do it using only the given derivations. Many thanks, Dave _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Hello, > But here I am only entitled to discharge (A /\ B) in the preceding > proof and not A and B on their own. > What proof which would allow me to discharge my assumptions A and B? > > I can see in my head how it makes perfect sense, but can't jiggle a > way to do it using only the given derivations. > You have (A /\ B) to work with. Remember that intuitionistic/classical logic places no restrictions on how many times you use each hypothesis. hth, Jeff --- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Dave Tapley-2
Whoops, okay after two lines (thanks to oerjan) on #haskell I realise
that yes, it is as easy as it should have been. For completeness: [A /\ B]1 ------------ (/\ E1) [A => (B => C)]2 A ------------------------------------------------- (=> E) B => C [A /\ B]1 ------------ (/\ E2) B B => C ------------------------------------------------- (=> E) C ------------------ (=> I)1 (A /\ B) => C ------------------------------------------------ (=> I)2 (A => (B => C)) => ((A /\ B) => C) Learning is fun :) Dave, _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
This seems rather complicated! What about this:
A => (B => C) = { X => Y == ¬X \/ Y } ¬A \/ (¬B \/ C) = {associativity} (¬A \/ ¬B) \/ C = { DeMorgan } ¬(A /\ B) \/ C = { X => Y == ¬X \/ Y } A /\ B => C E. Dave Tapley wrote: > Whoops, okay after two lines (thanks to oerjan) on #haskell I realise > that yes, it is as easy as it should have been. > > For completeness: > > [A /\ B]1 > ------------ (/\ E1) [A => (B => C)]2 > A > ------------------------------------------------- (=> E) > B => C > [A /\ B]1 > ------------ (/\ E2) > B B => C > ------------------------------------------------- (=> E) > C > ------------------ (=> I)1 > (A /\ B) => C > > ------------------------------------------------ (=> I)2 > (A => (B => C)) => ((A /\ > B) => C) > > > Learning is fun :) > > Dave, > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Dave Tapley-2
On Mon, 2007-06-25 at 20:41 +0100, Dave Tapley wrote:
> Hopefully this is just about on topic enough.. > (Oh and it's not home work, I just can't bring myself to let it go!) > > Taken from "Simon Thompson: Type Theory and Functional Programming" > > Section 1.1 > Exercise 1.3 > > Question: Give a proof of (A => (B => C)) => ((A /\ B) => C). Via the Curry-Howard correspondence, this corresponds to the type of uncurry ( :: (a -> b -> c) -> (a,b) -> c ) and thus uncurry corresponds to the proof. The @src lambdabot gives for uncurry is uncurry f p = f (fst p) (snd p) which most (careful) Haskell programmers would write as uncurry f ~(x,y) = f x y Try to see how the implementation of uncurry matches up to your proof of the proposition. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Eric-175
Eric wrote:
> This seems rather complicated! What about this: > > A => (B => C) > = { X => Y == ¬X \/ Y } > ¬A \/ (¬B \/ C) > = {associativity} > (¬A \/ ¬B) \/ C > = { DeMorgan } > ¬(A /\ B) \/ C > = { X => Y == ¬X \/ Y } > A /\ B => C > > E. That works for classical logic where ¬A \/ A always holds, but the task here is to prove it for intuitionistic logic. Regards, apfelmus _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Hello apfelmus,
Tuesday, June 26, 2007, 12:45:54 PM, you wrote: > That works for classical logic where ¬A \/ A always holds, but the task > here is to prove it for intuitionistic logic. is it the same as so-called "woman logic"? :) -- Best regards, Bulat mailto:[hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |