534 articles
Tarski's undefinability theorem
Tarski's undefinability theorem is a result in mathematical logic, proved by Alfred Tarski in 1933, showing that no sufficiently rich formal language can define its own truth predicate.
Tautology (logic)
In logic, a tautology, also known as a logical tautology, is a formula true under every possible interpretation, with p ∨ ¬p the standard example.
Temporal logic
Temporal logic is a formal logic extending propositional or first-order logic with operators about time, such as "always" and "eventually", used to specify reactive systems.
Temporal logic of actions
The temporal logic of actions (TLA) is a temporal logic invented by Leslie Lamport in the late 1980s, in which actions may appear directly inside temporal formulas.
Tense logic
Tense logic is a modal-style formalism for reasoning about time, introduced by Arthur Prior in the 1950s; it grew into temporal logic, now standard in computing and verification.
Term (logic)
In logic, a term is a first-order logic expression, such as a variable, constant, or function application, that refers to an object in the domain of discourse.
Theorem
A theorem is a statement in mathematics or logic proved from axioms by valid inference, in contrast with an unproved conjecture or an accepted axiom.
Theories of truth
Theories of truth are philosophical accounts of what it is for a proposition or belief to be true, including the correspondence, coherence, pragmatic, semantic, and deflationary theories.
Therefore sign
The therefore sign (∴), or therefore symbol, is a three-dot symbol used in mathematics and logic to introduce a conclusion, first published in 1659; its inverted mirror means 'because'.
Tiling problem
The tiling problem, also called the domino problem, asks whether a given finite set of Wang tiles can cover the infinite plane; it is undecidable.
Timed automaton
A timed automaton (plural: timed automata) is a finite automaton extended with real-valued clocks that can be reset and compared against constants, introduced by Rajeev Alur and David L. Dill.
TLA+
TLA+ is a formal specification language, created by Leslie Lamport, based on set theory and the Temporal Logic of Actions, used for designing and verifying concurrent and distributed systems.
Transfinite induction
Transfinite induction, also called well-ordered induction, is a proof technique extending ordinary mathematical induction from the natural numbers to any well-ordered class, most prominently the ordinal numbers.
Transitive relation
A transitive relation (also called the transitive property) is a binary relation in which aRb and bRc together imply aRc, forming the basis of equivalence relations and orderings.
Tree (descriptive set theory)
In descriptive set theory, a tree is a set of finite sequences closed under taking initial segments, the standard device for coding closed, analytic, and coanalytic sets of infinite sequences.
Triple bar
The triple bar (≡) is a mathematical symbol of three stacked lines meaning identically equal, defined as, or congruent modulo a number; Gauss introduced it for congruence in 1801.
Truth table
A truth table, or logical truth table, is a table listing the value of a propositional formula under every possible assignment of truth values to its variables.
Truth value
Truth value, also called logical value, is the value a sentence or proposition is assigned by a valuation: in classical logic, one of exactly two values, True and False.
Tu quoque
Tu quoque (Latin for "you too"), also called the appeal to hypocrisy, is an ad hominem fallacy dismissing an argument because its speaker does not practice it.
Tuple
A tuple, also called an ordered n-tuple, is a finite ordered list of elements, written (1, 2, 3), in which order and repetition count; tuples of two and three elements are called ordered pairs and triples.
Tupper's self-referential formula
Tupper's self-referential formula is an inequality published by computer scientist Jeff Tupper in 2001 which, plotted over a particular 106-by-17 pixel block, draws a bitmap picture of itself.
Turing degree
A Turing degree is an equivalence class of sets of natural numbers under relative computability, the central object of computability theory, with the halting problem at degree 0'.
Type (model theory)
In model theory, a type, or complete type, is a set of first-order formulas describing a possible element or tuple of a structure, realized when some tuple satisfies them all.
Type inference
Type inference, also known as type reconstruction or type deduction, is the process by which a compiler determines an expression's type without explicit programmer annotations, as in ML and Haskell.
Type theory
Type theory, or the theory of logical types, is a formal system where every entity carries a type, serving as a foundation for mathematics and proof assistants like Lean and Rocq.
Ultrapower
An ultrapower is a model-theoretic construction building a new structure from many copies of one structure using an ultrafilter, the special case of an ultraproduct behind nonstandard analysis.
Ultraproduct
An ultraproduct is a model theory construction combining an infinite family of mathematical structures into one via an ultrafilter, preserving first-order properties by Łoś's theorem, defined by Jerzy Łoś in 1955.
Uncountable set
An uncountable set is an infinite set too large to count, whose elements cannot be paired with the natural numbers, a fact first shown by Cantor in 1874.
Unification (computer science)
Unification in computer science is the algorithmic problem of finding a substitution making two logical expressions identical, introduced by Robinson in 1965 for resolution theorem proving.
Uniform interpolation
Uniform interpolation is a technique in modal and description logic that rewrites a formula or ontology over a reduced signature while preserving all its entailments in that signature.