% $Header: /cvsroot/latex-beamer/latex-beamer/examples/beamerexample5.tex,v 1.22 2004/10/08 14:02:33 tantau Exp $

\documentclass[11pt]{beamer}

\usetheme{Darmstadt}

\usepackage{times}
\usefonttheme{structurebold}

%%%%%%%
\usepackage{tikz}
%%%%%%%

\usepackage[english]{babel}
\usepackage{pgf,pgfarrows,pgfnodes,pgfautomata,pgfheaps}
\usepackage{amsmath,amssymb}
\usepackage[latin1]{inputenc}

\setbeamercovered{dynamic}

\newcommand{\Lang}[1]{\operatorname{\text{\textsc{#1}}}}

\newcommand{\Class}[1]{\operatorname{\mathchoice
  {\text{\sf \small #1}}
  {\text{\sf \small #1}}
  {\text{\sf #1}}
  {\text{\sf #1}}}}

\newcommand{\NumSAT}      {\text{\small\#SAT}}
\newcommand{\NumA}        {\#_{\!A}}

\newcommand{\barA}        {\,\bar{\!A}}

\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Set}[1]{\{#1\}}

\pgfdeclaremask{tu}{beamer-tu-logo-mask}
\pgfdeclaremask{computer}{beamer-computer-mask}
\pgfdeclareimage[interpolate=true,mask=computer,height=2cm]{computerimage}{beamer-computer}
\pgfdeclareimage[interpolate=true,mask=computer,height=2cm]{computerworkingimage}{beamer-computerred}
\pgfdeclareimage[mask=tu,height=.5cm]{logo}{beamer-tu-logo}

\logo{\pgfuseimage{logo}}

\title{Weak Cardinality Theorems for First-Order Logic}
\author{Till Tantau}
\institute[Technische Universit\"at Berlin]{%
  Fakultät für Elektrotechnik und Informatik\\
  Technische Universit\"at Berlin}
\date{Fundamentals of Computation Theory 2003}

\colorlet{redshaded}{red!25!bg}
\colorlet{shaded}{black!25!bg}
\colorlet{shadedshaded}{black!10!bg}
\colorlet{blackshaded}{black!40!bg}

\colorlet{darkred}{red!80!black}
\colorlet{darkblue}{blue!80!black}
\colorlet{darkgreen}{green!80!black}

\def\radius{0.96cm}
\def\innerradius{0.85cm}

\def\softness{0.4}
\definecolor{softred}{rgb}{1,\softness,\softness}
\definecolor{softgreen}{rgb}{\softness,1,\softness}
\definecolor{softblue}{rgb}{\softness,\softness,1}

\definecolor{softrg}{rgb}{1,1,\softness}
\definecolor{softrb}{rgb}{1,\softness,1}
\definecolor{softgb}{rgb}{\softness,1,1}

\newcommand{\Bandshaded}[2]{
  \color{shadedshaded}
  \pgfmoveto{\pgfxy(-0.5,0)}
  \pgflineto{\pgfxy(-0.6,0.1)}
  \pgflineto{\pgfxy(-0.4,0.2)}
  \pgflineto{\pgfxy(-0.6,0.3)}
  \pgflineto{\pgfxy(-0.4,0.4)}
  \pgflineto{\pgfxy(-0.5,0.5)}
  \pgflineto{\pgfxy(4,0.5)}
  \pgflineto{\pgfxy(4.1,0.4)}
  \pgflineto{\pgfxy(3.9,0.3)}
  \pgflineto{\pgfxy(4.1,0.2)}
  \pgflineto{\pgfxy(3.9,0.1)}
  \pgflineto{\pgfxy(4,0)}
  \pgfclosepath
  \pgffill

  \color{black}  
  \pgfputat{\pgfxy(0,0.7)}{\pgfbox[left,base]{#1}}
  \pgfputat{\pgfxy(0,-0.1)}{\pgfbox[left,top]{#2}}
}

\newcommand{\Band}[2]{
  \color{shaded}
  \pgfmoveto{\pgfxy(-0.5,0)}
  \pgflineto{\pgfxy(-0.6,0.1)}
  \pgflineto{\pgfxy(-0.4,0.2)}
  \pgflineto{\pgfxy(-0.6,0.3)}
  \pgflineto{\pgfxy(-0.4,0.4)}
  \pgflineto{\pgfxy(-0.5,0.5)}
  \pgflineto{\pgfxy(4,0.5)}
  \pgflineto{\pgfxy(4.1,0.4)}
  \pgflineto{\pgfxy(3.9,0.3)}
  \pgflineto{\pgfxy(4.1,0.2)}
  \pgflineto{\pgfxy(3.9,0.1)}
  \pgflineto{\pgfxy(4,0)}
  \pgfclosepath
  \pgffill

  \color{black}  
  \pgfputat{\pgfxy(0,0.7)}{\pgfbox[left,base]{#1}}
  \pgfputat{\pgfxy(0,-0.1)}{\pgfbox[left,top]{#2}}
}

\newcommand{\BaenderNormal}
{%
  \pgfsetlinewidth{0.4pt}
  \color{black}
  \pgfputat{\pgfxy(0,5)}{\Band{input tapes}{}}
  \pgfputat{\pgfxy(0.35,4.6)}{\pgfbox[center,base]{$\vdots$}}
  \pgfputat{\pgfxy(0,4)}{\Band{}{}}

  \pgfxyline(0,5)(0,5.5)
  \pgfxyline(1.2,5)(1.2,5.5)
  \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$w_1$}}

  \pgfxyline(0,4)(0,4.5)
  \pgfxyline(1.8,4)(1.8,4.5)        
  \pgfputat{\pgfxy(0.25,4.25)}{\pgfbox[left,center]{$w_n$}}
  \ignorespaces}

\newcommand{\BaenderZweiNormal}
{%
  \pgfsetlinewidth{0.4pt}
  \color{black}
  \pgfputat{\pgfxy(0,5)}{\Band{Zwei Eingabebänder}{}}
  \pgfputat{\pgfxy(0,4.25)}{\Band{}{}}

  \pgfxyline(0,5)(0,5.5)
  \pgfxyline(1.2,5)(1.2,5.5)
  \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$u$}}

  \pgfxyline(0,4.25)(0,4.75)
  \pgfxyline(1.8,4.25)(1.8,4.75)        
  \pgfputat{\pgfxy(0.25,4.5)}{\pgfbox[left,center]{$v$}}
  \ignorespaces}

\newcommand{\BaenderHell}
{%
  \pgfsetlinewidth{0.4pt}
  \color{black}
  \pgfputat{\pgfxy(0,5)}{\Bandshaded{input tapes}{}}
  \color{shaded}
  \pgfputat{\pgfxy(0.35,4.6)}{\pgfbox[center,base]{$\vdots$}}
  \pgfputat{\pgfxy(0,4)}{\Bandshaded{}{}}

  \color{blackshaded}
  \pgfxyline(0,5)(0,5.5)
  \pgfxyline(1.2,5)(1.2,5.5)
  \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$w_1$}}

  \pgfxyline(0,4)(0,4.5)
  \pgfxyline(1.8,4)(1.8,4.5)        
  \pgfputat{\pgfxy(0.25,4.25)}{\pgfbox[left,center]{$w_n$}}
  \ignorespaces}

\newcommand{\BaenderZweiHell}
{%
  \pgfsetlinewidth{0.4pt}
  \color{black}
  \pgfputat{\pgfxy(0,5)}{\Bandshaded{Zwei Eingabebänder}{}}%
  \color{blackshaded}
  \pgfputat{\pgfxy(0,4.25)}{\Bandshaded{}{}}
  \pgfputat{\pgfxy(0.25,4.5)}{\pgfbox[left,center]{$v$}}
  \pgfputat{\pgfxy(0.25,5.25)}{\pgfbox[left,center]{$u$}}%

  \pgfxyline(0,5)(0,5.5)
  \pgfxyline(1.2,5)(1.2,5.5)

  \pgfxyline(0,4.25)(0,4.75)
  \pgfxyline(1.8,4.25)(1.8,4.75)        
  \ignorespaces}

\newcommand{\Slot}[1]{%
  \begin{pgftranslate}{\pgfpoint{#1}{0pt}}%
    \pgfsetlinewidth{0.6pt}%
    \color{structure}%
    \pgfmoveto{\pgfxy(-0.1,5.5)}%
    \pgfbezier{\pgfxy(-0.1,5.55)}{\pgfxy(-0.05,5.6)}{\pgfxy(0,5.6)}%
    \pgfbezier{\pgfxy(0.05,5.6)}{\pgfxy(0.1,5.55)}{\pgfxy(0.1,5.5)}%
    \pgflineto{\pgfxy(0.1,4.0)}%
    \pgfbezier{\pgfxy(0.1,3.95)}{\pgfxy(0.05,3.9)}{\pgfxy(0,3.9)}%
    \pgfbezier{\pgfxy(-0.05,3.9)}{\pgfxy(-0.1,3.95)}{\pgfxy(-0.1,4.0)}%
    \pgfclosepath%
    \pgfstroke%
  \end{pgftranslate}\ignorespaces}

\newcommand{\SlotZwei}[1]{%
  \begin{pgftranslate}{\pgfpoint{#1}{0pt}}%
    \pgfsetlinewidth{0.6pt}%
    \color{structure}%
    \pgfmoveto{\pgfxy(-0.1,5.5)}%
    \pgfbezier{\pgfxy(-0.1,5.55)}{\pgfxy(-0.05,5.6)}{\pgfxy(0,5.6)}%
    \pgfbezier{\pgfxy(0.05,5.6)}{\pgfxy(0.1,5.55)}{\pgfxy(0.1,5.5)}%
    \pgflineto{\pgfxy(0.1,4.25)}%
    \pgfbezier{\pgfxy(0.1,4.25)}{\pgfxy(0.05,4.15)}{\pgfxy(0,4.15)}%
    \pgfbezier{\pgfxy(-0.05,4.15)}{\pgfxy(-0.1,4.2)}{\pgfxy(-0.1,4.25)}%
    \pgfclosepath%
    \pgfstroke%
  \end{pgftranslate}\ignorespaces}

\newcommand{\ClipSlot}[1]{%
  \pgfrect[clip]{\pgfrelative{\pgfxy(-0.1,0)}{\pgfpoint{#1}{4cm}}}{\pgfxy(0.2,1.5)}\ignorespaces}

\newcommand{\ClipSlotZwei}[1]{%
  \pgfrect[clip]{\pgfrelative{\pgfxy(-0.1,0)}{\pgfpoint{#1}{4.25cm}}}{\pgfxy(0.2,1.25)}\ignorespaces}


\AtBeginSection[]{\frame{\frametitle{Outline}\tableofcontents[current]}}

\begin{document}

\frame{\titlepage}

%\section*{Outline}
\part{Main Part}
\frame{\frametitle{Outline}\tableofcontents[part=1]}

\section{History}

\subsection{Enumerability in Recursion and Automata Theory}

\frame
{
  \frametitle{Motivation of Enumerability}

  \begin{block}{Problem}
    Many functions are not computable or not efficiently computable.\\
We are working on%
\raisebox{-1cm}%
{%
\begin{tikzpicture}
\filldraw [gray] (0,0) circle (2pt)
(1,1) circle (2pt)
(2,1) circle (2pt)
(2,0) circle (2pt);
\draw (0,0) .. controls (1,1) and (2,1) .. (2,0);
\draw (-1.5,0) -- (1.5,0);
\draw (0,-1.5) -- (0,1.5);
\end{tikzpicture}} this picture.
\end{block}
  \vskip-1em
  \begin{overprint}
  \onslide<1-2>
  \begin{example}
    \begin{overprint}
    \onslide<1>
      \vskip0.5em
      \begin{itemize}
      \item
        $\NumSAT$:\\
        How many satisfying assignments does a formula have?
      \end{itemize}

    \onslide<2>
      \vskip0.5em
        For difficult languages~$A$:
        \begin{itemize}
        \item
          Cardinality function $\NumA^n$:\\
          \alert{How many} input words are in~$A$?
        \item
          Characteristic function $\chi_A^n$:\\
          \alert{Which} input words are in~$A$?
        \end{itemize}
      \begin{pgfpicture}{-9cm}{0.75cm}{-9cm}{2cm}
        
        \pgfnodebox{words}[virtual]{\pgfxy(0,3.5)}{$(w_1, \alert{w_2},
          w_3, w_4, \alert{w_5})$}{2pt}{5pt}

        \color{red}
        \pgfputat{\pgfxy(0.75,4.5)}{\pgfbox[center,base]{in $A$}}
        \pgfxyline(0.75,4.4)(-0.6,3.7)
        \pgfxyline(0.75,4.4)(1.2,3.7)
        \color{black}

        \pgfnodebox{number}[virtual]{\pgfxy(-1,1)}{2}{2pt}{2pt}
        \pgfnodebox{string}[virtual]{\pgfxy(1,1)}{0\alert{1}00\alert{1}}{2pt}{2pt}

        \pgfsetstartarrow{\pgfarrowbar}
        \pgfsetendarrow{\pgfarrowto}

        \pgfnodeconnline{words}{string}%{-60}{120}{1cm}{1cm}
        \pgfnodeconnline{words}{number}%{-120}{60}{1cm}{1cm}

        \pgfputat{\pgfxy(-0.9,2.3)}{\pgfbox[center,base]{$\NumA^5$}}
        \pgfputat{\pgfxy(0.9,2.3)}{\pgfbox[center,base]{$\chi_A^5$}}
      \end{pgfpicture}
    \end{overprint}
  \end{example}

  \onslide<3>
    \begin{block}{Solutions}
      Difficult functions can be 
      \begin{itemize}
      \item
        computed using probabilistic algorithms,
      \item
        computed efficiently on average,
      \item
        approximated, or
      \item<alert@1->
        enumerated.
      \end{itemize}
    \end{block}
  \end{overprint}
}

\frame
{
  \frametitle{Enumerators Output Sets of Possible Function Values}
  \begin{columns}
    \begin{column}{4.5cm}
      \begin{pgfpicture}{-0.5cm}{0cm}{4cm}{6cm}

        \pgfputat{\pgfxy(0,0.5)}{\Band{}{output tape}}

        \BaenderHell

        \color{black}

        \only<1-4,6->{\pgfputat{\pgfxy(1.75,2.5)}{\pgfbox[center,center]{\pgfuseimage{computerimage}}}}
        \only<5>{\pgfputat{\pgfxy(1.75,2.5)}{\pgfbox[center,center]{\pgfuseimage{computerworkingimage}}}}

        \begin{pgfscope}
          \only<1>{\ClipSlot{0cm}}
          \only<2>{\ClipSlot{0.6cm}}
          \only<3>{\ClipSlot{1.2cm}}
          \only<4->{\ClipSlot{1.8cm}}
          \BaenderNormal
        \end{pgfscope}        

        \only<1>{\Slot{0cm}}
        \only<2>{\Slot{0.6cm}}
        \only<3>{\Slot{1.2cm}}
        \only<4->{\Slot{1.8cm}}
        
        \only<6->{
          \pgfxyline(0,0.5)(0,1)
          \pgfxyline(1,0.5)(1,1)
          \pgfputat{\pgfxy(0.5,0.75)}{\pgfbox[center,center]{$u_1$}}}
        \only<7->{
          \pgfxyline(2,0.5)(2,1)
          \pgfputat{\pgfxy(1.5,0.75)}{\pgfbox[center,center]{\alert<9>{$u_2$}}}}
        \only<8->{
          \pgfxyline(3,0.5)(3,1)
          \pgfputat{\pgfxy(2.5,0.75)}{\pgfbox[center,center]{$u_3$}}}
        
        \pgfsetlinewidth{0.6pt}
        \color{structure}
        \pgfsetendarrow{\pgfarrowto}
        
        \pgfsetlinewidth{0.6pt}
        \color{structure}
        \pgfsetendarrow{\pgfarrowto}
        \only<-5>{\pgfxycurve(1.75,1.5)(1.75,1)(0,1.5)(0,1.05)}
        \only<6>{\pgfxycurve(1.75,1.5)(1.75,1)(1,1.5)(1,1.05)}
        \only<7>{\pgfxycurve(1.75,1.5)(1.75,1)(2,1.5)(2,1.05)}
        \only<8->{\pgfxycurve(1.75,1.5)(1.75,1)(3,1.5)(3,1.05)}
        
        \only<1>{\pgfxycurve(1.75,3.5)(1.75,3.75)(0,3.5)(0,3.85)}
        \only<2>{\pgfxycurve(1.75,3.5)(1.75,3.75)(0.6,3.5)(0.6,3.85)}
        \only<3>{\pgfxycurve(1.75,3.5)(1.75,3.75)(1.2,3.5)(1.2,3.85)}
        \only<4->{\pgfxycurve(1.75,3.5)(1.75,3.75)(1.8,3.5)(1.8,3.85)}
      \end{pgfpicture}
    \end{column}
    \begin{column}{6.5cm}
      \begin{definition}[1987, 1989, 1994, 2001]
        An \alert{$m$-enumerator} for a function~$f$
        \begin{enumerate}
        \item<alert@1-4>
          reads $n$ input words $w_1$, \dots, $w_n$,
        \item<alert@5>
          does a computation,
        \item<alert@6-8>
          outputs at most $m$ values,
        \item<alert@9>
          one of which is $f(w_1,\dots,w_n)$.
        \end{enumerate}
      \end{definition}
    \end{column}
  \end{columns}
}

\subsection{Known Weak Cardinality Theorem}

\frame
{
  \frametitle{How Well Can the Cardinality Function Be Enumerated?}

  \begin{block}{Observation}
    For fixed~$n$, the cardinality function $\NumA^n$
    \begin{itemize}
    \item
      can be \alert{$1$}-enumerated by Turing machines only for \alert{recursive}~$A$,~but\hskip-0.5cm\hbox{}
    \item
      can be \alert{$(n+1)$}-enumerated for \alert{every} language~$A$.
    \end{itemize}
  \end{block}

  \begin{alertblock}{Question}<2->
    What about $2$-, $3$-, $4$-, \dots, $n$-enumerability?
  \end{alertblock}
}

\newtheorem{card}{Cardinality Theorem}[theorem]
\newtheorem{weakcard}{Weak Cardinality Theorems}[theorem]

\frame
{
  \frametitle{How Well Can the Cardinality Function\\ Be Enumerated
    by Turing Machines?}

  \begin{card}[Kummer, 1992]
    If $\NumA^n$ is $n$-enumerable by a Turing machine, then $A$ is
    recursive.
  \end{card}

  \begin{weakcard}[\uncover<2->{\alert<1-2>{1987},} \uncover<3->{\alert<3>{1989},}
      \uncover<4->{\alert<4>{1992}}]<2-> 
    \begin{enumerate}
    \item<2-| alert@2>
      If $\chi_A^n$ is $n$-enumerable by a Turing machine, then $A$ is
        recursive.
    \item<3-| alert@3>
      If $\NumA^2$ is $2$-enumerable by a Turing machine, then $A$ is
        recursive.
    \item<4-| alert@4>
      If $\NumA^n$ is $n$-enumerable by a Turing machine that never
        enumerates both $0$ and~$n$, then $A$ is recursive.
    \end{enumerate}
  \end{weakcard}
}


\frame
{
  \frametitle{How Well Can the Cardinality Function\\ Be Enumerated
    by Finite Automata?}

  \begin{alertblock}{Conjecture}
    If $\NumA^n$ is $n$-enumerable by a \alert{finite automaton}, then $A$ is
    \alert{regular}.
  \end{alertblock}

  \begin{weakcard}[2001, 2002]
    \begin{enumerate}
    \item
      If $\chi_A^n$ is $n$-enumerable by a \alert{finite automaton}, then $A$ is
      \alert{regular}.
    \item
      If $\NumA^2$ is $2$-enumerable by a \alert{finite automaton}, then $A$ is
      \alert{regular}.
    \item
      If $\NumA^n$ is $n$-enumerable by a \alert{finite automaton} that never
      enumerates both $0$ and~$n$, then $A$ is \alert{regular}.
    \end{enumerate}
  \end{weakcard}
}


\subsection{Why Do Cardinality Theorems Hold Only for Certain Models?}

\frame
{
  \frametitle{Cardinality Theorems Do Not Hold for All Models}

  \begin{pgfpicture}{-2.5cm}{0.3cm}{0.5cm}{6.5cm}
    \pgfsetlinewidth{0.6pt}
    
    \pgfsetendarrow{\pgfarrowto}
    \pgfxyline(0,0.5)(0,6.5)
    \pgfclearendarrow

    \pgfputat{\pgfxy(-0.2,5.75)}{\pgfbox[right,base]{Turing machines}}

    \only<2>{
    \pgfputat{\pgfxy(-0.2,3.75)}{\pgfbox[right,base]{\alert{resource-bounded}}}
    \pgfputat{\pgfxy(-0.2,3.25)}{\pgfbox[right,base]{\alert{machines}}}
    \pgfcircle[fill]{\pgfxy(0,3.6)}{2pt}
    \pgfputat{\pgfxy(0.4,3.5)}{\pgfbox[left,base]{Weak cardinality
        theorems do \alert{not} hold.}}}
    
    \pgfputat{\pgfxy(-0.2,1.5)}{\pgfbox[right,base]{finite}}
    \pgfputat{\pgfxy(-0.2,1)}{\pgfbox[right,base]{automata}}

    \pgfcircle[fill]{\pgfxy(0,5.85)}{2pt}
    \pgfcircle[fill]{\pgfxy(0,1.35)}{2pt}

    \pgfputat{\pgfxy(0.4,5.75)}{\pgfbox[left,base]{Weak cardinality
        theorems hold.}}
    \pgfputat{\pgfxy(0.4,1.25)}{\pgfbox[left,base]{Weak cardinality
        theorems hold.}}
  \end{pgfpicture}
}

\frame
{
  \frametitle{Why?}

  \begin{block}{First Explanation}<1>
    The weak cardinality theorems hold both for recursion and automata
    theory \alert{by coincidence}.
  \end{block}

  \begin{block}{Second Explanation}<1-2>
    The weak cardinality theorems hold both for
    recursion and automata theory, \alert{because they are
      instantiations of\\ single, unifying theorems}.
  \end{block}
  
  \vskip1em
  \visible<2->{
    The second explanation is correct.\\
    The theorems can (almost) be unified using first-order logic.
    }
}
   
    

\section[Unification by Logic]{Unification by First-Order Logic}

\subsection{Elementary Definitions}

\frame
{
  \frametitle{What Are Elementary Definitions?}

  \begin{definition}
    A relation~$R$ is \alert{elementarily definable in a
    logical structure~$\mathcal S$} if
    \begin{enumerate}
    \item
      there exists a first-order formula~$\phi$,
    \item
      that is true exactly for the elements of~$R$.
    \end{enumerate}    
  \end{definition}

  \begin{example}
    The set of even numbers is elementarily definable in $(\Nat, +)$
    via the formula $\phi(x) \equiv \exists z \centerdot z+z=x$.
  \end{example}

  \begin{example}
    The set of powers of 2 is not elementarily definable in $(\Nat, +)$.
  \end{example}
}


\frame
{
  \frametitle{Characterisation of Classes by Elementary Definitions}

  \begin{theorem}[B\"uchi, 1960]
    There exists a logical structure~$(\Nat, +, \mathrm e_2)$
    such that a set $A \subseteq \Nat$ is\\ \alert{regular} iff it is 
    \alert{elementarily definable in~$(\Nat, +, \mathrm e_2)$}.
  \end{theorem}

  \begin{theorem}
    There exists a logical structure~$\mathcal R$ such that a set $A
    \subseteq \Nat$ is \alert{recursively enumerable} iff it is \alert{positively
    elementarily definable in~$\mathcal R$}.\hskip-0.5cm\hbox{}
  \end{theorem}
}



\frame
{
  \frametitle{Characterisation of Classes by Elementary Definitions} 

  \begin{pgfpicture}{-5.4cm}{0.3cm}{5.4cm}{6.5cm}
    \pgfsetlinewidth{0.6pt}
    
    \pgfsetendarrow{\pgfarrowto}
    \pgfxyline(0,0.3)(0,6.5)
    \pgfclearendarrow

    \only<2->{
    \pgfputat{\pgfxy(-0.3,0.5)}{\pgfbox[right,base]{Presburger arithmetic}}
    \pgfcircle[fill]{\pgfxy(0,0.6)}{2pt}
    \pgfputat{\pgfxy(0.3,0.5)}{\pgfbox[left,base]{$(\Nat, +)$}}
    }
    \pgfputat{\pgfxy(-0.3,1.5)}{\pgfbox[right,base]{regular sets}}
    \pgfcircle[fill]{\pgfxy(0,1.6)}{2pt}
    \pgfputat{\pgfxy(0.3,1.5)}{\pgfbox[left,base]{$(\Nat, +, \mathrm e_2)$}}

    \pgfputat{\pgfxy(-0.3,2.5)}{\pgfbox[right,base]{\alert{resource-bounded classes}}}
    \pgfcircle[fill]{\pgfxy(0,2.6)}{2pt}
    \pgfputat{\pgfxy(0.3,2.5)}{\pgfbox[left,base]{\alert{none}}}

    \pgfputat{\pgfxy(-0.3,3.5)}{\pgfbox[right,base]{recursively enumerable sets}}
    \pgfcircle[fill]{\pgfxy(0,3.6)}{2pt}
    \pgfputat{\pgfxy(0.3,3.5)}{\pgfbox[left,base]{positively in $\mathcal R$}}

    \only<2->{
    \pgfputat{\pgfxy(-0.3,4.5)}{\pgfbox[right,base]{arithmetic hierarchy}}
    \pgfcircle[fill]{\pgfxy(0,4.6)}{2pt}
    \pgfputat{\pgfxy(0.3,4.5)}{\pgfbox[left,base]{$(\Nat, +, \cdot)$}}

    \pgfputat{\pgfxy(-0.3,5.5)}{\pgfbox[right,base]{ordinal number arithmetic}}
    \pgfcircle[fill]{\pgfxy(0,5.6)}{2pt}
    \pgfputat{\pgfxy(0.3,5.5)}{\pgfbox[left,base]{$(\mathrm{On}, +, \cdot)$}}}
  \end{pgfpicture}
}


\subsection{Enumerability for First-Order Logic}

\frame
{
  \frametitle{Elementary Enumerability is a Generalisation of\\ Elementary Definability}

  \begin{columns}
    \begin{column}{3.25cm}
      \begin{pgfpicture}{-0.25cm}{0cm}{3cm}{4cm}

        \color{shaded}
        \pgfmoveto{\pgfxy(0,1.3)}
        \pgfcurveto{\pgfxy(0.5,2.3)}{\pgfxy(2,1.5)}{\pgfxy(2.5,2.3)}
        \pgflineto{\pgfxy(2.5,1.7)}
        \pgfcurveto{\pgfxy(2,0.7)}{\pgfxy(1,1.7)}{\pgfxy(0,0.5)}
        \pgfclosepath
        \pgffill

        \pgfsetlinewidth{0.8pt}
        \color{black}
        \pgfmoveto{\pgfxy(0,1)}
        \pgflineto{\pgfxy(0.25,1.15)}
        \pgflineto{\pgfxy(0.5,1.5)}
        \pgflineto{\pgfxy(1,1.7)}
        \pgflineto{\pgfxy(1.5,1.5)}
        \pgflineto{\pgfxy(2,1.4)}
        \pgflineto{\pgfxy(2.25,1.5)}
        \pgflineto{\pgfxy(2.5,2)}
        \pgfstroke          

        \pgfsetlinewidth{0.4pt}
        \pgfsetendarrow{\pgfarrowto}
        \pgfxyline(0,0)(2.5,0)
        \pgfxyline(0,0)(0,3)
        \pgfputat{\pgfxy(0.5,1.9)}{\pgfbox[center,base]{$R$}}
        \pgfputat{\pgfxy(2.6,0)}{\pgfbox[left,center]{$x$}}
        \pgfputat{\pgfxy(0,3.2)}{\pgfbox[center,base]{$f(x)$}}
        \pgfputat{\pgfxy(2.55,2)}{\pgfbox[left,center]{$f$}}
      \end{pgfpicture}
    \end{column}
    \begin{column}{7.5cm}
      \begin{definition}
        A function~$f$ is\\
        \alert{elementarily $m$-enumerable in a structure~$\mathcal S$} if
        \begin{enumerate}
        \item
          its graph is contained in an\\
          \alert{elementarily definable} relation~$R$,
        \item
          which is \alert{$m$-bounded}, i.\kern1pt e., for each~$x$
          there are at most~$m$ different~$y$ with $(x,y) \in R$.
        \end{enumerate}
      \end{definition}
    \end{column}
  \end{columns}
}

\frame
{
  \frametitle{The Original Notions of Enumerability are Instantiations}

  \begin{theorem}
    A function is $m$-enumerable by a \alert{finite automaton} iff\\
    it is elementarily $m$-enumerable in \alert{$(\Nat, +, \mathrm e_2)$}.
  \end{theorem} 

  \begin{theorem}
    A function is $m$-enumerable by a \alert{Turing machine} iff\\
    it is positively elementarily $m$-enumerable in \alert{$\mathcal R$}.
  \end{theorem} 
}

%\subsection{Cross Product Theorem for First-Order Logic}

\subsection{Weak Cardinality Theorems for First-Order Logic}

\frame
{
  \frametitle{The First Weak Cardinality Theorem}
  
  \begin{theorem}
    Let $\mathcal S$ be a logical structure with universe~$U$ and let
    $A \subseteq U$. If
    
    \begin{enumerate}
    \item
      $\mathcal S$ is well-orderable and
    \item
      \alert{$\chi_A^n$} is elementarily \alert{$n$}-enumerable in~$\mathcal S$,
    \end{enumerate}
    
    then \alert{$A$ is elementarily definable} in~$\mathcal S$.    
  \end{theorem}
  \begin{overprint}
    \onslide<2>
      \begin{corollary}
        If $\chi_A^n$ is $n$-enumerable by a finite automaton, then
        $A$ is regular.
      \end{corollary}

    \onslide<3>
      \begin{corollary}[with more effort]
        If $\chi_A^n$ is $n$-enumerable by a Turing machine, then $A$
        is recursive.
      \end{corollary}
  \end{overprint}  
}

\frame
{
  \frametitle{The Second Weak Cardinality Theorem}
  
  \begin{theorem}
    Let $\mathcal S$ be a logical structure with universe~$U$ and let
    $A \subseteq U$. If
    
    \begin{enumerate}
    \item
      $\mathcal S$ is well-orderable,
    \item
      every finite relation on~$U$ is elementarily definable
      in~$\mathcal S$, and
    \item
      \alert{$\NumA^2$} is elementarily \alert{$2$}-enumerable in~$\mathcal S$,
    \end{enumerate}
    
    then \alert{$A$ is elementarily definable} in~$\mathcal S$.    
  \end{theorem}
%  \begin{overlayarea}{\textwidth}{2cm}
%    \only<2>{
%      \begin{corollary}
%        If $\NumA^2$ is $2$-enumerable by a finite automaton, then
%        $A$ is regular.
%      \end{corollary}}%
%    \only<3>{
%      \begin{block}{Corollary}
%        If $\NumA^2$ is $2$-enumerable by a Turing machine, then $A$
%        is recursive in the halting problem.
%      \end{block}
%      }
%  \end{overlayarea}
}

\frame
{
  \frametitle{The Third Weak Cardinality Theorem}
  
  \begin{theorem}
    Let $\mathcal S$ be a logical structure with universe~$U$ and let
    $A \subseteq U$. If
    
    \begin{enumerate}
    \item
      $\mathcal S$ is well-orderable,
    \item
      every finite relation on~$U$ is elementarily definable
      in~$\mathcal S$, and
    \item
      \alert{$\NumA^n$} is elementarily \alert{$n$}-enumerable in~$\mathcal S$ via a
      relation that \alert{never `enumerates' both $0$ and~$n$},
    \end{enumerate}
    
    then \alert{$A$ is elementarily definable} in~$\mathcal S$.    
  \end{theorem}
%  \begin{overlayarea}{\textwidth}{2cm}
%    \only<2>{
%      \begin{corollary}
%        If $\NumA^n$ is $n$-enumerable by a finite automaton that
%        never enumerates both $0$ and~$n$, then $A$ is regular.
%      \end{corollary}}%
%    \only<3>{
%      \begin{block}{Corollary}
%        If $\NumA^n$ is $n$-enumerable by a Turing machine that never
%        enumerates both $0$ and~$n$, then $A$ is recursive in the
%        halting problem.
%      \end{block}
%      }
%  \end{overlayarea}
}



\frame
{
  \frametitle{Relationships Between Cardinality Theorems (CT)}

  \begin{pgfpicture}{0cm}{0cm}{10cm}{5cm}
    \only<2>{%
    \color{alert}
    \pgfnodebox{autX}[virtual]{\pgfxy(2.2,4)}{CT}{2pt}{2pt}
    \color{black}}%
    \pgfnodebox{autA}[virtual]{\pgfxy(1,3)}{1st Weak CT}{2pt}{2pt}
    \pgfnodebox{autB}[virtual]{\pgfxy(1,2)}{2nd Weak CT}{2pt}{2pt}
    \pgfnodebox{autC}[virtual]{\pgfxy(1,1)}{3rd Weak CT}{2pt}{2pt}

    \only<2>{%
    \color{alert}
    \pgfnodebox{logX}[virtual]{\pgfxy(6.2,4.5)}{CT}{2pt}{2pt}%
    \color{black}}%
    \pgfnodebox{logA}[virtual]{\pgfxy(5,3.5)}{1st Weak CT}{2pt}{2pt}
    \pgfnodebox{logB}[virtual]{\pgfxy(5,2.5)}{2nd Weak CT}{2pt}{2pt}
    \pgfnodebox{logC}[virtual]{\pgfxy(5,1.5)}{3rd Weak CT}{2pt}{2pt}

    \pgfnodebox{recX}[virtual]{\pgfxy(10.2,4)}{CT}{2pt}{2pt}
    \pgfnodebox{recA}[virtual]{\pgfxy(9,3)}{1st Weak CT}{2pt}{2pt}
    \pgfnodebox{recB}[virtual]{\pgfxy(9,2)}{2nd Weak CT}{2pt}{2pt}
    \pgfnodebox{recC}[virtual]{\pgfxy(9,1)}{3rd Weak CT}{2pt}{2pt}

    \pgfputat{\pgfxy(1,4.5)}{\pgfbox[center,base]{\structure{automata theory}}}
    \pgfputat{\pgfxy(5,5)}{\pgfbox[center,base]{\structure{first-order logic}}}
    \pgfputat{\pgfxy(9,4.5)}{\pgfbox[center,base]{\structure{recursion
          theory}}}

    {%
    \color{structure}%
    \pgfxyline(3,0)(3,5)
    \pgfxyline(7,0)(7,5)
    }%
    \pgfsetendarrow{\pgfarrowto}
    \pgfnodeconnline{logA}{autA}
    \pgfnodeconnline{logA}{recA}
    \pgfnodeconnline{logB}{autB}
    \pgfnodeconnline{logC}{autC}

    \pgfnodeconncurve{recX}{recA}{-60}{5}{10pt}{10pt}
    \pgfnodeconncurve{recX}{recB}{-55}{5}{10pt}{20pt}
    \pgfnodeconncurve{recX}{recC}{-50}{5}{10pt}{30pt}

    \only<2>{%
      \alert{
        \pgfnodeconnline{logX}{autX}
        \pgfnodeconncurve{logX}{logA}{-60}{0}{10pt}{10pt}
        \pgfnodeconncurve{logX}{logB}{-55}{0}{10pt}{20pt}
        \pgfnodeconncurve{logX}{logC}{-50}{0}{10pt}{30pt}
        \pgfnodeconncurve{autX}{autA}{-60}{11}{10pt}{10pt}
        \pgfnodeconncurve{autX}{autB}{-55}{11}{10pt}{20pt}
        \pgfnodeconncurve{autX}{autC}{-50}{11}{10pt}{30pt}
      }
    }

    \pgfsetdash{{3pt}{3pt}}{0pt}
    \pgfnodeconnline{logB}{recB}
    \pgfnodeconnline{logC}{recC}

    \only<2>{%
    \alert{\pgfnodeconnline{logX}{recX}}}
  \end{pgfpicture}
}


\section{Applications}

\subsection{A Separability Result for First-Order Logic}

%\frame
%{
%  \begin{columns}
%    \begin{column}{2.4cm}
%      \begin{pgfpicture}{-1.2cm}{-1.2cm}{1cm}{1cm}
%        \color{shaded}
%        \pgfrect[fill]{\pgfxy(-1.4,-1)}{\pgfxy(2.8,2)}

%        \color{white}
%        \pgfcircle[fill]{\pgfxy(-0.6,0)}{0.5cm}
%        \pgfcircle[fill]{\pgfxy(0.6,0)}{0.5cm}
%        \only<2->{%      
%          \color{softred}
%          \pgfcircle[fill]{\pgfxy(-0.6,0)}{0.6cm}}%
%        %
%        \color{black}
%        \pgfcircle[stroke]{\pgfxy(-0.6,0)}{0.5cm}
%        \pgfcircle[stroke]{\pgfxy(0.6,0)}{0.5cm}

%        \pgfputat{\pgfxy(-0.6,0)}{\pgfbox[center,center]{$A^{(n)}$}}
%        \pgfputat{\pgfxy(0.6,0)}{\pgfbox[center,center]{$\barA{}^{(n)}$}}     
%      \end{pgfpicture}
%    \end{column}
%    \begin{column}{8cm}
%      \begin{block}{Notation}
%        Let $A^{(n)}$ contain all $n$ tuples of\\
%        distinct elements of~$A$.
%      \end{block}
      
%      \begin{block}{Theorem}
%        Let $\mathcal S$ be a well-orderable logical structure in which
%        all finite relations are elementarily definable.\\[0.5em]
%        If $A^{(n)}$ and $\barA{}^{(n)}$ are \alert<2>{elementarily separable}
%        in~$\mathcal S$, then~so~are~$A$~and~$\barA$.
%      \end{block}

%      \uncover<3>{
%        \begin{alertblock}{Note}
%          The theorem is no longer true if $\barA$ is replaced by an
%          arbitrary set~$B$.
%        \end{alertblock}
%      }
%    \end{column}
%  \end{columns}
%}


\frame
{
  \begin{columns}
    \begin{column}{4cm}
      \begin{pgfpicture}{-2cm}{-1.75cm}{2cm}{2.25cm}
        \color{shaded}
        \pgfrect[fill]{\pgfxy(-2,-1.75)}{\pgfxy(4,4)}
                                %\pgfcircle[fill]{\pgforigin}{2cm}

        \only<1>{%
          \color{white}%
          \pgfcircle[fill]{\pgfpolar{90}{1cm}}{\innerradius}
          \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\innerradius}
          \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\innerradius}}%
        \only<2->{%      
        \color{softred}
        \pgfcircle[fill]{\pgfpolar{90}{1cm}}{\radius}
        \color{softgreen}
        \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\radius}
        \color{softblue}
        \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}}%
        %
      \only<2->{%
        \begin{pgftranslate}{\pgfpolar{90}{1cm}}
          \pgfzerocircle{\radius}
          \pgfclip
          
          \begin{pgftranslate}{\pgfpolar{-90}{1cm}}
            \color{softrb}
            \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}
            \color{softrg}
            \pgfcircle[fill]{\pgfpolar{210}{1cm}}{\radius}
          \end{pgftranslate}
        \end{pgftranslate}

        \begin{pgftranslate}{\pgfpolar{210}{1cm}}
          \pgfzerocircle{\radius}
          \pgfclip
          
          \begin{pgftranslate}{\pgfpolar{30}{1cm}}
            \color{softgb}
            \pgfcircle[fill]{\pgfpolar{330}{1cm}}{\radius}
          \end{pgftranslate}
        \end{pgftranslate}}%
        %
        \color{black}
        \pgfcircle[stroke]{\pgfpolar{90}{1cm}}{\innerradius}
        \pgfcircle[stroke]{\pgfpolar{210}{1cm}}{\innerradius}
        \pgfcircle[stroke]{\pgfpolar{330}{1cm}}{\innerradius}

        \pgfputat{\pgfrelative{\pgfpolar{90}{1cm}}%
          {\pgfpoint{0pt}{-.5ex}}}%
        {\pgfbox[center,base]{$A\times \barA$}}
        \pgfputat{\pgfrelative{\pgfpolar{210}{1cm}}%
          {\pgfpoint{0pt}{-.5ex}}}%
        {\pgfbox[center,base]{$A\times A$}}
        \pgfputat{\pgfrelative{\pgfpolar{330}{1cm}}%
          {\pgfpoint{0pt}{-.5ex}}}%
        {\pgfbox[center,base]{$\barA\times \barA$}}

      \end{pgfpicture}
    \end{column}
    \begin{column}{6.8cm}
      \begin{theorem}
        Let $\mathcal S$ be a well-orderable logical structure in which
        all finite relations are elementarily definable.\\[0.5em]
        If there exist elementarily definable supersets of
        {\color<2>{darkgreen}$A \times A$},
        {\color<2>{darkred}$A \times \barA$}, and
        {\color<2>{darkblue}$\barA \times \barA$} whose
        intersection is empty,\\
        then $A$ is elementarily definable in~$\mathcal S$. 
      \end{theorem}  
      \begin{alertblock}{Note}<3>
        The theorem is no longer true\\
        if we add $\barA \times A$ to the list. 
      \end{alertblock}%
    \end{column}
  \end{columns}
}


\section*{Summary}

\frame
{
  \frametitle{Summary}

  \begin{block}{Summary}
  \begin{itemize}
  \item
    The weak cardinality theorems for first-order logic \alert{unify}\\
    the weak cardinality theorems of automata and recursion theory.
  \item
    The logical approach yields
    weak cardinality theorems for\\ \alert{other computational models}.
  \item
    Cardinality theorems are \alert{separability theorems} in disguise.
  \end{itemize}
  \end{block}{}

  \begin{block}{Open Problems}
    \begin{itemize}
    \item
      Does a cardinality theorem for first-order logic hold?
    \item
      What about non-well-orderable structures like $(\mathbb R, +,
      \cdot)$? 
    \end{itemize}
  \end{block}
}

\end{document}


