Propositional logic question

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

Propositional logic question

Dave Tapley-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Propositional logic question

Jeff Polakow

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
Reply | Threaded
Open this post in threaded view
|

Re: Propositional logic question

Dave Tapley-2
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Propositional logic question

Eric-175
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
Reply | Threaded
Open this post in threaded view
|

Re: Propositional logic question

Derek Elkins
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
Reply | Threaded
Open this post in threaded view
|

Re: Propositional logic question

Heinrich Apfelmus
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
Reply | Threaded
Open this post in threaded view
|

Re: Re: Propositional logic question

Bulat Ziganshin-2
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