534 articles
Infinitary logic
Infinitary logic, also called an infinitary language, is a family of extensions of first-order logic allowing infinitely long formulas; the best-studied case, L(ω₁,ω), permits countably infinite conjunctions and disjunctions.
Inner model theory
Inner model theory is the branch of set theory that constructs canonical inner models of ZFC satisfying large cardinal hypotheses, using fine structure theory, iteration trees, and extender models.
Intension
Intension, also called intensionality, is the sense or internal content of a term, as opposed to its extension, the range of things the term applies to.
Interaction nets
Interaction nets are a graphical model of computation, introduced by Yves Lafont in 1990, where computation is local rewriting of agents connected by wires, generalizing proof nets.
Intermediate logic
An intermediate logic, also called a superintuitionistic logic, is a consistent set of propositional formulas containing intuitionistic propositional calculus and contained in classical logic; Gödel showed in 1932 that infinitely many exist.
Interpretation (logic)
In logic, also called a structure, an interpretation gives meaning to a formal language by fixing a domain of objects and assigning each non-logical symbol a denotation over it.
Interpretation of theories and interpretability strength
An interpretation of a theory T in a theory S is a syntactic translation under which S proves every translated theorem of T, enabling comparison of logical strength.
Intersection (set theory)
In set theory, the intersection of sets A and B, written A ∩ B, is the set of elements they share, the set-level counterpart of logical conjunction.
Interval temporal logic
Interval temporal logic (ITL) is a family of modal logics evaluating formulas over time intervals rather than points, introduced by Halpern and Shoham and used to reason about concurrent and real-time systems.
Intuitionism
Intuitionism, also called mathematical intuitionism, is a philosophy of mathematics founded by the Dutch mathematician L. E. J. Brouwer in 1907, treating mathematics as a creation of the mind.
Intuitionistic logic
Intuitionistic logic, also called constructivist logic, is a logic without the law of excluded middle, abstracted by L. E. J. Brouwer's intuitionistic mathematics and formalized by Arend Heyting in 1930.
Inverse function
An inverse function is a function that reverses another function, sending each output back to its input. It exists only when the function is bijective.
Isabelle (proof assistant)
Isabelle is an interactive theorem prover, introduced by Lawrence C. Paulson at Cambridge in 1986 and developed with Tobias Nipkow in Munich; its main instance, Isabelle/HOL, uses classical higher-order logic.
Journal of Symbolic Logic
The Journal of Symbolic Logic (JSL) is a quarterly peer-reviewed journal of mathematical logic, founded in 1936 and published by Cambridge University Press for the Association for Symbolic Logic.
Jump operator
The jump operator (Turing jump) maps a set of natural numbers to its jump, the halting problem for machines with an oracle for that set, always strictly harder.
Junction tree algorithm
The junction tree algorithm is an exact inference method for probabilistic graphical models that computes marginals by message passing on a tree of variable clusters, introduced by Lauritzen and Spiegelhalter in 1988.
Just-world fallacy
The just-world fallacy, also called the just-world hypothesis, is the belief that people get what they deserve, introduced by social psychologist Melvin J. Lerner in 1965.
Kleene's O
Kleene's O is a set of natural numbers, called ordinal notations, that names the constructive ordinals; it was introduced by Stephen Cole Kleene in 1938.
Kleene's recursion theorem
Kleene's recursion theorem, also called the fixed point theorem, is a result in computability theory published by Stephen Kleene in 1938, implying self-reproducing programs called quines.
Knowledge base
A knowledge base is a structured store of facts, rules, and relationships that computers query and reason over, spanning expert systems like MYCIN and modern knowledge graphs such as Google's.
Knowledge-based systems
A knowledge-based system (KBS) is a computer program that solves problems using a stored knowledge base and a separate inference engine, as in expert systems.
Kolmogorov complexity
Kolmogorov complexity, also known as algorithmic entropy or program-size complexity, is the length of the shortest program producing a given string, a measure discovered independently by Solomonoff, Kolmogorov, and Chaitin.
Kripke semantics
Kripke semantics, also known as relational semantics, is the standard formal semantics for modal logic, in which formulas are evaluated at possible worlds, introduced by Saul Kripke in 1959.
Kripke–Platek set theory
Kripke–Platek set theory (KP) is a weak axiomatic set theory introduced independently by Saul Kripke and Richard Platek in the 1960s; its transitive models are called admissible sets.
Lambda calculus
The lambda calculus, also written λ-calculus, is a formal system invented by Alonzo Church in the 1930s that expresses computation through function definition and application, computing exactly what Turing machines compute.
Lambda cube
The lambda cube is Henk Barendregt's arrangement of eight typed lambda calculi, formed from the simply typed lambda calculus by adding polymorphism, type operators, and dependent types.
Lambek calculus
The Lambek calculus, or syntactic calculus, is a substructural logic introduced by Joachim Lambek in 1958, in which grammatical well-formedness is decided by logical derivability over syntactic types.
Large cardinal
A large cardinal, also called a large cardinal axiom, is an uncountable cardinal so large that its existence is unprovable in ZFC, set theory's standard axioms.
Law of excluded middle
The law of excluded middle (tertium non datur) is the classical logic principle that every proposition is either true or false, rejected in intuitionistic logic.
Law of noncontradiction
The law of noncontradiction, also called the principle of non-contradiction, is the logical principle that a proposition and its negation cannot both be true at the same time.