Quantifiers

Exercises

• P::(), A, B, C, D; forall x:().~P(x) |- ~exists y:().P(y)

Existential

• F1 :: (), F2 :: () |- (forall x : (). F1(x) -> F2(x)) -> (exists x : (). F1(x)) -> (exists x : (). F2(x))
• P :: (), Q :: () |- (exists x : (). P(x) && Q(x)) -> (exists y : (). Q(y) && P(y))

Syllogisms

• a : (), P :: (), Q :: () |- (forall x : (). P(x) -> Q(x)) -> (P(a) -> Q(a))
• P :: (), Q :: (), R :: () |- (forall x : (). P(x) -> Q(x)) -> (forall x : (). Q(x) -> R(x)) -> (forall x : (). P(x) -> R(x))
• P :: (), Q :: (), R :: () |- (exists x : (). P(x) -> Q(x)) -> (forall x : (). Q(x) -> R(x)) -> (exists x : (). P(x) -> R(x))
• P :: (), Q :: (), R :: () |- (forall x : (). P(x) -> Q(x)) -> (exists x : (). Q(x) -> R(x)) -> (exists x : (). P(x) -> R(x))