\begin{frame}
  \huge
  \vfill
  \centerline{What is a proof?}
  \vfill
\end{frame}

\begin{frame}
  \frametitle{Formal Proof System}

  We will consider a some set of logical formulas $\Formulas$ (e.g. propositional logic)

  \begin{definition}
    An proof system is $(\Formulas,\Infer)$
    where $\Infer \subseteq \Formulas^* \times \Formulas$ a decidable set of \emph{inference steps}.
  \end{definition}
  \begin{itemize}
  \item a set is \emph{decidable} iff there is a program to check if an element belongs to it
  \item given a set $S$, notation $S^*$ denotes all finite sequences with elements from $S$
  \end{itemize}
  
  We schematically write an inference step $((P_1,\ldots,P_n),C) \in \Infer$ by
  \[
    \frac{P_1 \ldots P_n}
    {C}
  \]
  and we say that from $P_1,\ldots,P_n$ (\textbf{premises}) we derive $C$ (\textbf{conclusion}).

  An inference step is called an \emph{axiom instance} when $n=0$ (it has no premises).

  Given a proof system $(\Formulas,\Infer)$, a proof is a finite sequence of inference steps
  such that, for every inference step, each premise is a conclusion of a previous step.  
\end{frame}

\begin{frame}
  \frametitle{Proof in a Proof System}

  \begin{definition}
  Given $(\Formulas,\Infer)$ where $\Infer \subseteq \Formulas^* \times \Formulas$
  a \textbf{proof} in $(\Formulas,\Infer)$ is a finite sequence of inference steps 
  $S_0,\ldots,S_m \in \Infer$ such that, 
  for each $S_i$ where $0 \le i \le m$, for each premise $P_j$ of $S_i$
  there exists $0 \le k < i$ such that $P_j$ is the conclusion of $S_k$.
  \end{definition}

  \[
  \begin{array}{rll}
    S_0: & ((), & C_0) \\
         & \cdots \\
    S_k: & ((\ldots \ldots \ldots), & \mathbf{P_j}) \\
         & \cdots \\
    S_i: & ((\ldots,\mathbf{P_j},\ldots), & C_i)
  \end{array}
  \]

  Given the definition of the proof, we can replace each premise $P_j$
  with the index $k$ where $P_j$ was the conclusion of $S_k$
  ($P_j \equiv \Conc{S_k}$)

  A proof is then a sequence of elements from $\{0,1,\ldots\}^* \times \Formulas$
  where each $S_i$ in the sequence is of the form $(k_1,\ldots,k_n,C)$ for
  $0 \le k_1,\ldots,k_n < i$ and where 
  $(\Conc{S_{k_1}},\ldots,\Conc{S_{k_n}},C) \in \Infer$.
\end{frame}

\begin{frame}
  \frametitle{Proofs as Dags}

  We can view proofs as directed acyclic graphs.

  \ 
  
  Given a proof as a sequence of steps, for each
  $(k_1,\ldots,k_n,C)$ in the sequence 
  we introduce a node labelled by $C$, and directed
  labelled edges $(\Conc{S_{k_j}},j,C)$ for all premises $k_1,\ldots,k_n$.

  \ 

  To check such proof, for each node, follow all of its incoming 
  edges backwards in the order
  of their indices to find the premises, then check that the inference step
  is in $\Infer$.

  \vspace{5cm}
\end{frame}

\begin{frame}
  \huge
  \vfill
  \centerline{An Example System for Propositional Logic}
  \vfill
\end{frame}


