slides-luminy2023.tex

\documentclass[12pt,utf8,notheorems,compress,t,aspectratio=169]{beamer}
%\documentclass[12pt,utf8,notheorems,compress,t]{beamer}
\usepackage{etex}

\usepackage{pgfpages}
\usepackage[export]{adjustbox}

% Workaround for the issue described at
% https://tex.stackexchange.com/questions/164406/beamer-using-href-in-notes.
\newcommand{\fixedhref}[2]{\makebox[0pt][l]{\hspace*{\paperwidth}\href{#1}{#2}}\href{#1}{#2}}

\usepackage[english]{babel}

\usepackage[normalem]{ulem}
\usepackage{graphbox}
\usepackage{mathtools}
\usepackage{booktabs}
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{manfnt}
\usepackage{array}
\usepackage{ragged2e}
\usepackage{multicol}
\usepackage{tabto}
\usepackage{xstring}
\usepackage{proof}
\usepackage{ifthen}
\usepackage[normalem]{ulem}
\usepackage[all]{xy}
\xyoption{rotate}
\usepackage{tikz}
\usetikzlibrary{calc,shapes,shapes.callouts,shapes.arrows,patterns,fit,backgrounds,decorations.pathmorphing,positioning,svg.path}
\hypersetup{colorlinks=true}

\newcommand*\circled[1]{\tikz[baseline=(char.base)]{%
  \node[shape=circle,draw,inner sep=1pt] (char) {#1};}}

\DeclareFontFamily{U}{bbm}{}
\DeclareFontShape{U}{bbm}{m}{n}
   {  <5> <6> <7> <8> <9> <10> <12> gen * bbm
      <10.95> bbm10%
      <14.4>  bbm12%
      <17.28><20.74><24.88> bbm17}{}
\DeclareFontShape{U}{bbm}{m}{sl}
   {  <5> <6> <7> bbmsl8%
      <8> <9> <10> <12> gen * bbmsl
      <10.95> bbmsl10%
      <14.4> <17.28> <20.74> <24.88> bbmsl12}{}
\DeclareFontShape{U}{bbm}{bx}{n}
   {  <5> <6> <7> <8> <9> <10> <12> gen * bbmbx
      <10.95> bbmbx10%
      <14.4> <17.28> <20.74> <24.88> bbmbx12}{}
\DeclareFontShape{U}{bbm}{bx}{sl}
   {  <5> <6> <7> <8> <9> <10> <10.95> <12> <14.4> <17.28>%
      <20.74> <24.88> bbmbxsl10}{}
\DeclareFontShape{U}{bbm}{b}{n}
   {  <5> <6> <7> <8> <9> <10> <10.95> <12> <14.4> <17.28>%
      <20.74> <24.88> bbmb10}{}
\DeclareMathAlphabet{\mathbbm}{U}{bbm}{m}{n}
\SetMathAlphabet\mathbbm{bold}{U}{bbm}{bx}{n}

\usepackage{pifont}
\newcommand{\cmark}{\ding{51}}
\newcommand{\xmark}{\ding{55}}
\DeclareSymbolFont{extraup}{U}{zavm}{m}{n}
\DeclareMathSymbol{\varheart}{\mathalpha}{extraup}{86}

\graphicspath{{images/}}

\usepackage[protrusion=true,expansion=true]{microtype}

\setlength\parskip{\medskipamount}
\setlength\parindent{0pt}

\title{New modal operators for constructive mathematics}

\author{Ingo Blechschmidt}
\date{May 2nd, 2023}

%\useinnertheme[shadow=true]
\setbeamerfont{block title}{size={}}

\useinnertheme{rectangles}

\usecolortheme{orchid}
\usecolortheme{seahorse}
\definecolor{mypurple}{RGB}{253,73,34}
\definecolor{mypurpledark}{RGB}{100,0,150}
\setbeamercolor{structure}{fg=mypurple}
\definecolor{myred}{RGB}{150,0,0}
%\setbeamercolor*{title}{bg=myred,fg=white}
%\setbeamercolor*{titlelike}{bg=myred,fg=white}
\setbeamercolor*{title}{bg=mypurple,fg=white}
\setbeamercolor*{titlelike}{bg=mypurple,fg=white}
\setbeamercolor{frame}{bg=black}

\usefonttheme{serif}
\usepackage[T1]{fontenc}
\usepackage{libertine}

% lifted from https://arxiv.org/abs/1506.08870
\DeclareFontFamily{U}{min}{}
\DeclareFontShape{U}{min}{m}{n}{<-> udmj30}{}
\newcommand\yon{\!\text{\usefont{U}{min}{m}{n}\symbol{'210}}\!}

\newcommand{\A}{\mathcal{A}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\M}{\mathcal{M}}
\renewcommand{\AA}{\mathbb{A}}
\newcommand{\BB}{\mathbb{B}}
\newcommand{\pp}{\mathbbm{p}}
\newcommand{\MM}{\mathbb{M}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\FF}{\mathbb{F}}
\newcommand{\G}{\mathcal{G}}
\newcommand{\J}{\mathcal{J}}
\newcommand{\GG}{\mathbb{G}}
\renewcommand{\O}{\mathcal{O}}
\newcommand{\K}{\mathcal{K}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\TT}{\mathbb{T}}
\newcommand{\PP}{\mathbb{P}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\CC}{\mathbb{C}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\aaa}{\mathfrak{a}}
\newcommand{\ccc}{\mathfrak{c}}
\newcommand{\ppp}{\mathfrak{p}}
\newcommand{\fff}{\mathfrak{f}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\defeq}{\vcentcolon=}
\newcommand{\defeqv}{\vcentcolon\equiv}
\newcommand{\Sh}{\mathrm{Sh}}
\newcommand{\GL}{\mathrm{GL}}
\newcommand{\Zar}{\mathrm{Zar}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\Set}{\mathrm{Set}}
\newcommand{\Eff}{\mathrm{Ef{}f}}
\newcommand{\Sch}{\mathrm{Sch}}
\newcommand{\Aff}{\mathrm{Aff}}
\newcommand{\Ring}{\mathrm{Ring}}
\newcommand{\Cov}{\mathrm{Cov}}
\newcommand{\LocRing}{\mathrm{LocRing}}
\newcommand{\LRS}{\mathrm{LRS}}
\newcommand{\Hom}{\mathrm{Hom}}
\newcommand{\Spec}{\mathrm{Spec}}
\newcommand{\lra}{\longrightarrow}
\newcommand{\RelSpec}{\operatorname{Spec}}
\renewcommand{\_}{\mathpunct{.}}
\newcommand{\?}{\,{:}\,}
\newcommand{\speak}[1]{\ulcorner\text{\textnormal{#1}}\urcorner}
\newcommand{\ul}[1]{\underline{#1}}
\newcommand{\affl}{\ensuremath{{\ul{\ensuremath{\AA}}^1}}}
\newcommand{\Ll}{\text{iff}}
\newcommand{\inv}{inv.\@}
\newcommand{\seq}[1]{\mathrel{\vdash\!\!\!_{#1}}}
\newcommand{\hg}{\mathbin{:}}  % homogeneous coordinates

\setbeamertemplate{blocks}[rounded][shadow=false]

\newenvironment{indentblock}{%
  \list{}{\leftmargin\leftmargin}%
  \item\relax
}{%
  \endlist
}

% Adapted from https://latex.org/forum/viewtopic.php?t=2251 (Stefan Kottwitz)
\newenvironment<>{hilblock}{
  \begin{center}
    \begin{minipage}{9.05cm}
      \setlength{\textwidth}{9.05cm}
      \begin{actionenv}#1
        \def\insertblocktitle{}
        \par
        \usebeamertemplate{block begin}}{
        \par
        \usebeamertemplate{block end}
      \end{actionenv}
    \end{minipage}
  \end{center}}

\newenvironment{changemargin}[2]{%
  \begin{list}{}{%
    \setlength{\topsep}{0pt}%
    \setlength{\leftmargin}{#1}%
    \setlength{\rightmargin}{#2}%
    \setlength{\listparindent}{\parindent}%
    \setlength{\itemindent}{\parindent}%
    \setlength{\parsep}{\parskip}%
  }%
  \item[]}{\end{list}}

\tikzset{
  invisible/.style={opacity=0,text opacity=0},
  visible on/.style={alt={#1{}{invisible}}},
  alt/.code args={<#1>#2#3}{%
    \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}}}
}

% https://tex.stackexchange.com/questions/172336/drawing-roman-laurel-leaves-spqr-in-tikz
\tikzset{
  laurel-wreath/.pic = {
    \fill svg{M14.4-24.6c-1.5-1.5-2.6-3.3-3.1-5.3l-.4-1.7c-.2-1.1-.2-4.1 .2-5.7 .2-.9 .3-1.3 .5-1.3l1.4 1.1 2.5 2.4c2.7 2.5 5.2 6 5.8 8 .2 .6-.5 .3-2.2-.9-1.6-1.3-3.3-2.6-5-3.8l.1 1.4c.2 1.4 .5 2.7 1.1 4.6s.8 2.5 .5 2.5l-1.4-1.3zm69.6 1.1 .3-1.2c.8-2.3 1.3-4.8 1.6-7.3l-1.5 1.1c-1.3 .9-2.6 1.9-3.7 3-1.6 1.1-2 1.3-2.1 1 .7-1.8 1.6-3.4 2.8-4.9 1.3-1.7 6.5-6.8 7-6.8 .2 0 .3 .2 .3 .5l.3 1.6c.3 2.2 .2 5.7-.5 7.4-.8 1.9-1.6 3.1-3 4.7-1.1 1.1-1.4 1.3-1.5 .9z};
    \fill svg{M10-29.4c-.8-1.1-1.4-2.2-2-4.1l-.7-3.5c-.2-3 .2-4.4 1.4-8.3l.5-1.4c.2-1.3 .3-1.9 .6-1.9 .3-.2 .6 .3 .7 .8s.9 2.2 1.9 3.6c1.4 2.2 2.7 4.4 3.9 6.6l.9 2.7c0 .6 0 .6-.3 .6-.6 0-4.9-4.4-5.8-6l-.2-.6-.1 1.7-.3 2.8c-.3 2.7-.3 3.8 0 5.5 .6 2 .5 2.4-.5 1.5zm79.2 .3 .4-2.4c.2-1.3 .2-2.7-.1-4.9l-.3-2.8v-1.6l-.7 1c-.8 1.3-5 5.5-5.5 5.5s-.5-.3 .2-1.9c.5-1.7 1.4-3.3 3.3-6.5 2.4-3.6 2.7-3.9 2.8-4.7 .5-1.3 .5-1.4 .8-1.2 .3 0 .6 .8 .6 1.5l.7 2.4c.9 2.7 1.1 3.6 1.2 6 .2 3.1-.5 6-2 8.2-.8 1.3-1.3 1.7-1.4 1.5z};
    \fill svg{M5-40c-.4-3.2-.1-6.5 .9-9.6 .5-1.1 1.6-2.8 2.2-3.4l1.3-1.6 2-2.7 .2 .6c.1 1.3 .4 2.6 .9 3.8l.3 1c.8 1.7 1.1 2.7 1.6 5.3 .6 2.5 .6 4.6 .2 4.6-.3 0-.9-.8-1-1.1l-.5-.8c-1.4-2-3-5.2-2.9-6.5-.9 2.7-2 5.4-3.5 7.9l-.3 .8-.3 .8c0 .5-.6 1.6-.8 1.6l-.3-.7zm89.2 .2-.2-.5-.3-.9-1.1-2.7-1.1-2.4c-.6-1.4-1.2-2.8-1.6-4.2l-.3 .9c-.3 1.3-1.6 3.9-3 6-1.3 2-1.6 2-1.5 0s1.1-6.3 2.2-9c.8-1.7 1.1-3.1 .9-4.1-.2-1.1 .5-.8 2.2 1.8 3.3 4.4 3.8 5.4 4.4 7.8 .6 2.4 .5 7.7-.3 7.8l-.3-.5z};
    \fill svg{M13.9-50.1c-.5-1.9-.8-3.9-.9-5.8-.2-1.6-.1-3.3 .1-4.9-.3 .8-1.7 2.5-4.2 5.1l-3 4.9-.3 .1c-.3 0-.3-2.2 0-3.3 .8-3 1.4-4.6 2.5-6.1 .9-1.3 1.7-1.9 2.5-2.5 1.1-.6 2.7-1.9 3.5-2.7 .9-.9 1.9-1.4 2.2-1.4v1.1l-.3 6.6c0 6.8 .2 6.3-1 8.9-.5 1.1-.8 1.1-1.1 0zm70.8-.4c-.8-2.2-.8-2.5-.7-6.3-.1-2.7-.1-5.5-.2-8.2-.3-1.6-.3-1.9 .5-1.6l.6 .5c1.4 1.4 3 2.5 3.9 3.1 1.3 .9 1.9 1.6 2.7 2.6l.6 .7 .2 .4 .2 .3c.8 .9 2 4.9 2 6.9 .2 1.9-.2 1.9-.9 .5-.7-1.4-1.5-2.7-2.6-4-1.6-1.5-3-3.2-4.2-5 .4 3 .3 6-.5 9 0 .8-.5 2.2-.8 2.3-.2 0-.5-.3-.8-1.2z};
    \fill svg{M16.4-58.5l.2-1.5 .3-3.7c.2-2.8 .3-3.5 1.1-5.4l.7-1.3-.5 .4-1 .7c-.5 .4-1.1 .8-1.5 1.3l-.5 .3-1.9 1.6c-2.2 1.6-2.7 2-3.9 3.6-.5 .8-1.1 1.3-1.3 1.3-.5 0 0-2.4 1.1-4.7 1.5-3.4 4.3-6 7.7-7.4l1.3-.4 1.9-.4 2-.5c1.4 0 1.4 0 1 1.1-.5 .8-.8 2-1.1 4.2-.3 2.3-1.1 4.5-2.2 6.5l-.4 .6c-.6 1.1-1.3 2.1-2 3.2-.5 .6-.8 .8-1 .5zm66.3-.2c-.8-.9-2.8-4.4-3.5-6.1-.6-1.3-.9-2.5-1.1-3.5-.2-2.1-.7-4.1-1.5-6 0-.3 0-.3 1.2-.3l2.1 .5 1.9 .4 1.2 .4 .6 .1 1 .6c3 1.4 5.7 4.6 6.8 8.5l.7 2.6c-.2 .6-.5 .5-1.4-.7-2.2-2.7-4.8-5-7.7-6.9l-1.7-1.3 .6 1.3c.3 .6 .6 1.2 .8 1.9l.3 2.5 .3 3.9c.3 2.4 .2 2.8-.6};
    \fill svg{M21.6-66.1l.4-1.1 .9-3.2c.3-1.9 1.1-3.3 2.4-4.7l.4-.8-1.2 .2-2.2 .3c-2.7 .3-5.3 1.2-7.7 2.5-.6 .5-1.3 .6-1.3 .3 0-.5 .9-1.9 2-2.9 .8-.9 2-1.9 3.2-2.6l.9-.4 2.2-1c.3-.2 1.3-.3 3.2-.1 3 0 4.1 .2 6.3 .7l1.1 .4c.5 .2 .6 .6 .3 .6-.5 0-1.4 .9-1.9 1.7l-1.2 1.8c-1.7 2.8-2.2 3.5-4.6 5.9l-3 2.7-.2-.3zm53.9-2c-2.7-2.8-3.5-3.8-5.4-6.8-.9-1.6-1.4-2.4-1.9-2.5l-.8-.5c-.3 0-.2-.5 .4-.6l1.1-.4c1.9-.6 3-.8 5.6-.9l3.3 .2c2 .6 3.8 1.5 5.4 2.8 .3 0 1.9 1.6 2.5 2.4l.9 1.8c0 .3-.3 .2-1.9-.6-2.8-1.4-4.4-1.9-7.7-2.2l-2.2-.5c-.9-.2-.9-.2-.6 .2 .6 .5 1.7 2 2.1 2.8l.9 2.5c.3 1.5 .6 3 .9 4.6l-2.6-2.3z};
    \fill svg{M34.1-78.7c-3.4-1.3-6.9-2.1-10.6-2.5-.9 0-1.4 0-2.3 .3-2 .5-2 0 0-1.3l2.8-1.2c1.4-.5 1.9-.5 3.8-.6 3.8-.2 6.1 .3 9.3 1.7l3.6 1.1 2.2 .3c1.3 0 1.7 0 2.7-.3 1.1-.3 2.8-1.1 2.8-1.3l-1.3-.9c-1.9-1.4-3.1-2.7-3.1-3.2l.8-.6c.9-.3 1.3-.2 2 .8 .5 .8 1.1 1.4 2.9 2.7 .2 .3 .3 .2 1.1-.3 .9-.8 2.4-2 2.6-2.7 .5-.6 .9-.8 1.8-.5l.8 .6c0 .5-1.4 1.7-3.2 3.2l-1.3 .9c0 .2 1.7 .9 2.9 1.3 .9 .3 1.4 .3 2.7 .3l2.2-.3c1.7-.4 3.4-1 5-1.7 2-.8 4.4-1.3 7.7-1.1 2 .2 2.5 .2 3.8 .6 .9 .3 2.2 .8 2.8 1.2 2 1.1 2 1.6 .2 1.3-1.6-.3-1.9-.3-4.4 0-2.4 .3-4.7 .8-7 1.6l-1.5 .6c-2.9 .3-5.9 .2-8.8-.3-1.7-.3-3.6-.9-6-2.1l-1.1-.4-1.3 .6c-4.5 2.2-9.6 3-14.6 2.2zm-6.3-9.1c};
  }
}

\newcommand{\pointthis}[3]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=0,outer sep=0] (#2) {#2};
    \node[visible on=#1,overlay,rectangle callout,rounded corners,callout relative pointer={(0.3cm,0.5cm)},fill=blue!20] at ($(#2.north)+(-0.1cm,-1.1cm)$) {#3};
  }%
}

\tikzset{
  invisible/.style={opacity=0,text opacity=0},
  visible on/.style={alt={#1{}{invisible}}},
  alt/.code args={<#1>#2#3}{%
    \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}}}
}

\newcommand{\hcancel}[5]{%
  \tikz[baseline=(tocancel.base)]{
    \node[inner sep=0pt,outer sep=0pt] (tocancel) {#1};
    \draw[red!80, line width=0.4mm] ($(tocancel.south west)+(#2,#3)$) -- ($(tocancel.north east)+(#4,#5)$);
  }%
}

\newcommand{\explain}[7]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=2pt,outer sep=0,fill=#3,rounded corners] (label) {#1};
    \node[anchor=north,visible on=<#2>,overlay,rectangle callout,rounded corners,callout
    relative pointer={(0.0cm,0.5cm)+(0.0cm,#6)},fill=#3] at ($(label.south)+(0,-0.3cm)+(#4,#5)$) {#7};
  }%
}

\newcommand{\explainstub}[2]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=2pt,outer sep=0,fill=#2,rounded corners] (label) {#1};
  }%
}

\newcommand{\squiggly}[1]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=0,outer sep=0] (label) {#1};
    \draw[thick,color=red!80,decoration={snake,amplitude=0.5pt,segment
    length=3pt},decorate] ($(label.south west) + (0,-2pt)$) -- ($(label.south east) + (0,-2pt)$);
  }%
}

% Adapted from https://latex.org/forum/viewtopic.php?t=2251 (Stefan Kottwitz)
\newenvironment<>{varblock}[2]{\begin{varblockextra}{#1}{#2}{}}{\end{varblockextra}}
\newenvironment<>{varblockextra}[3]{
  \begin{center}
    \begin{minipage}{#1}
      \begin{actionenv}#4
        {\centering \hil{#2}\par}
	\def\insertblocktitle{}%\centering #2}
        \def\varblockextraend{#3}
	\usebeamertemplate{block begin}}{
        \par
        \usebeamertemplate{block end}
        \varblockextraend
      \end{actionenv}
    \end{minipage}
  \end{center}}

\setbeamertemplate{headline}{}

\setbeamertemplate{frametitle}{%
  \leavevmode%
  \vskip-1.6em%
  \begin{beamercolorbox}[dp=1ex,center,wd=\paperwidth,ht=2.25ex]{title}%
    \vskip0.5em%
    \bf\insertframetitle
  \end{beamercolorbox}%

  \vskip-0.77em\hspace*{-2em}%
  \textcolor{mypurpledark}{\rule[0em]{1.1\paperwidth}{2.4pt}}

  \vskip-0.4em%
}

\setbeamertemplate{navigation symbols}{}

\newcounter{framenumberpreappendix}
\newcommand{\backupstart}{
  \setcounter{framenumberpreappendix}{\value{framenumber}}
}
\newcommand{\backupend}{
  \addtocounter{framenumberpreappendix}{-\value{framenumber}}
  \addtocounter{framenumber}{\value{framenumberpreappendix}}
}

\newcommand{\insertframeextra}{}
\setbeamertemplate{footline}{%
  \begin{beamercolorbox}[wd=\paperwidth,ht=2.25ex,dp=1ex,right,rightskip=1mm,leftskip=1mm]{}%
    % \inserttitle
    \hfill
    \insertframenumber\insertframeextra\,/\,\inserttotalframenumber
  \end{beamercolorbox}%
  \vskip0pt%
}


\newcommand{\hil}[1]{{\usebeamercolor[fg]{item}{\textbf{#1}}}}
\newcommand{\hill}[1]{{\usebeamercolor[fg]{item}{#1}}}
\newcommand{\bad}[1]{\textcolor{red!90}{\textnormal{#1}}}
\newcommand{\good}[1]{\textcolor{mypurple}{\textnormal{#1}}}

\newcommand{\bignumber}[1]{%
  \renewcommand{\insertenumlabel}{#1}\scalebox{1.2}{\!\usebeamertemplate{enumerate item}\!}
}
\newcommand{\normalnumber}[1]{%
  {\renewcommand{\insertenumlabel}{#1}\!\usebeamertemplate{enumerate item}\!}
}
\newcommand{\bigheart}{\includegraphics{heart}}

\newcommand{\subhead}[1]{{\centering\textcolor{gray}{\hrulefill}\quad\textnormal{#1}\quad\textcolor{gray}{\hrulefill}\par}}

\newcommand{\badbox}[1]{\colorbox{red!30}{#1}}
\newcommand{\infobox}[1]{\colorbox{yellow!70}{\color{black}#1}}

% taken from JDH "The modal logic of arithmetic potentialism and the universal algorithm"
\DeclareMathOperator{\possible}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,rotate=45,line width=.1ex]{\draw (-1,-1) rectangle (1,1);}}}
\DeclareMathOperator{\necessary}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,line width=.1ex]{\draw (-1,-1) rectangle (1,1);}}}
\DeclareMathOperator{\xpossible}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,rotate=45,line width=.1ex]{\draw (-1,-1) rectangle (1,1); \draw[very thin] (-.6,-.6) rectangle (.6,.6);}}}
\DeclareMathOperator{\xnecessary}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,line width=.1ex]{\draw (-1,-1) rectangle (1,1); \draw[very thin] (-.6,-.6) rectangle (.6,.6);}}}

\input{images/primes.tex}

\newcommand{\triang}{\hil{$\blacktriangleright$}}
\newcommand{\concat}{\mathbin{{+}\mspace{-8mu}{+}}}

\newcommand{\astikznode}[2]{\tikz[baseline,remember picture]{\node[anchor=base,inner sep=0,outer sep=0.1em] (#1) {#2};}}
\newcommand{\astikznodecircled}[3]{\tikz[baseline,remember picture]{\node[anchor=base,circle,draw=#2,thick,inner sep=0,outer sep=0.05em] (#1) {#3};}}
\newcommand{\astikznodetransparentlycircled}[2]{\tikz[baseline,remember picture]{\node[anchor=base,circle,opacity=0,draw=white,text opacity=1,thick,inner sep=0,outer sep=0.05em] (#1) {#2};}}

\setbeamersize{text margin left=1.60em,text margin right=1.60em}

\begin{document}

\addtocounter{framenumber}{-2}

{
\definecolor{mypurple}{RGB}{150,0,255}
\setbeamercolor{structure}{fg=mypurple}
\begin{frame}{}
  \begin{center}\includegraphics[width=0.2\textwidth]{eigenvector}\end{center}

  Let a continuous family of symmetric matrices be given:
  \[
  \begin{pmatrix}a_{11}(t)&\cdots&a_{1n}(t)\\\vdots&&\vdots\\a_{n1}(t)&\cdots&a_{nn}(t)\end{pmatrix}
  \]

  There for every parameter value~$t$, classically there is

  \hil{$\blacktriangleright$} a full list of eigenvalues~$\lambda_1(t),\ldots,\lambda_n(t)$ and \\
  \hil{$\blacktriangleright$} an eigenvector basis~$(v_1(t),\ldots,v_n(t))$.
  \bigskip

  \begin{columns}[c]
    \begin{column}{0.01\textwidth}
      \includegraphics[height=2.4em]{question-mark}
    \end{column}
    \begin{column}{0.9\textwidth}
      \mbox{Can locally the functions~$\lambda_i$ be chosen to be continuous?
      \only<2->{\hil{Yes.}}} \\
      How about the~$v_i$? \only<2->{\hil{No.}}
    \end{column}
  \end{columns}
\end{frame}
}

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\includegraphics[height=\paperheight]{night-sky}\end{minipage}}
\begin{frame}[c]
  \centering
  \color{white}

  \bigskip
  \bigskip
  \bigskip
  \bigskip

  \scriptsize
  \textit{-- an invitation --}

  \setbeamercolor{block body}{bg=black!100}
  \begin{minipage}{0.8\textwidth}
    \begin{block}{}
      \centering\normalsize\color{white}
      \hil{New modal operators for~constructive~mathematics}
    \end{block}
  \end{minipage}

  \bigskip
  \bigskip
  \bigskip
  \bigskip
  \bigskip
  \bigskip
  \bigskip

  \emph{Type Theory, Constructive Mathematics and Geometric Logic} \\
  \bigskip

  CIRM \\
  May 2nd, 2023
  \bigskip

  Ingo Blechschmidt \\
  j.w.w. Alexander Oldenziel
  \par
\end{frame}}

\definecolor{mypurple}{RGB}{150,0,255}
\setbeamercolor{structure}{fg=mypurple}


\section{Motivation}

\begin{frame}{Questions}
  \begin{enumerate}
    \item \!Why has the inductive revolution been so powerful?
    \bigskip

    \item \!Why do proofs using Zorn's maximal ideals work so well in constructive algebra?
    \bigskip

    \item \!Why are elements of~$\bigcap_\ppp \ppp$ not necessarily nilpotent?
    \bigskip

    \item How can we extract computational content from classical proofs?
  \end{enumerate}
\end{frame}


{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\includegraphics[height=\paperheight]{sea-of-clouds-2}\end{minipage}}
\begin{frame}{Infinite data}
  \vspace*{-1em}
  \[ \astikznodetransparentlycircled{xm}{7}\!,
    \quad \astikznodetransparentlycircled{x0}{4}\!,
    \quad \only<1-2>{\astikznodetransparentlycircled{t1}{3}}\only<3->{\astikznodecircled{t1}{mypurple}{3}}\!,
    \quad \only<1>{\ldots}\pause \astikznodetransparentlycircled{x1}{1}\!,
    \quad \only<2>{\ldots}\pause \astikznodecircled{t2}{mypurple}{8}\!,
    \quad \only<3>{\ldots} \visible<4->{\astikznodetransparentlycircled{x2}{2}\!,}
    \quad \only<4->{\ldots} \]
  {\centering\begin{tikzpicture}[remember picture,overlay]
    \node[draw=mypurple, circle, thick, inner sep=0.1em] (t3) {\scriptsize$\leq$};
    \path[draw=mypurple,thick]
      (t1)
      to [out=-90, in=180] (t3)
      to [out=0, in=-90] (t2);
  \end{tikzpicture}\par}
  \medskip
  \pause

  \textbf{Thm.} Every sequence~$\alpha : \NN \to \NN$ is \hil{good} in that
  there exist~$i < j$ with~$\alpha(i) \leq \alpha(j)$.
  \pause

  \emph{Proof.} \emph{(offensive?)} By~\badbox{\textsc{lem}}, there is a
  minimum~$\alpha(i)$.
  Set~$j \defeq i + 1$. \qed\par
  \pause
  \medskip

  \textbf{Def.} A preorder~$X$ is \hil{well\only<9->{$^\star$}} iff every sequence~$\NN \to X$ is good.
  
  \textbf{Examples.} $(\NN,{\leq}),\ \
  \color{white}\only<7->{\color{red!90}}\astikznode{onlyclass}{$\underbrace{\color{black}X \times Y,\ \ X^*,\ \ \mathrm{Tree}(X)}_{\text{\visible<7->{\bad{only classically}}}}$}$.
  \pause
  \pause
  \medskip

  \begin{tikzpicture}[remember picture,overlay]
    \node[thick, fill=black, rectangle, inner sep=0.3em, right=2em of onlyclass] (moral) {
      \begin{minipage}{6cm}
        \begin{columns}
          \begin{column}{0.15\textwidth}
            \hspace*{1.0em}\color{white}\dbend
          \end{column}
          \begin{column}{0.95\textwidth}
            \color{white}\footnotesize
            \it Don't quantify over points of spaces which might not have enough.
          \end{column}
        \end{columns}
      \end{minipage}
    };
    \path[draw=red!90,thick,-stealth]
      (moral) to
      [out=180, in=-00] (onlyclass.east);
  \end{tikzpicture}
  \pause

  \textbf{Def.} For a predicate~$P$ on finite lists over a set~$X$, inductively
  define:
  \[
    \infer{P \,|\, \sigma}{P\sigma}
    \qquad
    \infer{P \,|\, \sigma}{\forall(x \in X)\_\ P \,|\, \sigma x}
  \]

  \textbf{Def.} A preorder is \hil{well} iff~$\mathsf{Good} \,|\, [\,]$, where
  $\mathsf{Good}\,\sigma \defeqv (\exists(i < j)\_ \sigma[i] \leq \sigma[j])$.
\end{frame}}

\begin{frame}{Computational content from classical proofs}
  \textbf{Def.} A transitive relation~$({<})$ on a set~$X$ is \ldots
  \begin{enumerate}
    \item \hil{well-founded$^\star$} iff
    there is no \bad{infinite chain} $x_0 > x_1 > \cdots$,
    \item \hil{well-founded} iff for every~$x \in X$,
    $\mathsf{Acc}(x)$,
  \end{enumerate}
  where~$\mathsf{Acc}$ is inductively defined by:
  \[
    \infer{\mathsf{Acc}(x)}{\forall(y < x)\_\ \mathsf{Acc}(y)}
  \]
  \vspace*{-1em}
  \pause

  \textbf{Prop.} Let~$(X,{\leq})$ be preorder. Let~``$x < y$'' mean~$x \leq y \wedge \neg(y \leq x)$. \\
  Then: If~$X$ is well$^\star$, then~$({<})$ is well-founded$^\star$.

  \emph{Proof.} An infinite strictly descending chain would also be good. \qed
  \pause

  Can we extract a constructive proof that well preorders are well-founded?
\end{frame}

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\vspace*{5.95cm}\includegraphics[width=\paperwidth]{fr1}\end{minipage}}
\begin{frame}{Maximal ideals}
  \only<1-7>{\textbf{Thm.}
  Let~$M$ be a surjective matrix with more rows than columns over a
  ring~$A$. Then~$1 = 0$ in~$A$.

  \visible<2->{\emph{Proof.} \bad{Assume not.}}
  \visible<3->{Then there is~a \bad{maximal ideal} $\mmm$.}
  \visible<5->{The matrix is surjective over~$A/\mmm$.}
  \visible<6->{Since~$A/\mmm$ is a field, this is a contradiction to basic linear algebra.\qed}}

  \only<4-7>{\bigskip\par\centering\scalebox{0.9}{\centering\begin{tikzpicture}
    \node (0) at (0,1) {$(0) = \{0\}$};
    \node (1) at (0,5) {$(1) = \ZZ$};
    \node (2) at (-2,4) {$(2)$};
    \node [right of=2] (3) {$(3)$};
    \node [below of=2] (4) {$(4)$};
    \node [below of=2, xshift=0.7cm] (6) {$(6)$};
    \node [right of=3] (5) {$(5)$};
    \node [right of=5] (7) {$(7)$};
    \node [right of=7] (7d) {$\ldots$\phantom{(}};
    \node [right of=7d, xshift=3cm, yshift=-2cm] (max)
    {\vbox{\small\it maximal among the proper ideals \\ \medskip $\neg(1 \in
    \mmm)$ \\ \medskip $x \in \mmm \quad\vee\quad 1 \in \mmm + (x)$}};
    \node [below of=4] (8) {$(8)$};
    \node [right of=8, xshift=3cm] (8d) {$\ldots$};
    \draw (0) -- (8);
    \draw (0) -- (8d);
    \draw (0) -- (6);
    \draw (2) -- (1);
    \draw (3) -- (1);
    \draw (5) -- (1);
    \draw (7) -- (1);
    \draw (7d) -- (1);
    \draw (4) -- (2);
    \draw (8) -- (4);
    \draw (6) -- (2);
    \draw (6) -- (3);
    \draw [mypurple!30, thick, shorten <=-2pt, shorten >=-2pt, ->] (max) to [out=120, in=-30] (7d);
    \begin{pgfonlayer}{background}
      \draw[decorate, very thick, draw=mypurple!30]
        ($(2.south west) + (8pt, 0)$) arc(270:180:8pt) --
        ($(2.north west) + (0, -8pt)$) arc(180:90:8pt) --
        ($(7d.north east) + (-8pt, 0)$) arc(90:0:8pt) --
        ($(7d.south east) + (0, 8pt)$) arc(0:-90:8pt) --
        cycle;
    \end{pgfonlayer}
  \end{tikzpicture}\par}\par}

  \pause
  \pause
  \pause
  \pause
  \pause
  \pause
  \medskip
  \raggedright

  Let~$A$ be a ring. \emph{Does there exist a maximal ideal~$\mmm \subseteq A$?}
  \pause
  \begin{enumerate}
    \item \good{Yes}, if \bad{Zorn's lemma} is available.
    \bigskip
    \pause

    \item \good{Yes}, if~$A$ is countable and membership of finitely generated ideals is decidable:
    {\footnotesize
    \begin{align*}
      \mmm_0 &\defeq \{ 0 \}, &
      \mmm_{n+1} &\defeq \begin{cases}
        \mmm_n + (x_n), & \text{if $1 \not\in \mmm_n + (x_n)$}, {\qquad\quad\quad\!\!}\\
        \mmm_n, & \text{else.}
      \end{cases}
    \end{align*}}
    \pause

    \item \good{Yes}, if~$A$ is countable (irrespective of membership decidability):
    {\footnotesize\begin{align*}
      \mmm_0 &\defeq \{ 0 \}, &
      \mmm_{n+1} &\defeq \mmm_n + (\underbrace{\{ x \in A \,|\, x = x_n \wedge
        1 \not\in \mmm_n + (x_n) \}}_{\text{a certain subsingleton set}})
    \end{align*}}
    \vspace*{3.5em}
    \visible<11>{{
      \centering
      \raisebox{0pt}[0pt][0pt]{
        \hspace*{1.5em}
        \begin{tikzpicture}
          \node (inner) at (17.3mm,-20mm) {\textit{``a bad joke''}};
          \path (0,0) pic{laurel-wreath};
        \end{tikzpicture}
        \hspace*{-3em}
        \begin{tikzpicture}
          \node (inner) at (17.5mm,-18mm) {\vbox{\small\centering\textit{``non- \\informative''}}};
          \path (0,0) pic{laurel-wreath};
        \end{tikzpicture}
      }
      \par
    }}
    \pause
    \pause
    \vspace*{-3.5em}

    \item In the general case: \bad{No}\pause, \\ but \emph{first-order
    consequences} of the existence of a maximal ideal \good{do hold}.
  \end{enumerate}
\end{frame}}

\begin{frame}{Questions}
  \begin{enumerate}
    \item \!Why has the inductive revolution been so powerful?
    \bigskip

    \item \!Why do proofs using Zorn's maximal ideals work so well in constructive algebra?
    \bigskip

    \item \!Why are elements of~$\bigcap_\ppp \ppp$ not necessarily nilpotent?
    \bigskip

    \item How can we extract computational content from classical proofs?
  \end{enumerate}
\end{frame}

\renewcommand{\insertframeextra}{a}
{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\vspace*{3.23cm}\includegraphics[width=\paperwidth]{topos-horses-lighter-lighter}\end{minipage}}
\begin{frame}{Constructive forcing (= Grothendieck toposes)}
  \justifying
  Let~$L$ be a \hil{forcing notion}, a preorder equipped
  with a \hil{covering system}.\only<1-2>{\footnote{\scriptsize A covering system consists of a
  set~$\Cov(\sigma) \subseteq P({\downarrow}\sigma)$ of \emph{coverings} for
  each element~$\sigma \in L$ subject only to the following simulation
  condition: If~$\tau \preccurlyeq \sigma$ and~$R \in \Cov(\sigma)$, there
  should be a covering~$S \in \Cov(\tau)$ such that~$S \subseteq
  {\downarrow}R$.}}\only<3->{\textsuperscript{\phantom{1}}}
  \hil{Filters}~$F \subseteq L$ are subsets which are upward-closed,
  downward-directed and split the covering system.\only<1-2>{\footnote{\scriptsize
  A subset~$F$ splits the covering system iff for every~$\sigma \in L$ and~$R \in \Cov(\sigma)$,
  if~$\sigma \in F$, then~$\tau \in F$ for some~$\tau \in R$.}}\only<3>{\textsuperscript{\phantom{2}}}
  \pause

  {\centering\footnotesize\begin{tabular}{llll}
    \toprule
    & preorder~$L$ & coverings of an element~$\sigma \in L$ & filters of~$L$ \\
    \midrule
    \normalnumber{1} & $X^*$ & $\{ \sigma x \,|\, x \in X \}$ & maps~$\NN \to X$ \\
    \normalnumber{2} & $X^*$ & $\{ \sigma x \,|\, x \in X \}$,\ \ $\{ \sigma\tau \,|\, \tau \in X^*, a \in \sigma\tau \}$ for each~$a \in X$ & surjections~$\NN \twoheadrightarrow X$ \\
    \normalnumber{3} & f.g. ideals & --- & ideals \\
    \normalnumber{4} & f.g. ideals & $\{ \sigma+(a), \sigma+(b) \}$ for each~$ab \in \sigma$,\ \ $\{\}$ if~$1 \in \sigma$ & prime ideals \\
    \normalnumber{5} & opens & $\mathcal{U}$ such that~$\sigma = \bigcup \mathcal{U}$ & points \\
    \normalnumber{6} & $\{\star\}$ & $\{ \star \,|\, \varphi \} \cup \{ \star \,|\, \neg\varphi \}$ &
    witnesses of~\textsc{lem}
    \\
    \bottomrule
  \end{tabular}\par}
  \bigskip

  \only<3>{\textbf{Def.} Given a monotone predicate~$P$
  on~$L$, inductively define:
  \[
    \infer{P \,|\, \sigma}{P\sigma}
    \qquad
    \infer[{\small(R \in \Cov(\sigma))}]{P \,|\, \sigma}{\forall(\tau \in R)\_\ P \,|\, \tau}
  \]
  We use quantifier-like notation: ``$\nabla\sigma\_ P\sigma$'' means~$P \,|\, \sigma$.}
\end{frame}}

\addtocounter{framenumber}{-1}
\renewcommand{\insertframeextra}{b}
{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\vspace*{3.23cm}\includegraphics[width=\paperwidth]{topos-horses-lighter-lighter}\end{minipage}}
\begin{frame}{Constructive forcing (= Grothendieck toposes)}
  A forcing notion is a template for a \hil{forcing extension}~$V^\nabla$
  of the base universe~$V$:
  \medskip

  \begin{center}\begin{tikzpicture}[remember picture,overlay]
    \node[thick, draw=mypurpledark, rectangle, inner sep=0.3em] (kj) {
      \begin{minipage}{0.6\textwidth}
        \centering
        \emph{When we say that a statement \hil{holds in~$V^\nabla$},} \\
        we mean that its~$\nabla$-translation is true.\par
        \vspace*{0.3em}
      \end{minipage}
    };
  \end{tikzpicture}\end{center}
  \bigskip
  \pause

  \textbf{Examples.}
  \begin{enumerate}
  \justifying
  \item For~$L = \{\star\}$, ``every number is zero or a successor'' holds
  in~$V^\nabla$ because

  \vspace*{-1em}
  \[ \forall(n \in \NN)\_ \neg\neg\bigl(\neg\neg(n = 0) \vee
    \neg\neg(\exists(m \in \NN)\_ \neg\neg(n = S(m)))\bigr). \]

  \pause
  \item For~$L$ associated to a space, ``every symmetric matrix has an
  eigenvector'' holds in~$V^\nabla$ iff for every continuous family of
  symmetric matrices, locally there is a continuous eigenvector-picking
  function.
  \pause
  \medskip

  \item For any~$L$, ``there is a filter of~$L$'' holds in~$V^\nabla$,
  witnessed by the \hil{generic filter} of~$L$.
  \pause
  \medskip

  \item Let~$X$ be a preorder. Then:

  \hil{$\blacktriangleright$} $X$ is well iff the generic sequence~$\NN \to X$
  is good.

  \hil{$\blacktriangleright$} $({<})$ is well-founded iff the generic strictly
  descending chain validates~$\bot$.
  \end{enumerate}
\end{frame}}

\renewcommand{\insertframeextra}{}
\begin{frame}{The modal multiverse}
  \only<1-2>{In general, ``$\varphi$ holds in~$V^\nabla$'' and~``$\varphi$ holds in~$V$''
  are \emph{not} equivalent.

  \hil{$\blacktriangleright$}
  For \hil{positive} extensions, they are equivalent for coherent implications.\\
  %\footnote{bounded first-order formulas of the
  %form~$\forall\ldots\forall\_(\ldots\Rightarrow\ldots)$,
  %where antecedent and succedent do not contain~``$\forall$''
  %and~``${\Rightarrow}$''}.
  \phantom{\hil{$\blacktriangleright$}} {\footnotesize -- e.g. the ``Barr cover''.\par}

  \hil{$\blacktriangleright$}
  For \hil{positive overt} extensions, they are equivalent for bounded first-order formulas. \\
  \phantom{\hil{$\blacktriangleright$}} {\footnotesize -- e.g. $V^\nabla$ containing
  the generic surjection~$\NN \twoheadrightarrow X$, if~$X$ is inhabited.\par}
  \bigskip}
  \pause

  \textbf{Def.} A statement~$\varphi$ holds \ldots
  \begin{enumerate}
    \small
    \item[$\blacktriangleright$] \hil{everywhere} ($\necessary\varphi$) iff
    it holds in every extension.
    \item[$\blacktriangleright$] \hil{somewhere} ($\possible\varphi$) iff
    it holds in some positive extension.
    \item[$\blacktriangleright$] \hil{proximally} ($\xpossible\varphi$) iff
    it holds in some positive overt extension.
  \end{enumerate}
  \bigskip

  \visible<2>{\begin{tikzpicture}[overlay]
    \node[anchor=south east,inner sep=0] (image) at (14.8,-0.8) {
      \includegraphics[width=0.2\textwidth]{branching}
    };
  \end{tikzpicture}\vspace*{-1.6em}}
  \visible<3>{\begin{tikzpicture}[overlay]
    \node[anchor=south east,inner sep=0] (image) at (14.8,0.9) {
      \includegraphics[width=0.2\textwidth]{multiverse}
    };
  \end{tikzpicture}\vspace*{-0.3em}}

  \only<2>{\scriptsize Foreshadowed by:
  \begin{itemize}
    \scriptsize
    \item[1984\phantom{s}] André Joyal, Miles Tierney. \emph{An extension of the Galois theory of
    Grothendieck.}
    \item[1987\phantom{s}] Andreas Blass. \emph{Well-ordering and induction in intuitionistic
    logic and topoi.}
    \item[2010s] Milly Maietti, Steve Vickers. Ongoing work on arithmetic
    universes.
    \item[2011\phantom{s}] Joel David Hamkins. \emph{The set-theoretic multiverse.}
    \item[2013\phantom{s}] Shawn Henry. \emph{Classifying topoi and preservation of higher
    order logic by geometric morphisms.}
  \end{itemize}}
  \pause

  \small
  \begin{multicols}{2}
    For every inhabited set~$X$, \emph{proximally} \\
    there is an enumeration~$\NN \twoheadrightarrow X$.
    \bigskip

    A preorder is well iff \emph{everywhere}, \\
    every sequence is good.
    \bigskip

    A ring element is nilpotent iff \\
    all prime ideals \emph{everywhere} contain it.
    \bigskip

    For every ring, \emph{proximally} \\ there is a maximal ideal.
    \bigskip

    A relation is well-founded iff \emph{everywhere}, there is no descending chain.
    \bigskip

    \emph{Somewhere}, \\ the law of excluded middle holds.
  \end{multicols}
\end{frame}

\begin{frame}{The multiverse perspective}
  \begin{enumerate}
    \item \!\emph{Why has the inductive revolution been so powerful?}

    Because the inductive conditions
    are equivalent to truth in \emph{all} forcing extensions.
    \bigskip

    \item \!\emph{Why do proofs using Zorn's maximal ideals work so well in constructive algebra?}

    Because every ring proximally has a maximal ideal.
    \bigskip

    \item \!\emph{Why are elements of~$\bigcap_\ppp \ppp$ not necessarily nilpotent?}

    Because we forgot the prime ideals in forcing extensions.
    \bigskip

    \item \emph{How can we extract computational content from classical proofs?}

    By traveling the multiverse (upwards, keeping ties to the base), exploiting
    that \\
    -- \textsc{lem} holds \emph{somewhere} and \\
    -- instances of \textsc{dc} holds \emph{proximally}.
  \end{enumerate}
\end{frame}

\backupstart

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\includegraphics[width=\paperwidth]{eventually-monad-cropped}\end{minipage}}
\begin{frame}
  \vspace*{\paperheight}\vspace*{-2.05em}\centering
  \emph{Partial Agda formalization available.}
\end{frame}}

\backupend

\end{document}