534 articles
Grundlagen der Arithmetik
Die Grundlagen der Arithmetik (The Foundations of Arithmetic) is an 1884 book by the German logician Gottlob Frege, arguing that arithmetic is a development of logic.
Halting problem
The halting problem, also known as Turing's halting theorem, asks whether a program halts on a given input; Alan Turing proved in 1936 that no algorithm solves it.
Hausdorff maximal principle
The Hausdorff maximal principle, also called the Hausdorff maximality theorem, states that every chain in a partially ordered set is contained in a maximal chain, and is equivalent to Zorn's lemma.
Higher-order function
A higher-order function is a function that takes one or more functions as arguments, returns a function as its result, or both, as in map, filter, and fold.
Higher-order logic
Higher-order logic (HOL), also called simple type theory or Church's type theory, extends first-order logic by quantifying over predicates and functions via the simply typed lambda calculus; standard semantics is not axiomatizable, Henkin semantics is complete, and HOL underlies proof assistants like Isabelle/HOL and HOL Light.
Hilbert system
The Hilbert system, also called the Hilbert calculus, is a formal proof system for logic with many axiom schemas and few rules, usually just modus ponens.
Hilbert–Bernays provability conditions
The Hilbert–Bernays provability conditions, given by Hilbert and Bernays in Grundlagen der Mathematik (1939), are conditions on a formalized provability predicate sufficient for proving Gödel's second incompleteness theorem.
Hilbert's paradox of the Grand Hotel
Hilbert's paradox of the Grand Hotel, also known as Hilbert's Hotel, is a thought experiment in which a fully occupied infinite hotel still makes room for new guests.
Hilbert's problems
Hilbert's problems, also listed as the List of Hilbert's problems, are 23 mathematical problems David Hilbert presented at the 1900 Paris congress; several, including the Riemann Hypothesis, remain unsolved.
Hilbert's program
Hilbert's program was David Hilbert's 1920s proposal to secure mathematics by proving formal axiomatic systems consistent using finitary methods; Gödel's incompleteness theorems showed it could not succeed.
Hindley–Milner type system
The Hindley–Milner type system, also known as Hindley–Milner type inference, is a polymorphic type system for the lambda calculus, the foundation of type inference in ML, OCaml, and Haskell.
History of the Church–Turing thesis
The history of the Church–Turing thesis traces the idea that every effectively calculable function is computable, from Hilbert's Entscheidungsproblem to the independent 1936 proposals of Alonzo Church and Alan Turing.
History of type theory
The history of type theory runs from Russell's 1908 ramified response to the set-theoretic paradoxes, through Church's simply typed lambda calculus of 1940, to modern proof assistants.
Hoare logic
Hoare logic, also known as Floyd–Hoare logic, is a formal system for reasoning about the correctness of imperative programs, introduced by Tony Hoare in 1969.
Homotopy type theory
Homotopy type theory, also known as homotopical type theory or HoTT, combines Martin-Löf type theory with homotopy theory, with Voevodsky's univalence axiom and higher inductive types at its core.
Horn clause
A Horn clause, also known as a Horn sentence, is a clause containing at most one positive literal, named after logician Alfred Horn, central to logic programming and Prolog.
Hybrid logic
Hybrid logic is a family of extensions of modal logic in which formulas can name the possible worlds, times, or states at which they are evaluated.
Hydra game
The hydra game is a mathematical process, introduced by Laurie Kirby and Jeff Paris in 1982, in which a player cuts heads from a regrowing tree and always wins.
Hyperarithmetical theory
Hyperarithmetical theory, which studies the hyperarithmetic sets, or HYP, is the branch of computability theory that iterates the Turing jump through the computable ordinals, a hierarchy begun by Stephen Cole Kleene in the 1950s.
If and only if
"If and only if" (iff) is the connective of formal logic and mathematics asserting that two statements each imply the other, true exactly when their truth values match.
Image (mathematics)
In mathematics, the image of a function is the set of all outputs it produces, and the image of a set under a function collects those outputs.
Implementation of mathematics in set theory
The implementation of mathematics in set theory defines every mathematical object, such as numbers, functions, and ordered pairs, as a set, giving ZFC its foundational role in mathematics.
Implicational propositional calculus
The implicational propositional calculus is the fragment of propositional logic in which the only connective is material implication, with theorems derived from axiom schemas by modus ponens.
Independence property (model theory)
The independence property in model theory is a combinatorial property of formulas, isolated by Shelah as a dividing line marking the boundary of NIP, or dependent, theories.
Index set (computability)
In computability theory, an index set is a set of program indices that depends only on the function computed, so all programs computing the same function share membership.
Indicator function
The indicator function, also called the characteristic function of a set, maps elements of a set to 1 if they belong to a subset and 0 otherwise.
Inductive inference
Inductive inference is a recursion-theoretic theory of learning in which algorithms fed growing data samples output hypotheses converging to a correct description of an unknown object.
Inductive reasoning
Inductive reasoning, also called inductive logic or weak induction, is inference whose conclusion goes beyond its premises, so true premises support but never guarantee the conclusion.
Inference
Inference, also known as logical inference, is the process of deriving a conclusion from premises with certainty, as in deduction, or to a lesser degree, as in induction and abduction.
Inference engine
An inference engine is a software module that applies the stored knowledge of an expert system to problem facts, deriving new facts and deciding which actions to take.