Solution to CS375 Homework Assignment 3 (40 points)
Due Date: October 2, 2014
1. Give a formal proof for the following tautology by using the CP rule. Do not use the IP rule.
(B → C) → (B → A ∨ C) (8 points).
Proof:
1
2
3
4
5
P
P[for B → A ∨ C]
1,2, MP
3, Add
2,4, CP
1,5, CP
B→C
B
C
A∨C
B →A∨C
QED
2. Give a formal proof for the following tautology by using the CP rule and by using the IP rule
at least once in the proof. (B → C) → (B → A ∨ C) (8 points).
Proof:
1
2
3
4
5
6
7
8
9
B→C
B
¬(A ∨ C)
¬A ∧ ¬C
¬C
¬B
False
A∨C
B →A∨C
QED
P
P[for B → A ∨ C]
P[for A ∨ C]
3, DM
4, Simp
1,5, MT
2,6, Contr
3,7, IP
2,8, CP
1,9, CP
3. Prove the following basic property of conjunction. B ∧ False ≡ False (8 points).
Proof of B ∧ False → False:
1
2
B ∧ False
False
QED
P
1, Simp
1,2, CP
Proof of False → B ∧ False:
1
1
2
3
4
5
6
F alse
¬(B ∧ False)
¬B∨True
True
False
B ∧ False
QED
P
P[for B ∧ False]
2, DM
3, Basic
1,4, Contr
2,5 IP
1,6, CP
4. Prove the following basic property of disjunction. B ∨ False ≡ B (8 points).
Proof of B ∨ False → B:
1
2
3
4
P
P[for B]
1,2, DS
2,3, IP
1,4, CP
B ∨ False
¬B
False
B
QED
Proof of B → B ∨ False:
1
2
B
B ∨ False
QED
P
1, Add
1-2, CP
5. In Frege’s axiom system (6.12), prove (¬A → ¬B) → (B → A) (8 points).
Proof: Note that CP can be proved using Axioms 1 and 2 of F-L axiom system and these
axioms are exactly the same as the first two axioms of Frege’s axiom system, hence, CP can
be used for Frege’s axiom system as well.
With CP, we can also do a simple proof of the Hypothetical Syllogism (HS) as follows:
(A → B) ∧ (B → C) → (A → C)
1
2
3
4
5
6
A→B
B→C
A
B
C
A→C
QED
P
P
P[for A → C]
1,3, MP
2,4, MP
3,5, CP
1,2,6 CP
This means we can use CP and HS for both F-L and Frege’s axiom systems. The proof of this
problem is shown below.
2
1
2
3
4
5
6
7
¬A → ¬B
(¬A → ¬B) → (¬¬B → ¬¬A)
¬¬B → ¬¬A
¬¬A → A
¬¬B → A
B → ¬¬B
B→A
QED
P
Axiom 4
1-2, MP
Axiom 5
3,4 HS
Axiom 6
6,5 HS
1,7 CP
Solutions must be typed (word processed) and submitted by email as a pdf file to your grader
at: [email protected] before 23:59 on 10/2/2014.
3

Movable Objects (1) Movable Objects (2) Movable Objects (3

Jaguar Land Rover EMC Approved Lab

タップでジャンプするための処理