∀x.∀y. (P x y) ⇒ (P y x)
F2
Write the formula that represents the fact that the predicate P is
transitive.
∀x.∀y.∀z. ((P x y) ∧ (P y z)) ⇒ (P x z)
or
∀x.∀y.∀z. (P x y) ⇒ (P y z) ⇒ (P x z)
F3
Write the formula that represents the fact that a function f with
one parameter is injective. One can assume the existence of an equality
predicate, written x=y.
∀x.∀y. (f x)=(f y) ⇒ x = y
F4
Write the formula that represents the fact that a function f with
one parameter is surjective.
∀y.∃x. y=(f x)
Natural Deduction
G1
Prove that
(∃x. ∀y. (P x y)) ⇒ (∀y. ∃x. (P x y)).
∃x. ∀y. (P x y)
∀y. (P a y) (P a c)
∃x. (P x c)
∃x. (P x c)
∀y. ∃x. (P x y)
(∃x. ∀y. (P x y)) ⇒ (∀y. ∃x. (P x y))
G2
Prove that
(∀y. ∃x. (P x y)) ⇒ (∃x. ∀y. (P x y)).
There is no such a proof.
G3
Prove that
(¬(∃x. (P x))) ⇒ (∀x. ¬(P x)).
(P c) ∃x. (P x)
¬(∃x. (P x)) False
¬(P c)
∀x. ¬(P x)
(¬(∃x. (P x))) ⇒ (∀x. ¬(P x))
G4
Prove that
(∀x. ¬(P x)) ⇒ ¬ (∃ x. (P x)).
∃x. (P x)
(P c)
∀x. ¬(P x) ¬(P c)
False
False
¬(∃x. (P x))
(∀x. ¬(P x)) ⇒ ¬ (∃x. (P x))
G5
Prove that (∃x. ¬(P x)) ⇒ ¬(∀x. (P x)).
∃x. ¬(P x)
∀x. (P x) (P c)
¬(P c) False
False
¬(∀x. (P x))
(∃x. ¬(P x)) ⇒ ¬(∀x. (P x))
G6
Prove in the classical logic that
¬(∀x. (P x)) ⇒ (∃x. ¬(P x)).
¬(P c) ∃x. ¬(P x)
¬(∃x. ¬(P x)) False
(P c)
∀x. (P x)
¬(∀x. (P x)) False
∃x. ¬(P x) ¬(∀x. (P x)) ⇒ (∃x. ¬(P x)) G7
Prove in the classical logic that
((∀x. (P x)) ⇒ Q) ⇒ ∃x. ((P x) ⇒ Q).
First suppose that ∀x. (P x) is true:
(∀x. (P x))⇒ Q
∀x. (P x)
Q
(P a) ⇒ Q
∃x. ((P x) ⇒ Q)
((∀x. (P x)) ⇒ Q) ⇒ ∃x. ((P x) ⇒ Q)
Second suppose that ¬(∀x. (P x)) is true, so by G1 we know that ∃x. ¬(P x) is true.
∃x. ¬(P x)
(P c) ¬(P c) False
Q
(P c) ⇒ Q
∃x. ((P x) ⇒ Q)
∃x. ((P x) ⇒ Q)
((∀x. (P x)) ⇒ Q) ⇒ ∃x. ((P x) ⇒ Q)
G8
Prove that
(∃x. ((P x) ⇒ Q)) ⇒ ((∀x. (P x)) ⇒ Q).
∃x. ((P x)⇒Q)
(P a)⇒Q
∀x. (P x) (P a)
Q
Q
(∀x. (P x)) ⇒ Q (∃x. ((P x) ⇒ Q)) ⇒ ((∀x. (P x)) ⇒ Q)
G9
Prove that
((∃x. (P x)) ⇒ Q) ⇒ ∀x. ((P x) ⇒ Q).
(∃x. (P x))⇒Q
(P c) ∃x. (P x)
Q (P c)⇒Q
∀x. ((P x) ⇒ Q) ((∃x. (P x)) ⇒ Q) ⇒ ∀x. ((P x) ⇒ Q)
G10
Prove that
(∀x. ((P x) ⇒ Q)) ⇒ ((∃x. (P x)) ⇒ Q).
∃x. (P x)
∀x. ((P x) ⇒ Q) (P c) ⇒ Q
(P c)
Q
Q
(∃x. (P x)) ⇒ Q (∀x. ((P x) ⇒ Q)) ⇒ ((∃x. (P x)) ⇒ Q)
G11
Prove that
(Q ⇒ (∀x. (P x))) ⇒ ∀x. (Q ⇒ (P x)) .
Q⇒ (∀x. ((P x))
Q
∀x. (P x)
(P c)
Q ⇒ (P c)
∀x. (Q ⇒ (P x))
(Q ⇒ (∀x. (P x))) ⇒ ∀x. (Q ⇒ (P x))
G12
Prove that
(∀x. (Q ⇒ (P x))) ⇒ (Q ⇒ (∀x. (P x))).
∀x. (Q ⇒ (P x)) Q ⇒ (P c)
Q (P c)
∀x. (P x)
Q ⇒ (∀x. (P x))
(∀x. (Q ⇒ (P x))) ⇒ (Q ⇒ (∀x. (P x)))
G13
Prove in classical logic that
(Q ⇒ (∃x. (P x))) ⇒ (∃x. (Q ⇒ (P x))).
Suppose that the proposition Q is true:
Q ⇒ (∃x. (P x))
Q
∃x.(P x)
(P c) Q ⇒ (P c)
∃x. (Q ⇒ (P x))
∃x. (Q ⇒ (P x))
(Q ⇒ (∃x. (P x))) ⇒ (∃x. (Q ⇒ (P x)))
Suppose that the proposition ¬Q is true:
Q ¬Q False
(P a)
Q ⇒ (P a)
∃x. (Q ⇒ (P x))
(Q ⇒ (∃x. (P x))) ⇒ (∃x. (Q ⇒ (P x)))
G14
Prove that
(∃x. Q ⇒ (P x)) ⇒ (Q ⇒ (∃x. (P x))).
∃x. (Q ⇒ (P x))
Q⇒ (P c)
Q
(P c)
∃x. (P x)
∃x. (P x)
Q ⇒ (∃x. (P x)) (∃x. Q ⇒ (P x)) ⇒ (Q ⇒ (∃x. (P x)))
G15
Prove that
((∀x. (P x)) ∨ Q) ⇒ (∀x. (P x) ∨ Q).
(∀x. (P x))∨ Q
∀x. (P x) (P c)
(P c) ∨ Q
∀x. ((P x) ∨ Q)
Q (P c) ∨ Q
∀x. ((P x) ∨ Q)
(∀x. ((P x) ∨ Q)
((∀x. (P x)) ∨ Q) ⇒ (∀x. ((P x) ∨ Q))
G16
Prove in classical logic that
(∀x. ((P x) ∨ Q)) ⇒ ((∀x. (P x)) ∨ Q.
Suppose that the proposition Q is true:
Q (∀x. (P x)) ∨ Q
(∀x. ((P x) ∨ Q)) ⇒ ((∀x. (P x)) ∨ Q)
Suppose that the proposition ¬Q is true:
(∀x. (P x))∨ Q
∀x. (P x) (∀x. (P x))∨ Q
Q ¬Q False
(∀x. ((P x)) ∨ Q
(∀x. (P x)) ∨ Q
(∀x. ((P x) ∨ Q)) ⇒ ((∀x. (P x)) ∨ Q)
G17
Prove that
((∃x. (P x)) ∨ Q) ⇒ ∃x. ((P x) ∨ Q).
(∃x. (P x))∨ Q
(∃x. (P x))
(P c) (P c) ∨ Q
∃x. ((P x) ∨ Q)
∃x. ((P x) ∨ Q)
Q (P a) ∨ Q
∃x. ((P x) ∨ Q)
(∃x. ((P x) ∨ Q)
((∃x. (P x)) ∨ Q) ⇒ (∃x. ((P x) ∨ Q))
G18
Prove that
(∃x. ((P x) ∨ Q)) ⇒ (∃x. (P x)) ∨ Q.
∃x. ((P x) ∨ Q))
(P c) ∨ Q
(P c) ∃x. (P x)
(∃x. (P x)) ∨ Q
Q (∃x. (P x)) ∨ Q
(∃x. (P x)) ∨ Q
(∃x. (P x)) ∨ Q
(∃x. ((P x) ∨ Q)) ⇒ (∃x. (P x)) ∨ Q
G19*
Prove that
(P a) ⇒ ((∀x. ((P x) ⇒ (Q x))) ⇒ (Q a)).
∀x. ((P x) ⇒ (Q x)) (P a) ⇒ (Q a)
(P a) (Q a)
(∀x. ((P x) ⇒ (Q x))) ⇒ (Q a) (P a) ⇒ ((∀x. ((P x) ⇒ (Q x))) ⇒ (Q a))
G20*
Prove that
(∃x. ((P x) ⇒ (Q x))) ⇒ ((∀x. (P x)) ⇒ (∃x. (Q x))).
∃x. ((P x) ⇒ (Q x))
∃x. ((P x) ⇒ (Q x))
∀x. (P x) (P c)
(Q c)
∃x. (Q x)
∃x. (Q x)
(∀x. (P x)) ⇒ (∃x. (Q x)) (∃x. ((P x) ⇒ (Q x))) ⇒ ((∀x. (P x)) ⇒ (∃x. (Q x)))
*G21
Prove that
(∀x. (P x) ⇒ (Q x)) ⇒ ((∃x. (P x)) ⇒ (∃x. (Q x))) .
∃x. (P x)
∀x. ((P x) ⇒ (Q x)) (P c) ⇒ (Q c)
(P c) (Q c)
∃x. (Q x)
∃x. (Q x) (∃x. (P x)) ⇒ (∃x. (Q x))
(∀x. (P x) ⇒ (Q x)) ⇒ ((∃x. (P x)) ⇒ (∃x. (Q x))) *G22
Prove that
(∃x. ((P x) ∧ (Q x))) ⇒ (∃x. ((Q x) ∧ (P x))).
∃x. ((P x) ∧ (Q x))
(P c) ∧ (Q c) (Q c)
(P c) ∧ (Q c) (P c)
(Q c) ∧ (P c) ∃x. ((Q x) ∧ (P x))
∃x. ((Q x) ∧ (P x))
(∃x. ((P x) ∧ (Q x))) ⇒ (∃x. ((Q x) ∧ (P x)))