\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{Kripke-Joyal semantics}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{formulation}{Formulation}\dotfill \pageref*{formulation} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{lawvere_on_kripkejoyal_semantics}{Lawvere on Kripke-Joyal semantics}\dotfill \pageref*{lawvere_on_kripkejoyal_semantics} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

\textbf{Kripke-Joyal semantics} is a higher order generalization of the [[semantics|semantic]] interpretation proposed initially by Beth, Gregorczyk, and Kripke for [[intuitionistic logic|intuitionistic predicate logic]]. It provides a notion of \emph{`local truth'} or \emph{`validity at a stage'} in a [[topos]].

Since it is closely related to [[Paul Cohen|Paul Cohen's]] [[forcing]] technique in [[set theory]], a connection that was already observed by Gregorczyk and Kripke, it is sometimes called \emph{forcing} semantics. Other terms in use for it are \emph{external} semantics , \emph{cover} semantics or \emph{Beth-Kripke-Joyal} semantics.

By giving a semantics to formulas written in the [[higher-order logic|higher-order]] [[type theory]] used to express [[ordinary mathematics]] in a topos, the Kripke-Joyal semantics serves as [[semantics|semantic]] interface between the [[internalisation|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 [[Saul Kripke|Kripke]] et al.

There should be a version of Kripke-Joyal semantics for [[homotopy type theory]], as claimed \href{n-types+cover#InModels}{here}.

\hypertarget{formulation}{}\subsection*{{Formulation}}\label{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 $\varphi (x)$ with one free variable $x$ of type $X$. The straight forward generalization to the case with (less or) more free variables can be found in Johnstone (\href{JT77}{1977}) or Borceux (\hyperlink{Borceux94}{1994}).

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

\begin{displaymath}
\itexarray{
\{x|\varphi(x)\}&\to & 1& \\
\downarrow &  &\downarrow &\mathsf{true} \\
X &\underset{\varphi(x)}{\to} & \Omega&
}
\end{displaymath}
Now a global element $1\overset{x_0}{\to} X$ satisfies $\varphi(x)$ if it is contained in $\{x|\varphi(x)\}$ in the sense that the following commutes:

\begin{displaymath}
\itexarray{
& &\{x|\varphi(x)\}&\to & 1 &\\
 &\nearrow&\downarrow &  &\downarrow &\mathsf{true} \\
1&\underset{x_0}{\to}& X &\underset{\varphi(x)}{\to} & \Omega&
}
\end{displaymath}
Kripke-Joyal semantics results from the generalization of this satisfaction relation from global elements to \emph{generalized} elements $U\overset{\alpha}{\to} X$.

\begin{defn}
\label{forcing}\hypertarget{forcing}{}
A generalized element $U\overset{\alpha}{\to} X$ is said to \emph{satisfy the formula} $\varphi(x)$ or more suggestively, $U$ \emph{forces} $\varphi$ , denoted $U\models \varphi (\alpha)$ , when $\alpha$ factors through $\{x|\varphi(x)\}$ i.e. there exists a map $m$ making the following commute:

\begin{displaymath}
\itexarray{
& &\{x|\varphi(x)\}&\to & 1& \\
 &\overset{m}\nearrow&\downarrow &  &\downarrow &\mathsf{true} \\
U&\overset{\alpha}{\to}& X &\underset{\varphi(x)}{\to} & \Omega&
}
\end{displaymath}
\end{defn}
This is the same as to say that $im\,\alpha\subseteq \{x|\varphi(x)\}$ as subobjects of $X$.

Whereas $\{x|\varphi(x)\}$ represents the set of elements satifying $\varphi$ internally, the collection of global elements has in general no such representation thereby motivating the terminology `external semantics'.

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

One can now unwind the forcing relation $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 \emph{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\'e{}nabou into a concrete mathematical object in the topos.

First of all, the forcing relation is \emph{monotone} and \emph{local} :

\begin{prop}
\label{Monotone_Local}\hypertarget{Monotone_Local}{}
If $f:V\to U$ and $U\models \varphi (\alpha)$ then $V\models \varphi (\alpha\circ f)$. Conversely, if $f:V\to U$ is \emph{epic} and $V\models \varphi (\alpha\circ f)$ then $U\models \varphi (\alpha)$.

\end{prop}
The short proof can be found in MacLane-Moerdijk (\hyperlink{MM94}{1994}, p.304).

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

\begin{prop}
\label{Kripke-Joyal}\hypertarget{Kripke-Joyal}{}
Let $\mathcal{E}$ be an elementary topos and $\alpha:U\to X\,$ a generalized element of $X\in\mathcal{E}$ . The forcing relation $\models$ satisfies

\begin{enumerate}%
\item $U\models \varphi(\alpha)\wedge \psi(\alpha)$ iff $U\models \varphi(\alpha)$ and $U\models \psi(\alpha)\,$.


\item $U\models \varphi(\alpha)\vee \psi(\alpha)$ iff there exists maps $g:U_1\to U$ and $g_2:U_2\to U$ with $g_1+g_2:U_1+U_2\to U$ epic and such that $U_1\models \varphi(\alpha\circ g_1)$ and $U_2\models \psi(\alpha\circ g_2)\,$.


\item $U\models \varphi(\alpha)\Rightarrow \psi(\alpha)$ iff for any $g:V\to U\,$, $V\models \varphi(\alpha\circ g)$ implies $V\models\psi(\alpha\circ g)\,$.


\item $U\models\neg \varphi(\alpha)$ iff for all $g:V\to U\,$, $V\models \varphi(\alpha\circ g)$ implies that $V\simeq 0$.



\end{enumerate}
Let $\varphi(x,y)$ be a formula with free variables x,y of type $X$ and $Y$ respectively. Then

\begin{enumerate}%
\item $U\models \exists y\varphi(\alpha, y)$ iff there exists $g:V\to U$ epic and a generalized element $h:V\to Y$ such that $V\models \varphi(\alpha\circ g,h)\,$.


\item $U\models \forall y\varphi(\alpha, y)$ iff for every object $V$ and all pairs of generalized elements $g:V\to U$ and $h:V\to Y\,$, $V\models \varphi(\alpha\circ g,h)\,$.



\end{enumerate}
\end{prop}
For a proof see MacLane-Moerdijk (\hyperlink{MM94}{1994}, pp.305f).

\hypertarget{lawvere_on_kripkejoyal_semantics}{}\subsection*{{Lawvere on Kripke-Joyal semantics}}\label{lawvere_on_kripkejoyal_semantics}

\begin{quote}%
To workers in algebraic geometry and analysis, it may appear somewhat excessive to detour through an elaborate Mitchell-B\'e{}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.


\end{quote}
Lawvere (\hyperlink{Law00}{2000}, pp.717f).

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[Mitchell–Bénabou language]]


\item [[internal logic]]


\item [[semantics]]


\item [[stack semantics]]


\item [[forcing]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

For the origins in the semantics of intuitionistic logic consult

\begin{itemize}%
\item E. W. Beth, \emph{Semantic construction of intuitionistic logic} , Mededel. Kon. Ned. Akad. Wetensch. Afd. letterkunde N. S. \textbf{19} no.13 (1956) pp.357-388.


\item A. Grzegorczyk, \emph{A philosophically plausible formal interpretation of intuitionistic logic} , Indagationes Mathematicae \textbf{26} (1964) pp.596--601.


\item [[Saul Kripke|S. A. Kripke]], \emph{Semantical analysis of intuitionistic logic I} , pp.92-130 in Crossley, Dummett (eds.), \emph{Formal Systems and Recursive Functions} , North-Holland Amsterdam 1965.


\item H. C. M. de Swart, \emph{An intuitionistically plausible interpretation of intuitionistic logic} , JSL \textbf{42} no. 4 (1977) pp.564-578.


\item W. Veldman, \emph{An intuitionistic completeness theorem for intuitionistic predicate calculus} , JSL \textbf{41} no. 1 (1976) pp.159-166.



\end{itemize}
A (non-categorical) textbook presentation of the original Kripke semantics can be found in

\begin{itemize}%
\item [[John Lane Bell|J. Bell]], M. Machover, \emph{A Course in Mathematical Logic} , North-Holland Amsterdam 1977. (section IX.6 pp.416-422)

\end{itemize}
A more recent overview is in

\begin{itemize}%
\item D. van Dalen, \emph{Intuitionistic Logic} , pp.224-257 in Goble (ed.), \emph{The Blackwell Guide to Philosophical Logic} , Oxford 2001. (pp.237-240)

\end{itemize}
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

\begin{itemize}%
\item [[Gerhard Osius|G. Osius]], \emph{A note on Kripke-Joyal semantics for the internal language of topoi} , Springer LNM \textbf{445} (1975) pp.349-354.

\end{itemize}
The following texts stress the connection to Cohen and Kripke's work

\begin{itemize}%
\item [[F. William Lawvere]], \emph{Variable sets etendu and variable structure in topoi} , Lecture notes University of Chicago 1975.


\item [[F. William Lawvere]], \emph{Variable quantities and variable structures in topoi} , pp.101-131 in Heller, Tierney (eds.), Algebra, Topology and Category Theory, Academic Press New York 1976.



\end{itemize}
Most textbooks on topos theory have a section on Kripke-Joyal semantics. Particularly thorough are

\begin{itemize}%
\item [[Francis Borceux]], \emph{Handbook of Categorical Algebra vol.3} , Cambridge UP 1994. (section 6.6)


\item [[Saunders MacLane]], [[Ieke Moerdijk]], \emph{[[Sheaves in Geometry and Logic]]} , Springer Heidelberg 1994. (section VI.6-7)



\end{itemize}
More concise are

\begin{itemize}%
\item [[Peter Johnstone]], \emph{Topos Theory} , Academic Press New York 1977. (Reprinted by Dover Mineola 2014; pp.157-161)


\item [[Colin McLarty]], \emph{Elementary Categories, Elementary Toposes} , Oxford UP 1992. (chapter 18)



\end{itemize}
Freely available online are

\begin{itemize}%
\item R. Goldblatt, \emph{Topoi - The Categorical Analysis of Logic} , 2nd ed. North-Holland Amsterdam 1984. (Dover reprint New York 2006; \href{http://projecteuclid.org/euclid.bia/1403013939}{project euclid}, section XIV.6)


\item [[Ieke Moerdijk]], [[Jaap van Oosten]], \emph{Topos theory}, lecture notes (2007). (\href{http://www.staff.science.uu.nl/~ooste110/syllabi/toposmoeder.pdf}{pdf}, page 58ff)



\end{itemize}
The above Lawvere quote stems from

\begin{itemize}%
\item F. W. Lawvere, \emph{Comments on the development of topos theory} , pp.715-734 in Pier (ed.), \emph{Development of Mathematics 1950-2000} , Birkh\"a{}user Basel 2000. Reprinted as TAC reprint \textbf{24} (2014) pp.1-22. (\href{http://www.tac.mta.ca/tac/reprints/articles/24/tr24abs.html}{TAC})

\end{itemize}
For a philosophical assessment and comparison to ordinary Tarski semantics see

\begin{itemize}%
\item J. Petitot, \emph{La Neige est Blanche ssi\ldots{} Pr\'e{}dication et Perception} , Math. Inf. Sci. Hum \textbf{35} no.140 (1997) pp.35-50. (\href{http://archive.numdam.org/article/MSH_197_140_35_0.pdf}{pdf})

\end{itemize}
A generalization to [[quantales]] is in

\begin{itemize}%
\item R. Goldblatt, \emph{A Kripke-Joyal Semantics for Noncommutative Logic in Quantales} , pp.209-225 in Governatori, Hodkinson, Venema (eds.), \emph{Advances in Model Logic vol. 6} , College Publications London 2006. (\href{http://www.mcs.vuw.ac.nz/~rob/papers/aiml11printed.pdf}{draft})

\end{itemize}
[[!redirects Kripke model]] [[!redirects Kripke models]]

[[!redirects Beth-Kripke-Joyal semantics]] [[!redirects Kripke-Joyal semantics]] [[!redirects Kripke–Joyal semantics]] [[!redirects Kripke--Joyal semantics]]

[[!redirects external semantics]]



\end{document}