\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{csquotes}
\usepackage[foundations, settheory]{../lib/tex/naproche}

\newcommand{\F}{\mathcal{F}}

\title{Paradoxes}
\author{Marcel Schütz}
\date{2022}

\begin{document}
  \maketitle

  \noindent This is a small collection of some famous (mathematical) paradoxes.
  On mid-range hardware \Naproche needs approximately 15 seconds to check it,
  plus approximately 25 minutes to check the library files it depends on.

  \begin{forthel}
    [readtex \path{vocabulary.ftl.tex}]

    [readtex \path{macros.ftl.tex}]

    [readtex \path{axioms.ftl.tex}]
  \end{forthel}


  \section*{The Drinker Paradox}

  The \emph{Drinker Paradox} is a principle of classical predicate logic
  popularised by the logician Raymond Smullyan in his 1978 book \textit{What Is
  the Name of this Book?} which can be stated as:

  \begin{quotation}
    \noindent There is someone in the pub such that, if he is drinking then
    everyone in the pub is drinking.
  \end{quotation}

  \noindent We can formalize and prove this assertion in \Naproche:

  \begin{forthel}
    \begin{signature*}
      A person is a notion.
    \end{signature*}

    \begin{signature*}
      Let $P$ be a person.
      $P$ is drinking is an atom.
    \end{signature*}

    \begin{signature*}
      The pub is an object.
    \end{signature*}

    \begin{signature*}
      Let $P$ be a person and $A$ be an object.
      $P$ is inside $A$ is a relation.
    \end{signature*}

    \begin{theorem*}
      Assume that there is a person inside the pub.
      Then there is a person $P$ such that $P$ is inside the pub and if $P$ is
      drinking then every person inside the pub is drinking.
      %Then there is a person $P$ inside the pub such that if $P$ is drinking
      %then every person inside the pub is drinking.
    \end{theorem*}
    \begin{proof}[by case analysis]
      Case every person inside the pub is drinking.
        Choose a person $P$ inside the pub.
        Then $P$ is drinking and every person inside the pub is drinking.
        Hence if $P$ is drinking then every person inside the pub is drinking.
      End.

      %Case there is a person inside the pub that is not drinking.
      Case there is a person that is inside the pub and not drinking.
        %Consider a person $P$ inside the pub that is not drinking.
        Consider a person $P$ that is inside the pub and not drinking.
        Then if $P$ is drinking then every person inside the pub is drinking.
      End.
    \end{proof}
  \end{forthel}


  \section*{Russell's Paradox}

  \emph{Russell's Paradox} is a set-theoretical paradox discovered by Bertrand
  Russell in 1901 which shows that every set theory with an unrestricted
  comprehension principle leads to contradictions.
  Using \Naproche's ontology of classes and sets and its inbuilt axiom of class
  comprehension we can formalize this paradox as follows.

  \begin{forthel}
    \begin{theorem*}
      There exists a class that is not a set.
    \end{theorem*}
    \begin{proof}
      Define $R = \{ x \mid x$ is a set such that $x \notin x \}$.
      Assume that $R$ is a set.
      Then $R \in R$ iff $R \notin R$.
      Contradiction.
    \end{proof}
  \end{forthel}

  By considering \emph{propositions} instead of \emph{sets}, Russell came up
  with the following variant of his 1901 paradox.
  If, for any class $P$ of propositions, we write $\sqcap P$ for the proposition
  ``every proposition in $P$ is true'' then one can show that for any classes of
  propositions $P$ and $Q$ it does not need to be the case that $P = Q$ if
  $\sqcap P = \sqcap Q$:

  \begin{forthel}
    \begin{signature*}
      A proposition is an object.
    \end{signature*}

    \begin{signature*}
      Let $p$ be a proposition.
      $p$ is true is an atom.
    \end{signature*}

    \begin{signature*}
      Let $P$ be a class such that every element of $P$ is a proposition.
      $\sqcap P$ is a proposition such that $\sqcap P$ is true iff every element
      of $P$ is true.
    \end{signature*}

    \begin{theorem*}
      It is wrong that for any classes $P, Q$ such that every element of $P$ is a
      proposition and every element of $Q$ is a proposition we have
      \[ \sqcap P = \sqcap Q \implies P = Q. \]
    \end{theorem*}
    \begin{proof}
      Assume the contrary.
      Define $Q = \{ q \mid$ there exists a class $P$ such that every element of
      $P$ is a proposition and $q = \sqcap P$ and $q \notin P \}$.
      Consider $q = \sqcap Q$.
      Then for any class $P$ such that every element of $P$ is a proposition and
      $\sqcap q = P$ we have $P = Q$.
      Hence $q \in Q$ iff $q \notin Q$.
      Contradiction.
    \end{proof}
  \end{forthel}

  If we replace the term ``proposition'' by \Naproche's inbuilt term ``object''
  and consider an arbitrary meta function $\F$ instead of the operation
  $\sqcap$, this paradox leads to the observation that there are more classes
  than objects in the sense that the meta collection of all classes cannot be
  embedded into the collection of all objects:

  \begin{forthel}
    \begin{signature*}
      Let $A$ be a class.
      $\F(A)$ is an object.
    \end{signature*}

    \begin{theorem*}
      There exist distinct classes $A, B$ such that $\F(A) =
      \F(B)$.
    \end{theorem*}
    \begin{proof}
      Assume the contrary.
      Define $B = \{ b \mid$ there exists a class $A$ such that $\F(A) = b$ and
      $b \notin A \}$.
      Consider $b = \F(B)$.
      Then for any class $A$ such that $\F(A) = b$ we have $A = B$.
      Hence $b \in B$ iff $b \notin B$.
      Contradiction.
    \end{proof}
  \end{forthel}


  \section*{The Barber Paradox}

  The \emph{Barber Paradox} is a puzzle illustrating Russell's Paradox,
  formulated by Bertrand Russell in 1918 with the following words:

  \begin{quotation}
    \noindent You can define the barber as \enquote{one who shaves all those,
    and those only, who do not shave themselves}.
    The question is, does the barber shave himself?
  \end{quotation}

  \noindent We can show in \Naproche that the existence of such a barber would
  be contradictory.

  \begin{forthel}
    \begin{signature*}
      A barber is a person.
    \end{signature*}

    \begin{signature*}
      Let $B, P$ be persons.
      $B$ shaves $P$ is an atom.
    \end{signature*}

    Let $P$ shaves himself stand for $P$ shaves $P$.

    \begin{theorem*}
      Let $B$ be a barber such that for any person $P$ $B$ shaves $P$ iff $P$
      does not shave himself.
      Then we have a contradiction.
    \end{theorem*}
    \begin{proof}
      $B$ shaves himself iff $B$ does not shave himself.
    \end{proof}
  \end{forthel}


  \section*{Burali-Forti's Paradox}

  \emph{Burali-Forti's paradox}, named after Cesare Burali-Forti, demonstates
  that the assumption of the collection $\Ord$ of all all ordinal numbers being
  a set leads to contradictions.

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{set-theory/sections/02_ordinals.ftl.tex}]

    %[prove on][check on]
  \end{forthel}

  \begin{forthel}
    \begin{theorem*}
      $\Ord$ is not a set.
    \end{theorem*}
    \begin{proof}[by contradiction]
      Assume that $\Ord$ is a set.
      $\Ord$ is transitive and every element of $\Ord$ is transitive.
      Hence $\Ord$ is an ordinal.
      Thus $\Ord \in \Ord$.
      Contradiction.
    \end{proof}
  \end{forthel}


  \section*{Cantor's Paradoxes}

  Similar to Burali-Forti's Paradox, \emph{Cantor's First Paradox}, discovered
  by Georg Cantor in 1897, states that the collection of all cardinal numbers
  cannot be a set.

  \begin{forthel}
    %[prove off][check off]

    [readtex \path{set-theory/sections/06_cardinals.ftl.tex}]

    %[prove on][check on]
  \end{forthel}

  \begin{forthel}
    \begin{theorem*}
      Let $C$ be the collection of all cardinals.
      $C$ is not a set.
    \end{theorem*}
    \begin{proof}
      Assume the contrary.
      Then $\bigcup C$ is a set.

      Let us show that $\bigcup C$ contains every ordinal.
        Let $\alpha$ be an ordinal.
        Choose a cardinal $\kappa$ greater than $\alpha$.
        Then $\alpha \in \kappa \in C$.
        Hence $\alpha \in \bigcup C$.
      End.

      Therefore $\Ord \subseteq \bigcup C$.
      Thus $\Ord$ is a set.
      Contradiction.
    \end{proof}
  \end{forthel}

  \emph{Cantor's Second Paradox} denotes the observation that the collection
  of all sets cannot be a set itself.
  It was shown by Cantor in 1899 via his famous theorem stating that the
  cardinality of any set is strictly smaller than the cardinality of its
  powerset.

  \begin{forthel}
    \begin{theorem*}
      Let $V$ be the collection of all sets.
      $V$ is not a set.
    \end{theorem*}
    \begin{proof}
      Assume the contrary.
      Then $\pow(V)$ is a set.
      Hence $\pow(V)$ is a subset of $V$.
      Thus $|\pow(V)| \leq |V|$.
      Contradiction.
      Indeed $|x| < |\pow(x)|$ for any set $x$.
    \end{proof}
  \end{forthel}
\end{document}
