Tutorial 7

Logical proofs

Exercise sheet 4 questions

Proof systems

Let’s trial run the different proof systems. For each of the following, provide a logical proof in our Hilbert calculus, sequent calculus, and tableaux.

  1. A ⊢ A ∨(A∧B)

  2. A ∨(A∧B) ⊢A

Solution

  1. Here we go:

    • Hilbert:

      1. A (Premise)
      2. A → (A ∨ (A ∧ B)) (Axiom 6 with B = A ∧ B)
      3. (A ∨ (A ∧ B)) (1., 2., MP)

    • Sequent:

    • Tableaux:

  2. Here we go:

    • Hilbert:

      1. A ∨(A ∧ B) (Premise)

      2. (A →A) → (((A ∧ B) → A)→((A ∨(A ∧ B))→ A)) (Axiom 7.)

      3. (A →A) (Theorem from textbook)

      4. ((A ∧ B) → A)→((A ∨(A ∧ B))→ A)(2., 3., MP)

      5. (A ∧ B) → A) (Axiom 5.)

      6. ((A ∨(A ∧ B))→ A)(4., 5., MP)

      7. A (1., 6., MP)

    • Sequent:

    • Tableaux:

Natural deduction

For this exercise, you do a deep dive into natural deduction: below are a series of laws to prove for arbitrary formulas A,B,C. Some require the rule ¬⊥, take note of which ones.

Conjunction and Disjunction

  1. A ∨ (B ∧ C) ⊢ (A ∨ B)∧(A ∨ C)

  2. (A ∨ B)∧(A ∨ C)⊢ A ∨ (B ∧ C)

  3. A ∧ (B ∨ C) ⊢ (A ∧ B)∨(A ∧ C)

  4. (A ∧ B)∨(A ∧ C)⊢ A∧ (B ∨ C)

Negation

  1. A ⊢¬¬ A

  2. ¬¬ A⊢ A

  3. ¬(A ∧B) ⊢ ¬A ∨¬B

  4. ¬A ∨¬B ⊢ ¬(A ∧B)

  5. ¬(A ∨B) ⊢ ¬A ∧¬B

  6. ¬A ∧¬B ⊢ ¬(A ∨B)

Conditionals

  1. ¬A ∨ B⊢A→B

  2. A → B ⊢¬A ∨ B

  3. (¬A→ A) ⊢ A

  4. (A→B)⊢(¬B →¬A)

  5. (¬B →¬A)⊢(A → B)

Solution

Conjunction and Disjunction

  1. A ∨ (B ∧ C) ⊢ (A ∨ B)∧(A ∨ C)

    This solution is interactive! Click through the slides to get an explanation of how to find the derivation:

    These slides live on link.excalidraw.com

    Loading them tells that server your IP address. Nothing is sent until you press the button.

    The deck is hosted on Excalidraw. If it does not load, or you would rather view it full screen: Open the slides

  2. (A ∨ B)∧(A ∨ C)⊢ A ∨ (B ∧ C)

  3. A ∧ (B ∨ C) ⊢ (A ∧ B)∨(A ∧ C)

    This solution is interactive! Click through the slides to get an explanation of how to find the derivation:

    These slides live on link.excalidraw.com

    Loading them tells that server your IP address. Nothing is sent until you press the button.

    The deck is hosted on Excalidraw. If it does not load, or you would rather view it full screen: Open the slides

  4. (A ∧ B)∨(A ∧ C)⊢ A∧ (B ∨ C)

Negation

  1. A ⊢¬¬ A

    This solution is interactive! Click through the slides to get an explanation of how to find the derivation:

    These slides live on link.excalidraw.com

    Loading them tells that server your IP address. Nothing is sent until you press the button.

    The deck is hosted on Excalidraw. If it does not load, or you would rather view it full screen: Open the slides

    This is perhaps the most difficult one of this set.

  2. ¬¬ A⊢ A

    Note that this derivation requires classicality.

  3. ¬(A ∧B) ⊢ ¬A ∨¬B

  4. ¬A ∨¬B ⊢ ¬(A ∧B)

  5. ¬(A ∨B) ⊢ ¬A ∧¬B

  6. ¬A ∧¬B ⊢ ¬(A ∨B)

