Mathematical logic

Mathematical logic studies formal languages, proofs, models, computability, and the foundations of mathematics.

A logic allowing quantification over relations or subsets of the object domain as well as over its individual objects. The range of relation quantifiers depends on the chosen semantics.

Second-order quantifiers range over specified collections of relations, which can be proper subcollections of all external relations. With these collections as additional sorts, this is a form of first-order logic. Full-class conclusions cannot be inferred merely from truth with Henkin semantics.

Every subset or relation of the appropriate arity on the object domain is allowed as a value of a second-order variable. For a domain $V_{\lambda }$, an external functional graph with all its individual ordered pairs in $V_{\lambda }$ is therefore available, even if the whole graph does not belong to $V_{\lambda }$.

Second-order arithmetic has variables for natural numbers and for sets of natural numbers. Subsystems restrict comprehension and induction; arithmetical transfinite recursion theory is one important subsystem stronger than the first-order system Peano arithmetic.

Arithmetical transfinite recursion theory permits arithmetic recursive definitions along coded countable well-orders, together with the usual arithmetic comprehension background. Friedman's finite form of Kruskal's theorem is not provable in this theory.

A formal proof is a finite sequence of formulae in which every line is an axiom, an assumption, or follows from earlier lines by a specified inference rule.

The infinitary language $L_{\kappa ,\lambda }$ permits conjunctions and disjunctions of fewer than $\kappa$ formulas and simultaneous quantification over fewer than $\lambda$ variables. Ordinary first-order logic is $L_{\omega ,\omega }$.

The logic $L_{{\omega }_1,\omega }$ extends first-order logic by countable logical conjunctions and logical disjunctions. Each formula has finitely many free variables, and quantifier strings are finite. In a countable first-order language, every countable structure has a Scott sentence in this logic that characterizes its isomorphism class among countable structures.

Every countable structure in a countable first-order language has a Scott sentence. Hence countable structures satisfying the same sentences of countable infinitary logic are isomorphic. The proof uses Scott formulas, stabilization on the countable set of finite tuples, and the back-and-forth method.

A Scott sentence for a countable structure is a sentence of countable infinitary logic satisfied, among countable structures in the same first-order language, exactly by its isomorphic copies. It may also have uncountable models. Scott formulas and stabilized back-and-forth method equivalences give its construction.

A Scott formula describes a finite tuple at a transfinite stage of the back-and-forth method. Stage zero specifies the complete atomic description; successor stages specify matching one-element extensions in both directions; limit stages conjoin the earlier descriptions. For a countable structure the equivalences on its finite tuples stabilize at a countable ordinal.

A propositional theory is a set of propositional formulas, sometimes identified with its deductive closure. It is a consistent set of formulae when contradiction is not derivable from it. The completeness theorem for propositional logic identifies consistency with existence of a satisfying Boolean valuation.

A propositional type is a collection of propositional formulas to be jointly realized by a Boolean valuation. A valuation realizes it when every member is true and omits it when some member is false. For propositional omission arguments, the collection need not itself be consistent.

If a consistent propositional theory locally omits every member of a countable family of propositional types, it has a Boolean valuation omitting them all. One may also impose any finite condition consistent with the theory. Successively extend the condition by a negated member of the next type; local omission preserves consistency. The propositional compactness theorem then supplies the valuation. Countability of the ambient language and decidability of consistency are not needed for this argument.

Relative to a consistent propositional theory $T$, a nonprincipal propositional type has no formula consistent with $T$ that implies every member modulo $T$. Equivalently, for each finite condition $\theta$ consistent with $T$, some member $\sigma$ leaves $T\cup \{\theta ,\neg \sigma \}$ consistent. This is the local omission condition for the extended omitting types theorem for propositional logic.

A propositional formula is built from atomic propositions using logical connectives. Unlike a first-order formula, it has no quantifiers over individuals. A Boolean valuation interprets its atoms as truth values and evaluates its connectives recursively.

An implication is derivable from a theory precisely when its conclusion is derivable after adjoining its antecedent. Together with classical contradiction rules, this identifies failure to prove a proposition with consistency after adjoining its negation.

Classical propositional logic interprets propositions as true or false and validates principles such as the law of excluded middle and double-negation elimination.

The law of excluded middle asserts that every proposition $A$ satisfies $A\vee \neg A$.

Double-negation elimination is the inference from $\neg \neg A$ to $A$.

A Boolean valuation assigns each primitive proposition one of the truth values zero and one and extends recursively through the logical connectives.

A truth table lists a finite formula's value for every Boolean valuation of the finitely many primitive propositions that occur in it.

A proposition is a statement to which a logical truth value can be assigned.

