Formal Logic & Axiomatic Foundations

← Back to Domain-Specific Families

Abstractions about the syntax and axiomatic structure of formal systems, covering proof calculi and metatheory (Hilbert system, Gödel numbering, metalogic, reverse mathematics), set-theoretic foundations (Zermelo set theory, Von Neumann-Bernays-Gödel set theory, extensionality), and algebraic encodings of logic like the Lindenbaum-Tarski algebra.

21 abstractions in this family — domain-specific abstractions that sit near one another in structural-signature space (k-means over structural-signature embeddings). Each is shown with its short description.

• Axiom schema — A metalanguage template with substitution conditions that generates a potentially infinite family of object-language axioms.
• B, C, K, W system — A basis for combinatory logic using composition, permutation, constant and duplication combinators as primitives.
• BCK algebra — An algebra with a binary implication-like operation and a distinguished zero satisfying the BCI identities plus an axiom that enforces the BCK weakening condition.
• Extensionality — The principle that objects of a given kind are equal when they have the same externally observable members, values or behavior, as formalized for sets, functions and relations.
• Gödel numbering — An effective injective encoding of symbols, formulas, proofs, or other formal objects as natural numbers so syntax can be represented and reasoned about arithmetically.
• Heyting arithmetic — A first-order theory of natural-number arithmetic using intuitionistic rather than classical logic while retaining arithmetic axioms and induction.
• Hilbert system — An axiomatic proof calculus in which theorems are generated from axiom schemata by a small set of inference rules, often only modus ponens plus a rule for quantification.
• Inhabited set — A set for which an element can be constructively exhibited or otherwise supplied as a witness, a stronger datum than double-negated nonemptiness in intuitionistic logic.
• Law of continuity — Leibniz's heuristic that rules valid across finite cases may be extended consistently to limiting, infinitesimal or infinite cases, provided the resulting transition preserves the relevant relations.
• Lindenbaum–Tarski algebra — The quotient algebra of formulas or sentences of a logical theory by provable equivalence, with logical connectives inducing well-defined algebraic operations on equivalence classes.
• Logical cube — A three-dimensional opposition diagram that organizes eight categorical propositions and displays their contradiction, contrariety, subcontrariety and subalternation relations.
• Metalogic — The formal study of logical languages and deductive systems as mathematical objects, including their semantics, proof theory and global properties.
• Metatheorem — A theorem proved in a metalanguage about the syntax, derivability, semantics or other properties of a formal object system.
• Regular modal logic — A classical modal logic closed under a rule lifting conjunction-preserving implication through necessity and containing the duality of necessity and possibility.
• Reverse mathematics — A program classifying mathematical theorems by the weakest axiomatic subsystems sufficient to prove them.
• Universe (mathematics) — A contextually fixed collection large enough to contain every object and construction under consideration while controlling size, paradox, and quantification in mathematical foundations.
• Vague set — A set-valued uncertainty model assigning separate lower evidence for membership and lower evidence against membership, leaving an explicit hesitation interval.
• Von Neumann–Bernays–Gödel set theory — A finitely axiomatizable two-sorted set theory with sets and classes that conservatively extends ZFC for statements about sets.
• Zermelo set theory — The original axiomatic set theory built from extensionality, elementary sets, separation, power set, union, choice, and infinity without the later replacement axiom.
• Ω-complete theory — A first-order arithmetic theory that proves a universal formula whenever it proves every numeral instance of that formula.
• Ω-consistent theory — A consistent arithmetic theory that never proves every standard numeral instance of a formula while also proving that some natural number is a counterexample.