edgepedia

Formal logic and foundations

534 articles

Enumeration degree

An enumeration degree is an equivalence class of sets of natural numbers under enumeration reducibility, where one set is computed from positive information about another.

Epimenides paradox

The Epimenides paradox, also called the Cretan paradox, is a self-reference puzzle from the saying "all Cretans are liars" by Epimenides of Crete, quoted at Titus 1:12.

Epistemic modal logic

Epistemic modal logic, also called epistemic logic, is the branch of modal logic that formalizes knowledge and belief with operators like "agent a knows that". Jaakko Hintikka's 1962 book founded the field.

Equational logic

Equational logic is the formal logic whose only formulas are identities s = t between terms, underlying universal algebra and term rewriting; Birkhoff proved it sound and complete in 1935.

Equivalence class

An equivalence class is the subset collecting all elements related to a given element by an equivalence relation; the classes form a partition of the set.

Equivalents of the axiom of choice

The equivalents of the axiom of choice are statements provably equivalent to it over ZF, including Tychonoff's theorem, Zorn's lemma, and every vector space having a basis.

Ernst Mally

Ernst Mally (1879–1944) was an Austrian philosopher at the University of Graz, a pupil of Alexius Meinong, who proposed the first formal system of deontic logic in 1926.

Euler diagram

An Euler diagram represents sets as labeled closed curves whose spatial arrangement shows containment, intersection, and exclusion. Euler introduced it in 1761, and unlike Venn diagrams it draws only relevant intersections.

Exclusive or

Exclusive or (XOR, exclusive disjunction) is the logical connective that yields true when exactly one of its two operands is true, written ⊕ or ⊻.

Existential quantification

Existential quantification, or the existential quantifier, is the logical operation written ∃ asserting a formula holds for at least one value of a variable, one of the two standard quantifiers of first-order logic.

Existentially closed model

An existentially closed model, also called an existentially complete model, is a model of a theory that already solves every existential condition solvable in an extension.

Fagin's theorem

Fagin's theorem, proved by Ronald Fagin in 1974, states that a property of finite structures is in NP if and only if it is definable in existential second-order logic.

False dilemma

A false dilemma, also called a false dichotomy or either-or fallacy, is an informal fallacy that assumes only two options exist when other alternatives do.

Filter model

A filter model is a mathematical model of the untyped lambda-calculus whose elements are filters of intersection types, introduced by Barendregt, Coppo, and Dezani-Ciancaglini in 1983.

Filtration method

The filtration method is a proof technique in modal logic that converts an infinite Kripke model of a formula into a finite one, proving the finite model property.

Finite model property

The finite model property (FMP) is a property of a logic: every satisfiable formula has a finite model, giving a standard route to proving decidability in modal logic.

Finite set

A finite set is a set whose elements can be counted with a natural number n; the number n is the set's cardinality, and any set that is not finite is infinite.

Finite-variable infinitary logic

Finite-variable infinitary logic, L^k∞ω, allows infinitely long conjunctions and disjunctions but limits formulas to at most k variables, and its union over all finite k is the main yardstick of expressiveness in finite model theory.

Finitism

Finitism is a position in the philosophy of mathematics, due to David Hilbert, restricting reasoning to finite, executable arguments; it underpinned his program for proving mathematics consistent.

First-order logic

First-order logic, also called first-order predicate calculus, is a formal logical system whose quantifiers range over individual objects only; it is the standard language for formalizing mathematics.

First-order theory

A first-order theory is a set of sentences in a first-order language, typically given by a signature and axioms, and is the standard way to axiomatize parts of mathematics.

Fixed-point combinator

The fixed-point combinator, known as the Y combinator, is a lambda calculus term Y satisfying Y f = f(Y f), supplying recursion in a language without named definitions.

Fixed-point logic

Fixed-point logic is a family of extensions of first-order predicate logic with operators defining relations as fixed points; its best-known member, least fixed-point logic, captures polynomial time on finite ordered structures.

Focused proof

A focused proof is a cut-free sequent calculus proof organized into alternating phases around a single formula in focus, shown complete by Andreoli's 1992 focalization theorem.

Forcing (mathematics)

Forcing, also called the forcing method, is a technique in mathematical logic, devised by Paul Cohen in 1963, for proving independence results in set theory.

Forking (model theory)

Forking is a dependence relation on types in model theory, introduced by Saharon Shelah, whose negation, non-forking, serves as an abstract independence relation generalizing linear and algebraic independence.

Formal language

A formal language is a possibly infinite set of finite strings over an alphabet, defined purely by form rather than meaning, usually specified by a formal grammar such as a context-free grammar.

Formal science

A formal science is a discipline, such as mathematics, logic, and theoretical computer science, that establishes its claims by proof within defined symbolic systems rather than by experiment.

Formal system

A formal system, or formal logical system, is a set of axioms and inference rules for generating theorems, with proofs checkable mechanically; it underlies Gödel's incompleteness theorems.

Foundations of mathematics

Foundations of mathematics, also known as foundations of math, studies the logical and set-theoretic frameworks underlying mathematics, from Russell's paradox and Gödel's incompleteness theorems to modern proof assistants.