\chapter{First-order logic}


\section{Syntax}
\marginnote{Syntax}
The symbols of propositional logic are:
\begin{descriptionlist}
    \item[Constants]
        Known elements of the domain. Do not represent truth values.
        
    \item[Variables]
        Unknown elements of the domain. Do not represent truth values.
    
    \item[Function symbols] 
        Function $f^{(n)}$ applied on $n$ elements of the domain to obtain another element of the domain.

    \item[Predicate symbols]
        Function $P^{(n)}$ applied on $n$ elements of the domain to obtain a truth value.

    \item[Connectives] $\forall$ $\exists$ $\land$ $\vee$ $\Rightarrow$ $\lnot$ $\Leftrightarrow$ $\top$ $\bot$ $($ $)$
\end{descriptionlist}

Using the basic syntax, the following constructs can be defined:
\begin{descriptionlist}
    \item[Term] Denotes elements of the domain.
        \[ t := \texttt{constant} \,|\, \texttt{variable} \,|\, f^{(n)}(t_1, \dots, t_n) \]

    \item[Proposition] Denotes truth values.
        \[
            P := \top \,|\, \bot \,|\, P \land P \,|\, P \vee P \,|\,  P \Rightarrow P \,|\, P \Leftrightarrow P \,|\, 
                \lnot P \,|\, \forall x. P \,|\, \exists x. P \,|\, (P) \,|\, P^{(n)}(t_1, \dots, t_n) 
        \]
\end{descriptionlist}


\begin{description}
    \item[Well-formed formula] \marginnote{Well-formed formula}
        The definition of well-formed formula in first-order logic extends the one of
        propositional logic by adding the following conditions:
        \begin{itemize}
            \item If S is well-formed, $\exists X. S$ is well-formed. Where $X$ is a variable.
            \item If S is well-formed, $\forall X. S$ is well-formed. Where $X$ is a variable.
        \end{itemize}

    \item[Free variables] \marginnote{Free variables}
        The universal and existential quantifiers bind their variable within the scope of the formula.
        Let $\mathcal{F}_v(F)$ be the set of free variables in a formula $F$, $\mathcal{F}_v$ is defined as follows:
        \begin{itemize}
            \item $\mathcal{F}_v(p(t)) = \bigcup \{ \text{variables of $t$} \}$
            \item $\mathcal{F}_v(\top) = \mathcal{F}_v(\bot) = \varnothing$
            \item $\mathcal{F}_v(\lnot F) = \mathcal{F}_v(F)$
            \item $\mathcal{F}_v(F_1 \land F_2) = \mathcal{F}_v(F_1 \vee  F_2) = \mathcal{F}_v(F_1 \Rightarrow F_2) = \mathcal{F}_v(F_1) \cup \mathcal{F}_v(F_2)$
            \item $\mathcal{F}_v(\forall X.F) = \mathcal{F}_v(\exists X.F) = \mathcal{F}_v(F) \smallsetminus \{ X \}$
        \end{itemize}

        \begin{description}
            \item[Closed formula/Sentence] \marginnote{Sentence}
                Proposition without free variables.
            
            \item[Theory] \marginnote{Theory}
                Set of sentences.

            \item[Ground term/Ground formula] \marginnote{Ground term/Ground formula}
                Proposition without variables.
        \end{description}
\end{description}



\section{Semantics}

