Classical propositional and predicate logic: operators, quantifiers, and fundamental laws of reasoning. The substrate every other tree in this layer depends on.
logic
Logical conjunction (AND)
A binary operator returning true iff both operands are true.
Logical disjunction (OR)
A binary operator returning true iff at least one operand is true.
Logical negation (NOT)
A unary operator returning the opposite truth value of its operand.
Material implication
A binary operator: A implies B is false only when A is true and B is false.
Biconditional (IFF)
A binary operator returning true iff both operands share the same truth value.
Universal quantifier
Asserts a predicate holds for every element of a domain of discourse.
Existential quantifier
Asserts a predicate holds for at least one element of a domain.
Law of non-contradiction
No proposition is both true and false at the same time and in the same sense.
Law of excluded middle
Every proposition is either true or its negation is true.
Modus ponens
From A and (A implies B), one may infer B.
Exclusive disjunction (XOR)
Exclusive-or connective ⊕. p ⊕ q is true exactly when p and q differ in truth value; false when both are true or both are false. Equivalent…
Sheffer stroke (NAND)
The NAND connective | (Sheffer stroke). p | q is false exactly when both p and q are true. NAND is functionally complete on its own: every…
Peirce arrow (NOR)
The NOR connective ↓ (Peirce arrow). p ↓ q is true exactly when both p and q are false. Like NAND, NOR is functionally complete on its own.
Proposition
A declarative sentence that is either true or false but not both. Propositions are the atomic carriers of truth values in propositional…
Truth table
An exhaustive enumeration of the truth values a compound proposition takes for every combination of truth values assigned to its atomic…
Tautology
A compound proposition that is true in every row of its truth table — true under every possible assignment of truth values to its atomic…
Contradiction (propositional form)
A compound proposition that is false in every row of its truth table. Canonical example: p ∧ ¬p. Distinct from the inferential…
Contingency
A compound proposition that is true in some rows of its truth table and false in others — neither a tautology nor a contradiction. Most…
Satisfiability
A proposition is satisfiable iff there exists at least one assignment of truth values to its atomic propositions under which it is true —…
Logical equivalence
Two propositions φ and ψ are logically equivalent (written φ ≡ ψ) iff they have identical truth tables — i.e. iff φ ↔ ψ is a tautology.…
Converse of a conditional
Given a conditional p → q, its converse is q → p. A conditional and its converse are NOT in general logically equivalent; assuming the…
Inverse of a conditional
Given a conditional p → q, its inverse is ¬p → ¬q. A conditional and its inverse are NOT in general logically equivalent; assuming the…
Contrapositive of a conditional
Given a conditional p → q, its contrapositive is ¬q → ¬p. A conditional and its contrapositive ARE always logically equivalent; this is the…
De Morgan's laws
The two De Morgan equivalences connect negation with conjunction and disjunction. Negating a conjunction distributes as a disjunction of…
Double-negation equivalence
Two negations cancel: ¬¬p is logically equivalent to p. Accepted in classical logic; intuitionistic logic rejects the ¬¬p ⊨ p direction.
Distributive laws (logic)
Conjunction distributes over disjunction and vice versa. Mirror of arithmetic distributivity; key for CNF/DNF normal-form transformations.
Associative laws (logic)
Grouping of ∧ and ∨ is irrelevant. Allows writing chained conjunctions and disjunctions without parentheses.
Commutative laws (logic)
Order of operands in ∧, ∨, ↔, ⊕ does not matter. NOT commutative: → (material implication).
Idempotent laws (logic)
Conjoining or disjoining a proposition with itself yields the same proposition.
Identity laws (logic)
True acts as the identity for ∧; False acts as the identity for ∨.
Domination laws (logic)
True dominates ∨; False dominates ∧. Also called annihilation laws.
Absorption laws (logic)
A disjunct/conjunct absorbs a nested occurrence of itself.
Implication-as-disjunction equivalence
Material implication can be re-expressed as a disjunction of the negated antecedent with the consequent. This is the gateway identity for…
Contrapositive equivalence
A conditional is logically equivalent to its contrapositive. Basis for proof by contrapositive: to prove p → q, prove ¬q → ¬p instead.
Biconditional decomposition
The biconditional p ↔ q is logically equivalent to the conjunction of the two directional conditionals. Also equivalent to (p ∧ q) ∨ (¬p ∧…
Modus tollens
If p → q holds and q is false, then p is false. The 'denying the consequent' inference rule. Derivable from modus ponens + contrapositive.
Hypothetical syllogism
Chaining of conditionals. If p → q and q → r, then p → r. Sometimes called the 'transitivity of implication'.
Disjunctive syllogism
If p ∨ q is true and p is false, then q must be true. The 'elimination of alternatives' rule.
Simplification (∧-elimination)
From a conjunction, either conjunct may be inferred individually.
Conjunction introduction (∧-introduction)
From two separately-established premises, the conjunction may be inferred. Also called 'adjunction'.
Addition (∨-introduction)
From p alone, p ∨ q may be inferred for any proposition q. Also called 'disjunction introduction'.
Resolution
Resolves a pair of clauses containing complementary literals. The foundational inference rule of automated theorem proving, SAT solvers,…
Principle of bivalence
Every declarative proposition is either true or false — there is no third truth value. This is the meta-principle on top of which classical…
Open sentence
A sentence whose truth value depends on the values assigned to one or more free variables appearing in it — e.g., Q(x): 'the integer x is…
Predicate
A function-like abstraction that maps a tuple of individuals from some domain to a truth value — the formal counterpart of an open…
Quantifier-negation rules (De Morgan for quantifiers)
The two named equivalences connecting negation with the universal and existential quantifiers. Negating a universal produces an existential…
Sufficient condition
Given a conditional P → Q, the antecedent P is said to be a *sufficient* condition for the consequent Q — P being true is enough…
Necessary condition
Given a conditional P → Q, the consequent Q is said to be a *necessary* condition for the antecedent P — Q must be true whenever P is true,…
Argument (deductive)
A finite sequence of propositions in which one (the conclusion) is claimed to follow from the others (the premises). Written schematically…
Valid argument
An argument is valid iff it is impossible for all the premises to be true while the conclusion is false — equivalently, iff the conjunction…
Soundness (of an argument)
An argument is sound iff it is (a) valid AND (b) all of its premises are true. Soundness is the gold-standard property for a deductive…
Affirming the consequent (fallacy)
The invalid inference pattern: from P → Q and Q, conclude P. This is NOT a valid rule of inference — it is a named formal fallacy. Confuses…
Denying the antecedent (fallacy)
The invalid inference pattern: from P → Q and ¬P, conclude ¬Q. This is NOT a valid rule of inference — it is a named formal fallacy.…
Modal logic
An extension of propositional/predicate logic with unary operators □ (necessity) and ◇ (possibility) interpreted over Kripke frames. …
Kripke semantics
Relational semantics for modal, intuitionistic, and related non-classical logics: a Kripke frame (W, R) with valuation V specifies truth at…
Intuitionistic logic
A constructive logic rejecting the law of excluded middle (A ∨ ¬A) as a universal axiom; propositions are identified with proofs (BHK…
Second-order logic
Extension of first-order logic with quantifiers that range over relations and functions, not merely individuals. Strictly more expressive…
Infinitary logic
Logics L_{κ,λ} allowing conjunctions/disjunctions over sets of cardinality <κ and quantification over sequences of length <λ. Loses…
Dependent type theory
A formal system (Martin-Löf 1975) where types may depend on values; propositions-as-types realises the Curry–Howard correspondence. …
Homotopy type theory (HoTT)
A foundation identifying types with ∞-groupoids and propositional equality with paths; Voevodsky's univalence axiom asserts that equivalent…
Sequent calculus
Gentzen's (1934) formal system manipulating sequents Γ ⊢ Δ by structural and logical rules. The left/right rules treat connectives…
Natural deduction
Gentzen's introduction/elimination calculus for logical connectives; mirrors informal mathematical reasoning and underlies the Curry–Howard…
Cut-elimination theorem (Hauptsatz)
Gentzen (1935): every proof in the sequent calculus can be transformed into a cut-free proof. Implies consistency, subformula property,…
Gödel's completeness theorem
A first-order sentence is provable from a theory T if and only if it holds in every model of T (T ⊨ φ ⇔ T ⊢ φ). First-order logic is…
Löwenheim-Skolem theorems
Downward LS: consistent T in countable signature has a countable model. Upward LS: infinite model ⟹ models of every κ ≥ |T|. Compactness…
Gödel completeness theorem
First-order theory T ⊨ φ iff T ⊢ φ. Every consistent theory has a model. Gödel 1929 dissertation. Compactness as corollary.
Gödel incompleteness theorems
1st: Any consistent recursively axiomatizable T containing PA is incomplete. 2nd: T cannot prove its own consistency. Diagonal lemma.
Peano arithmetic PA
First-order theory with 0, S, +, ·, induction schema. PA incomplete (Gödel), consistent with ε_0 induction (Gentzen 1936).
ZFC axioms
Extensionality, pairing, union, power set, infinity, replacement, regularity, choice, separation. Standard foundation; independence of CH,…
Homotopy type theory (HoTT)
Martin-Löf intensional type theory + univalence axiom (Voevodsky): equivalence ≃ equality. Types as ∞-groupoids; constructive foundation.