Metalogic & Formal Foundations

← Back to Domain-Specific Families

Abstractions about formal theories, axiom schemata, consistency, definability, proof systems, metatheorems, reverse mathematics, and computational foundations.

13 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.
• Church–Turing–Deutsch principle — The physical-computation principle that a universal computing device can simulate every finitely realizable physical process.
• Constructive nonstandard analysis — A constructive framework for infinitesimal and infinitely large reasoning that develops nonstandard analysis without classical choice-dependent foundations.
• Diagram (mathematical logic) — The set of first-order sentences with named parameters that are true in a structure, with atomic and elementary variants preserving different amounts of information.
• 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.
• 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.
• Reverse mathematics — A program classifying mathematical theorems by the weakest axiomatic subsystems sufficient to prove them.
• Self-verifying theories — Weak consistent first-order arithmetical systems constructed to prove an internal statement of their own consistency without containing enough arithmetic for Gödel's second incompleteness theorem to apply in its usual form.
• Subject reduction — The type-preservation property that evaluation of a well-typed expression cannot change or destroy its assigned type.
• Tarski's undefinability theorem — A limit theorem stating that sufficiently strong consistent formal systems cannot define within themselves the full truth predicate for their standard arithmetic interpretation.
• Ω-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.