slides-abmv2024.tex

\documentclass[12pt,utf8,notheorems,compress,t,aspectratio=169]{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{mathtools}
\usepackage{xspace}
\usepackage{booktabs}
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{manfnt}
\usepackage{array}
\usepackage{ragged2e}
\usepackage{multicol}
\usepackage{tabto}
\usepackage{xstring}
\usepackage{proof}
\usepackage{agda}
\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}

\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{Modal operators for a constructive account of well quasi-orders}

\author{Ingo Blechschmidt}
\date{November 30th, 2024}

\setbeameroption{show notes on second screen=bottom}
\newcommand{\jnote}[2]{\only<#1>{\note{\setlength\parskip{\medskipamount}\footnotesize\justifying#2\par}}}

%\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}
\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{\bbb}{\mathfrak{b}}
\newcommand{\ccc}{\mathfrak{c}}
\newcommand{\ppp}{\mathfrak{p}}
\newcommand{\fff}{\mathfrak{f}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\defeq}{\vcentcolon=}
\newcommand{\defeqv}{\vcentcolon\equiv}
\newcommand{\Cov}{\mathrm{Cov}}
\renewcommand{\_}{\mathpunct{.}}
\newcommand{\?}{\,{:}\,}
\newcommand{\speak}[1]{\ulcorner\text{\textnormal{#1}}\urcorner}
\newcommand{\inv}{inv.\@}
\newcommand{\forces}{\vDash}
\newcommand{\ind}{\ensuremath{_\text{ind}}\xspace}
\newcommand{\sinf}{\ensuremath{_\infty}}
\newcommand{\impl}{\ensuremath{_\text{impl}}\xspace}

\setbeamertemplate{blocks}[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.05em,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.05em,outer sep=0.05em] (#1) {#2};}}

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

\newlength\stextwidth
\newcommand\makesamewidth[3][c]{%
  \settowidth{\stextwidth}{#2}%
  \makebox[\stextwidth][#1]{#3}%
}

\newcommand{\dnote}[1]{%
  \begin{tabular}{@{}m{2em}@{}m{0.83\textwidth}@{}}%
    \textdbend &#1%
  \end{tabular}%
  \par
}

\newcommand{\genalpha}{\mbox{$\hspace{0.12em}\shortmid\hspace{-0.62em}\alpha$}}

\usepackage{newunicodechar}

\newunicodechar{∇}{\ensuremath{\nabla}}
\newunicodechar{λ}{\ensuremath{\lambda}}
\newunicodechar{σ}{\ensuremath{\sigma}}
\newunicodechar{τ}{\ensuremath{\tau}}
\newunicodechar{∷}{\ensuremath{\!\!\!}}
\newunicodechar{⧺}{\ensuremath{\!\!\!}}
\newunicodechar{₁}{\ensuremath{_1}}
\newunicodechar{₂}{\ensuremath{_2}}
\newunicodechar{∈}{\ensuremath{\in}}

\begin{document}

\addtocounter{framenumber}{-1}

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\centering\includegraphics[width=\paperwidth]{tower}\end{minipage}}
\begin{frame}[c]
  \centering
  \color{white}

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

  \scriptsize

  \setbeamercolor{block body}{bg=black!100}
  \begin{minipage}{0.62\textwidth}
    \begin{block}{\centering Arbeitstagung Bern--München--Verona}
      \centering\normalsize\color{white}
      \hil{Modal operators for \\ a constructive account of
      well quasi-orders} \\[-0.9em]
      \
    \end{block}
  \end{minipage}

  \bigskip
  \bigskip
  \bigskip
  \bigskip
  \bf
  \colorbox{black}{November 30th, 2024}%
  \bigskip

  \colorbox{black}{\begin{minipage}{0.2\textwidth}
    \centering
    Ingo Blechschmidt \\
    University of Antwerp
  \end{minipage}}
\end{frame}}

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

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\vspace*{2.1em}\includegraphics[height=\paperheight]{sea-of-clouds-1}\end{minipage}}
\begin{frame}{Well quasi-orders}
  \jnote{2-3}{
    The presented proof rests on the law of excluded middle and hence cannot
    immediately be interpreted as a program for finding suitable indices~$i <
    j$. However, constructive proofs are also possible (for instance by
    induction on the value of a given term of the sequence, see
    \href{https://www.math.lmu.de/~petrakis/Dickson.pdf}{Constructive
    combinatorics of Dickson's Lemma} by Iosif Petrakis for several fine
    quantitative results). And even more:
    There is a procedure for regarding this proof---and many others in the
    theory of well quasi-orders---as \emph{blueprints} for more informative
    constructive proofs. This shall be our motto for today:

    \emph{Do not take classical proofs literally, instead ask which
    constructive proofs they are blueprints for.}
  }

  \jnote{3}{
    The displayed stability results, along with several others, provide a
    flexible toolbox for constructing new well quasi-orders from given ones.
    However, with the classical formulation of \emph{well},
    renamed~``well\sinf'' on the next slide, these results are inherently
    classical.

    In Higman's lemma, the set~$X^*$ of finite lists of elements of~$X$ is
    equipped with the following ordering: We have~$x_0 \ldots x_{n-1} \leq y_0
    \ldots y_{m-1}$ iff there is an increasing injection~$f : \{ 0,\ldots,n-1 \} \to \{
    0,\ldots,m-1 \}$ such that~$x_i \leq y_{f(i)}$ for all~$i < n$.
  }

  \jnote{4}{
    The dependence of the theory on well quasi-orders on classical transfinite
    methods is already present in one of basic observations of this theory:

    \textbf{Lemma.} Let~$X$ be well\sinf. Let~$\alpha : \NN \to X$. Then there
    is an increasing subsequence~$\alpha\,i_0 \leq \alpha\,i_1 \leq
    \ldots$.

    \emph{Proof.} Let~$K \defeq \{ n \in \NN \,|\, \neg \exists m > n\_
    \alpha\,n \leq \alpha\,m \}$ be the set of indices of those terms which cannot
    appear as the first component of a good pair. If~$K$ is in bijection
    with~$\NN$, there is a subsequence~$\alpha\,k_0 \leq \alpha\,k_1 \leq
    \ldots$ with~$k_0, k_1, \ldots \in K$. As~$X$ is well\sinf, this sequence
    is good, a contradiction.

    Hence~$K$ is not in bijection with~$\NN$. Assuming~\bad{\textsc{lem}},
    it is hence bounded by a number~$N$, and (again
    with~\bad{\textsc{lem}}), for every index~$a > N$ there is an index~$b >
    a$ such that~$\alpha\,a \leq \alpha\,b$. Thus,
    assuming~\bad{\textsc{dc}}, every number~$i_0 > N$ is a suitable
    starting index for an infinite increasing subsequence. \qed

    The appeal to dependent choice can be removed by always picking the
    smallest possible next index in~$\NN \setminus K$, doable by yet another
    invocation of~\bad{\textsc{lem}}, but the result remains fundamentally
    noneffective---in the special case~$X = (\{ 0, 1 \}, {=})$, the statement
    of the lemma implies the infinite pigeonhole principle.
  }

  \jnote{5-7}{
    Luckily, thanks to work by Thierry Coquand, Daniel Fridlender and Monika
    Seisenberger, a constructive substitute is available, the notion well\ind.
    In classical mathematics (where~\textsc{lem} and~\textsc{dc} and hence bar
    induction are available), this notion is equivalent to well\sinf.

    The assertion~``$\mathsf{Good} \mid [\,]$'' is pronounced ``$\mathsf{Good}$
    bars the empty list'', and is defined as follows: Let~$B$ be a predicate
    on~$X^\star$. Then~$B \mid
    \sigma$ is inductively generated by the following two clauses.

    \vspace*{-0.5em}
    \begin{enumerate}
      \item If~$B\sigma$, then~$B \mid \sigma$.
      \\[-1.3em]
      \item If~$B \mid \sigma x$ for all~$x \in X$, then~$B \mid \sigma$.
    \end{enumerate}
    \vspace*{-0.5em}

    Here~$\sigma x$ denotes the concatenation of the list~$\sigma$ with the
    element~$x$. The accompanying induction principle is the following: Let~$Q$
    be a predicate on~$X^*$ such that, for all~$\sigma \in X^*$,~$B\sigma \Rightarrow Q\sigma$ and
    $(\forall x \in X\_ Q(\sigma x)) \Rightarrow Q\sigma$. Then, for
    all~$\sigma \in X^*$: If~$B \mid \sigma$, then~$Q\sigma$.

    Intuitively, the assertion~``$B \mid \sigma$'' expresses (in a positive
    direct way) that no matter how~$\sigma$ evolves to a longer finite
    list~$\tau$, eventually~$B\tau$ will hold.
  }

  \jnote{8}{
    \begin{columns}[t]
      \begin{column}{0.60\textwidth}
        The original notion well\sinf:
        \begin{itemize}
          \justifying
          \item[\cmark] short and simple
          \\[-1.3em]
          \item[\cmark] constructively satisfied for the main examples (but
          only because of the theory around well\ind)
          \\[-1.3em]
          \item[\cmark] concise abstract proofs (albeit employing transfinite methods)
          \\[-1.3em]
          \item[\xmark] main results not constructively attainable
          \\[-1.3em]
          \item[\xmark] philosophically strenuous by the quantification over all sequences
          \\[-1.3em]
          \item[\xmark] not stable under ``change of base''---a forcing extension
          of the universe may well contain more sequences than the base universe
          \\[-1.3em]
          \item[\xmark] negative (universal) condition
        \end{itemize}
      \end{column}

      \begin{column}{0.45\textwidth}
        The constructive substitute well\ind:
        \begin{itemize}
          \justifying
          \item[\cmark] main results constructive
          \\[-1.3em]
          \item[\cmark] stable under change of base
          \\[-1.3em]
          \item[\cmark] positive (existential) condition
          \\[-1.3em]
          \item[\xmark] proofs intriguing, but also somewhat alien, not just some
          trivial reshuffling of the classical arguments, classical sequence
          language cannot be used
        \end{itemize}
      \end{column}
    \end{columns}
  }

  \jnote{9}{
    Constructively, the notion~well\ind is much stronger than~well\sinf, as it
    ensures goodness (in an appropriate sense) of sequence-like entities
    which are not actually honest maps~$\NN \to X$.

    For partial maps~$\alpha$, by~$\alpha\,n\,\downarrow$ we mean that~$\alpha$
    is defined on the input~$n$. If~\bad{\textsc{lem}} is available, then a
    partial map such that~$\neg\neg(\alpha\,n\,\downarrow)$ for all~$n \in \NN$
    is already a total map, but without~\bad{\textsc{lem}} the hypothesis
    well\sinf{} does not have anything to say about such a partially-defined
    sequence.

    If~\bad{\textsc{dc}} is available, then every multivalued map contains a
    singlevalued map, but again without~\bad{\textsc{dc}} the hypothesis well\sinf{}
    does not have anything to say about multivalued sequences.
  }

  \jnote{10}{
    It turns out that these entities are, or give rise to, actual maps~$\NN \to
    X$---but in a forcing extension of the universe.

    Forcing originated in set theory to construct new models for set theory
    from given ones, in order to explore the range of set-theoretic
    possibility. For instance, by forcing we can construct models of~\text{zfc}
    validating the continuum hypothesis and also models which falsify it.

    We here refer to a simplification of original forcing which is useful in a
    constructive metatheory. At its core, every forcing extension is just a
    formula and proof translation of a certain form. For instance, there is a
    forcing extension validating~\bad{\textsc{lem}} even if the base universe
    does not; this forcing extension is not a deep mystery, for a statement holds
    in that forcing extension iff its double negation translation holds in the
    base universe and it is well-known that the double negation translation
    of~\bad{\textsc{lem}} is an intuitionistic tautology.

    \href{https://www.speicherleck.de/iblech/stuff/slides-herrsching2023.pdf}{Here
    is a set of slides on constructive forcing}, and Section~4 of
    \href{https://raw.githubusercontent.com/iblech/constructive-maximal-ideals/master/tex/extended.pdf}{this
    joint paper with Peter Schuster} contains a written summary of constructive
    forcing.
  }

  \textbf{Def.} Let~$(X,{\leq})$ be a quasi-order.
  \vspace*{-0.3em}
  \begin{itemize}
    \item A sequence~$\alpha : \NN \to X$ is \hil{good} iff
    there exist~$i < j$ with~$\alpha\,i \leq \alpha\,j$.
    \item The quasi-order~$X$ is \hil{well\only<4->{\sinf}} iff every sequence~$\NN \to X$ is good.
  \end{itemize}
  \pause
  \vspace*{-0.9em}

  \begin{columns}[t]
    \begin{column}{0.46\textwidth}
      \begin{block}{Natural numbers\phantom{y}}
        \textbf{Prop.} $(\NN, {\leq})$ is well\only<4->{\sinf}.
        \smallskip

        \emph{Proof.} Let~$\alpha : \NN \to \NN$. By~\badbox{\textsc{lem}}, there is a
        \bad{minimum}~$\alpha\,i$.
        Set~$j \defeq i + 1$. \qed

        \hfill\color{gray}offensive?
      \end{block}
      \only<2-4>{
        \vspace*{-2em}
        \[ \astikznodetransparentlycircled{xm}{7}\!,
        \quad \astikznodetransparentlycircled{x0}{4}\!,
        \quad \astikznodecircled{t1}{mypurple}{3}\!,
        \quad \astikznodetransparentlycircled{x1}{1}\!,
        \quad \astikznodecircled{t2}{mypurple}{8}\!,
        \quad \astikznodetransparentlycircled{x2}{2}\!,
        \quad \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}}
    \end{column}

    \pause

    \begin{column}{0.50\textwidth}
      \begin{block}{Key stability results}
        \justifying
        \only<1-5>{Assuming~\badbox{\textsc{lem}}
        and~\badbox{\textsc{dc}}}\only<6->{Constructively}, \ldots

        \hil{Dickson:} \tabto{1.8cm} If~$X$ and~$Y$ are well\only<4-5>{\sinf}\only<6->{\ind}, so is~$X \times Y$. \\
        \hil{Higman:}  \tabto{1.8cm} If~$X$ is well\only<4-5>{\sinf}\only<6->{\ind}, so is~$X^\star$. \\
        \hil{Kruskal:} \tabto{1.8cm} If~$X$ is well\only<4-5>{\sinf}\only<6->{\ind}, so is~$\mathrm{Tree}(X)$.
      \end{block}
    \end{column}
  \end{columns}
  \pause
  \pause

  \textbf{Def.} A quasi-order~$X$ is \hil{well\ind} iff~$\mathsf{Good} \mid
  [\,]$, where~$\mathsf{Good}\,x_0 \ldots x_{n-1}$ iff~$\exists i < j\_ x_i \leq x_j$.
  \pause
  \pause

  \small
  With \bad{bar induction},\tabto{3.10cm} $\text{well}\ind \Leftarrow \text{well}\sinf$. \\[-0.2em]
  Constructively,\tabto{3.10cm} $\text{well}\ind \Rightarrow \text{well}\sinf$.
  \only<8>{
    \bigskip
    \begin{columns}[c]
      \begin{column}{0.01\textwidth}
	\includegraphics[height=2.4em]{question-mark}
      \end{column}
      \begin{column}{0.9\textwidth}
      Is there a procedure for reinterpreting \hil{classical proofs}
      regarding well\sinf{} as \newline \hil{blueprints for constructive proofs} regarding well\ind?
      \end{column}
    \end{columns}
  }
  \pause
  \pause
  Moreover, if~$X$ is well\ind, then \ldots
  \begin{itemize}
  \vspace*{-0.7em}
    \small
    \item for every \emph{partial} function~$\alpha$,\tabto{5.25cm}
    if~$\forall n\_ \neg\neg(\alpha\,n\,{\downarrow})$,
    then~$\neg\neg \exists i < j\_ \alpha\,i\,{\downarrow} \wedge
    \alpha\,j\,{\downarrow} \wedge \alpha\,i \leq \alpha\,j$. \\[-2.0em]\
    \item for every \emph{multivalued} function~$\alpha$,\tabto{5.25cm}
    $\exists i < j\_ \exists x \in \alpha\,i\_
    \exists y \in \alpha\,j\_ x \leq y$.
  \end{itemize}
  \pause

  \vspace*{-0.7em}
  \hil{Central insight:} A quasi-order $X$ is well\ind iff $\hil{$\necessary$}\,\forall\alpha : \NN \to
  X\_ \exists i < j\_ \alpha\,i \leq \alpha\,j$.
\end{frame}}

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\includegraphics[width=\paperwidth]{staircase-more-faded}\end{minipage}}
\begin{frame}{The modal multiverse of constructive forcing}
  \jnote{1}{
    By \emph{topos}, we mean \emph{Grothendieck topos}. In constructive
    forcing, a ``forcing extension of the base universe'' is exactly the same
    thing as a Grothendieck topos.

    A particular member of the rich and varied landscape of toposes is the
    \emph{trivial topos}, in which every statement whatsoever holds. By
    restricting to positive toposes, we exclude this special case.

    For positive toposes~$\E$, a geometric implication holds in~$\E$ iff it
    holds in the base universe. For positive overt toposes~$\E$, we even have
    that a bounded first-order formula holds in~$\E$ iff it holds in the base.
    Hence, for the purpose of verifying a bounded first-order assertion about
    the base, we can freely pass to a positive overt topos with problem-adapted
    better higher-order properties (such as that some uncountable set from the
    base now appears countable, or that an infinite sequence whose existence is
    predicted by failing dependent choice now actually exists).

    \href{https://www.speicherleck.de/iblech/stuff/early-draft-modal-multiverse.pdf}{Here
    is a rough early draft of a preprint with more details about the modal
    multiverse.}
  }

  \jnote{2}{
    The idea to study the modal multiverse of toposes in a principled manner
    was proposed by Alexander Oldenziel in 2016. \emph{Foreshadowed by:}
    \begin{itemize}
      \item[1984\phantom{s}] André Joyal, Miles Tierney. ``An extension of the Galois theory of Grothendieck''.
      \\[-1em]
      \item[1987\phantom{s}] Andreas Blass. ``Well-ordering and induction in intuitionistic logic and topoi''.
      \\[-1em]
      \item[2010s] Milly Maietti, Steve Vickers. Ongoing work on arithmetic universes.
      \\[-1em]
      \item[2011\phantom{s}] Joel David Hamkins. ``The set-theoretic multiverse''.
      \\[-1em]
      \item[2013\phantom{s}] Shawn Henry. ``Classifying topoi and preservation of higher order logic by geometric morphisms''.
    \end{itemize}
  }

  \jnote{3}{
    With the modal language we seek to provide an accessible and modular
    framework for constructivization results.

    For instance, conservativity of classical logic over intuitionistic logic
    for geometric implications (known under various names such as Barr's
    theorem, Friedman's trick, escaping the continuation monad, \ldots) is
    packaged up by the observation that \emph{somewhere}, the law of excluded
    middle holds.

    Another example:
    In the community around Krull's lemma, it is well-known that
    we can constructively infer that a given ring element~$x \in A$ is nilpotent from
    knowing that it is contained in the \emph{generic prime ideal} of~$A$. This entity
    is not actually an honest prime ideal of the ring~$A$ in the base
    universe, but a certain combinatorial notion (efficiently dealt with using
    \emph{entailment relations}). Constructive forcing allows us to reify the
    generic prime ideal as an actual prime ideal in a suitable forcing extension.
  }

  \jnote{4}{
    Here is an example how the modal language helps us to give a constructive
    proof (for well\ind) of Dickson's lemma. In a similar vein Higman's lemma
    and Kruskal's theorem can be proven; with the exception of a preparatory
    first paragraph the original proofs can be copied word for word.

    \textbf{Prop.} Let~$X$ and~$Y$ be well\ind quasi-orders. Then~$X \times Y$
    is well\ind.

    \emph{Proof.} Let~$\alpha = (\beta,\gamma) : \NN \to X \times Y$ be a sequence in an
    arbitrary topos. We need to show that~$\alpha$ is good. It suffices to
    prove that \emph{somewhere}, $\alpha$ is good, as goodness is a geometric
    implication (in fact even a geometric formula). Without loss of generality,
    we may suppose~\textsc{lem} as it holds \emph{somewhere}.

    Hence there is an infinite increasing subsequence
    \[ \beta\,k_0 \leq \beta\,k_1 \leq \ldots. \]
    As~$Y$ is well\ind, the sequence~$\gamma\,k_0, \gamma\,k_1, \ldots$
    is good, so there exist~$i < j$ with~$\gamma\,k_i \leq \gamma\,k_j$. Since we
    also have~$\beta\,k_i \leq \beta\,k_j$, we are done. \qed
  }

  \textbf{Def.} A statement~$\varphi$ holds \ldots
  \begin{itemize}
    \small
    \item \hil{everywhere} \tabto{2.15cm}($\necessary\varphi$)\tabto{3.08cm} iff it holds in every topos
    (over the current base).
    \item \hil{somewhere} \tabto{2.15cm}($\possible\varphi$)\tabto{3.08cm} iff it holds in some positive topos.
    \item \hil{proximally} \tabto{2.15cm}($\xpossible\varphi$)\tabto{3.08cm} iff it holds in some positive overt topos.
  \end{itemize}
  \bigskip

  \begin{tikzpicture}[overlay]
    \node[anchor=south east,inner sep=0] (image) at (14.8,0.6) {
      \includegraphics[width=0.2\textwidth]{branching}
    };
  \end{tikzpicture}\vspace*{-2.3em}
  \pause

  \colorbox{white}{\bignumber{1} A quasiorder is well\ind iff \emph{everywhere}, every sequence is good.}

  \mbox{\qquad
  \colorbox{white}{\bignumber{2} A relation is well-founded iff \emph{everywhere}, there is
  no infinite descending chain.}}

  \qquad
  \qquad
  \colorbox{white}{\bignumber{3} A ring element is nilpotent iff all prime ideals \emph{everywhere} contain it.}

  \mbox{\qquad
  \qquad
  \qquad
  \colorbox{white}{\bignumber{4} For every inhabited set~$X$, \emph{proximally} there is an
  enumeration~$\NN \twoheadrightarrow X$.}}

  \qquad
  \qquad
  \qquad
  \qquad
  \colorbox{white}{\bignumber{5} For every ring, \emph{proximally} there is a maximal ideal.}

  \qquad
  \qquad
  \qquad
  \qquad
  \qquad
  \colorbox{white}{\bignumber{6} \emph{Somewhere}, the law of excluded middle holds.}

  \pause
\end{frame}}

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\vspace*{-4.68em}\includegraphics[width=1.2\paperwidth]{wqo-faded}\end{minipage}}
\begin{frame}{Answering a question by Berardi--Buriola--Schuster}
  \jnote{1-3}{
    Stefano Berardi, Gabriele Buriola and Peter Schuster recognized in their
    recent article
    \href{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.16}{A
    general constructive form of Higman's lemma} the displayed implication as an
    efficient organizing principle for structuring a constructive account of
    well quasi-orders, which they elevated to the status of a definition.

    They recognized that their definition implies well\ind (and hence
    well\sinf), and posed the converse as an open question.

    The generating clauses for~$B \mid_\text{incr} \sigma$, for increasing
    finite lists~$\sigma$, are the following:

    \vspace*{-0.5em}
    \begin{enumerate}
      \item If~$B\sigma$, then~$B \mid_\text{incr} \sigma$.
      \\[-1.3em]
      \item If~$B \mid_\text{incr} \sigma x$ for all~$x \in X$ such that~$\sigma x$ is
      increasing, then~$B \mid_\text{incr} \sigma$.
    \end{enumerate}
  }

  \jnote{4}{
    The modal language unlocked the displayed positive answer to their
    question. As the modal framework is fully constructive, the proof can in
    principle be unrolled to yield a direct (but likely longer) argument not
    involving constructive forcing, giving an explicit algorithm of type
    \[ \mathsf{Good} \mid [\,] \ \times\ B \mid_\text{incr} [\,]
    \ \longrightarrow\ B \mid [\,] \]
    for transforming given witnessing trees. This unwinding is work in
    progress.
  }

  \textbf{Def.} A quasi-order~$X$ is \hil{well\impl} iff (approximately) for
  every monotone predicate~$B$,
  \[ \text{if $B \mid_{\text{incr}} [\,]$, then $B \mid [\,]$.} \]
  \justifying
  {\small``Assume that no matter how the empty list evolves to an \emph{increasing}
  list~$\sigma$, eventually~$B\,\sigma$. Then no matter how the empty
  list evolves to an \emph{arbitrary} list~$\tau$, eventually~$B\,\tau$.''\par}
  \pause

  \hil{Equivalently:} If everywhere every \emph{increasing} infinite sequence~$\alpha : \NN
  \to X$ has a finite prefix validating~$B$, then so does every
  \emph{arbitrary} infinite sequence everywhere.
  \pause

  \textbf{Prop.} $\text{well\impl} \Rightarrow \text{well\ind}$.

  \emph{Proof.} Trivially~$\mathsf{Good} \mid_{\text{incr}} [\,]$,
  hence~$\mathsf{Good} \mid [\,]$ by assumption. \qed
  \pause

  \textbf{Thm.} $\text{well\impl} \Leftarrow \text{well\ind}$.

  \small
  \emph{Proof.} Let~$x_0,x_1,\ldots$ be an infinite sequence (in an arbitrary topos).
  \emph{Somewhere,} \textsc{lem} holds and implies that there is an increasing infinite subsequence~$x_{i_0},
  x_{i_1}, \ldots$. \emph{There} we have, by assumption, a finite prefix
  with~$B\,x_{i_0}\ldots x_{i_n}$. As~$B$ is monotone, \emph{there}
  we also have~$B\,x_0x_1\ldots x_{i_n}$. So \emph{somewhere} there is a finite
  prefix validating~$B$. Hence there actually is a finite prefix
  validating~$B$. \qed
\end{frame}}

\backupstart
{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\vspace*{-2.2em}\includegraphics[width=\paperwidth]{agda-wqo}\end{minipage}}
\begin{frame}
  \vspace*{\paperheight}\vspace*{-2.5em}\centering
  \emph{Agda formalization in progress.}
\end{frame}}
\backupend

\end{document}