A logical connective forms a compound proposition from one or more propositions.

Logical implication forms the proposition $A\to B$. In intuitionistic logic its proof consists of a construction that transforms any proof of $A$ into a proof of $B$.

The contrapositive of $A\to B$ is $\neg B\to \neg A$. In classical propositional logic an implication and its contrapositive are logically equivalent, so either can be proved in place of the other.

The conjunction $A\wedge B$ holds when both $A$ and $B$ hold.

The disjunction $A\vee B$ holds when at least one of $A$ and $B$ holds. Constructively, a proof records which disjunct holds and provides its proof.

Logical truth is the nullary connective that is always true.

Logical falsity is the nullary connective with no proof.

Natural deduction presents logic through introduction and elimination rules for each logical connective.

The rule with premises $C,D$ and conclusion $C$ retains the first derivation while allowing an unused second assumption. Under the Curry-Howard correspondence, the output term is the first premise term, with the enlarged context. This allows a lambda abstraction whose bound variable does not occur in its body.

From $A\to B$ and $A$, implication elimination derives $B$. Under the Curry-Howard correspondence, this is application: from lambda terms $f:A\to B$ and $a:A$ form $fa:B$.

The implication introduction rule discharges a temporary assumption $A$ from a derivation of $B$, producing $A\to B$. Under the Curry-Howard correspondence, a body $t:B$ under $a:A$ gives the lambda abstraction $\lambda a^A.t:A\to B$. Unused assumptions may also be discharged.

Intuitionistic propositional logic omits unrestricted excluded middle and interprets implication constructively.

A lattice is a partially ordered set in which every pair has a greatest lower bound, called its meet, and a least upper bound, called its join.

A complete lattice is a partially ordered set in which every subset has a meet and a join, including the empty subset.

Every order-preserving function from a complete lattice to itself has a least and a greatest fixed point. More strongly, its set of fixed points is itself a complete lattice.

A distributive lattice is a lattice in which meet distributes over join and, equivalently, join distributes over meet.

In a distributive lattice,

A Boolean algebra is a bounded distributive lattice in which every element has a complement. Its meet, join, and complement abstract conjunction, disjunction, and negation.

A lattice filter is a nonempty upward-closed subset closed under finite meets. A proper filter omits the bottom element.

A prime filter is a proper lattice filter $P$ such that $a\vee b\in P$ implies $a\in P$ or $b\in P$.

If a lattice filter $F$ and lattice ideal $I$ in a distributive lattice are disjoint, there is a prime filter of a distributive lattice containing $F$ and disjoint from $I$.

A lattice ideal is a nonempty downward-closed subset closed under finite joins. It is the order-dual notion to a lattice filter.

Priestley duality is a dual equivalence between bounded distributive lattices and compact totally order-disconnected ordered topological spaces.

The Priestley dual space $\hat{L}$ of a bounded distributive lattice $L$ consists of its prime filters, ordered by inclusion and topologized by the sets $a^{\ast }=\{P:a\in P\}$ and their complements.

A clopen up-set is both clopen in the topology and upward closed in the order. The clopen up-sets of a Priestley space form a distributive lattice under intersection and union.

The Stone map sends an element $a$ of a distributive lattice to the clopen up-set $a^{\ast }=\{P:a\in P\}$ of its Priestley dual space. The Stone prime filter theorem makes this lattice homomorphism injective.

A Heyting algebra is a bounded distributive lattice with an implication $a\Rightarrow b$ characterized by $x\le (a\Rightarrow b)$ exactly when $x\wedge a\le b$.

Meets of subsheaves are pointwise intersections. Joins are J-closures of pointwise unions: a section lies in the join when its restrictions locally belong to some member, with the member allowed to vary. Implication consists of sections every restriction of which belongs to $D$ whenever it belongs to $A$; this gives $C\le (A\Rightarrow D)$ exactly when $C\cap A\le D$. Negation is implication into the initial subobject. Empty covers mean that the initial sheaf need not be pointwise empty.

An element $a$ of a Heyting algebra is regular when $\neg \neg a=a$. The regular elements form its Booleanization.

In a Heyting algebra, meet with a fixed element is left adjoint to Heyting implication, so it preserves joins:The dual distributive law follows from this one by the lattice absorption laws.

In the implicational fragments, assumptions correspond to typed variables, implication introduction to lambda abstraction, and implication elimination to function application. Typing derivations in the simply typed lambda calculus correspond inductively to natural-deduction proofs.

The Curry-Howard correspondence identifies propositions with types and proofs with typed programs; implication corresponds to a function type, conjunction to a product type, and falsity to the empty type.

