|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
Kripke-Joyal semantics is a higher order generalization of the semantic interpretation proposed initially by Beth, Gregorczyk, and Kripke for intuitionistic predicate logic. 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 Gregorczyk 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 provide 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.
Let be an elementary topos. We will now specify the Kripke-Joyal semantics for formulas in the Mitchell-Bénabou language of restricting ourselves mainly to formulas with one free variable of type . The straight forward generalization to the case with (less or) more free variables can be found in Johnstone (1977) or Borceux (1994).
Recall that such a formula is interpreted by a morphism and gets an extension assigned to by the pullback
Now a global element satisfies if it is contained in in the sense that the following commutes:
Kripke-Joyal semantics results from the generalization of this satisfaction relation from global elements to generalized elements .
A generalized element is said to satify the formula or more suggestively, forces , denoted , when factors through i.e. there exists a map making the following commute:
This is the same as to say that as subobjects of .
Whereas represents the set of elements satifying internally, the collection of global elements has in general no such representation thereby motivating the terminology ‘external semantics’.
One can now unwind the forcing relation recursively over the syntactic composition of . 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 into a concrete mathematical object in the topos.
First of all, the forcing relation is monotone and local :
If and then . Conservely, if is epic and then .
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.
Let be an elementary topos and a generalized element of . The forcing relation satisfies
iff and .
iff there exists maps and with epic and such that and .
iff for any , implies .
iff for all , implies that .
Let be a formula with free variables x,y of type and respectively. Then
iff there exists epic and a generalized element such that .
iff for every object and all pairs of generalized elements and , .
For a proof see MacLane-Moerdijk (1994, pp.305f).
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).
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 (non-categorical) textbook presentation of the original Kripke semantics can be found in
A more recent overview is in
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
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
Francis Borceux, Handbook of Categorical Algebra vol.3 , Cambridge UP 1994. (section 6.6)
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)
The above Lawvere quote stems from
For a philosophical assessment and comparison to ordinary Tarski semantics see
A generalization to quantales is in