Conditionals

  1. ¬A ∨ B⊢A→B

    This solution is interactive! Click through the slides to get an explanation of how to find the derivation:

    These slides live on link.excalidraw.com

    Loading them tells that server your IP address. Nothing is sent until you press the button.

    The deck is hosted on Excalidraw. If it does not load, or you would rather view it full screen: Open the slides

  2. A → B ⊢¬A ∨ B

  3. (¬A→ A) ⊢ A

  4. (A→B)⊢(¬B →¬A)

  5. (¬B →¬A)⊢(A → B)

Lean verification

For this exercise, you verify your natural deduction inferences using Lean. Below are templates for the code to use. The proofs are replaced by sorry, which makes Lean not complain about the missing proof. The sorry-tactic is very useful when writing a proof, because it makes Lean “shut up”, while allowing you to type your proof. You need to replace each sorry with the correct proof, of course.

Note that some of the proofs below require open Classical. Which ones?

In your proofs, you can use previous theorems using apply. Note that theorems like distribution_one_rtl need to be passed a proof term h.

Conjunction and Disjunction

  variable (A B C : Prop)

  theorem distribution_one_ltr (h : (A ∧ (B ∨ C))) : (A ∧ B) ∨ (A ∧ C) := by
    sorry

  theorem distribution_one_rtl (h : (A ∧ B) ∨ (A ∧ C) ) : (A ∧ (B ∨ C)) := by
    sorry

  theorem distribution_two_ltr (h : (A ∨ (B ∧ C))) : (A ∨ B) ∧ (A ∨ C) := by
    sorry

  theorem distribution_two_rtl (h : (A ∨ B) ∧ (A ∨ C) ) : (A ∨ (B ∧ C)) := by
    sorry

Click this link to open the browser playground.

Negation:

  variable (A B : Prop)

  theorem double_negation_ltr (h: ¬¬ A) : A := by
    sorry

  theorem double_negation_rtl (h : A) : ¬¬ A := by
    sorry

  theorem de_morgan_one_ltr (h : ¬(A ∧ B)) : (¬ A ∨ ¬ B) := by
    sorry

  theorem de_morgan_one_rtl (h : (¬ A ∨ ¬ B)) : ¬(A ∧ B) := by
    sorry

  theorem de_morgan_two_ltr (h : ¬(A ∨ B)) : (¬ A ∧ ¬ B) := by
    sorry

  theorem de_morgan_two_rtl (h : (¬ A ∧ ¬ B)) :  ¬(A ∨ B) := by
    sorry

Click this link to open the browser playground.

Conditionals

  variable (A B : Prop)

  theorem cond_def_ltr (h : ¬A ∨ B) : A → B := by
    sorry

  theorem cond_def_rtl (h : A → B ) : ¬A ∨ B  := by
    sorry

  theorem consequentia_mirabilis (h : ¬ A → A) : A := by
    sorry

  theorem contrapos_ltr (h : A → B) : ¬B → ¬A := by
    sorry

  theorem contrapos_rtl (h: ¬B → ¬A) : A → B := by
    sorry

Click this link to open the browser playground.

Solution

