PREDICATE CALCULUS IN-CLASS EXERCISES
State the rules of inference and replacement used in the following proofs:
Example
1. ∀x(Fx → Gx)
2. Ǝx(Fx & Hx) / ˫ Ǝx (Hx & Gx)
3. Fa & Ha [2 ƎE]
4. Fa → Ga [1 ∀E]
5. Fa [3 &E SIMP]
6. Ga [4, 5 →E MP]
7. Ha & Fa [3 COM]
8. Ha [7 &E SIMP]
9. Ha & Ga [8 &I CONJ]
10. ˫ Ǝx (Hx & Gx) [9 ƎI]
(1)
1. ∀x(Fx → Gx) / ˫ Ǝx[~Fx v (Gx v Hx)]
2. Fa → Ga [1 ∀E]
3. ~Fa v Ga [2 MI]
4. (~Fa v Ga) v Ha [3 ADD (vI)]
5. ~Fa v (Ga v Ha) [4 ASSOC]
6. ˫ Ǝx[~Fx v (Gx v Hx)] [5 ƎI]
(2)
1. Ǝx(~Fx)
2. Ǝx (~Gx) / ˫ Ǝx(Fx ↔ Gx)
3. ~Fa [1 ƎE]
4. ~Ga [2 ƎE]
5. ~Fa & ~Ga [3, 4 CONJ (&I)]
6. (Fa & Ga) v (~Fa & ~Ga) [5 ADD (vI)]
7. Fa ↔ Ga [6 ME (↔I)]
8. ˫ Ǝx(Fx ↔ Gx) [7 ƎI]
Adding one or two statements to the premises will produce a formal proof of validity. Supply the statement and indicate the rule:
Example
1. Fy / ˫ ∀x(Fx)
2. ˫ ∀x(Fx) [1 ∀I (UG)]
(3)
1. ∀x(Fx) / ˫ Fy
2. ˫ Fy [1 ∀E (UI)]
(4)
1. Ǝx(Fx) / ˫ Fa
2. ˫ Fa [1 ƎE (EI)]
(5)
1. ∀x(Fx) / ˫ Ǝx(Fx)
2. Fy [1 ∀E (UI)]
3. ˫ Ǝx(Fx) [2 ƎI (EU)]
Adding two or three statements to the premises will produce a formal proof of validity. Supply these statements and indicate the rules of inference and replacement used:
Example
1. ∀x(Fx → Gx)
2. Fa / ˫ Ga
3. Fa → Ga [1 ∀E]
4. ˫ Ga [3, 2 MP (→E)]
(6)
1. ∀x (Fx → Gx) / ˫ ~Ga → ~Fa
2. Fa → Ga [1 ∀E (UI)]
3. ˫ ~Ga → ~Fa [2 TRANS]
(7)
1. ∀x (Fx → Gx) / ˫ ∀x(~Gx → ~Fx)
2. Fy → Gy [1 ∀E (UI)]
3. ~Gy → ~Fy [2 TRANS]
4. ˫ ∀x(~Gx → ~Fx) [4 ∀I (UG)]
(8)
1. ∀x(Fx → Gx)
2. Fy / ˫ ∀x(Gx)
3. Fy → Gy [1 ∀E (UI)]
4. Gy [3, 2 MP (→E)]
5. ˫ ∀x (Gx) [4 ∀I (UG)]
(9)
1. ∀x(Fx → Gx) / ˫ ∀x(~Fx v Gx)
2. Fy → Gy [1 ∀E (UI)]
3. ~Fy v Gy [2 MI]
4. ˫ ∀x(~Fx v Gx) [3 ∀I (UG)
(10)
1. ∀x(Fx → Gx)
2. ∀x(Gx → Hx) / ˫ ∀x(Fx → Hx)
3. Fy → Gy [1 ∀E]
4. Gy → Hy [2 ∀E]
5. (Fy → Hy) [3, 4 HS]
6. ˫ ∀x(Fx → Hx) [5 ∀I]
(11)
1. ∀x (~Fx → ~Gx) / ˫ Ǝx (~Gx v Fx)
2. ~Fa → ~Ga [1 ∀E]
3. Ga → Fa [2 TRANS]
4. ~Ga v Fa [3 MI]
5. ˫ Ǝx (~Gx v Fx) [4 ƎI (EG)]
(12)
1. Ǝx(~Fx v ~Gx) / ˫ Ǝx~(Fx & Gx)
2. ~Fa v ~Ga [1 ƎE]
3. ~(Fa & Ga) [2 DM]
4. ˫ Ǝx~(Fx & Gx) [3 ƎI (EG)]
(13)
1. Ǝx(~Fx) / ˫ Ǝx~(Fx & Gx)
2. ~Fa [1 ∀E]
3. ~Fa v ~Ga [2 ADD (vI)]
4. ~(Fa & Ga) [3 DM]
5. ˫ Ǝx~(Fx & Gx) [4 ƎI (EG)]
(14)
1. Ǝx (Fx & Gx)
2. Fa → (Ga → Ha) / ˫ Ǝx (Hx)
3. Fa & Ga [1 ƎE]
4. (Fa & Ga) → Ha [2 EXP]
5. Ha [4, 3 MP (→E)]
6. ˫ Ǝx(Hx) [5 ƎI (EG)]
(15)
1. ∀x(~Gx → ~Fx)
2. Ǝx(Fx) / ˫ Ǝx(Gx)
3. ~Ga → ~Fa [1 ∀E]
4. Fa → Ga [3 TRANS]
5. Fa [2 ƎE]
6. Ga [4, 5 MP (→E)]
7. ˫ Ǝx(Gx) [6 ƎI (EG)]
The following examples involve relational predicates. Adding three statements to the premises will produce a formal proof of validity. Supply these statements and indicate the rules of inference and replacement used.
Example
1. Ǝx Ǝy(Fxy & Fyx) / ˫ Fba
2. Ǝy(Fay & Fya) [1 ƎE (EI)]
3. Fab & Fba [2 ƎE (EI)]
4. Fba [3 SIMP (&E)]
(16)
1. ∀x ∀y(Fxy → Fyx)
2. Fab / ˫ Fba
3. ∀y (Fay → Fya) [1 ∀E (UI)]
4. Fab → Fba [3 ∀E (UI)]
5. ˫ Fba [4, 2 MP (→E)]
(17)
1. ∀x(Fx → Gx)
2. Fa
3. a=b / ˫ Gb
4. Fa → Ga [1 ∀E (UI)]
5. Ga [2, 4 MP (→E)]
6. ˫ Gb [3, 5 ID]