\begin{description}
    \item[Interpretation] \marginnote{Interpretation}
        An interpretation in first-order logic $\mathcal{I}$ is a pair $(D, I)$:
        \begin{itemize}
            \item $D$ is the domain of the terms.
            \item $I$ is the interpretation function such that:
            \begin{itemize}
                \item The interpretation of an n-ary function symbol is a function $I(f): D^n \rightarrow D$.
                \item The interpretation of an n-ary predicate symbol is a relation $I(p) \subseteq D^n$.
            \end{itemize}
        \end{itemize}

    \item[Variable evaluation] \marginnote{Variable evaluation}
        Given an interpretation $\mathcal{I} = (D, I)$ and a set of variables $\mathcal{V}$,
        a variable is evaluated through $\eta: \mathcal{V} \rightarrow D$.

    \item[Model] \marginnote{Model}
        Given an interpretation $\mathcal{I}$ and a formula $F$,
        $\mathcal{I}$ models $F$ ($\mathcal{I} \models F$) 
        when $\mathcal{I}, \eta \models F$ for every variable evaluation $\eta$.

        A sentence $S$ is:
        \begin{descriptionlist}
            \item[Valid] $S$ is satisfied by every interpretation ($\forall \mathcal{I}: \mathcal{I} \models S$).
            \item[Satisfiable] $S$ is satisfied by some interpretations ($\exists \mathcal{I}: \mathcal{I} \models S$).
            \item[Falsifiable] $S$ is not satisfied by some interpretations ($\exists \mathcal{I}: \mathcal{I} \cancel{\models} S$).
            \item[Unsatisfiable] $S$ is not satisfied by any interpretation ($\forall \mathcal{I}: \mathcal{I} \cancel{\models} S$).
        \end{descriptionlist}

    \item[Logical consequence] \marginnote{Logical consequence}
        A sentence $T_1$ is a logical consequence of $T_2$ ($T_2 \models T_1$) if
        every model of $T_2$ is also model of $T_1$:
        \[ \mathcal{I} \models T_2 \Rightarrow \mathcal{I} \models T_1 \]

        \begin{theorem}
            Determining if a first-order logic formula is a tautology is undecidable.
        \end{theorem}

    \item[Equivalence] \marginnote{Equivalence}
        A sentence $T_1$ is equivalent to $T_2$ iff $T_1 \models T_2$ and $T_2 \models T_1$.
\end{description}

\begin{theorem}
    The following statements are equivalent:
    \begin{enumerate}
        \item $F_1, \dots, F_n \models G$.
        \item $F_1 \land \dots \land F_n \Rightarrow G$ is valid (i.e. deduction).
        \item $F_1 \land \dots \land F_n \land \lnot G$ is unsatisfiable (i.e. refutation).
    \end{enumerate}
\end{theorem}


\section{Substitution}

\begin{description}
    \item[Substitution] \marginnote{Substitution}
        A substitution $\sigma: \mathcal{V} \Rightarrow \mathcal{T}$ is a mapping from variables to terms.
        It is written as $\{ X_1 \mapsto t_1, \dots, X_n \mapsto t_n \}$.

        The application of a substitution is the following:
        \begin{itemize}
            \item $p(t_1, \dots, t_n)\sigma = p(t_1\sigma, \dots, t_n\sigma)$
            \item $f(t_1, \dots, t_n)\sigma = fp(t_1\sigma, \dots, t_n\sigma)$
            \item $\bot\sigma = \bot$ and $\top\sigma = \top$
            \item $(\lnot F)\sigma = (\lnot F\sigma)$
            \item $(F_1 \star F_2)\sigma = (F_1\sigma \star F_2\sigma)$ for $\star \in \{ \land, \vee, \Rightarrow \}$
            \item $(\forall X.F)\sigma = \forall X' (F \sigma[X \mapsto X'])$ where $X'$ is a fresh variable (i.e. it does not appear in $F$).
            \item $(\exists X.F)\sigma = \exists X' (F \sigma[X \mapsto X'])$ where $X'$ is a fresh variable.
        \end{itemize}

    \item[Unifier] \marginnote{Unifier}
        A substitution $\sigma$ is a unifier for $e_1, \dots, e_n$ if $e_1\sigma = \dots = e_n\sigma$.
        
        \begin{description}
            \item[Most general unifier] \marginnote{Most general unifier}
                A unifier $\sigma$ is the most general unifier (MGU) for $\bar{e} = e_1, \dots, e_n$ if
                every unifier $\tau$ for $\bar{e}$ is an instance of $\sigma$ ($\tau$ = $\sigma\rho$ for some substitution $\rho$).
                In other words, $\sigma$ is the smallest substitution to unify $\bar{e}$.
        \end{description} 
\end{description}