nLab Kripke-Joyal semantics

Contents

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

Kripke–Joyal semantics is a higher order generalization of the semantic interpretation proposed initially by Beth, Grzegorczyk, and Kripke for intuitionistic predicate logic (IPL). It provides a notion of ‘local truth’ or ‘validity at a stage’ in a topos.

Since it is closely related to Paul Cohen's forcing technique in set theory, a connection that was already observed by Grzegorczyk and Kripke, it is sometimes called forcing semantics. Other terms in use for it are external semantics, cover semantics or Beth–Kripke–Joyal semantics.

By giving a semantics to formulas written in the higher-order type theory used to express ordinary mathematics in a topos, the Kripke–Joyal semantics serves as semantic interface between the internal (syntactic) description of mathematical objects using the Mitchell–Bénabou language and the external description.

Kripke–Joyal semantics provides rules and prescriptions for semantic interpretation for general toposes but these prescriptions may simplify for special classes of toposes e.g. the rules resulting for presheaf toposes over posets (when restricted to first-order formulas) correspond to the original notion of model for IPL considered by Kripke et al.

Kripke–Joyal semantics for homotopy type theory, as claimed here, can be found in Awodey, Gambino, and Hazratpour (2021).

Formulation

Let \mathcal{E} be an elementary topos. We will now specify the Kripke–Joyal semantics for formulas φ\varphi in the Mitchell–Bénabou language of \mathcal{E} restricting ourselves mainly to formulas φ(x)\varphi (x) with one free variable xx of type XX. The straightforward generalization to the case with (less or) more free variables can be found in Johnstone (1977) or Borceux (1994).

Recall that such a formula φ(x)\varphi (x) is interpreted by a morphism Xφ(x)ΩX\overset{\varphi(x)}{\to}\Omega and gets an extension {x|φ(x)}\{x|\varphi(x)\} assigned to by the pullback

{x|φ(x)} 1 true X φ(x) Ω \array{ \{x|\varphi(x)\}&\to & 1& \\ \downarrow & &\downarrow &\mathsf{true} \\ X &\underset{\varphi(x)}{\to} & \Omega& }

Now a global element 1x 0X1\overset{x_0}{\to} X satisfies φ(x)\varphi(x) if it is contained in {x|φ(x)}\{x|\varphi(x)\} in the sense that the following commutes:

{x|φ(x)} 1 true 1 x 0 X φ(x) Ω \array{ & &\{x|\varphi(x)\}&\to & 1 &\\ &\nearrow&\downarrow & &\downarrow &\mathsf{true} \\ 1&\underset{x_0}{\to}& X &\underset{\varphi(x)}{\to} & \Omega& }

Kripke–Joyal semantics results from the generalization of this satisfaction relation from global elements to generalized elements UαXU\overset{\alpha}{\to} X.

Definition

A generalized element UαXU\overset{\alpha}{\to} X is said to satisfy the formula φ(x)\varphi(x) or more suggestively, UU forces φ\varphi, denoted Uφ(α)U\models \varphi (\alpha), when α\alpha factors through {x|φ(x)}\{x|\varphi(x)\} i.e. there exists a map mm making the following commute:

{x|φ(x)} 1 m true U α X φ(x) Ω \array{ & &\{x|\varphi(x)\}&\to & 1& \\ &\overset{m}\nearrow&\downarrow & &\downarrow &\mathsf{true} \\ U&\overset{\alpha}{\to}& X &\underset{\varphi(x)}{\to} & \Omega& }

This is the same as to say that imα{x|φ(x)}im\,\alpha\subseteq \{x|\varphi(x)\} as subobjects of XX.

Whereas {x|φ(x)}\{x|\varphi(x)\} represents the set of elements satisfying φ\varphi internally, the collection of global elements has in general no such representation thereby motivating the terminology ‘external semantics’.

Properties

One can now unwind the forcing relation Uφ(α)U\models \varphi (\alpha) recursively over the syntactic composition of φ\varphi. This results in a collection of semantic rules that is commonly referred to as the Kripke–Joyal semantics and permits to make contact with the original rules proposed by Kripke for intuitionistic logic in 1965.

