534 articles
Soundness
Soundness (logical soundness) is the property of a proof system that proves only what is semantically valid: derivable conclusions hold in every model of the premises.
Soundness and completeness
Soundness and completeness are the properties linking a formal proof system to its semantics: what is provable is valid, and what is valid is provable.
Specker sequence
A Specker sequence is a computable, monotonically increasing, bounded sequence of rational numbers whose limit is an uncomputable real, first given by Ernst Specker in 1949.
Stability theory
Stability theory is the branch of model theory, founded on Saharon Shelah's classification program, that sorts first-order theories into dividing lines such as stable, simple, and NIP.
Stable group
A stable group is a group definable in a model of a stable first-order theory; examples include abelian groups, algebraic groups over algebraically closed fields, and free groups.
Stable theory
A stable theory is a complete first-order theory that forbids the combinatorial pattern called the order property, a tameness condition central to Shelah's classification program in model theory.
Standard translation
The standard translation is a translation in modal logic that rewrites propositional modal formulas as first-order logic formulas, turning modal operators into quantifiers over possible worlds.
Star-free languages and first-order logic on words
Star-free languages are the regular languages definable by regular expressions using union, concatenation, and complement but no Kleene star, characterized equivalently by aperiodic monoids and by first-order logic on words.
Statement (logic)
A statement in logic is a declarative sentence, or part of one, that is capable of being true or false, and the basic unit of propositional logic.
Stationary set
A stationary set is a subset of a limit ordinal that meets every closed unbounded (club) subset of that ordinal, the standard notion of largeness in set theory.
Strange loop
A strange loop is a hierarchical system that twists back on itself so moving through its levels returns to the start, coined by Douglas Hofstadter in 1979.
Straw man
A straw man is an informal fallacy in which a speaker misrepresents an opponent's position and then refutes the distorted version instead of the real one.
Structural induction
Structural induction is a proof technique that establishes a property for all elements of an inductively defined data type, such as lists, trees, or formulae.
Structure (mathematical logic)
In mathematical logic, a structure, also called a model, is a set with relations and functions that interpret a formal language's symbols, making sentences true or false.
Subobject classifier
A subobject classifier is an object Ω in a category that classifies subobjects via pullbacks, generalizing characteristic functions of subsets; it is a defining axiom of a topos.
Subset
A subset, also called a set inclusion, is a set all of whose members also belong to another set B, written A ⊆ B; a proper subset leaves at least one member out.
Substructural logic
Substructural logic is a family of non-classical logics lacking one or more structural rules of classical logic, including relevant logics, the Lambek calculus, and linear logic.
Substructural type system
A substructural type system removes one or more structural rules, such as weakening or contraction, so the type system controls whether variables can be reordered, discarded, or duplicated.
Sum-of-squares proof
A sum-of-squares proof is a certificate that a polynomial is nonnegative, given by writing it as a sum of squares of polynomials, testable efficiently through semidefinite programming.
Super-recursive algorithm
A super-recursive algorithm is, in Mark Burgin's classification of algorithmic models, a model of computation exceeding Turing machines, exemplified by inductive Turing machines that produce results by output stabilizing.
Superstable theories
In model theory, a superstable theory is a stable theory in which every type does not fork over a finite subset of its domain, a class introduced by Saharon Shelah.
Surjective function
A surjective function, also called an onto function or surjection, is a function in which every element of the codomain is the output of at least one domain element.
Suslin cardinal
A Suslin cardinal is an ordinal κ for which some set of reals is κ-Suslin but no smaller ordinal suffices; ℵ₁ is the classical example in descriptive set theory.
Suslin operation
The Suslin operation, also called operation A, is a set-theoretic operation that takes families indexed by finite sequences of naturals; applied to closed sets, it yields the analytic sets.
Symmetric difference
The symmetric difference, also called the disjunctive union, is the set operation containing elements that belong to exactly one of two sets, corresponding to XOR in logic.
System L (logic)
System L is a name used in formal logic for several distinct deductive systems, chiefly Łukasiewicz's Hilbert-style axiomatization of classical propositional logic and the Curien–Herbelin term syntax for classical sequent calculus.
System T
System T, also called Gödel's T, is a quantifier-free theory of functionals of finite type introduced by Kurt Gödel in 1958 as the target of his Dialectica interpretation.
Tagged union
A tagged union, also called a variant record or sum type, is a data structure holding a value of several fixed types with a tag recording which type is stored.
Takeuti's conjecture
Takeuti's conjecture, also called Takeuti's fundamental conjecture, is the claim that Gentzen's cut-elimination theorem extends from first-order logic to simple type theory, formulated by Gaisi Takeuti in 1953.
Tarski–Grothendieck set theory
Tarski–Grothendieck set theory is an axiomatic set theory extending Zermelo–Frænkel set theory with Tarski's axiom, introduced by Alfred Tarski in 1938, and serves as the foundation of the Mizar system for formalizing mathematics.