Mathematical Logic¶

← Back to Domain-Specific Abstractions by Domain

36 domain-specific abstractions whose origin domain is Mathematical Logic.

Accessibility Relation — A binary relation on the worlds or states of a Kripke frame that fixes which alternatives a modal operator quantifies over from each evaluation point.
Axiom of infinity — Assert in Zermelo–Fraenkel set theory that an inductive set exists—one containing the empty set and closed under the successor x mapped to x union singleton x—thereby supplying a set from which omega and the natural-number sequence can be isolated.
Axiom schema — A metalanguage template with substitution conditions that generates a potentially infinite family of object-language axioms.
Bounded arithmetic — A family of weak arithmetic theories whose bounded quantifiers and restricted induction calibrate feasible reasoning, linking provably total functions and proofs to computational-complexity classes and propositional proof systems.
Cointerpretability — Compare formal theories by a logic-preserving translation in the reverse language direction that reflects the translated theory's theorems, a dual of interpretability tied to Σ₁-conservativity for suitable arithmetical theories.
Deductive closure — The smallest superset of a set of formulas that contains every formula derivable from it under a specified consequence relation or proof system.
Equisatisfiability — The logical relation in which two formulas share the same existence-of-a-model status—both satisfiable or both unsatisfiable—without requiring the same models, enabling compact satisfiability-preserving transformations such as Tseitin encoding and Skolemization.
Fragment (logic) — A syntactically restricted sublanguage of a logic interpreted with the parent logic's semantics, often trading expressive power for decidability or lower computational complexity.
Functional completeness — The property of a set of Boolean connectives from which every Boolean function can be expressed by composition.
Ground expression — A formal term or formula containing no free variables because every constituent is a constant, function application or fully closed construction.
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.
Infinite expression — A mathematical expression with infinitely many operands or unbounded nesting whose meaning is defined only through a limit, fixed point, formal topology or other explicit semantic construction.
Internal Set Theory — Nelson's conservative enrichment of ZFC with a standardness predicate and Transfer, Idealization, and Standardization schemes for internal nonstandard analysis.
Kripke–Platek set theory — A weak axiomatic set theory centered on bounded separation and collection, used to formalize admissible sets and the predicative or recursion-theoretic fragment of set theory.
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.
Monadic predicate calculus — The function-free fragment of first-order logic whose predicate symbols all have arity one.
Monadic second-order logic — The fragment of second-order logic that permits quantification over individual elements and unary predicates or sets, but not arbitrary higher-arity relations.
Negation normal form — A logical formula form using only conjunction, disjunction and literals, with every negation applied directly to an atomic proposition.
Non-logical symbol — A constant, function or relation symbol in a formal language whose denotation varies with the chosen interpretation or model.
Non-well-founded set theory — Study axiomatic set universes in which membership may contain infinite descent or cycles because Foundation is omitted or replaced by a declared anti-foundation principle, with graph decoration and bisimulation specifying which circular presentations denote equal sets.
Pairing function — A bijection that uniquely encodes an ordered pair of natural numbers as one natural number, with generalizations to higher arity or other infinite sets.
Positive set theory — A family of alternative set theories permitting comprehension for positive membership formulas while restricting negation so broad set formation avoids classical paradoxes.
Prenex normal form — A first-order formula form in which all quantifiers occur in one leading prefix followed by a quantifier-free matrix.
Propositional function — An open sentence containing free variables that becomes true or false when admissible values are substituted.
Quantifier Rank — Assign a logical formula the maximum nesting depth of its quantifiers, stratifying expressibility so bounded-rank formulas, types, and structure-distinguishing games can be compared at a fixed logical depth.
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.
Sequent — Package antecedent and succedent formula contexts into a two-sided formal judgment whose interpretation and admissible transformations are fixed by a proof calculus.
Skolem Normal Form — A first-order formula shape in which a universal prenex prefix governs a quantifier-free matrix and existential witnesses have been encoded by fresh Skolem terms, preserving satisfiability across a signature expansion.
Syntax (logic) — The formal symbols, formation rules and derivation or transformation rules that determine which expressions and proofs are well formed independently of their interpretation.
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.
Uniqueness quantification — The logical assertion that exactly one object in a domain satisfies a specified predicate.
Universal quantification — The logical operation asserting that a predicate holds for every member of a declared domain of discourse.
Ω-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.