These rules are often useful for translating step by step an object defined by a formula of the Mitchell–Bénabou language into a concrete mathematical object in the topos.

First of all, the forcing relation is monotone and local :

Proposition

If f:VUf:V\to U and Uφ(α)U\models \varphi (\alpha) then Vφ(αf)V\models \varphi (\alpha\circ f). Conversely, if f:VUf:V\to U is epic and Vφ(αf)V\models \varphi (\alpha\circ f) then Uφ(α)U\models \varphi (\alpha).

The short proof can be found in MacLane–Moerdijk (1994, p.304).

Note that the proposition gives a first hint of the importance of epimorphisms or covers in this semantics, testimony of its geometric underpinning.

Theorem

Let \mathcal{E} be an elementary topos and α:UX\alpha:U\to X\, a generalized element of XX\in\mathcal{E} . The forcing relation \models satisfies

  1. Uφ(α)ψ(α)U\models \varphi(\alpha)\wedge \psi(\alpha) iff Uφ(α)U\models \varphi(\alpha) and Uψ(α)U\models \psi(\alpha)\,.

  2. Uφ(α)ψ(α)U\models \varphi(\alpha)\vee \psi(\alpha) iff there exists maps g:U 1Ug:U_1\to U and g 2:U 2Ug_2:U_2\to U with g 1+g 2:U 1+U 2Ug_1+g_2:U_1+U_2\to U epic and such that U 1φ(αg 1)U_1\models \varphi(\alpha\circ g_1) and U 2ψ(αg 2)U_2\models \psi(\alpha\circ g_2)\,.

  3. Uφ(α)ψ(α)U\models \varphi(\alpha)\Rightarrow \psi(\alpha) iff for any g:VUg:V\to U\,, Vφ(αg)V\models \varphi(\alpha\circ g) implies Vψ(αg)V\models\psi(\alpha\circ g)\,.

  4. U¬φ(α)U\models\neg \varphi(\alpha) iff for all g:VUg:V\to U\,, Vφ(αg)V\models \varphi(\alpha\circ g) implies that V0V\simeq 0.

Let φ(x,y)\varphi(x,y) be a formula with free variables x,y of type XX and YY respectively. Then

  1. Uyφ(α,y)U\models \exists y\varphi(\alpha, y) iff there exists g:VUg:V\to U epic and a generalized element h:VYh:V\to Y such that Vφ(αg,h)V\models \varphi(\alpha\circ g,h)\,.

  2. Uyφ(α,y)U\models \forall y\varphi(\alpha, y) iff for every object VV and all pairs of generalized elements g:VUg:V\to U and h:VYh:V\to Y\,, Vφ(αg,h)V\models \varphi(\alpha\circ g,h)\,.

For a proof see MacLane–Moerdijk (1994, pp.305f).

Lawvere on Kripke–Joyal semantics

To workers in algebraic geometry and analysis, it may appear somewhat excessive to detour through an elaborate Mitchell–Bénabou language which in turn requires a Kripke–Joyal semantics in order to get back at the mathematical content of a specific topos. (That sometimes-recommended procedure is strictly analogous to defining a group to be the quotient of the free group generated by itself, which analogously is sometimes useful). The key clause in that semantics was presupposed in the title ‘Quantifiers and Sheaves’, but the linear case was a theorem in Godement 1958 and indeed just expresses in terms of 20th century concepts the content of Volterra’s local existence theorem. Briefly,

a) the rule of inference for existential quantification is just a symbolic expression of the universal property enjoyed by the geometric image of any map (not only in the category of sets where the axiom of choice holds, but) in any topos,

b) a figure lying in such an image comes in fact only locally from figures in the domain of the map.

Lawvere (2000, pp.717f).

References