A Kripke model is a poset of worlds with a persistent valuation of atoms. Conjunction and disjunction are forced pointwise, while $w⊩\alpha \to \beta$ exactly when every $v\ge w$ that forces $\alpha$ also forces $\beta$.

The Kripke forcing relation $w⊩A$ records that formula $A$ holds at world $w$. For intuitionistic implication, $w⊩A\to B$ exactly when every extension of $w$ that forces $A$ also forces $B$.

If $w\le v$ and $w⊩A$, then $v⊩A$. The proof is by structural induction on $A$.

A Kripke countermodel to a formula $A$ is a Kripke model for intuitionistic propositional logic containing a world $w$ such that $w⊮A$.

A proposition is derivable in intuitionistic propositional logic exactly when it is forced at every world of every intuitionistic Kripke model.

Filtration identifies worlds that force the same formulas in a fixed finite subformula-closed set. With order induced by inclusion of these finite theories, the quotient preserves forcing of every retained formula and has at most $2^n$ worlds for $n$ formulas.

The unravelling of a rooted Kripke model has finite increasing paths from the root as worlds, ordered by extension and labelled by their endpoints. It is tree-like and preserves forcing.

Every intuitionistically underivable proposition has a finite rooted Kripke countermodel. Filtration and witness pruning bound the model in terms of the number of subformulas.

The disjunction property says that if ${⊢}_{\mathrm{IPC}}A\vee B$, then ${⊢}_{\mathrm{IPC}}A$ or ${⊢}_{\mathrm{IPC}}B$.

The implication-free fragment uses only conjunction, disjunction, truth, and falsity, with their intuitionistic natural-deduction rules.

An implication-free formula is provable exactly when every valuation into every bounded distributive lattice assigns it the top element.

The implicational fragment of intuitionistic propositional logic contains formulas built from atoms using only logical implication, with only implication introduction, implication elimination, and assumptions as proof rules.

The canonical worlds are deductively closed implicational theories ordered by inclusion. A world forces an atom exactly when the atom belongs to that theory. The truth lemma says that a world forces an implicational formula exactly when the formula belongs to the theory.

For implicational formulas $\Gamma$ and $\phi$,The reverse implication follows from the canonical Kripke model for implicational intuitionistic logic and its truth lemma.

If $\Gamma$ and $\phi$ are implicational and $\Gamma {⊢}_{\mathrm{IPC}}\phi$, then $\Gamma {⊢}_{\mathrm{IPC}(\to )}\phi$. Soundness for Kripke semantics followed by Kripke completeness of implicational intuitionistic logic proves the claim.

If $\Gamma ⊢t$, every valuation that satisfies all formulae in $\Gamma$ also satisfies $t$.

For a set of formulae $\Gamma$ and a formula $\phi$,Together with the soundness theorem for propositional logic, this says that semantic consequence and syntactic provability coincide. Equivalently, every consistent set of formulae has a satisfying Boolean valuation.

Assign a primitive proposition true exactly when it belongs to a maximal consistent set. An induction on formulas proves that truth agrees with membership: maximal consistency gives the negation dichotomy, and deductive closure gives the implication truth table. This builds a model of every consistent propositional theory.

Consistency is preserved under unions of chains because proofs use finitely many assumptions. A maximal consistent extension then gives a valuation through its truth lemma, proving propositional completeness.

When the primitive propositions are not countable, replace sequential enumeration of the formulae by Zorn lemma. The union of a chain of consistent extensions is consistent because every formal proof is finite, so every consistent theory extends to a maximal consistent set in propositional logic. Declaring an atom true exactly when it belongs to that maximal set and proving the truth lemma by structural induction produces a model.

There is an algorithm deciding whether any finite propositional formula is a theorem. A formula contains only finitely many atoms, so a finite truth table decides whether it is valid; the completeness theorem for propositional logic identifies validity with provability.

A set $S$ of formulae is deductively closed whenEquivalently, $S$ equals its deductive closure $\mathrm{Cn}(S)$.

A set $S$ is syntactically consistent when $S/⊢\perp$. Equivalently in classical logic, there is no formula $\phi$ for which both $S⊢\phi$ and $S⊢\neg \phi$.

A set $S$ is finitary when it is deductively equivalent to some finite set $F$: both $S⊢F$ and $F⊢S$.

Ifare deductively closed, then each $T_i$ is consistent and their union is consistent and deductively closed. The union is not finitary. Each conclusion follows from the finite character of formal proofs.

A consistent set $T$ is maximal consistent when no proper extension is consistent. It is deductively closed and decides every formula: exactly one of $t$ and $\neg t$ belongs to $T$. Therefore $v(t)=1$ exactly when $t\in T$ defines a model of $T$.

