Actema Actema
  • Courses
  • Docs
  • About

Courses

  • Introduction
  • Propositional logic
    • Conjunction
    • Disjunction
    • Negation
  • Predicate logic
    • Quantifiers
    • Equality
  • Theories
    • Peano arithmetic
    • Edukera

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))
© Actema 2021