For the origins in the semantics of intuitionistic logic consult

  • E. W. Beth, Semantic construction of intuitionistic logic, Mededel. Kon. Ned. Akad. Wetensch. Afd. letterkunde N. S. 19 no.13 (1956) pp.357–388.

  • A. Grzegorczyk, A philosophically plausible formal interpretation of intuitionistic logic, Indagationes Mathematicae 26 (1964) pp.596–601.

  • S. A. Kripke, Semantical analysis of intuitionistic logic I, pp.92–130 in Crossley, Dummett (eds.), Formal Systems and Recursive Functions, North-Holland Amsterdam 1965.

  • H. C. M. de Swart, An intuitionistically plausible interpretation of intuitionistic logic, JSL 42 no. 4 (1977) pp.564–578.

  • W. Veldman, An intuitionistic completeness theorem for intuitionistic predicate calculus, JSL 41 no. 1 (1976) pp.159–166.

A categorical-constructive take on these completeness results is in

  • Erik Palmgren, Constructive Sheaf Semantics, Math. Log. Quart. 43 (1997) pp.321-327.

A (non-categorical) textbook presentation of the original Kripke semantics can be found in

  • J. Bell, M. Machover, A Course in Mathematical Logic, North-Holland Amsterdam 1977. (section IX.6 pp.416–422)

A more recent overview is in

  • D. van Dalen, Intuitionistic Logic, pp.224–257 in Goble (ed.), The Blackwell Guide to Philosophical Logic, Oxford 2001. (pp.237–240)

The topos-theoretic generalization is usually attributed to André Joyal who observed in the early 70s that this topos semantics subsumes various notions of forcing but his work was apparently not published. An early reference is

  • G. Osius, A note on Kripke–Joyal semantics for the internal language of topoi, Springer LNM 445 (1975) pp.349–354.

The first section of the following sums up a 1973 talk and gives an interesting informal overview of the basics involved emphazising sites

  • Anders Kock, Universal Projective Geometry via Topos Theory, JPAA 9 (1976) pp.1-24.

The following texts stress the connection to Cohen and Kripke’s work

  • F. William Lawvere, Variable sets etendu and variable structure in topoi, Lecture notes University of Chicago 1975.

  • F. William Lawvere, Variable quantities and variable structures in topoi, pp.101–131 in Heller, Tierney (eds.), Algebra, Topology and Category Theory, Academic Press New York 1976.

Most textbooks on topos theory have a section on Kripke–Joyal semantics. Particularly thorough are

More concise are

  • Peter Johnstone, Topos Theory, Academic Press New York 1977. (Reprinted by Dover Mineola 2014; pp.157–161)

  • Colin McLarty, Elementary Categories, Elementary Toposes, Oxford UP 1992. (chapter 18)

Freely available online are

  • R. Goldblatt, Topoi – The Categorical Analysis of Logic, 2nd ed. North-Holland Amsterdam 1984. (Dover reprint New York 2006; project euclid, section XIV.6)

  • Ieke Moerdijk, Jaap van Oosten, Topos theory, lecture notes (2007). (pdf, page 58ff)

The above Lawvere quote stems from

  • F. W. Lawvere, Comments on the development of topos theory, pp.715–734 in Pier (ed.), Development of Mathematics 1950–2000, Birkhäuser Basel 2000. Reprinted as TAC reprint 24 (2014) pp.1–22. (TAC)

For a philosophical assessment and comparison to ordinary Tarski semantics see

  • Jean Petitot, La neige est blanche ssi… Prédication et perception, Mathématiques et Sciences humaines, Tome 140 (1997) pp.35–50. (pdf)

A generalization to quantales is in

  • R. Goldblatt, A Kripke–Joyal Semantics for Noncommutative Logic in Quantales, pp.209–225 in Governatori, Hodkinson, Venema (eds.), Advances in Model Logic vol. 6, College Publications London 2006. (draft)

Semantics via generalized elements in categories with pullbacks is studied in

  • Anders Kock, Elementwise semantics in categories with pull-backs, arXiv:2004.14731 (2020). (abstract)

Kripke-Joyal semantics for Homotopy type theory are developed in

Last revised on April 30, 2023 at 04:22:14. See the history of this page for a list of all contributions to it.