A set of propositions has a model exactly when every finite subset has a model. Syntactically, a contradiction uses only finitely many assumptions, and every consistent set extends by Zorn lemma to a maximal consistent set in propositional logic.

With atoms $p_{x,y}$, finitary propositions can enforce that the true pairs form an injective partial function. If the codomain is infinite, they cannot enforce that every $x$ has a value: adjoining every $\neg p_{x_0,y}$ remains finitely satisfiable, so compactness produces a model omitting $x_0$.

First-order logic permits quantification over elements of a structure while its nonlogical symbols describe operations, constants, and relations.

The fragment uses finite conjunction, set-indexed disjunction and existential quantification, with equality and atomic relations. It is preserved under inverse image functors of geometric morphisms. The universal closure of an axiom is expressed by its variable context, not an unrestricted universal-quantifier constructor.

A set of sequents between geometric formulas over a many-sorted signature. Its geometric syntactic category and geometric syntactic topology yield its classifying topos. A model satisfies a sequent when the interpreted antecedent subobject is contained in the consequent in the indicated context.

A geometric quotient adds geometric sequents over the same signature. Quotients are compared modulo provable equivalence. In a syntactic site the extra sequents become additional covers, giving a subtopos of the original classifying topos. Stronger axioms correspond to a larger site topology and a smaller subtopos.

Objects are geometric formulas in context modulo provable equivalence. Morphisms are provably total, single-valued geometric relations; composition is existential conjunction. Conjunction and equality give finite limits. Interpreting formulas in a model gives a finite-limit-preserving functor, with the additional continuity condition supplied by the geometric syntactic topology.

A family of definable arrows covers a formula when the theory proves that their images jointly exhaust that formula. Such covers encode disjunction and existential quantification. The resulting site presents the classifying topos of the geometric theory. Adding geometric axioms adds covering sieves, yielding the duality between geometric quotients and subtoposes.

A geometric formula is built from atoms by finite conjunction, arbitrary small disjunction and existential quantification. Empty conjunction and disjunction give truth and falsity. In a Grothendieck topos, these constructions use finite limits, unions and images. Formula contexts have finitely many variables.

Regular logic has atomic formulas and equality, truth, finite conjunction and unrestricted existential quantification. Its categorical semantics uses regular categories: conjunction is intersection and existential quantification is image. Disjunction and falsity are not added as formula constructors in the regular fragment.

A regular theory has axioms that are sequents between regular formulas. It has a regular syntactic category and a classifying topos of sheaves for the regular coverage. Its regular formulas enjoy the disjunction property of regular theories when a finite disjunction is allowed as an outer coherent conclusion.

If a regular theory proves an outer coherent sequent $\varphi ⊢{\bigvee }_{i=1}^n{\psi }_i$ with all formulas regular, it proves $\varphi ⊢{\psi }_i$ for some $i$. In the classifying topos, the corresponding subobjects cover the representable associated with $\varphi$. Irreducibility of that representable and full faithfulness of the syntactic Yoneda embedding produce the desired derivation.

The regular syntactic category has regular formulas-in-context as objects and provably functional regular relations as arrows. It has finite limits and stable image factorizations, with existential quantification supplying images. The regular coverage on this category presents the classifying topos of the theory.

A regular formula is built using the constructors of regular logic, with a finite variable context. The image of a definable relation interprets an existential quantifier. Regular formulas remain regular after substitution, conjunction and existential quantification.

A Cartesian theory uses a many-sorted first-order signature and sequents between Cartesian formulas. The fragment contains equality, atomic relations, truth, finite conjunction and existential quantification with provably unique witnesses. It has a Cartesian syntactic category with finite limits, whose finite-limit-preserving functors classify its internal models. Arbitrary existential quantification, disjunction and falsity are not added as finite-limit constructors.

In the positive finite-limit convention, a Horn theory uses atomic finite-conjunction sequents; uniquely witnessed existential extensions remain Cartesian. Its models are the finite-limit-preserving functors out of its Cartesian syntactic category. This convention does not insert arbitrary existential witnesses or falsity as Cartesian constructors. Its classifier is the presheaf classifier of a Horn theory.

Internal Horn models are finite-limit-preserving functors out of the Cartesian syntactic category. Since that category has finite limits, these are exactly flat functors; the presheaf Diaconescu equivalence for geometric morphisms proves the classifying property. Equivalently the classifier is the covariant functor category on finitely presented set-based models.

Objects are Cartesian formulas-in-context modulo provable equivalence, and arrows are provably total single-valued Cartesian relations. Composition quantifies the unique intermediate tuple. Context concatenation, conjunction and equality give finite limits. Its canonical model interprets a formula as its own context subobject, so factorization of antecedent through consequent is exactly sequent derivability.