534 articles
Laws of Form
Laws of Form is a 1969 book by the British mathematician G. Spencer-Brown that introduces the calculus of indications, showing it equivalent to Boolean algebra and the propositional calculus.
Leon van der Torre
Leon van der Torre, also known as Leendert van der Torre, is a Dutch-born computer scientist and professor of artificial intelligence at the University of Luxembourg.
LF (logical framework)
LF, short for the Edinburgh Logical Framework, is a typed lambda-calculus with dependent types designed as a meta-language for defining logics, presented by Harper, Honsell, and Plotkin in 1987.
Liar paradox
The Liar paradox, also known as Eubulides' paradox, is the semantic paradox of a sentence like "This sentence is not true" that seems both true and false.
Lindström's theorem
Lindström's theorem, proved by the Swedish logician Per Lindström in 1969, characterizes first-order logic as maximal in expressive power among logics satisfying compactness and the Löwenheim–Skolem theorem.
Linear logic
Linear logic is a substructural logic introduced by Jean-Yves Girard in 1987 that treats formulas as resources, dropping contraction and weakening so each assumption must be used exactly once.
Linear temporal logic
Linear temporal logic (LTL) is a modal temporal logic over infinite sequences of states, proposed by Amir Pnueli in 1977 and now the most widely used temporal logic in computer science.
List of forcing notions
The list of forcing notions covers the classical partial orders used in Cohen's forcing method, from Cohen and random forcing to Sacks, Laver, and Miller forcing.
List of logic symbols
Logic symbols are the fixed signs of formal logic for connectives, quantifiers, truth constants, and proof relations, such as ¬, ∧, ∨, →, ↔, ∀, ∃, ⊢, and ⊨.
List of paradoxes
The list of paradoxes collects the best-known paradoxes of logic, mathematics, statistics, and ancient philosophy, including the Liar, Russell's, the sorites, Zeno's, Simpson's, and the Monty Hall problem.
List of statements independent of ZFC
A list of statements independent of ZFC, also undecidable in ZFC: assertions neither provable nor disprovable from standard set theory axioms, such as the Continuum Hypothesis.
Löb's theorem
Löb's theorem, proved by Martin Löb in 1955, states that if a theory proves that a provable sentence is true, the theory already proves that sentence.
Logic
Logic, also known as Logike, is the systematic study of valid inference, which patterns of reasoning preserve truth from premises to conclusion, now underpinning mathematics, philosophy, and computer science.
Logic Colloquium
The Logic Colloquium is the European Summer Meeting of the Association for Symbolic Logic, an annual logic conference first held in Oxford in 1956 and one of the ASL's two major meetings.
Logical biconditional
The logical biconditional, also called biimplication, is the two-place propositional connective "P if and only if Q", true when P and Q have the same truth value.
Logical conjunction
Logical conjunction, also called logical and, is the two-place logical operation written ∧ that combines two statements into a compound true only when both are true.
Logical connective
A logical connective, or logical operator, is a symbol such as "and", "or", "not", or "if...then" that binds one or more sentences into a new compound sentence in formal logic.
Logical disjunction
Logical disjunction, also called the inclusive or, is the logical connective written ∨, a compound sentence true when at least one of its two disjuncts is true.
Logical NOR
Logical NOR, also called joint denial, is the logical connective true only when both of its statements are false; on its own it can express every truth-function of propositional logic.
Logical reasoning
Logical reasoning is the process of drawing conclusions from premises by rules evaluated independently of subject matter, divided into deductive, inductive, and abductive modes, first formally studied by Aristotle.
Logical relations
A logical relation is a family of relations between program meanings, indexed by types and defined by recursion over type structure; it proves program equivalence and compiler correctness.
Löwenheim–Skolem theorem
The Löwenheim–Skolem theorem is a pair of results in model theory of first-order logic, proved by Löwenheim in 1915 and Skolem in 1922.
Ludwig Wittgenstein
Ludwig Josef Johann Wittgenstein was an Austrian-British philosopher, born in Vienna in 1889, whose Tractatus and Philosophical Investigations shaped analytic philosophy and ideas of meaning as use.
Luzin space
A Luzin space, also called a Luzin topological space, is an uncountable T1-space without isolated points in which every nowhere-dense subset is countable, named for Nikolai Luzin.
Many-one reduction
Many-one reduction, also called mapping reduction, is a way of comparing decision problems in computability theory: A reduces to B when a computable function preserves membership.
Many-sorted logic
Many-sorted logic is a version of first-order logic in which quantification ranges over several distinct domains, called sorts; it underlies the SMT-LIB standard used by SMT solvers.
Many-valued logic
Many-valued logic, also called multivalued logic, is a family of logical systems generalizing classical two-valued logic to three or more truth values, originating with Jan Łukasiewicz in 1920 and including fuzzy logic.
Martin-Löf type theory
Martin-Löf type theory (MLTT), also called intuitionistic type theory, is a constructive formal system devised by Per Martin-Löf that underlies proof assistants like Coq and Agda.
Martin's axiom
Martin's axiom (MA) is a set-theoretic statement that any family of fewer than continuum many dense subsets of a ccc partial order can all be met by one filter.
Martin's maximum
Martin's Maximum (MM) is a forcing axiom of set theory, isolated by Foreman, Magidor, and Shelah in 1988 and ostensibly the strongest possible of its general form.