Natural Deduction

Due: 11:59pm ET Thursday, April 16, 2020

Stencil Files

We have provided a stencil file. It can be found in /course/cs1950y/pub/natdeduce. Please do not edit the stencil or you may lose points.

Natural Deduction

Recall from class that natural deduction is a system of rewriting propositions, where a proposition is a composition of the following symbols:

- A ∧ B, (and)
- A ∨ B, (or)
- ~A, (not)
- A -> B, (implies)
- A <-> B, (if and only if)

Using rules of introduction (e.g. ∧I, “and introduction”), we can introduce symbols and using rules of elimination (e.g. ∨E, “or elimination”), we can eliminate symbols. You can find the list of tactics you may use at the bottom of the support code, starting from ∧I through fE.

Note that you will be proving the statements in classical logic which has the additional axiom of the law of excluded middle, which states that every proposition is either true or false, and is not an axiom in Coq by default.

Natural Deduction Rules

Below are the rules we have in natural deduction, which you will use in this assignment. You can also find these at the bottom of the support code, starting from ∧I through fE.

And (∧):

- ∧I : A, B |- A ∧ B
- ∧E1 : A ∧ B |- A
- ∧E2 : A ∧ B |- B

Or (∨):

- ∨I1 : A |- A ∨ B
- ∨I2 : B |- A ∨ B
- ∨E : A ∨ B, A...C, B...C |- C

Not (~):

- ~I : A...⊥ |- ~A
- ~E : ~A, A |- ⊥

Implication (->):

- ->I : A...B |- A -> B
- ->E : A, A -> B |- B

Bi-implication (<->):

- <->I : A -> B, B -> A |- A <-> B
- <->El : A <-> B |- A -> B
- <->Er : A <-> B |- B -> A

True and False:

- tI : A |- ⊤
- fE : ⊥ |- A

Using Coq

For this assignment, you will be proving statements using natural deduction in the Coq proof assistant. We suggest using the online IDE to write your proofs. On the left, we have our script pane, where we write our definitions, theorems, and proofs. In the top-right, we have the goals pane, where we have the current hypotheses and goals we need to prove. In the bottom-right, we have the messages pane, where we get other outputs from Coq.

You can use Alt + Enter to run the proof up to your cursor and Alt + ↑ and Alt + ↓

to move up and down through the proofs.

In Coq, we prove things by transforming our goals (on the bottom of the goals pane) until it matches one of our hypotheses (things we assume to be true). We have provided a set of tactics that match the natural deduction rules discussed above. You might also need to use the following tactic:

- exact <hypothesis> - completes the proof when the goal exactly matches the given hypothesis.

When you have multiple goals that need to be proved in the goals pane, you can focus on each one in succession using bullets as in the following:

<top-level tactic here>

- <proof of goal one>

- <proof of subgoal 1>
- <proof of subgoal 2>

- <proof of goal two>

- <proof of subgoal 1>
- <proof of subgoal 2>

Homework Problems

Fill out the proofs for the following problems using the tactics specified above. We have provided the problem statements in the stencil; your job is to fill in the proof!

Example: And commutes

To help you along, we’ve provided an example proof for the commutativity of and below:

Lemma and_commutes : A ∧ B <-> B ∧ A.

Proof.

<->I.

- =>I. ∧I.

+ ∧Er. exact H.

+ ∧El. exact H.

- =>I. ∧I.

+ ∧Er. exact H.

+ ∧El. exact H.

Qed.

#1: Or commutes

Show that or (∨) commutes. In other words, prove that

A ∨ B <-> B ∨ A

#2: Not A-and-B

Prove that if we know ~(A ∧ B) and A are true, then ~B must be true.

~(A ∧ B) -> (A -> ~B)

#3: Contrapositive

Show that if we have an implication, the contrapositive must also be true:

(A -> B) -> (~B -> ~A)

#4: Propositional Resolution

Show the following property:

(A ∨ ~B) ∧ (B ∨ C) -> A ∨ C

Handing In

Run cs1950y_handin natdeduce from a directory containing your Coq proof file (NatDeduce.v). You should receive an email confirming that your handin has worked.