Metamath Proof Explorer


Logic can be defined as the "study of the principles of correct reasoning" (Merrilee H. Salmon's 1991 "Informal Reasoning and Informal Logic" in Informal Reasoning and Education) or as "a formal system using symbolic techniques and mathematical methods to establish truth-values" (the Oxford English Dictionary).

This section formally defines the logic system we will use. In particular, it defines symbols for declaring truthful statements, along with rules for deriving truthful statements from other truthful statements. The system defined here is classical first-order logic (often abbreviated as FOL) with equality and no terms (the most common logic system used by mathematicians).

We begin with a few housekeeping items in pre-logic, and then introduce propositional calculus (both its axioms and important theorems that can be derived from them). Propositional calculus deals with general truths about well-formed formulas (wffs) regardless of how they are constructed. This is followed by proofs that other axiomatizations of classical propositional calculus can be derived from the axioms we have chosen to use.

We then define predicate calculus, which adds additional symbols and rules useful for discussing objects (beyond simply true or false). In particular, it introduces the symbols ("equals"), ("is a member of"), and ("for all"). The first two are called "predicates". A predicate specifies a true or false relationship between its two arguments.

  1. Pre-logic
    1. Inferences for assisting proof development
  2. Propositional calculus
    1. Recursively define primitive wffs for propositional calculus
    2. The axioms of propositional calculus
    3. Logical implication
    4. Logical negation
    5. Logical equivalence
    6. Logical conjunction
    7. Logical disjunction
    8. Mixed connectives
    9. The conditional operator for propositions
    10. The weak deduction theorem for propositional calculus
    11. Abbreviated conjunction and disjunction of three wff's
    12. Logical "nand" (Sheffer stroke)
    13. Logical "xor"
    14. Logical "nor"
    15. True and false constants
    16. Truth tables
    17. Half adder and full adder in propositional calculus
  3. Other axiomatizations related to classical propositional calculus
    1. Minimal implicational calculus
    2. Implicational Calculus
    3. Derive the Lukasiewicz axioms from Meredith's sole axiom
    4. Derive the standard axioms from the Lukasiewicz axioms
    5. Derive Nicod's axiom from the standard axioms
    6. Derive the Lukasiewicz axioms from Nicod's axiom
    7. Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom
    8. Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms
    9. Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom
    10. Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom
    11. Derive the Lukasiewicz axioms from the Russell-Bernays Axioms
    12. Stoic logic non-modal portion (Chrysippus of Soli)
  4. Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
    1. Universal quantifier (continued); define "exists" and "not free"
    2. Rule scheme ax-gen (Generalization)
    3. Axiom scheme ax-4 (Quantified Implication)
    4. Axiom scheme ax-5 (Distinctness) - first use of $d
    5. Equality predicate (continued)
    6. Axiom scheme ax-6 (Existence)
    7. Axiom scheme ax-7 (Equality)
    8. Define proper substitution
    9. Membership predicate
    10. Axiom scheme ax-8 (Left Equality for Binary Predicate)
    11. Axiom scheme ax-9 (Right Equality for Binary Predicate)
    12. Logical redundancy of ax-10 , ax-11 , ax-12 , ax-13
  5. Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
    1. Axiom scheme ax-10 (Quantified Negation)
    2. Axiom scheme ax-11 (Quantifier Commutation)
    3. Axiom scheme ax-12 (Substitution)
    4. Axiom scheme ax-13 (Quantified Equality)
    5. Alternate definition of substitution
  6. Uniqueness and unique existence
    1. dfmoeu
    2. dfeumo
    3. Uniqueness: the at-most-one quantifier
    4. Unique existence: the unique existential quantifier
  7. Other axiomatizations related to classical predicate calculus
    1. Aristotelian logic: Assertic syllogisms
    2. Intuitionistic logic