Credit: Alexander Apers

  variable (A B C : Prop)

  theorem distribution_one_ltr (h : (A ∧ (B ∨ C))) : (A ∧ B) ∨ (A ∧ C) := by
    apply Or.elim (And.right h)
    · intro b
      apply Or.inl
      apply And.intro
      · exact And.left h
      · exact b
    · intro c
      apply Or.inr
      apply And.intro
      · exact And.left h
      · exact c

  theorem distribution_one_rtl (h : (A ∧ B) ∨ (A ∧ C) ) : (A ∧ (B ∨ C)) := by
    apply And.intro
    apply Or.elim h
    · intro a_and_b
      apply And.left a_and_b
    · intro a_and_c
      apply And.left a_and_c
    apply Or.elim h
    · intro a_and_b
      apply Or.inl
      apply And.right a_and_b
    · intro a_and_c
      apply Or.inr
      apply And.right a_and_c

  theorem distribution_two_ltr (h : (A ∨ (B ∧ C))) : (A ∨ B) ∧ (A ∨ C) := by
    apply And.intro
    apply Or.elim h
    · intro a
      apply Or.inl a
    · intro b_and_c
      apply Or.inr
      · exact And.left b_and_c
    apply Or.elim h
    · intro a
      apply Or.inl a
    · intro b_and_c
      apply Or.inr
      · exact And.right b_and_c

  theorem distribution_two_rtl (h : (A ∨ B) ∧ (A ∨ C) ) : (A ∨ (B ∧ C)) := by
    apply Or.elim (And.left h)
    · intro a
      apply Or.inl a
    · intro b
      apply Or.elim (And.right h)
      · intro a
        apply Or.inl a
      · intro c
        apply Or.inr
        apply And.intro
        · exact b
        · exact c

  open Classical

  variable (A B : Prop)

  theorem double_negation_ltr (h: ¬¬ A) : A := by
    apply byContradiction
    apply h

  theorem double_negation_rtl (h : A) : ¬¬ A := by
    intro a
    apply a
    exact h

  theorem de_morgan_one_ltr (h : ¬(A ∧ B)) : (¬ A ∨ ¬ B) := by
    apply byContradiction
    intro neg_goal
    apply h
    apply And.intro
    apply byContradiction
    intro neg_a
    apply neg_goal
    apply Or.inl neg_a
    apply byContradiction
    intro neg_b
    apply neg_goal
    apply Or.inr neg_b

  theorem de_morgan_one_rtl (h : (¬ A ∨ ¬ B)) : ¬(A ∧ B) := by
    apply Or.elim h
    · intro neg_a
      · intro a_and_b
        apply neg_a
        apply And.left a_and_b
    · intro neg_b
      · intro a_and_b
        apply neg_b
        apply And.right a_and_b

  theorem de_morgan_two_ltr (h : ¬(A ∨ B)) : (¬ A ∧ ¬ B) := by
    apply And.intro
    · intro a
      apply h
      apply Or.inl a
    · intro b
      apply h
      apply Or.inr b

  theorem de_morgan_two_rtl (h : (¬ A ∧ ¬ B)) :  ¬(A ∨ B) := by
    intro a_or_b
    apply Or.elim a_or_b
    · intro a
      apply And.left h
      exact a
    · intro b
      apply And.right h
      exact b

  variable (A B : Prop)

  theorem cond_def_ltr (h : ¬A ∨ B) : A → B := by
    intro a
    apply Or.elim h
    · intro neg_a
      apply False.elim
      apply neg_a
      exact a
    · intro b
      exact b

  theorem cond_def_rtl (h : A → B ) : ¬A ∨ B  := by
    apply byContradiction
    intro neg_goal
    · apply neg_goal
      apply Or.inl
      · intro a
        apply neg_goal
        apply Or.inr
        apply h
        exact a

  theorem consequentia_mirabilis (h : ¬ A → A) : A := by
    apply byContradiction
    intro neg_a
    apply neg_a
    apply h
    apply neg_a

  theorem contrapos_ltr (h : A → B) : ¬B → ¬A := by
    intro neg_b
    · intro a
      apply neg_b
      apply h
      exact a

  theorem contrapos_rtl (h: ¬B → ¬A) : A → B := by
    intro a
    apply byContradiction
    · intro neg_b
      apply h
      apply neg_b
      exact a

You can review the code in the Lean playground by following this link .

Interpreting Lean

Consider the following two Lean proofs. Translate them into natural deduction proofs:

  variable (A B : Prop)

  theorem absorption_one_ltr : (A ∧ (A ∨ B)) → A := by
    intro h
    apply And.left 
    exact h

  theorem absorption_one_rtl : A → (A ∧ (A ∨ B)) := by
    intro hA
    apply And.intro
    · exact hA
    · exact Or.inl hA

Click this link to open the browser playground.

Solution