\def\pgfsysdriver{pgfsys-dvipdfmx.def} % ★PGFドライバを強制
\documentclass{amsart}
\usepackage[left=2cm, right=2cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{amsfonts, amsthm, amssymb, mathtools,etoolbox}
\usepackage{blindtext}
\usepackage[colorlinks=true, urlcolor=blue, linkcolor=blue, citecolor=blue]{hyperref}
\usepackage{tikz,tikz-cd}
\usepackage{cleveref}
\usepackage{array}
\usepackage[style=alphabetic,sorting=nyt]{biblatex}
\renewbibmacro{in:}{}
% \addbibresource{biblio.bib}
\addbibresource{CommonBiblio20240922.bib}
\tikzset{pullback/.style={minimum size=1.2ex,path picture={
\draw[opacity=1,black,-,#1] (-0.5ex,-0.5ex) -- (0.5ex,-0.5ex) -- (0.5ex,0.5ex);%
}}}
\usetikzlibrary{calc}
\usepackage{epigraph}


\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{todo}[theorem]{Todo}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{fact}[theorem]{Fact}

\theoremstyle{definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{notation}[theorem]{Notation}
\newtheorem{question}[theorem]{Question}
\newtheorem{answer}[theorem]{Answer}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{slogan}[theorem]{Slogan}

\newcommand{\dq}[1]{``#1"}
\newcommand{\memo}[1]{\textcolor{red}{memo: #1}}
\newcommand{\invmemo}[1]{\textcolor{blue}{本当は話したいこと: #1}}
\newcommand{\summary}[1]{\textcolor{green!70!black}{\textbf{summary: #1}}}
\newcommand{\para}[1]{\paragraph{\textbf{#1}}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\ob}{\mathrm{ob}}
\newcommand{\Set}{\mathbf{Set}}
\newcommand{\Top}{\mathbf{Top}}
\newcommand{\Topprof}{\mathbf{Top}_{\textrm{prof.}}}
\newcommand{\BoolAlg}{\mathbf{BoolAlg}}
\newcommand{\Topoi}{\mathbf{Topoi}}
\newcommand{\FinSet}{\mathbf{FinSet}}
\newcommand{\PSh}{\mathbf{PSh}}
\newcommand{\Sh}{\mathbf{Sh}}
\newcommand{\Cont}{\mathbf{Cont}}
\newcommand{\Func}[2]{[#1,#2]}
\newcommand{\abs}[1]{\left|#1\right|}
\newcommand{\demph}[1]{\textbf{#1}}
\font\maljapanese=dmjhira at 2.5ex
\newcommand{\yo}{\textrm{\!\maljapanese\char"48}}
\newcommand{\Pow}{\mathcal{P}}
\newcommand{\ignore}[1]{{\color{red!70!black} #1}}

\title{連結性とトポスの充満部分圏}
\author{Ryuya Hora}
\thanks{Graduate School of Mathematical Sciences, University of Tokyo. \url{hora@ms.u-tokyo.ac.jp}}
% % \date{\today}
% \subjclass[2020]{MSC}
% \keywords{Keywords}


\begin{document}
\begin{abstract}
このノートは，池先生に洞の博士論文の内容を説明するセミナーの参考資料である．
前半で，「幾何学と論理学をつなぐ理論」としてのトポス理論を，幾何学者向けに話す．
後半で，博士論文の$3$つの主定理について概説する．
\end{abstract}
\maketitle


\ignore{無視すると幾らかの正確さが失われるが，}赤い文字は無視して良い．
\tableofcontents
目的
\begin{itemize}
    \item \Cref{sec:ToposTheory}: 幾何学的な対象であるトポスが，なぜ論理学者(or 理論計算機学者)にとって有益なのか?を伝える
    \item \Cref{sec:PhDthesis}: 博士論文の$3$つの定理を，背景込みで概説する．
\end{itemize}




% \part{トポス入門}
% \section{幾何学におけるトポス (15分)}
% \section{論理学におけるトポス (15分)}
% \section{なぜ繋がるのか？(30分)}
\part{トポス理論入門}\label{sec:ToposTheory}
この節では，トポスが幾何と論理の双方に本質的に現れるということを説明する．全体に共通する思想は，\demph{操作論的}であるということで，超越的な仮定をおかず，「実際に我々に操作可能なもの」に徹底的に還元する立場である．



\section{幾何学におけるトポス (Grothendieck の見たトポス)}

\subsection{位相空間の一般化としてのトポス}

位相空間$X$に対して，その上の(集合値)層の圏を$\Sh(X)$と書く．このとき，位相空間$X$が最悪でなければ\footnote{Soberであれば，の意味．例えば，Hausdorff空間や多様体やschemeはsober．}，$X$は圏$\Sh(X)$から復元できる．この意味で，位相空間上の層の圏は位相空間の情報を十分に持っていると言える．\memo{微分構造や構造層などの付加構造も，$\Sh(X)$への付加構造だと思える．}

グロタンディークは，幾何学的道具(コホモロジーや基本群など)を数論へ応用できるようにするため，空間概念を拡張しようと試みた．そして，彼は
\[
\begin{tikzcd}
\text{空間}
  \arrow[r]
&
\text{空間上の層(=\dq{計測\footnote{arpentage\cite{grothendieck1992recoltes}}})}%
\end{tikzcd}
\]

というこれまでの枠組みを反転させ，
\[
\begin{tikzcd}
\text{空間}
&
\text{空間上の層(=\dq{計測})}\arrow[l]
\end{tikzcd}
\]
という\dq{操作論的な}立場に立った．
そして，位相空間上の層の圏を公理化したものを「空間にとって最も本質的なものの受肉\cite{grothendieck1992recoltes}」であるとし，\demph{トポス}と名付けた．

\begin{definition}[\cite{grothendieck1972SGA4}]
    圏$\E$がGrothendieck トポス\footnote{トポスと呼ばれる概念は二つある．Grothendieck トポスは，\cite{grothendieck1972SGA4}でtoposと呼ばれている概念である．Lawvereらによって導入された初等トポスは，Grothendieck トポスを含むより大きな圏のクラスである．See also \cite{johnstone2002sketchesv1, johnstone2002sketchesv2, maclane1994sheaves, caramello2018theories}.}であるとは，以下の同値な条件のいずれか，従って全てを満たすことをいう．
    \begin{itemize}
        \item ある小さい景$(\C,J)$が存在し，$\E\simeq \Sh(\C,J)$となる．
        \item $\E$は以下の圏論的条件を満たす．
        \begin{itemize}
        \item ある小圏$\C$が存在し，
            \item $\C$の前層圏$\PSh(\C)\coloneqq \Func{\C^{\op}}{\Set}$に$\E$は忠実充満に埋め込め$i\colon \E \hookrightarrow \PSh(\C)$,
            \item さらに埋め込み$i$は左随伴$L\dashv i$を持ち，
            \item さらに$L$は有限極限を保つ.
    \end{itemize}
        \item $\E$はlocally presentableな初等トポス\Cref{def:}である．
    \end{itemize}
\end{definition}


\subsection{連続写像の一般化としての幾何学的射}
さらに，トポス理論は連続写像の概念も一般化する．
\begin{fact}
    任意の連続写像$f\colon X\to Y$は，層の圏の間の随伴
\[
\begin{tikzcd}
\Sh(X)
  \arrow[r, shift right=1.4ex, "f_*"']
  \arrow[r, phantom, "\rotatebox{270}{$\dashv$}" description]
&
\Sh(Y)
  \arrow[l, shift right=1.4ex, "f^*"']
\end{tikzcd}
\]
を誘導し，さらに引き戻し関手$f^*$は有限極限を保つ．
\end{fact}

% 連続写像の概念の一般化も同様に存在する．
\begin{definition}[幾何学的射]
    トポス$\E$からトポス$\F$への\demph{幾何学的射}$f\colon \E \to \F$とは，随伴
    \[
\begin{tikzcd}
\E
  \arrow[r, shift right=1.4ex, "f_*"']
  \arrow[r, phantom, "\rotatebox{270}{$\dashv$}" description]
&
\F
  \arrow[l, shift right=1.4ex, "f^*"']
\end{tikzcd}
\]であって，左随伴部分$f^*$が有限極限を保つもののことをいう．
\end{definition}

引き戻し関手$f^*\colon \Sh(Y)\to \Sh(X)$を$X$は幾何学的射である．さらに，連続写像$f$は，「$X,Y$がsoberである」という非常にマイルドな条件を満たすとき，幾何学的射$f^*\colon \Sh(Y)\to \Sh(X)$から復元される．





\begin{fact}[トポスは位相空間の一般化]
    層の圏をとる操作$\Sh:\Top \to \Topoi$は，位相空間の圏$\Top$をだいたい\footnote{厳密には，$\Top$をsoberな位相空間の圏 (もしくは，より自然にはLocaleの圏)に取り替える必要がある．さらに，$\Topoi$は本来$2$圏なので，$2$圏的な構造も考慮する必要がある．この$2$点を訂正すれば厳密な主張になる．}忠実充満にトポスと幾何学的射の圏$\Topoi$に埋め込む.
\end{fact}


% \subsection{思想と広がり}

\memo{その思想: 群論的操作を空間とみなす．}

\section{論理学におけるトポス  (Lawvere の見たトポス)}

\subsection{論理学とトポスは密接に結びついているという事実}
\begin{itemize}
    \item \demph{連続体仮説の$ZFC$からの独立性}の Cohen トポスによる証明 (cf. \cite{maclane1994sheaves})
    \item \demph{選択公理の$ZF$からの独立性}のFreyd toposによる証明 \cite{freyd1980axiom}
    \item 様相論理の可能世界意味論と，トポスの内部言語 (cf. \cite{maclane1994sheaves})
    \item 時間軸\footnote{$+$ 付加構造}上の層のトポスを用いた，時制論理とシステムの\demph{安全性検証}\cite{schultz2019temporal}
    \item ボーアトポスを用いた，\demph{量子基礎論}\cite{landsman2017foundations}
    \item Lawvere-Tierney位相を用いた\demph{計算可能性理論} \cite{kihara2023lawvere}
    \item Schanuel toposを用いた\demph{選択公理}の(より繊細な)破壊 (\cite{fourman1980sheaf}+ongoing)
    \item Classifying topos of geometric theory
    \item Deligne's theorem (ある種の景に関する，stalk functorの存在定理)を用いた，ゲーデルの完全性定理の証明
\end{itemize}



\subsection{「意味 vs 構文」からトポスへの歴史}
\subsubsection{「意味 vs 構文」からトポスへの歴史 (1/) SignifiantとSignifi\'e}





\section{統一的なトポス理論へ}
\subsection{「論理 vs 幾何」からトポスへの歴史}
\begin{itemize}
    \item トポスは「操作の圏」であり，トポスによる架橋は\demph{空間への操作と論理的操作の対応}によって実現している．
    \item 「空間への操作と論理的操作の対応」という原理の原型は，ベン図(より正確にはオイラー図)まで遡ることができる．
    \item 
\end{itemize}
\subsubsection{「論理 vs 幾何」からトポスへの歴史(1/4) 命題とベン図}

\begin{quote}Leonhard Euler \cite{Euler1761LettreCIII}:
    これらの丸い図形，いやむしろ(どのような形を与えようともかまわないのですから)\textbf{空間}は，この主題についての考察を容易にするのに非常に適しており，\textbf{論理学}の中で自慢げに語られ，多大な苦労をして証明される神秘の全てを，私たちに明らかにしてくれるのです\footnote{著者訳, 強調も著者による．原文: Ces figures rondes, ou plutôt ces espaces (car il n'importe quelle figure nous leur donnions) sont très propres à faciliter nos réflexions sur cette matière, \& à nous découvrir tous les mystères dont on se vante dans la Logique, \& qu'on y démontre avec bien de la peine, ...
% pendant que par le moyen de ces signes tout saute d'abord aux yeux.
}．
\end{quote}

\subsubsection{「論理 vs 幾何」からトポスへの歴史(2/) ブール代数とprofinite space}

\begin{fact}[ストーン双対{\cite{stone1936theory, stone1937applications, doctor1964categories}}]
    $\BoolAlg^{\op} \simeq \Topprof$
\end{fact}

\subsubsection{「論理 vs 幾何」からトポスへの歴史 (3/) 直観主義論理と位相空間}
See \cite{maclane1994sheaves} for now.
\subsubsection{「論理 vs 幾何」からトポスへの歴史 (4/) 量化子と層}
\cite{lawvere1970quantifiers}
\subsection{トポスによる架橋} ローヴェアは，彼の論文「量化子と層」(Quantifiers and Sheaves \cite{lawvere1970quantifiers})の中で，グロタンディークの理論と論理の関係を明らかにした．そして，\demph{トポスに対する理論は幾何学的解釈と論理学的解釈の二面性を持つ}ことがわかった．数あるそのような「架橋の定理」の中でも，\cite{lawvere1970quantifiers}に現れる最も古典的な例が次である．
% 本来ならその主題である量化子の解釈について述べるべきだが(その時間はないので)，ここでは次の言葉を引用する．
\begin{quote} F. William Lawvere \cite{lawvere1970quantifiers}:
グロタンディーク「位相」は様相演算子という形で最も自然に現れる．
\footnote{著者訳．原文:
    ... a Grothendieck \dq{topology} appears most naturally
as a modal operator ...}
% , of the nature \dq{it is locally the case that}, 
\end{quote}

この言葉は，通常次の定理の形で述べられる．

\begin{fact}
    任意のトポス$\E$について，以下の$2$つのデータには一対一対応が存在する．
    \begin{description}
        \item[部分空間] \ignore{$\E$の部分トポス, つまり$\E$への幾何学的射$\E \leftarrow \F \colon f^*$であって，忠実充満な右随伴を持つもの．}
        \item[様相演算子] \ignore{$\E$の部分対象分類子$\Omega$上の自己射$j\colon \Omega \to \Omega$ であって，
        \begin{enumerate}
            \item $j(\top )=\top$
            \item $j(j(p))=j(p)$
            \item $j(p\land q)=j(p)\land j(q)$
        \end{enumerate}
        を満たすもの．}
    \end{description}
\end{fact}

\invmemo{ゲーデルの完全性定理とDeligneの存在定理，強制法とCohen topos，Kripke意味論とKripke-Joyal意味論，内部選択公理とBoolean étendue，排中律とBoolean topos．}


\section{ローヴェアの7つの未解決問題}
残念ながらローヴェアは2023年に亡くなった．しかし2009年，既に70歳を超えていたローヴェアは，集会でトポスの7つの未解決問題を提示し，次のように述べた．
\begin{quote}
    F. William Lawvere \cite{lawvere2025opennLab}: ここに挙げる七つの問題は，私がまだ解くことができていないものである．
これらが明確になれば，トポス理論やその熱力学，代数幾何学，論理学への応用の研究は，さらに前進するだろう\footnote{著者訳.原文: Here are seven problems that I have not yet been able to solve. Clarification on them would further advance work on topos theory and its applications to thermomechanics, to algebraic geometry, and to logic.}.
\end{quote}

\newpage
\part{博士論文概説}\label{sec:PhDthesis}
\section{toposの完全連結性 (20min)}\cite{hora2025grothendieck}\\

トポス$\E$の持つ様々な幾何学的な性質は，$\E$から$\Set$への唯一の幾何学的射
\[
\E\leftarrow \Set \colon \gamma_0
\]
の性質で表現される．
\ignore{例えば，
\begin{description}
    \item[連結性] トポス$\E$が\demph{連結}であるのは，\underline{$\gamma_0$が忠実充満}であるとき．
    % これは位相空間の連結性と整合的である．
    任意の位相空間$X$について，$X$が位相空間として連結なこととトポス$\Sh(X)$が連結なことは同値である．
    \item[局所連結性] トポス$\E$が\demph{局所連結}であるのは，\underline{$\gamma_0$が左随伴を持つ}とき．
    % これは位相空間の局所連結性と整合的である．
    任意の位相空間$X$について，$X$が位相空間として局所連結なこととトポス$\Sh(X)$が局所連結なことは同値である．
    \item[局所性]  トポス$\E$が\demph{局所}であるのは，\underline{$\gamma_0$が右随伴の右随伴を持つ}とき．
    任意の可換環$A$について，$A$が局所環なこととトポス$\Sh(\mathrm{Spec}A)$が局所なことは同値である．
\end{description}}


\cite{hora2025grothendieck}を元にした博論の第一部では，\ignore{まず$\gamma_0$の左右に続く随伴列を分類することで，「随伴の存在」として語ることができる}トポスの性質が$5$つであることを示した．さらに，その中で極端に研究が少ない\footnote{ないわけではない．\cite{hemelaer2021monoid}}ものを「完全連結性」と呼ぶことにした\footnote{本当のモチベーションはこのような技術的なものではなくて別にあるのだが...}．
\begin{definition}
    トポス$\E$が\demph{完全連結}であるとは，$\gamma_0$が左随伴の左随伴を持つことをいう．
\end{definition}

完全連結性は，これまで調べられてきたトポスの連結性概念\ignore{(連結性，局所連結性，安定局所連結性\cite{johnstone2011remarks}強連結性，トータル連結性\cite{bunge1996spreads})}のどれよりも強い，非常に極端な連結性概念である．それにもかかわらず，次が成立する．
\begin{proposition}[完全連結トポスは少なすぎない{\cite{hora2025grothendieck}}]
    \ignore{任意のトポスはある完全連結トポスの閉部分トポスである．}
\end{proposition}

完全連結性の定義は，\ignore{局所トポスの定義の「右随伴」を「左随伴」に形式的に変更したものになっており，}一見双対概念のように見える．しかし，\ignore{そもそもトポスの双対圏がトポスになることはほとんどなく\footnote{$\E$も$\E^\op$もトポスであれば，どちらも$1$点圏になる．}，}この双対性を数学的に記述するのは難しそうに見える．しかし，\cite{hora2025grothendieck}では，完全連結性が局所性と\dq{双対な\ignore{景による}特徴づけ}を持つことを示した．\ignore{この定理は，論文中の用語を用いて次のように述べられている．
\begin{theorem}\cite{hora2025grothendieck}
    トポスが完全連結であることと，ある完全連結景上の層の圏であることとは同値である．
\end{theorem}}

\invmemo{次の予想を示したい．良いトポスには，その双対トポスが存在する．互いに双対であるトポスについては，それらの次元の完備束が同型になる．}
\section{toposの商に関するLawvereの問題 (20min)}\cite{kamio2024solution}\\

トポスにも，商の概念がある．
\begin{definition}[商トポス]
    \ignore{トポス$\E$の(連結)\demph{商トポス}とは，$\E$からの幾何学的射$\E \leftarrow \F\colon f^*$であって忠実充満なものをいう．}
\end{definition}
商の概念は，トポスの論理学でも自然に現れる．例えば，(内部)選択公理を満たさないようなトポスの最も簡単な構成\footnote{基礎の公理を満たさないので独立性証明には使えないらしい．}は，Freydの論文「選択公理\cite{freyd1980axiom}」の導入部にも書かれている通り，\ignore{群$\Z$作用のトポス$\PSh(\Z)$の}商をとることである．
\invmemo{Permutation modelとの類似}

しかし，前述の「部分トポスと様相演算子の対応定理」に対して，商トポスの振る舞いに関する理論的成果はあまり知られていなかった．商トポスは本当に統制できないほどめちゃくちゃに氾濫しているのだろうか?それとも実は部分トポスのように，商トポスにも「商トポスと??の対応定理」が存在しているのだろうか?この問いこそがローヴェアの未解決問題の第一問であった．

\begin{quote}\cite{lawvere2025opennLab}
    Is there a Grothendieck topos for which the number of these quotients is not small? At the other extreme, could they be parameterized internally, as subtoposes are?
\end{quote}

未解決問題は二つの部分に分かれている．後半は，「商トポスと??の対応定理」が存在するかを聞いていて，これは著者の修論の一部\cite{hora2024internal}で部分的に\footnote{部分的と言ったものの，\cite{johnstone2025remarks}でJohnstoneが言ったように，これこそがローヴェアが\dq{本来問うべきだった問い}の答えであったと思う．}肯定した．博論第二部の元になった\cite{kamio2024solution}では，前半の問いにYesと回答している．つまり，あるトポスが真クラス個の商を持つことを示した．
\begin{theorem}\cite{kamio2024solution}
    \ignore{可算無限生成自由モノイド作用の}トポス\ignore{$\PSh(M_\omega)$}は真クラス個の商トポスをもつ．
\end{theorem}
そこでは，任意の集合上にリジッドな二項関係が入るというVopenka, Pultr, Hedrlinの結果\cite{vopvenka1965rigid}を用いている．


\section{toposの次元に関するLawvereの問題 (20min)}\cite{hora2025lawvere}\\

ローヴェアは，彼の物理学的および関数解析的バックグラウンドから，特定のトポスに強い興味(執着?)を抱いていた．その一つが，\demph{ブール代数の分類トポス}\ignore{$\PSh(\FinSet_{>0})$}である．例えば，彼の論文「組合せトポロジーと関数解析における，余離散的対象で生成されたトポス
\cite{lawvere1988toposesGenerated}」の中で彼は，次のことを考えている．
\begin{question}[真と偽を幾何的に同一視するブール代数]
    Hausdorffな位相ブール代数\footnote{位相空間上のブール代数構造であって，全てのブール演算が連続になるようなもの．}であって，$\bot \neq \top$だが可縮なものはあるか？
\end{question}
\begin{answer}
    無限次元球面$S^\infty$ \cite{lawvere1988toposesGenerated}.
\end{answer}
彼はこのことを，まず$S^\infty$を関数空間$L^2([0,1])$に埋め込むことで実現し，さらにブール代数の分類トポス$\PSh(F)$の言葉で記述した．

この問題は，おそらく彼のヘーゲル哲学への情熱と関連している．(絵を書いて説明する) 実際，彼はトポスにおける\demph{アウフヘーベン}の概念を定義し\cite{lawvere1989display, lawvere1991more}，それを用いてトポスにおける次元論を展開した\cite{lawvere2006some}．ローヴェアの未解決問題の4番は，ブール代数の分類トポスのアウフヘーベンを計算することである．
\begin{quote}\cite{lawvere2025opennLab}
    ... What is, in combinatorial or number theoretic terms, the way below relation for this basic topos?
\end{quote}

博論の第三部の元になった\cite{hora2025lawvere}では，\ignore{simplicial setに対する\cite{kennett2011levels}の手法を利用して，}この問題を解いた．その解答は，諸々の定義を省略して，以下の通りである．
\begin{theorem}\cite{hora2025lawvere}
    ブール代数の分類トポスのアウフヘーベンは，$l\geq 3$に対して$2l-1$である．
\end{theorem}

\printbibliography



\appendix

\section{証明不可能性の証明 -- その目的と手法}
論理学者(resp. 理論計算機学者)は，証明不可能性の証明 (resp. 計算不可能性の証明)をしたがる．


証明不可能性の証明の意義は，単なる好奇心や無駄な努力の排除，というだけではなく，より根源的な目的がある．
論理学者であるあなたは，新しい論理体系\footnote{例えば，排中律をなくしたシステムに別の公理を入れるとか，$\mathrm{ZFC}+\lnot \textrm{連続体仮説}$とか，
$\mathrm{ZF}+\lnot \textrm{選択公理}$とか，
もっとradicalなシステムなど}を提案する．
あなたの次の仕事は，
\[
\begin{tikzcd}[column sep = 50pt]
    \text{この論理体系が破綻していないこと}\ar[r, "\text{だいたい}", Leftrightarrow] &\demph{矛盾を証明できてしまわないこと}
\end{tikzcd}
\]
の証明である．

あなたが理論計算機科学者なら，新たなプログラミング言語や制御のためのシステムを考え，それが致命的な破綻をしないように保証する必要がある．その仕事は，実質的に証明不可能性の証明と同じものになる\footnote{cf. Curry-Howard(-Lambek) 対応, プログラム論理，モデル検査}．
\[
\begin{tikzcd}[column sep = 50pt]
    \text{計算システムの振る舞い}\ar[r, "\text{だいたい}", leftrightarrow] &\demph{対応する証明体系の振る舞い}
\end{tikzcd}
\]




\end{document}