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.

- Pre-logic
- Propositional calculus
- Recursively define primitive wffs for propositional calculus
- The axioms of propositional calculus
- Logical implication
- Logical negation
- Logical equivalence
- Logical conjunction
- Logical disjunction
- Mixed connectives
- The conditional operator for propositions
- The weak deduction theorem for propositional calculus
- Abbreviated conjunction and disjunction of three wff's
- Logical "nand" (Sheffer stroke)
- Logical "xor"
- Logical "nor"
- True and false constants
- Truth tables
- Half adder and full adder in propositional calculus

- Other axiomatizations related to classical propositional calculus
- Minimal implicational calculus
- Implicational Calculus
- Derive the Lukasiewicz axioms from Meredith's sole axiom
- Derive the standard axioms from the Lukasiewicz axioms
- Derive Nicod's axiom from the standard axioms
- Derive the Lukasiewicz axioms from Nicod's axiom
- Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom
- Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms
- Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom
- Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom
- Derive the Lukasiewicz axioms from the Russell-Bernays Axioms
- Stoic logic non-modal portion (Chrysippus of Soli)

- Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)
- Universal quantifier (continued); define "exists" and "not free"
- Rule scheme ax-gen (Generalization)
- Axiom scheme ax-4 (Quantified Implication)
- Axiom scheme ax-5 (Distinctness) - first use of $d
- Equality predicate (continued)
- Axiom scheme ax-6 (Existence)
- Axiom scheme ax-7 (Equality)
- Define proper substitution
- Membership predicate
- Axiom scheme ax-8 (Left Equality for Binary Predicate)
- Axiom scheme ax-9 (Right Equality for Binary Predicate)
- Logical redundancy of ax-10 , ax-11 , ax-12 , ax-13

- Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)
- Uniqueness and unique existence
- Other axiomatizations related to classical predicate calculus