Actema Actema
  • Courses
  • Docs
  • About

Courses

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

Equality

Exercises

  • Symmetry : a:(), b:(); a=b|- b=a
  • Transitivity: a:(), b:(), c:(); a=b, b=c |- a=c
  • Leibniz: P ::(), a:(); P(a) |- forall x:(). x=a -> P(x)
  • Dual: P ::(), a:(); forall x:(). x=a -> P(x) |- P(a)
  • Basic algebra: type A, type B, f : A->B, g : B -> A; forall y:B.f(g(y)) = y , forall x:A. exists y:B. x = g(y)|- forall x:A.g(f(x)) = x
© Actema 2021