534 articles
Degree spectrum
A degree spectrum is the set of Turing degrees that compute isomorphic copies of a mathematical structure, introduced by Linda Jean Richter in computable structure theory.
Denotational semantics
Denotational semantics, also known as the Scott-Strachey approach, is a formal method assigning each programming language phrase a mathematical meaning, built compositionally from its parts using domain theory.
Deontic logic
Deontic logic, or deontic modal logic, is the branch of logic studying obligation, permission, and prohibition, with roots in ethics and law and modern uses in computer science.
Dependent (NIP) theories
Dependent (NIP) theories, meaning theories without the independence property, are first-order theories in which no formula encodes the random bipartite graph; introduced by Shelah, they include the real field and p-adic numbers.
Dependent type
Dependent typing is the defining feature of dependent type theories: a family of types indexed by a value, so each value may yield a distinct type.
Descriptive complexity theory
Descriptive complexity theory is a branch of finite model theory that characterizes complexity classes by the logic needed to define problems, notably NP via Fagin's 1974 theorem.
Descriptive set theory
Descriptive set theory is the branch of mathematical logic that studies definable sets of real numbers and Polish spaces, including Borel, analytic, and coanalytic sets.
Determinacy (set theory)
In set theory, determinacy is the property of an infinite two-player game that one player has a winning strategy; the full Axiom of Determinacy contradicts the Axiom of Choice.
Diagonal lemma
The diagonal lemma, also called the diagonalization or fixed-point lemma, is a mathematical logic theorem giving each arithmetic formula a sentence describing itself, key to Gödel's incompleteness theorems.
Dialectica interpretation
The Dialectica interpretation, also called Gödel's functional interpretation or D-interpretation, is a proof interpretation reducing Heyting arithmetic to Gödel's quantifier-free System T, published by Kurt Gödel in 1958.
Dialetheism
Dialetheism is the view that some contradictions, called dialetheias, are both true and false, developed by Graham Priest and Richard Routley in the late 1970s.
Dichotomy
A dichotomy is a division of a whole into exactly two mutually exclusive, jointly exhaustive parts. In logic it divides a genus into two species by a single attribute.
Die Grundlagen der Arithmetik
Die Grundlagen der Arithmetik (The Foundations of Arithmetic) is an 1884 book by the German philosopher and logician Gottlob Frege that argues arithmetic can be derived from logic alone.
Differentially closed field
A differentially closed field is a field with a derivation containing enough solutions of differential equations, the differential analog of an algebraically closed field, in a precise first-order sense.
Dilemma
A dilemma is a logical argument form built from two conditional statements and a disjunctive premise, so a stated conclusion follows from either alternative; in ethics it names conflicting obligations.
Direct proof
A direct proof establishes a statement by assuming its hypotheses and deriving the conclusion through an explicit chain of deductions, proving the proposition in its originally stated form rather than a transformed equivalent.
Disjoint sets
Disjoint sets, also called mutually exclusive sets, are sets that share no elements, so their intersection is empty; the concept underlies partitions and counting rules.
Domain of a function
The domain of a function, also called the function domain, is the set of inputs for which it is defined, the X in f: X → Y.
Doxastic logic
Doxastic logic is a branch of modal logic that formalizes reasoning about belief, initiated by Jaakko Hintikka in 1962 and distinguished from knowledge by beliefs that can be false.
DPLL algorithm
The DPLL algorithm (Davis–Putnam–Logemann–Loveland) is a complete backtracking search procedure for deciding whether a Boolean CNF formula is satisfiable, published in 1960–1962 by Davis, Putnam, Logemann, and Loveland.
Drools
Drools, also known as JBoss Rules, is an open source rule engine and business rule management system written in Java, begun in 2001 and now part of Apache KIE.
Dynamic epistemic logic
Dynamic epistemic logic (DEL) is a family of modal logics in which operators describe actions, like public announcements, that transform what a group of agents knows.
Dynamic logic (computer science)
Dynamic logic is a family of modal logics whose modalities are indexed by programs, generalizing box and diamond; its propositional variant PDL was introduced by Fischer and Ladner in 1979.
Effective descriptive set theory
Effective descriptive set theory is the lightface study of effective Borel, analytic, and co-analytic sets on recursive Polish spaces, merging classical descriptive set theory with Kleene's recursion theory.
Ehrenfeucht–Fraïssé game
The Ehrenfeucht–Fraïssé game (EF game) is a two-player game on two structures in which Spoiler tries to expose differences and Duplicator tries to match every move.
Element of a set
An element of a set, also called a member, is an object that belongs to the set, written a ∈ A; membership is the basic relation of set theory.
Elementary equivalence
Elementary equivalence, or elementarily equivalent structures, is a relation between structures of the same first-order language that satisfy exactly the same first-order sentences, formulated by Alfred Tarski in 1930.
Embeddings and elementary maps between model-theoretic structures
In model theory, an elementary map between two structures preserves and reflects the truth of every first-order formula; every isomorphism is elementary, but elementary embeddings need not be surjective.
Empty set
The empty set, or empty subset, is the unique set containing no elements, denoted ∅; it has cardinality zero and is a subset of every set.
Entscheidungsproblem
The Entscheidungsproblem, also known as Church's theorem, is the problem of deciding validity in first-order logic, posed by Hilbert and Ackermann in 1928 and proved unsolvable by Church and Turing in 1936.