logicalmethods.ai – Logical proofs

Tutorial 7. Logical proofs

Exercise sheet

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.

A A (A B)
A (A B) A

Solution

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:
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

A (B C) (A B) (A C)
(A B) (A C) A (B C)
A (B C) (A B) (A C)
(A B) (A C) A (B C)

Negation

A A
A A
(A B) A B
A B (A B)
(A B) A B
A B (A B)

Conditionals

A B A B
A B A B
( A A) A
(A B) ( B A)
( B A) (A B)

Solution

Conjunction and Disjunction

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:
(A B) (A C) A (B C)
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:
(A B) (A C) A (B C)

Negation

A A

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

This is perhaps the most difficult one of this set.
A A

Note that this derivation requires classicality.
(A B) A B
A B (A B)
(A B) A B
A B (A B)

Conditionals

A B A B

This solution is interactive! Click through the slides to get an explanation of how to find the derivation:
A B A B
( A A) A
(A B) ( B A)
( 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 theorem’s like distribution_one_rtl require to be passed a proof term h.

Conjunction and Disjunction

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13


  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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19


  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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16


  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

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160


  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 plaground by following this link .

Interpreting Lean

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


  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.