CODEWITHSUNDEEP
functional-programminglogiccoqagdaproofs
Eric Johnson
Eric Johnson

Reputation: 47

Propositional Logic and Proofs

I am trying to prove the below case for a homework assignment and have been working hours on it, still no luck.

((q, p) -> r) -> p -> q -> r

Any suggestions or comments as to what I am doing wrong?

Upvotes: 0

Views: 524

Answers (3)

Frank Hubeny
Frank Hubeny

Reputation: 178

This is a proof using Klement's Fitch-style natural deduction proof checker and the forallx textbook providing explanation. (The links are below.)

enter image description here

The main problem with the original attempt is that lines 8 and 9 did not discharge the assumptions. They appeared to stay in the same subproofs based on the indents and braces.

Otherwise the proof is the same as what I provided. On my line 6 I discharged the assumption I made of "Q" on line 3 by introducing the conditional (lines 3-5). On my line 7 I discharged the assumption "P" made on line 2 by introducing the conditional (lines 2-6).

Reference

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

Upvotes: 0

Musa Al-hassy
Musa Al-hassy

Reputation: 982

We have a Coq proof thanks to @Aadit, and it would only be fair ---ethical?--- to present an Agda proof.

An immediate and simple proof is

open import Data.Product

portation : {P Q R : Set} → (P × Q → R) → (P → Q → R)
portation P×Q→R = λ p q → P×Q→R (p , q)

Of course this may not at all be clear if the asker is not familiar with Agda and is seeking a formalisation. So let's throw in some detail!!

In constructive logic, propositions can be seen as the small types:

ℙrop = Set

Then pairing is the usual way to form conjugation,

data _∧_ (P Q : ℙrop) : Set where
 ∧I : P → Q → P ∧ Q

In constructive logic, implication is just function space: to say one thing implies another is tantamount to yielding a procedure that with input of the first kind returns output of the second kind.

_⇒_ : (P Q : ℙrop) → Set
_⇒_ = λ P Q → (P → Q)

Implication introduction is then just usual function-definition, and implication elimination is then nothing more than function application.

⇒I : ∀ {P Q} → (P → Q) → P ⇒ Q
⇒I P→Q = P→Q

⇒E : ∀ {P Q} → P ⇒ Q → P → Q
⇒E P→Q p = P→Q p

Now the asker is using natural-deduction style of proofs, so let us introduce some syntactic sugar to bridge the gap from the paper-and-pencil proof to the Agda formalisation.

syntax ⇒I {P} {Q} (λ p → q) = ⇒-I-assuming-proof p of P we-have Q proved-by q

Now the proof!

shunting : (P Q R : ℙrop) → (P ∧ Q) ⇒ R → P ⇒ (Q ⇒ R)
shunting P Q R P∧Q⇒R =
                    ⇒-I-assuming-proof p of P
                    we-have Q ⇒ R proved-by

                        ⇒-I-assuming-proof q of Q
                        we-have R proved-by

                            ⇒E P∧Q⇒R (∧I p q)

Which is not only quite readable, but also somewhat close to the asker's presentation!

Agda is such a joy!

Upvotes: 1

Aadit M Shah
Aadit M Shah

Reputation: 74204

This is how you'd prove it in Coq:

Coq < Theorem curry : forall p q r, ((q /\ p) -> r) -> p -> q -> r.
1 subgoal

  ============================
   forall (p q : Prop) (r : Type), (q /\ p -> r) -> p -> q -> r

First, we name all the premises:

curry < intros p q r f x y.
1 subgoal

  p : Prop
  q : Prop
  r : Type
  f : q /\ p -> r
  x : p
  y : q
  ============================
   r

The only premise that produces the subgoal r is f:

curry < apply f.
1 subgoal

  p : Prop
  q : Prop
  r : Type
  f : q /\ p -> r
  x : p
  y : q
  ============================
   q /\ p

To apply f we first need to satisfy the subgoals q and p:

curry < split.
2 subgoals

  p : Prop
  q : Prop
  r : Type
  f : q /\ p -> r
  x : p
  y : q
  ============================
   q

subgoal 2 is:
 p

The premise y is a proof for subgoal q:

curry < exact y.
1 subgoal

  p : Prop
  q : Prop
  r : Type
  f : q /\ p -> r
  x : p
  y : q
  ============================
   p

The premise x is a proof of subgoal p:

curry < exact x.
No more subgoals.

We're done. Here's the full proof:

curry < Qed.
intros p q r f x y.
apply f.
split.
 exact y.

 exact x.

curry is defined

In function programming languages like Haskell you'd have:

curry :: ((q, p) -> r) -> p -> q -> r
curry f x y = f (y, x)

Everything works out due to the Curry-Howard correspondence.

Upvotes: 4

Related Questions