WEEK 9 :: Homework

Using ∃LOGIC construct annotated derivations showing that the following arguments are valid.


3:12 ∃y∀x(Fx↔Fy). ∃xFx ∴ ∀xFx

3:13 ∀x((Fx ∧ (Gx ∨ Hx)) → Jx). ∀x((Jx ∧ Hx) → Kx). ∀x(Lx → Hx) ∴ ∀x((Fx ∧ Lx) → Kx)

3:14 ∀x(Fx ↔ (Gx ∨ Hx)). ∃xGx. ∀x(Fx → ∀xHx) ∴ ∀xFx

3:15 ∀x(Fx → Gx). ∃x((Fx ∧ Hx) ∨ (Fx ∧ Jx)) → ¬∀x(Fx → Gx) ∴ ∀x(Fx → ¬Jx)

3:16 ∃x(Fx ∧ ¬Gx) → ∀x(Fx → Hx). ∃x(Fx ∧ Jx) ∴ ∀x(Fx → ¬Hx) → ∃x(Jx ∧ Gx)

3:17 ¬∃x(Fx ∧ (Gx ∨ Hx)). ∃x(Ix ∧ Fx). ∀x(¬Hx → Jx) ∴ ∃x(Ix ∧ Jx)

3:18 ∀x(Fx → ∀xGx) ∴ ∀x(Fx → ∀x(Gx ∨ Hx))

3:19 ∃xFx → ∀xGx. ∀x(Gx ∨ Hx)→∀xJx ∴ ∀x(Fx → Jx)

3:40 ∃y∀x(Fx ↔ Fy) . ∃xFx ∴ ∀xFx

3:43 ∃y∀x(Fx ∧ Gy) ∴ ∀x∃y(Fx ∧ Gy)

3:44 T201 ∴ ∀x(Fx → Gx) → (∀xFx → ∀xGx)

3:47 T204 ∴ ¬∃xFx ↔ ∀x¬Fx

3:48 T205 ∴ ∀xFx ↔ ¬∃x¬Fx

3:49 T206 ∴ ∃xFx ↔ ¬∀x¬Fx

3:80 T238 ∴ ∀xFx → ∃xFx

3:104 ∀x(Fx ↔ (¬Gx ∨ ¬Hx)). ¬∀x(Gx ∧ Hx) → ∃x(Ix ∧ ¬Gx) ∴ ∃xFx → ∃x(Ix ∧ Fx)

3:125 ∃x(Fx → ∀xGx) ∴ ∃x∃y(¬Fx ∨ Gy)

3:129 ∴ ∀y∃x(Fy ∧ Gx) → ∃x(Gx ∧ Fx)    

http://www.elogic.brianrabern.net/