Top-level context.


The database covers currently a greater part of the first 1400 theorems of the file by Norman Megill, splitted into several 'modules'. The following diagram lists the dependencies between these modules; solid line means the axioms and theorems of the referred module are assumed ('imported'); dotted line means that an interpretation for the axioms is provided and the theorems are used ('exported'). For example, the general transitivity theorems in equiv are used in equ for the equality relation between sets.

The following modules are defined:

equEquality and Substitution
equ-axAxioms for equality and substitution.
equivEquivalence relations.
equiv-axAxioms for equivalence relations
extent-axAxiom of Extensionality
orderPartial order relations
order-axAxioms for partial order relations
predPure predicate calculus.
pred-axAxioms for predicate calculus.
propPropositional Calculus.
prop-axAxioms and definitions for propositional calculus.
set-extent-axAxiom of Extensionality (for sets)
uniqueExists unique, exists at most one