\documentclass[aspectratio=169]{beamer}
\usepackage{bbm}
\usepackage{stmaryrd}
\usepackage[mathletters]{ucs}
\usepackage[utf8x]{inputenc}

\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{wasysym}
\usepackage{listings}

\input{../common/scalalistings}

%\usepackage{../common/newunicodechar}
\input{../common/mysymbols}
%\usepackage{../common/mathunicode}

\input{../common/mywords-en}
\input{../common/constructors}

\setbeamersize{text margin left=0.3cm, text margin right=0.3cm}
\usepackage{pgf}
\usepackage{tikz}
\usetikzlibrary{arrows,automata,fit}

%\title{Lecturecise 20 \\ Herbrand's Theorem \\ Resolution for First-Order Logic}
%\date{2013}

\beamertemplatenavigationsymbolsempty

\begin{document}
        
%\maketitle

\begin{frame}{}

  \vfill
  \centerline{\Large Term Models for First-Order Logic}
  \vfill
\end{frame}

\begin{frame}{Example Formula in First-Order Logic}

model of a formula = interpretation (structure) that makes a formula true
\[
\begin{array}{rl}
  ¬ \big( & (∀ x. ∃ y.\ R(x,y))\ ∧ \\
          & (∀ x. ∀ y.\ (R(x,y) \rightarrow ∀ z.\ R(x,f(y,z))))\ ∧ \\
          & (∀ x.\ (P(x) ∨ P(f(x,a))))\ \\
          & \rightarrow ∀ x. ∃ y.\ (R(x,y) ∧ P(y)) \big)
\end{array}
\]
\pause
After normal form and Skolemization we obtain these first-order clauses:
\[
\begin{array}{l}
  R(x,g_1(x)) \\
  ¬ R(x,y) ∨ R(x,f(y,z)) \\
  P(x) ∨ P(f(x,a)) \\
  ¬ R(c_0,y) ∨ ¬P(y) 
\end{array}\]
\begin{itemize}
\item variables are implicitly $∀$ quantified; there are no $∃$ quantifiers
\item each clause is disjunction of literals (atomic formulas or their negation)
\item from any model of these clauses we can obtain model for the original formula
(just ignore interpretation of Skolem constants $g_1$, $c_0$)
\end{itemize}

\pause
Do given universally quantified formulas have a model?
\end{frame}

\begin{frame}{Remark on Notation}

  We can view $n$ ary relation on $D$ either as a function
  \[
      r_f : D^n \to \{ 0, 1 \}
  \]
  which is how we defined it, so far, or, more conventionally, as the subets
  \[
      r \subseteq D^n
  \]
  through isomorphism such that
  \[
      (d_1,\ldots,d_n) \in r \ \ \iff \ \ r_f(d_1,\ldots,d_n) = 1
  \]
  In the following slides we will use the view $r \subseteq D^n$
\end{frame}

\begin{frame}{Finding a Smaller Model}

\textbf{Small model theorems} in logic:
``if a given set of formulas has a model, then it has a model of a particular kind (e.g. small)''
\begin{itemize}
\item First place to look for smaller models: \textbf{substructures}
\end{itemize}
Given a structure (interpretation) $(D,α)$ a substructure is $(D',α')$ where
\begin{itemize}
\item $D' ⊆ D$
\item for elements in $D'$, $α'$ defines the relations and functions in the same way, so 
$α'(R) = α(R) ∩ (D')^n$ for $n=ar(R)$, and $α'(f)(x_1,...,x_n) = α(f)(x_1,...,x_n)$ for $n=ar(f)$
\item $(D',α')$ is a valid interpretation, in particular, it maps function symbols of arity $n$ to total 
functions on $(D')^n \to D'$
\end{itemize}
\textbf{Observation:}
Given $(D,α)$, a substructure is uniquely given by its domain $D' ⊆ D$. The domain $D'$ defines
a substructure if and only if it is closed under the interpretation of all function symbols $f$:
\[
    ⋀_{f ∈ {\cal L}_F}  ∀ x_1,...,x_n ∈ D'.\ α(f)(x_1,...,x_n) ∈ D'
\]

\end{frame}

\begin{frame}{Examples of Substructures}

${\cal L} = \{ f, a, b, T \}$ where
\begin{itemize}
\item $f,a,b$ are functions symbols of arity $2, 0, 0$, respectively; ${\cal L}_F = \{ f,a,b\}$
\item $T$ is a binary relation symbol
\end{itemize}
$(D,α)$ is given by $D = ℝ$ (real numbers) and
\begin{itemize}
\item $α(a) = 0$, $α(b)=1$
\item $α(f)(x,y) = x+y$
\item $α(T) = \{ (x,y) | x ≤ y \}$ 
\end{itemize}
How do substructures look like?
\begin{itemize}
\item \pause The set $D'_1 = \{ 1, 2, \ldots \}$ is not a substructure because
$α(a) ∉ D'$.
\item \pause Then the set $D'_2 = \{ 0, 1, 2 \}$ does not form a substructure because it is not closed
under addition, e.g. $1 + 2 ∉ D'_2$.
\item \pause The set of integers $D'_3 = ℤ$ induces a substructure because: \\
(i) $α(a) ∈ ℤ$, (ii) $α(b) ∈ ℤ$, and (iii) $x,y ∈ ℤ \rightarrow x+y ∈ ℤ$.
\end{itemize}
\end{frame}

\begin{frame}{Universal Formulas Stay True in Substructures}

Consider a \textbf{universal} formula, with only universal quantifiers (e.g. after Skolemization)
\[
   ∀ x_1,...,x_n.\ G(x_1,...,x_n)
\]
where $G$ is quantifier free. Suppose this formula is true in $(D,α)$. This means
\[
   ∀ e_1,...,e_n ∈ \alert{D}.\ \tr{G(x_1,...,x_n)}^{α[x_i:=e_i]_{i=1}^n}
\]
Let $(D',α)$ be a substructure of $(D,α)$. Then from $D' ⊆ D$ follows also
\[
   ∀ e_1,...,e_n ∈ \alert{D'}.\ \tr{G(x_1,...,x_n)}^{\alert{α'}[x_i:=e_i]_{i=1}^n}
\]
so the formula remains true in substructure.

\pause
\begin{theorem}
If a set of universal first-order formulas is true in a structure, then it is true in each of its substructures.
\end{theorem}

\pause Our goal: find a small substructure
\end{frame}

\begin{frame}{Smallest Substructure}

$(D,α)$ is given by $D = ℝ$ (real numbers) and
\begin{itemize}
\item $α(a) = 0$, $α(b)=1$
\item $α(f)(x,y) = x+y$
\item $α(T) = \{ (x,y) | x ≤ y \}$ 
\end{itemize}
Let $D'$ be a substructure. Which elements must it contain?
\begin{itemize}
\item \pause $0$, $1$ (interpretations of constants)
\item \pause $0+1$, $1+0$, $1+1$ (adding up constants), so $2 ∈ D'$
\item \pause $2+1 = 3 ∈ D'$
\item \pause every non-negative integer
\end{itemize}
\pause Define: $D_0 = ∅$,
$D_{i+1} = \{ 0, 1 \} ∪ \{ x + y | x,y ∈ D_i \}$ i.e.
\pause
$D_{i+1} = \{ α(a), α(b) \} ∪ \{ α(f)(x,y) | x,y ∈ D_i \}$.
\pause
Let $D^* = ⋃\limits_{i ≥ 0}  D_i$

\pause Least fixpoint of function $H(D_k) = \{ α(a), α(b) \} ∪ \{ α(f)(x,y) | x,y ∈ D_k \}$
\pause Evey set $D_i$ is finite. $D^*$ is countable: can enumerate elements of $D_1$,
followed by the elements of $D_2$, $D_3$,... establishing bijection with $ℕ$
\end{frame}

\begin{frame}{Definition of Smallest Substructure}

Language $\cal L$ with function symbols ${\cal L}_F ⊆ {\cal L}$.

\[
   D_0 = ∅
\]
\[
   D_{i+1} = ⋃_{f ∈ {\cal L}_F} \{ α(f)(x_1,...,x_n) | x_1,...,x_n ∈ D_i \}
\]
\[
   D^* = ⋃_{i ≥ 0} D_i
\]
Note: $D_i$ for $i ≥ 1$ includes the interpretations of all constants, which are
functions of arity $n=0$

\begin{theorem}
\begin{itemize}
\item $D^*$ is the domain of the smallest substructure of $(D,α)$
\item $D^*$ is 
\begin{itemize}
\item always countable
\item non-empty $\leftrightarrow$ ${\cal L}$ contains at least one constant symbol
\item finite when ${\cal L}$ has no function symbols except for constants
\end{itemize}
\end{itemize}
\end{theorem}

\end{frame}

\begin{frame}{Countable Model Theorem}

\begin{lemma}
A set of \textbf{universal} first-order formulas has a model if and only if it has
a countable model.
\end{lemma}
\begin{proof}
Let $(D,α)$ be a model. Then $D^*$ induces a countable sub-structure.
Because all formulas are universal, they remain true in $D^*$.
\end{proof}

\begin{theorem}[Downward L\"owenheim-Skolem]
A set of first-order formulas has a model if and only if it has
a countable model.
\end{theorem}
\begin{proof}
Let the set of formulas have a model. Transform the formulas into normal form
and skolemize them to eliminate existential quantifiers, which introduces a countable
number of skolem functions. Then there is a model for the
resulting set of universal formulas as well. By previous lemma, then there is also
a countable model. Ignoring the interpretation of Skolem constants, we obtain a countable 
model for the original formula.
\end{proof}
\end{frame}

\begin{frame}{Example: Dense Orders}

Consider these axioms, which define \textsl{dense linear orders} without upper bound:
\[\begin{array}{l}
 ∀ x. ¬ T(x, x) \\
 ∀ x ∀ y ∀ z. T(x,y) ∧ T(y,z) \rightarrow T(x,z) \\
 ∀ x ∀ y. (T(x,y) \rightarrow ∃ z. (T(x,z) ∧ T(z,y))) \\
 ∀ x ∃ y. T(x,y)
\end{array}\]
Real numbers with strict inequality $<$ interpreting relation symbol $T$
are a model of these axioms. Find one countable non-empty model using our construction.

\pause
Skolemizing the existential quantifier for density using $g(x,y)$ and for no-bound with $h(x)$:
\[\begin{array}{l}
¬ T(x, x) \\
¬ T(x,y) ∨ ¬ T(y,z) ∨ T(x,z) \\
¬ T(x,y) ∨ (T(x,g(x,y)) ∧ T(g(x,y),y)) \\
T(x,h(x))
\end{array}\]
\end{frame}

\begin{frame}{Finding Non-Empty Countable Model}
\[\begin{array}{l}
¬ T(x, x) \\
¬ T(x,y) ∨ ¬ T(y,z) ∨ T(x,z) \\
¬ T(x,y) ∨ (T(x,g(x,y)) ∧ T(g(x,y),y)) \\
T(x,h(x))
\end{array}\]
Theorem ensures we can find interpretation of $g,h$. 

One possibility: \pause $g(x,y) = (x+y)/2$ \ \ $h(y) = y + 1$

Since we have no constant and do not wish to have an empty domain, just pick any element
as the starting point. \pause Say, 0.

Apply closure under operations. Here they are all Skolem operations, but in general we use
all operations we have, original or Skolem. Describe the set generated in this way.

\pause Answer: The set of all non-negative numbers 
representable in binary notation $\overline{b_1...b_p \mathbf{.} d_1 ... d_q}$, that is:
\[
    \left\{ \frac{p}{2^k} \mid p,k ∈ ℕ \right\}
\]
Note that this is a countable set. \pause Try also $g(x,y)= x + 1/(1+y-x)$
\end{frame}

\newcommand{\GT}{GT_{\cal L}}

\begin{frame}{Herbrand (Term) Model: A Generic Countable Model}

Instead of looking at arbitrary countable domains and functions on them, we show we can
consider a more special class of structures: \textit{ground term models}.

In these models the domain the set of expressions (group terms) built from constants
and function symbols, and operations as just constructors.

Remember $(D,α)$ is given by $D = ℝ$ (real numbers) and
\begin{itemize}
\item $α(a) = 0$, $α(b)=1$
\item $α(f)(x,y) = x+y$
\item $α(T) = \{ (x,y) | x ≤ y \}$ 
\end{itemize}
The smallest substructure is given by $D_0 = ∅$,
$D_{i+1} = \{ 0, 1 \} ∪ \{ x + y | x,y ∈ D_i \}$, $D^* = ⋃\limits_{i ≥ 0}  D_i$.

This is precisely the set of values of all expressions built from $0,1$ and $+$.

In general, the least substructure is the set of values of ground terms:
\[
   D^* = \{ \tr{t}^{\alpha}  \mid t \in \GT \}
\]
$\GT$ is the set of all ground terms (terms without variables) in language ${\cal L}$
\end{frame}

\begin{frame}{Values of Ground Terms Induce Smallest Substructure}

$\GT$ is the least set such that if $f ∈ {\cal L}$, $ar(f)=n$ ($n ≥ 0$) and
$t_1,...,t_n ∈ \GT$ then $f(t_1,...,t_n) ∈ \GT$. 

In other words, define $GT^0 = ∅$ and 
\[
   GT^{i+1} = \{ f(t_1,...,t_n) \mid f ∈ {\cal L} ∧ t_1,...,t_n ∈ GT^i \}
\]
Then the set of all ground terms is $⋃_{i ≥ 0} GT^i$ 
\begin{itemize}
\item $GT^i$ is the set of terms of height (depth) at most $i-1$
\end{itemize}

Compare to: $D_0 = ∅$, $D_{i+1} = ⋃_{f ∈ {\cal L}_F} \{ α(f)(x_1,...,x_n) | x_1,...,x_n ∈ D_i \}$

\pause
By induction we prove easily 
\[
   D_i = \{ \tr{t}^α \mid t ∈ GT^i \}
\]
Therefore, $D^* = \{ \tr{t}^α \mid t ∈ \GT \}$

\pause How to define meaning of $f ∈ {\cal L}$ as function $GT_{\cal L}^n → GT_{\cal L}$
\end{frame}

\begin{frame}{Interpreting Functions on Ground Terms}

Given a language ${\cal L}$ we are defining an interpretation $(\GT,α_H)$.
If there are no constants, invent a fresh constant $a_0$ and add it into ${\cal L}$.

For function symbols $f$, we just let
\[
   α_H(f)(t_1,...,t_n) = f(t_1,...,t_n)
\]
because we can always build a larger term.

This definition does not depend on the original model $(D,α)$.

\ \\

We next want to define $α_H(R)$ for each relation symbols $R ∈ {\cal L}$ 

Idea: define the truth value following the truth value in $(D,α)$
\[
   α_H(R) = \{ (t_1,...,t_n) \mid (\tr{t_1}^α,...,\tr{t_n}^α) ∈ α(R) \}
\]
To determine if relation holds on ground terms, just check if it holds
on their values.

It is in this step that we used the original structure $(D,α)$ to define
the new structure $(\GT,α_H)$. We postponed evaluation to relations.
\end{frame}

\begin{frame}{Revisiting Example of Dense Orders}

\[\begin{array}{l}
¬ T(x, x) \\
¬ T(x,y) ∨ ¬ T(y,z) ∨ T(x,z) \\
¬ T(x,y) ∨ (T(x,g(x,y)) ∧ T(g(x,y),y)) \\
T(x,h(x))
\end{array}\]
Use the model $(ℝ,α)$ in which $T$ is $<$, $g(x,y) = (x+y)/2$, $h(y) = y + 1$
to define Herbrand model $(\GT,α_H)$. Add fresh constant $c$.

Define 
\begin{itemize}
\item $α_H(c)$
\item $α_H(g)$
\item $α_H(h)$
\item $α_H(T)$
\end{itemize}

\end{frame}

\begin{frame}{Example: why a formula holds in the ground model}

Now use this definition of $α_H(T)$.

Take any formula, say 
\[
  ¬ T(x,y) ∨ (T(x,g(x,y)) ∧ T(g(x,y),y))
\]
We wonder if it holds in $(\GT,α_H)$.
 Let $x,y,z \in \GT$.
Say $x=c$, $y = h(c)$. Why does
\[
   ¬ T(c,h(c)) ∨ (T(c,g(c,h(c))) ∧ T(g(c,h(c)),h(c)))
\]
hold?

\pause Because the same formula holds in the original structure. We defined
$\tr{T}^{α_H}$ so that
\[
   (c,h(c)) ∈ \tr{T}^{α_H} \ \ \leftrightarrow \ \ (\tr{c}^α,\tr{h(c)}^α) ∈ \tr{T}^α
\]
\end{frame}


\begin{frame}{Herbrand Model is a Model of Same Universal Formulas}

\begin{lemma}
%Given $(D,α)$ and the corresponding $(\GT,α_H)$, for every term $t(x_1,...,x_n)$,
%\[
%   \tr{t(x_1,...,x_n)}^{α_H} = t(α_H(x_1),...,α_H(x_n))
%\]
For every quantifier-free formula $G(x_1,...,x_n)$, if $α_H(x_i)=t_i$ then
\[
   \tr{G(x_1,...,x_n)}^{α_H} \leftrightarrow 
   \tr{G(x_1,...,x_n)}^{α[x_i:=α(t_i)]_{i=1}^n} 
\]
\end{lemma}
Proof by induction, using the definition of $α_H(R)$ in the base cases.

\begin{theorem}[Herbrand]
Let $(D,α)$ be a model of a set $S$ of universal first-order formulas in the language ${\cal L}$
containing at least one constant.
Then $(\GT,α_H)$ is also a model of these formulas.
\end{theorem}
Proof. Let $F ∈ S$ be of the form $∀ x_1,...,x_n. G(x_1,...,x_n)$. Then $F$ holds in $(D,α)$.
Let $t_1,...,t_n ∈ \GT$ be arbitrary. Then by the above lemma,
\[
   \tr{G(x_1,...,x_n)}^{α_H[x_i:=t_i]_{i=1}^n} \leftrightarrow \tr{G(x_1,...,x_n)}^{α[x_i:=α(t_i)]}
\]
Last formula is true because $F$ holds in $(D,α)$. So, $F$ holds in $(\GT,α_H)$.
\end{frame}

\newcommand{\HA}{HA}

\begin{frame}{Viewing Herbrand Model as Propositional Model}

Set $S$ of universal formulas. Suppose we write universal
variables as free variables.
There is a model $(D,α)$ if and only if there is Herbrand model $(\GT,α_H)$.

How do we check if a set $S$ has some Herbrand model? 
Function symbol interpretations
are fixed. Need to check if there exists interpretation of each relation symbol $R$ 
such that 
\[
   ∀ G ∈ S. ∀ t_1,...,t_n ∈ \GT. \ \tr{G[x_1:=t_1,...,x_n:=t_n]}^{α_H}=true
\]
Expand all these universal quantifiers:
\[
   S' = \{ G[x_1:=t_1,...,x_n:=t_n] \mid G ∈ S \}
\]
Then $S$ holds in $\GT$ if and only if  $S'$ holds in $\GT$.
We have countable domain $\GT$ and allow countable sets, so we instantiated.

$S'$ has no variables, so it is like a propositional model.
\end{frame}

\begin{frame}{Propositions with Long Names}

For each relation symbol $R$ define Herbrand atoms (ground instances):
\[
    \HA = \{ R(t_1,...,t_n) \mid ar(R)=n, t_1,...,t_n ∈ \GT \}
\]
Then $S'$ is a set of propositional formulas over the countable set $\HA$.

Moreover, $S'$ has a model if and only if each finite subset of $S'$ has a model
(compactness).

A finite subset has a model if and only if propositional resolution does not
derive empty clause.

Propositional resolution derives an empty clause iff rules with ground
instantiation and resolution derive an empty clause.

\ \\

\textbf{Theorem. A set of FOL formulas is unsatisfiable if and only if it is possible to derive empty clause from it using resolution with instantiation.}

\

We can also show: ground instantiation with resolution on ground clauses derives an empty
clause if and only iff resolution with unification does (which works better).

\end{frame}



% ============================= Playing with E

\begin{frame}{A Resolution-Based Prover: \textbf{E} by Stephan Schulz}

The principles behind Skolemization, transformation to clauses lead to automated theorem provers
(ATPs).

\

Example: E prover. Try E by downloading and building it from:

 \url{https://github.com/eprover/eprover}

\

To try an example file example.p, use e.g.

\begin{center}
\tt eprover --auto --proof-object example.p
\end{center}

\

Theorem proving problems, links to competition, other provers:
\begin{itemize}
\item \url{http://www.tptp.org}
\end{itemize}

\end{frame}

\begin{frame}{Let us Give Our Example to E}

Our example in math:
\[
\begin{array}{rl}
  ¬ \big( & (∀ x. ∃ y.\ R(x,y))\ ∧ \\
          & (∀ x. ∀ y.\ (R(x,y) \rightarrow ∀ z.\ R(x,f(y,z))))\ ∧ \\
          & (∀ x.\ (P(x) ∨ P(f(x,a))))\ \\
          & \rightarrow ∀ x. ∃ y.\ (R(x,y) ∧ P(y)) \big)
\end{array}
\]
Our example in TPTP ASCII format:

\lstinputlisting[language=tptp]{example.p}


\[\begin{array}{c|c|c|c|c|c|c}
   ∧ & ∨ & ¬ & \rightarrow & \leftrightarrow & ∀ & ∃ \\ \hline
  \texttt{\&} & \texttt{|} & \sim & \texttt{=>} & \texttt{<=>} & \texttt{!} & \texttt{?} 
\end{array}
\]
\end{frame}

\end{document}
