Theory of proveit.logic

Theory dealing with basic logic concepts: boolean arithmetic, equality, and set theory.

import proveit
%theory

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

booleans	Boolean arithmetic operations: implication, negation, conjunction, disjunction, and universal/existential quantification.
equality	Equals, not equals, and various forms of substitution.
sets	Basic theory of sets.
classes	Classes are collections of sets.

All axioms contained within this theory

This theory contains no axioms directly.

proveit.logic.booleans

proveit.logic.booleans.true_axiom

proveit.logic.booleans.bools_def

proveit.logic.booleans.false_not_true

proveit.logic.booleans.eq_true_intro

proveit.logic.booleans.eq_true_elim

proveit.logic.booleans.implication.implies_t_f

proveit.logic.booleans.implication.affirmation_via_contradiction

proveit.logic.booleans.implication.denial_via_contradiction

proveit.logic.booleans.implication.iff_def

proveit.logic.booleans.negation.not_t

proveit.logic.booleans.negation.not_f

proveit.logic.booleans.negation.negation_elim

proveit.logic.booleans.negation.operand_is_bool

proveit.logic.booleans.conjunction.and_t_t

proveit.logic.booleans.conjunction.and_t_f

proveit.logic.booleans.conjunction.and_f_t

proveit.logic.booleans.conjunction.and_f_f

proveit.logic.booleans.conjunction.left_in_bool

proveit.logic.booleans.conjunction.right_in_bool

proveit.logic.booleans.conjunction.empty_conjunction

proveit.logic.booleans.conjunction.multi_conjunction_def

proveit.logic.booleans.disjunction.or_t_t

proveit.logic.booleans.disjunction.or_t_f

proveit.logic.booleans.disjunction.or_f_t

proveit.logic.booleans.disjunction.or_f_f

proveit.logic.booleans.disjunction.left_in_bool

proveit.logic.booleans.disjunction.right_in_bool

proveit.logic.booleans.disjunction.empty_disjunction

proveit.logic.booleans.disjunction.multi_disjunction_def

proveit.logic.booleans.quantification.universality.forall_in_bool

proveit.logic.booleans.quantification.existence.exists_def

proveit.logic.booleans.quantification.existence.not_exists_def

proveit.logic.equality

proveit.logic.equality.equality_in_bool

proveit.logic.equality.equals_transitivity

proveit.logic.equality.equals_reflexivity

proveit.logic.equality.equals_symmetry

proveit.logic.equality.not_equals_def

proveit.logic.equality.substitution

proveit.logic.sets

proveit.logic.sets.membership.not_in_set_def

proveit.logic.sets.equivalence.set_equiv_def

proveit.logic.sets.equivalence.set_not_equiv_def

proveit.logic.sets.enumeration.enum_set_def

proveit.logic.sets.enumeration.empty_set_def

proveit.logic.sets.inclusion.subset_eq_def

proveit.logic.sets.inclusion.not_subset_eq_def

proveit.logic.sets.inclusion.proper_subset_def

proveit.logic.sets.inclusion.not_proper_subset_def

proveit.logic.sets.unification.union_def

proveit.logic.sets.unification.union_all_def

proveit.logic.sets.intersection.intersection_def

proveit.logic.sets.intersection.intersect_all_def

proveit.logic.sets.subtraction.difference_def

proveit.logic.sets.comprehension.comprehension_def

proveit.logic.sets.power_set.power_set_def

proveit.logic.sets.cartesian_products.cart_prod_def

proveit.logic.sets.cartesian_products.cart_exp_def

proveit.logic.sets.disjointness.vacuously_disjoint

proveit.logic.sets.disjointness.disjoint_pair_def

proveit.logic.sets.disjointness.disjoint_induction

proveit.logic.sets.disjointness.distinct_def

proveit.logic.sets.cardinality.empty_card

proveit.logic.sets.cardinality.card_induction

proveit.logic.sets.functions.functions_def

proveit.logic.sets.functions.images.set_image_def

proveit.logic.sets.functions.injections.injective_def

proveit.logic.sets.functions.surjections.surjective_def

proveit.logic.sets.functions.bijections.bijective_def

proveit.logic.classes

proveit.logic.classes.membership.not_in_class_def