Formal Logic & Type Theory

← Back to Domain-Specific Families

Abstractions about logical languages, models, proof rules, quantification, entailment, automata, and typed calculi. They describe how expressions receive structure and meaning, how conclusions follow, and where decidability, consistency, reachability, or well-foundedness constrain formal systems.

34 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.

• B, C, K, W system — A basis for combinatory logic using composition, permutation, constant and duplication combinators as primitives.
• Codd's theorem — The database-theory result that relational algebra and domain-independent relational calculus have exactly the same expressive power.
• Default logic — A nonmonotonic formal logic that licenses defeasible conclusions when prerequisites hold and their justifications remain consistent with the evolving belief set.
• Deterministic automaton — An automaton whose current state and next input determine at most one successor state, eliminating branching choice from transition execution.
• Empty type — A type with no inhabitants, representing falsehood under Curry–Howard and serving as the codomain from which negation and ex falso elimination are defined.
• Entscheidungsproblem — The historical decision problem asking for an algorithm that determines whether any first-order logical sentence is valid, proved impossible by Church and Turing.
• Extension (predicate logic) — The set of ordered tuples for which a predicate is true under a particular interpretation.
• 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.
• Hidden algebra — An algebraic specification framework for stateful and concurrent systems that distinguishes visible data sorts from hidden state sorts and characterizes state by observable behavior.
• Independence of premise — A constructive-logical principle allowing an existential witness to be moved outside an implication when the premise does not contain that witness variable.
• Logical form — A precise formal-semantic representation of a statement or argument that exposes the structure relevant to validity and interpretation.
• Metric temporal logic — A temporal logic whose modalities carry quantitative time intervals, allowing formulas to require that events occur within explicit deadlines or durations.
• Model elimination — A goal-directed automated theorem-proving calculus that extends resolution with ancestor links and a chain-based proof state.
• Monotonicity of entailment — A logical property whereby every conclusion entailed by a premise set remains entailed after any additional premises are added.
• Negation introduction — A rule of inference that derives not-P after assuming P and deriving a contradiction within a properly discharged subproof.
• Non-logical symbol — A constant, function or relation symbol in a formal language whose denotation varies with the chosen interpretation or model.
• 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.
• Paraconsistent logic — A logic whose consequence relation does not validate explosion, allowing some contradictions without every proposition becoming derivable.
• Peano–Russell notation — The symbolic logical notation adapted from Peano by Russell and Whitehead for Principia Mathematica.
• Postcondition — A predicate required to hold immediately after a program operation or specified code region completes normally.
• Propositional function — An open sentence containing free variables that becomes true or false when admissible values are substituted.
• Reachability problem — The decision problem asking whether allowed transitions can carry a system from a specified initial state to a target state.
• Set-builder notation — A symbolic notation defining a set by a variable, an optional source domain, and a predicate its members satisfy.
• Structure (mathematical logic) — A nonempty carrier together with interpretations of the constants, functions and relations in a formal signature.
• Symbol (formal) — An abstract atomic item in a formal language whose concrete inscriptions or encodings are token instances rather than the symbol itself.
• Type theory — The family of formal systems that classify expressions by types and govern how typed terms may be formed, transformed and interpreted.
• Typed lambda calculus — A lambda-calculus formalism assigning types to variables and terms and restricting abstraction and application through typing rules.
• Typing rule — A formal inference rule specifying how types of component expressions and contextual assumptions justify a type judgment for a larger syntactic construction.
• 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.
• Vector logic — An algebraic representation of logical truth values and connectives as vectors and matrices acting on a finite-dimensional space.
• Well-founded semantics — A unique three-valued semantics for general logic programs that assigns each ground atom true, false or undefined.
• ΛProlog — A higher-order typed logic-programming language using hereditary Harrop formulas, lambda-tree syntax, and higher-order unification to represent binding structures declaratively.