\begin{frame}
  \frametitle{A Minimal Propositional Logic Proof System}

  Formulas $\Formulas$ defined by $F ::= x \mid 0 \mid F \to F$

  \ 

  Shorthand:

  $\lnot F \equiv F \to 0$
  % ,  \ \
  % $1 \equiv \lnot 0$,  \ \
  % $F_1 \lor F_2 \equiv (\lnot F_1) \to F_2$, \ \
  % $F_1 \land F_2 \equiv \lnot (\lnot F_1 \lor \lnot F_2)$ 

  \ 

  Inference rules:\ $\Infer = P_2 \cup P_3 \cup \MP$ where: \hfill (see e.g. \wiki{Hilbert system})
  \[\begin{array}{rcl@{}lll}
    P_2 &=& \{ (&(),  & F \to (G \to F) &) \mid F,G \in \Formulas  \} \\ % K
    P_3 &=& \{ (&(),  & ((F \to (G \to H)) \to ((F \to G) \to (F \to H)) &) \mid 
                         F,G,H \in \Formulas \} \\  % S
    \MP &=& \{ (&(F \to G,F), & G & ) \mid F,G \in \Formulas \}
  \end{array}\]
  Elements of $P_1,P_2,P_3$ are all axioms. These are infinite sets, but
  are given a schematic way and there is an algorithm to check if a given
  formula satisfies each of the schemas.

  \ 

  Exercise: draw a DAG representing proof of $a \to a$ where $a$ is a propositional
  variable.

\end{frame}

\begin{frame}
  \frametitle{Proof of $a \to a$}
  {Proof system:\small
  \[
  F \to (G \to F)
  \hspace*{1.5cm}
  ((F \to (G \to H)) \to ((F \to G) \to (F \to H))
  \hspace*{1.5cm}
  \frac{F \to G,F}{G}
  \]}

  
  % Hint: use $P_3$ for $F \equiv a$, $G \equiv a \to a$, $H \equiv a$

  %\pause 
  %Apply MP to the above instance of $P_3$ and an instance of $P_2$, then
  %to another instance of $P_2$.

  \vspace*{5cm}
  \centerline{$a \to a$}
\end{frame}

\begin{frame}
  \huge
  \vfill
  \centerline{Soundness of a Proof System}
  \vfill
\end{frame}


\begin{frame}
  \frametitle{Derivation is a Proof from Assumptions}

  \begin{definition}
  Given $(\Formulas,\Infer)$, $\Infer \subseteq \Formulas^* \times \Formulas$
  \textbf{and a set of assumptions $A \subseteq \Formulas$}, a \textbf{derivation from}
  $A$ in $(\Formulas,\Infer)$ is
  a proof in $(\Formulas, \Infer')$ where:
  \[
    \Infer' = \Infer \cup \{ ( (),F) \mid F \in A \}
  \]
  \end{definition}
  Thus, assumptions from $A$ are treated just as axioms.

  \begin{definition}
  We say that $F \in \Formulas$ is provable from assumptions $A$, denoted
  $A \vdash_{\Infer} F$ iff there exists a derivation from $A$ in $\Infer$
  that contains an inference step whose conclusion is $F$.
  \end{definition}

  We write $\vdash_{\Infer} F$ to denote that there exists a proof in $\Infer$ containing $F$ as a conslusion (same as $\emptyset \vdash_{\Infer} F$).
\end{frame}

\begin{frame}
  \frametitle{Consequence and Soundness in Propositional Logic}

  Given a set $A \subseteq \Formulas$ where $\Formulas$ are in propositional logic,
  and $C \in \Formulas$, we say that $C$ is a \textbf{semantic consequence} of $A$,
  denoted $A \models C$ iff for every environment $e$ that defines
  all variables in 
  $
      FV(C) \cup \bigcup_{P \in A} FV(P),
  $
  if $\interp{P}{e} = 1$ for all $P \in A$, then then $\interp{C}{e}=1$.  

  \begin{definition}
  Given $(\Formulas,\Infer)$ where $\Formulas$ are propositional, step
  $((P_1 \ldots P_n), C) \in \Infer$ is \textbf{sound} iff $\{P_1,\ldots,P_n\} \models C$. Proof system $\Infer$ is sound if every inference step is sound.
  \end{definition}
  For axioms, this definition reduces to saying that $C$
  is true for all interpretations, i.e., that $C$ is a valid formula
  (tautology).

  \begin{theorem}
    Let $(\Formulas,\Infer)$  where $\Formulas$ are propositional logic
    formulas. If every inference rule in $\Infer$ is sound, then
    $A \vdash_{\Infer} F$ implies $A \models F$.
  \end{theorem}
  Proof is immediate by induction on the length of the formal proof.

  Consequence: $\vdash_{\Infer} F$ implies $F$ is a tautology.
\end{frame}

\begin{frame}
  \frametitle{Semantic vs Syntactic Consequence}

  \textbf{Semantic consequence:}
  We check whether $\{A_1 \} \models G$ by checking all possible interpretations:
  in every propositional assignment (any ``world'' we can imagine) if $A_1$
  is true, then so if $G$.  For propositional logic, a world gives truth values
  (0 or 1) for the variables.

  \textbf{Syntactic consequence (provability):}
  We check whether $\{ A_1 \} \vdash G$ by 
  finding a derivation of $G$ with $A_1$ as an additional axiom.
  Syntactic consequence is specific for a particular proof system.


  \
  
  In general we have a set of assumptions, $A = \{ A_1,A_2,\ldots \}$

  \

  For a given proof system, we have two possible inclusions:
  \begin{itemize}
  \item soundness: if $A \vdash G$, then $A \models G$ \\
    (without this, our proof system is ``broken'')
  \item completeness: if $A \models G$, then $A \vdash G$ \\
    (without this, there are true things we cannot prove, which may be OK)
  \end{itemize}
\end{frame}
