notas-lc/logica_predicados.tex

\documentclass[10pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage[spanish]{babel}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{multicol}
\usepackage{hyperref}
\usepackage{graphicx}
\usepackage{listings}
\usepackage{xcolor}
\usepackage{caption}
\renewcommand{\rmdefault}{ptm}
\usepackage{pgf}
\usepackage{tikz}
\usetikzlibrary{automata,positioning,arrows}
%\tikzset{->,  % makes the edges directed
%			>=stealth’, % makes the arrow heads bold
%			node distance=3cm, % specifies the minimum distance between two nodes. Change if necessary.
%			every state/.style={thick, fill=gray!10}, % sets the properties for each ’state’ node
%			initial text=$ $ % sets the text that appears on the start arrow
%			}
%\usetikzlibrary{arrows,automata}
%\usepackage[all,cmtip]{xy}
%\usepackage{graphicx}
\author{Lógica computacional}
\title{Lógica de predicados (de primer órden)}
\begin{document}
\maketitle

Al tratar con objetos matemáticos, como seguramente ya lo han hecho en los semestres que llevan de la carrera, por lo regular se buscan relaciones generales de todos los objetos de un conjunto, o reconocer un elemento muy particular que sólo tiene ese sentido de particularidad cuando se piensa en todos los demás.

En la lógica de proposiciones sólo se hablaba de los átomos, las proposiciones, y las posibles operaciones sobre ellos, pero nada se hablaba de la relación entre átomos. Eso nos ahorra tener que dar enunciados lógicos para cada elemento de un conjunto y poder hablar de una generalidad, o de una singularidad que se diferencia de una generalidad.

De nueva cuenta definimos este lenguaje de manera recursiva, pero antes de ponerlo formalmente hay que listar lo que necesitamos (para ir a la tienda matemática y conseguir nuestra lista del súper):

\begin{enumerate}
\item Las \emph{variables}, que trataran de la generalidad, cuando queramos referir a la singularidad usaremos \emph{constantes}, en contraposición.
\item \emph{Símbolos predicados}, los que dará las características a las variables o constantes.
\item Los \emph{cuantificadores}, que justo nos dirán si una propiedad se cumple para todas las variables, o sólo para una o alguna.
\end{enumerate}

Realmente para definir algunos de estos elementos vienen en diversas presentaciones:

\newtheorem{defi}{Definición}
\begin{defi}
  Un lenguaje de lógica de predicados consiste de los siguientes símbolos fundamentales:
  \begin{itemize}
  \item Símbolos lógicos
    \begin{itemize}
    \item \emph{Variables}: $x,y,z,...,x_0,y_0,z_0,...,x_i,y_i,z_i,...$
    \item \emph{Conectores lógicos}: $\neg, \wedge, \vee, \rightarrow, \iff$
    \item Coma y paréntesis: , ()
    \item Cuantificadores: $\exists, \forall$
    \end{itemize}
  \item Símbolos específicos
    \begin{itemize}
    \item \emph{Símbolos predicados}: $P,Q,R,...,P_0,Q_0,R_0,...,P_i,...$
    \item \emph{Símbolos de constantes}: $a,b,...,a_0,b_0,...,a_i,b_i,...$
    \item \emph{Símbolos de funciones}: $f,g,f_0,g_0,...,f_i,...$
    \end{itemize}
  \end{itemize}
\end{defi}

Los símbolos predicados tendrán una \emph{aridad} dependiendo de cuantos símbolos sean parte de su argumento. Cada cuantificador es dual al otro, es decir que puede traducirse:
\begin{itemize}
\item $(\forall x)Q(x)\iff \neg(\exists x)\neg Q(x)$
  \item $(\exists x)Q(x)\iff \neg(\forall x)\neg Q(x)$
\end{itemize}

\begin{defi}
  Un \emph{término} se define inductivamente como:
  \begin{itemize}
  \item Una \textbf{constante} es un término.
  \item una \textbf{variable} es un término.
  \item Si $f$ es una \textbf{función} de aridad-n, y $t_1,...,t_n$ son términos, $f(t_1,...,t_n)$ es un término.
  \end{itemize}
\end{defi}

\begin{defi}
  Una \textbf{fórmula atómica} o \textbf{átomo} es toda secuencia de símbolos $P(t_1,...,t_n)$ donde $P$ es un símbolo predicado de aridad-n y $t_i$ son términos, para $i=1,2,...,n$.
\end{defi}

\begin{defi}
  Una \textbf{fórmula} es definida inductivamente como:
  \begin{itemize}
  \item Todo \textbf{átomo} es una fórmula
  \item Si $\sigma_1$ y $\sigma_2$ son fórmulas, $\neg \sigma_1$, $\sigma_1\wedge \sigma_2$, $\sigma_1\vee \sigma_2$, $\sigma_1\rightarrow \sigma_2$ y $\sigma_1\iff \sigma_2$ son fórmulas también.
  \item Si $v$ es una variable y $\phi$ una fórmula entonces $((\exists v)\phi)$ y $((\forall v)\phi)$ también son fórmulas.
  \item Solo las secuencias de símbolos formadas de acuerdo a los puntos anteriores son fórmulas.
  \end{itemize}
\end{defi}

Bueno, ¿y eso para qué sirve o qué tiene que ver con programación? Pues lo prometido es deuda, veamos un poco de Haskell.

Definamos todos los posibles factores de un número natural cualquiera:

\lstinputlisting[firstline=1,lastline=3]{fact.hs}

Todos los número natural menores a un número natural dado:

\lstinputlisting[firstline=4,lastline=6]{fact.hs}

Algunos ejemplos. ¿Cómo escribirían las siguientes frases de canciones populares (de hace años)?

\begin{itemize}
\item ``Todos tienen tortita menos yo'' $\exists x.\neg T(x)$
\item ``Siempre existe un roto para un descosido'' $\forall d(\exists r.R(d,r))$
\item ``Si tienes un hondo pesar, piensa en mí'' $\exists.h P(x)$
\item ``De noche todos los gatos son pardos'' $\forall x(\exists t.Gato(x)\wedge Pardo(x,t)$
\end{itemize}

\section*{Variables libres y ligadas}

\begin{defi}
  \begin{itemize}
  \item La ocurrencia de una variable $v$ en una fórmula $\phi$ se llama \textbf{ligada} si existe una subfórmula $\psi$ de $\phi$ que contiene tal ocurrencia y empieza con $\forall v$ o $\exists v$.
    \item Una ocurrencia de una variable $v$ en una fórmula se llama \textbf{libre} si no está ligada.
  \end{itemize}
\end{defi}

La idea intuitiva (esa es una palabra poco usada en este curso) de libre o ligada es que en el primer caso podemos hacer uso de ella a nuestro antojo, en caso de ser ligada no es tan fácil pues hay constricciones que nos evitan hacer lo que nos de la gana con ella. Si un cuantificador está asociado a esa variable se darán cuenta de que hay una constricción, esa variable tiene una función por cumplir en la fórmula, y no es que podamos disponer de ella a nuestro gusto, sólo dentro de las limitaciones que nos permite el cuantificador, sea $\forall$ o $\exists$.

En general hablamos de una \textbf{variable libre} en la fórmula $\phi$ si tiene al menos una libre ocurrencia en $\phi$. Por el contrario la variable es ligada si no es libre.

Por ejemplo, si tenemos la fórmula:

\begin{equation*}
  \phi': \forall x.P(x,y)
\end{equation*}

Vemos que $y$ es una variable libre, y $x$ es una variable ligada. Pero de forma más general, si tenemos la fórmula:

\begin{align*}
  \phi':& \forall x.(\exists y.(P(x)\vee Q(x,y))\rightarrow \neg R(x)) \text{ donde podemos subdividir}\\
  & \psi': \exists y.(P(x)\vee Q(x,y))\rightarrow \neg R(x)
\end{align*}

Para la subfórmula $\psi'$, $x$ tiene una ocurrencia libre, pero en la fórmula completa $\phi'$ está ligada. Observamos que podemos hablar de libre localmente, pero no implica libre globalmente.

\begin{defi}
  Un término sin variables es llamado un término base.
\end{defi}

\begin{defi}
  Una \textbf{fórmula cerrada} es una fórmula sin variables libres.
\end{defi}

\section*{Sustituciones}

\begin{defi}
  Un conjunto de sustitución, o simplemente una sustitución, es el conjunto:
  \begin{equation*}
    \theta = \{ x_1/t_i, x_2/t_2,...,x_n/t_n \},
  \end{equation*}
  \noindent donde $x_i$ y $t_i$, $1\leq i\leq n$, son correspondientemente variables y términos tales que si $x_i=x_j$, entonces $t_i=t_j$, $i\leq j\leq n$.
  Otra forma de escribirlo es:
  \begin{equation*}
    \alpha \theta = \alpha_{x_1:=t_1, X_2:=t_2,...,x_n:=t_n}
  \end{equation*}
  \noindent donde $\alpha$ es un término (fórmula, variable, constante, predicado o la combinación posible de ellos).
\end{defi}

Para expresar la sustitución, por lo regular se tiene la expresión (átomo, término o fórmula) $\phi$ y la sustitución $\theta$. La expresión con la sustitución se escribe $\phi \theta$. La sustitución vacía se expresa como $E$, $E=\{ \}$.

\textbf{Ejemplo:} Sea la fórmula
\begin{equation*}
  \phi(x,y,z) : \exists y.R(x,y) \wedge \exists z. \neg Q(x,z),
\end{equation*}

\noindent y el término base $f(a,b)$. Aplica la sustitución $[x/f(a,b)]$ en $\phi(x,y,z)$.

\textbf{Solución:} Es un conjunto pequeño, sólo es una sustitución:

\begin{equation*}
  \phi(f(a,b),y,z) : \exists y.R(f(a,b),y) \wedge \exists z. \neg Q(f(a,b),z)
\end{equation*}

Ya sabemos que se puede sustituir. pero si definimos la sustitución como un conjunto ¿porque no operar ahora sobre sustituciones? Esa operación básica será la composición, y la composición de dos o más sustituciones es una sustitución, el neutro de esa operación es la sustitución vacía y también existe un inverso.

\begin{defi}
  Sean $\theta = \{ u_1/s_1,...,u_m/s_m \}$ y $\psi=\{ v_1/t_1,...,v_n/t_n \}$ dos sustituciones, la composición de ambas es la sustitución:

    \begin{align*}
      \theta \psi = &\{ u_1/s_1\psi,...,u_m/s_m\psi, v_1/t_1,...,v_n/t_n\}\\
      &-(\{ u_i/s_i\psi \mid u_i= s_i\psi\}\cup \{ v_i/t_i \mid v_i \in \{ u_1,...,u_m \} \}).
    \end{align*}
\end{defi}

Es decir, aplicamos la sustitución $\psi$ a $\theta$ y rellenamos con los elementos de $\psi$, pero omitimos los términos $u_i$ de $\theta$ que toman la forma $s_i\psi$, y los términos $v_i$ de $\psi$ que contiene las variables $u_j$ de $\theta$.

\textbf{Ejemplo:} Sea $\theta = \{ x/f(x),y/z \}$ (lo que sería $\{u_i/s_i\}$) y $\psi = \{ x/a, y/b, z/y \}$ (lo que sería $\{ v_i/t_i \}$) dos sustituciones. ¿Cómo sería la sustitución de ambas?

\textbf{Respuesta:}
\begin{align*}
  \theta \psi = &\{x/f(y)\psi, y/z\psi, x/a, y/b, z/y\}\\
  &- (\{ u_i/s_i\psi \mid u_i= s_i\psi\}\cup \{ v_i/t_i \mid v_i \in \{ u_1,...,u_m \} \})\\
  = &\{x/f(y)\psi, y/z\psi, x/a, y/b, z/y\} - (\{y/y\}\cup \{x/a, y/b\})\\
  = &\{ x/f(b),z/y \} 
\end{align*}

Algunas reglas para poder hacer las sustituciones que son útiles (en la ora forma de escribirlo):

\begin{itemize}
\item $x_{[x:=t]}=t$ 
\item $y_{[x:=t]}=y$ siempre que $y\neq x$
\item $c_{[x:=t]} = c$ si $c\in C$, es una constante
\item $f_m^n(t_1,...,t_n)_{[x:=t]}=f_m^n({t_1}_{[x:=t]},...,{t_n}_{[x:=t]})$
\item  $P_m^n(t_1,...,t_n)_{[x:=t]} = P_m^n({t_1}_{[x:=t]},...,{t_n}_{[x:=t]})$
\item $\neg(\alpha)_{[x:=t]}= \neg(\alpha_{[x:=t]})$
\item $(\alpha \vee \beta)_{[x:=t]} = (\alpha_{[x:=t]} \vee \beta_{[x:=t]})$
\item $(\alpha \wedge \beta)_{[x:=t]} = (\alpha_{[x:=t]} \wedge \beta_{[x:=t]})$
\item $(\alpha \implies \beta)_{[x:=t]}= (\alpha_{[x:=t]} \implies \beta_{[x:=t]})$
\item $(\alpha \iff \beta)_{[x:=t]} = (\alpha_{[x:=t]} \iff \beta_{[x:=t]})$
\item $(\forall x.\alpha)_{[x:=t]}=\forall x.\alpha$
\item $(\forall y.\alpha)_{[x:=t]} = \forall x.(\alpha)_{[x:=t]}$ si $x\notin F(\alpha)$ ni $y\notin t$.
\item $(\forall y.\alpha)_{[x:=t]} = \forall z.(\alpha_{[y:=z]})_{[x:=t]}$ si $x\in F(\alpha)$ ni $y\in t$.
\item $(\exists x.\alpha)_{[x:=t]}=\exists x.\alpha$
\item $(\exists y.\alpha)_{[x:=t]} = \exists x.(\alpha)_{[x:=t]}$ si $x\notin F(\alpha)$ ni $y\notin t$.
\item $(\exists y.\alpha)_{[x:=t]} = \exists z.(\alpha_{[y:=z]})_{[x:=t]}$ si $x\in F(\alpha)$ y $y\in t$.
\end{itemize}

Para la conjunción, disyunción, implicación y equivalencia me parece que la cuestión es clara (pero puedo equivocarme, si no les queda claro no dejen de preguntar), pero los casos de los cuantificadores pueden necesitar una revisión extra.

Si la variable a cambiar está ligada, no se cambia, como se definió en su caso, si la variable está ligada nos impide operar sobre ella de esa forma, no tenemos libertad sobre ella. Si no está ligada podemos cambiarla con toda libertad, sustituirla.

Pero el último caso para $\forall$ y $\exists$ requiere una explicación extra. Para eso veamos un ejemplo.

\textbf{Ejemplo:} Sea el término $\alpha$:

\begin{equation*}
  \forall x.(\exists y.(x+y=z))
\end{equation*}

Y la transformación $\theta=\{z/(y-1)\}$. ¿Cómo es $\alpha \theta$?

\textbf{Respuesta:} No importa, podemos hacer la sustitución ya que $z$ no es ligada ¿no? Pues no, porque en efecto $z$ no es ligada, pero será sustituida por una función de una variable ligada, de $y$. En este caso debemos hacer un cambio de variable para el término original, llamemos $\tau = \{y/w\}$ \textbf{que se aplicara sobre el cuantificador y el predicado (es un caso único en el que se puede hacer esto, por eso lo ponemos entre paréntesis)}, junto con $\theta = \{z/(y-1)\}$.

\begin{align*}
  \alpha (\tau) \theta =& (\forall x.(\exists y.(x+y=z))_{[y/w]})_{[z/(y-1)]} \\
  =& (\forall x.(\exists y.(x+y=z))_{[y/w]})_{[z/(y-1)]} \\
  =& (\forall x.(\exists w.(x+w=z)))_{[z/(y-1)]} \\
  =& (\forall x.(\exists w.(x+w=y-1)))
\end{align*}


\section*{Diferencia entre relaciones y funciones}

Imaginemos que tenemos un dominio $U$ al que pertenecen todas las variables y constantes de nuestro universo a trabajar. Las \emph{funciones} tendrán dominio en $U^n$ y codominio en $U$.Y una relación igualmente se define en $U^n$ para cada símbolo de relación n-aria.

Pongamos un ejemplo:

\begin{itemize}
\item $U=\{1,2,3,4\}$
\item $R=\{\langle 1,1 \rangle, \langle 1,2 \rangle, \langle 1,3 \rangle, \langle 1,4 \rangle, \langle 2,3 \rangle\}$
\item $f=\{ \langle 1,2 \rangle, \langle 2,3 \rangle, \langle 3,4 \rangle, \langle 4,1 \rangle \}$
\item $a=1$, $b=2$
\end{itemize}

Y tendremos las siguientes fórmulas en el cálculo de predicados:

\begin{enumerate}
\item $\forall x.R(x,f(x))$ falso
\item $\exists x.R(x,f(x))$ Cierto
\item $\forall x.R(a,x)$ Cierto
\item $\exists x.R(b,x)$ Cierto
\item $\forall x.[\exists y.R(x,y)\rightarrow R(x,3)]$ Cierto (ver tabla de verdad de $\rightarrow$)
\end{enumerate}

\section{Satisfacción: verdad y validez}

Vamos a tener una lista de sabores de helado y si están sabrosos, entonces tendremos $forall x.S(x)$. Tendremos un universo de interpretaciones $U$ y las tres funciones:
\begin{align*}
  \Psi&: Var_U C \rightarrow U \\
  \Phi&: \{f_k^n\}\rightarrow \{\phi: U^n\rightarrow U\}\\
  \Pi&: \{P_k^n\}\rightarrow \{R\subseteq U^n\}
\end{align*}

Las funciones pueden combinar más de un sabor, o incluso ponerlo en otra presentación, las relaciones se deben satisfacer.

Pero imaginemos que ahora tenemos una interpretación de cócteles de mariscos, en esa interpretación algunos valores darán verdadero en el predicado S(x), pero no lo harán así en la interpretación de sabores de helado.

¿Y las tortillas de harina? Para que no suene tan raro nos quedamos con crepas.

\begin{itemize}
\item Dada una fórmula $\sigma$ y una asignación $s$, la interpretación satisface a $\sigma$ con $s$ si
  \begin{equation}
    \sigma_U(s) = V
  \end{equation}
\item Una fórmula es satisfacible en el sistema de interpretación $U$ si existe algún valor de asignación para el cual
  \begin{equation}
    \sigma_U(s) = V
  \end{equation}
\item Una fórmula es válida (o verdadera) en $U$ si
  \begin{equation}
    \sigma_U(s) = V
  \end{equation}
  \noindent para toda asignación $s$.
\end{itemize}

\textbf{Ejemplo}: Para dar un ejemplo primero construiremos una estructura de primer orden. Definimos el lenguaje de la aritmética con $\mathbf{CS}= \{0\}$ y $\mathbf{CF}= \{S,+,*\}$. Si nos plantamos en los naturales (modelo), las costantes y símbolos funcionales se interpretan de la siguiente manera:

\begin{itemize}
\item $0$ es el $0$ en los naturales,
\item $S$ es la función sucesor, tal que $S(x)=x+1$,
\item $+$ es la suma sobre los naturales,
\item $*$ es la multiplicación sobre los naturales.
\end{itemize}

Noten que si cambiamos de modelo, si en lugar de estar en los naturales nos vamos a los racionales y a los reales, la estructura se sigue manteniendo.

Ahora si ya estamos en esa estructura y ese modelo ¿qué podemos decir de las siguientes afirmaciones?

\begin{align*}
  \forall x.(\neg(S(x)\doteq& 0))\\
  \forall x.(\forall y.((S(x)\doteq S(y))\rightarrow& (x\doteq y)))\\
  \forall x.(x+0 \doteq& x)\\
  \forall x.(\forall y.(x+S(y) \doteq& S(x+y)))\\
  \forall x.(x*0\doteq& 0)\\
  \forall x.(\forall y.(x*S(y) \doteq& x*y + x))\\
  \text{Para toda fórmula $A$ con una variable libre $x$}& \\
  (A(0)\wedge \forall x.(A(x)\rightarrow A(S(x)))) \rightarrow& \forall y.A(y)
\end{align*}

%\section*{Sustitución}
Venaos un poco las definiciones para ver si queda más claro el tema.

\begin{defi}
  Dado un lenguaje de primer orden $\mathbf{L}$, una $\mathbf{L}$-estructura (o simplemente una estructura) $\mathbf{M}$ es una pareja $\mathbf{M}= \{ M,I \}$ donde $M$ es un conjunto no vacío llamado el dominio de la estructura e $I$ es una función llamada \emph{función de interpretación} que asigna funciones y predicados en $M$ a los símbolos $\mathbf{L}$ de acuerdo a:

  \begin{itemize}
  \item Para todo símbolo función $f$ de rango $n>0$, $I(f): M^n\rightarrow M$, o $f_M$, es una función n-aria.
  \item Para toda constante $c$, $I(c)$, o $c_M$, es un elemento de $M$
    \item Para todo símbolo predicado $P$ de rango $n\geq 0$, $I(P): M^n \rightarrow BOOL$, o $P_M$,  es un predicado n-ario. En particular, los símbolos predicados de rango $0$ son interpŕetados como valores de verdad.
  \end{itemize}
\end{defi}

Esto es un tanto abstracto, pero lo que sucede es que podemos definir un lenguaje de primer orden, pero también debemos darle sentido a lo que hacemos, para eso necesitamos de una estructura en la que podamos evaluar los términos. Tal como los ejemplos de las combinaciones de sabores de helado, podemos tener el lenguaje para armarlos, pero sólo bajo la estructura de helado (que por lo regular es frío y de sabor dulce) es que tienen sentido sólo ciertas combinaciones de sabores. Ahora veamos como es que evaluamos los términos de acuerdo a este formalismo.

\begin{defi}
  Dado un lenguaje $\mathbf{L}$ de primer orden y una $\mathbf{L}$-estructura $\mathbf{M}$, una asignación es una función $s: \mathbf{V}\rightarrow M$ del conjunto de variables $\mathbf{V}$ al dominio $M$. El conjunto de todas esa funciones lo escribimos como $[\mathbf{V}\rightarrow M]$ 
\end{defi}

Asignamos un valor para eventualmente tener una respuesta de verdadero o falso, el significado de una fórmula es una función de esta asignación a los booleanos, entonces el conjunto de todas las funciones se convierte en $[[\mathbf{V}\rightarrow M]\rightarrow BOOL]$.

Para tratar de que quede más claro veamos un ejemplo.

\textbf{Ejemplo:} Sea el lenguaje de primer orden $\mathbf{L}= \{=, \leq, +,*,0,1\}$, una interpretación de este lenguaje es:

\begin{equation*}
  M = \{\mathbb{N}, =, \leq, +, * ...,0,1\},
\end{equation*}

\noindent donde $\mathbb{N}$ es el conjunto de los números naturales, ``$=$'' es la relación de igualdad en sobre el mismo conjunto, $\leq$ la relación ``mnor o igual'' sobre los naturales, y ``$+$'' y ``$+$'' son la suma y multiplicación en $\mathbb{N}$ respectivamente. 

\newtheorem{teo}{Teorema}
\begin{teo}
  Si $\phi$ y $\sigma$ son fórmulas en lógica de predicados. las siguientes fórmulas son derivadas en lógica de predicados:
  \begin{itemize}
  \item $\forall x.(\phi \rightarrow \sigma) \rightarrow \forall x.\phi \rightarrow \forall x.\sigma$
  \item $(\forall x.\phi \rightarrow \forall x.\sigma) \rightarrow \exists x.(\phi \rightarrow \sigma)$
  \item $(\exists x.\phi \rightarrow \exists x.\sigma) \rightarrow \exists x.(\phi \rightarrow \sigma)$
  \item $\exists x.(\phi \iff \sigma) \rightarrow \forall x.\phi \rightarrow \exists x.\sigma$
  \item $x.\phi \vee \forall x.\sigma \rightarrow \forall x.(\phi \vee \sigma)$
  \item $\forall x.(\phi \vee \sigma) \rightarrow \exists x.\phi \vee \forall x.\sigma$
  \item $\exists x.(\phi \vee \sigma) \iff \exists x.\phi \vee \exists x.\sigma$
  \item $\exists x.(\phi \wedge \sigma) \rightarrow \exists x.\phi \wedge \exists x.\sigma$
  \item $\forall x.(\phi \wedge \sigma) \rightarrow \forall x.\sigma \wedge \exists x.\sigma$
  \item $\forall x.(\phi \wedge \sigma) \iff \forall x.\phi \wedge \forall x.\sigma$
  \item $\exists y. (\forall x. \phi) \rightarrow \forall x.(\exists y.\phi)$
  \item $\forall x.(\forall y. \phi) \iff \forall y.(\forall x. \phi)$
  \item $\exists x.(\exists y. \phi) \iff \exists y.(\exists x. \phi)$
  \item $\forall x.\phi \iff \phi$ si no hay ninguna ocurrencia libre de $x$ en $\phi$
  \item $\exists x.\phi \iff \phi$ si no hay ninguna ocurrencia libre de $x$ en $\phi$
  \end{itemize}
\end{teo}

\section*{Indecibilidad}

\section*{Deducción natural}

La deducción natural para la lógica de predicados es una ampliación de la de la lógica de proposiciones. Si recuerdan algo de lo más relevante que se agregó fueron los cuantificadores ($\forall, \exists$), ¿cómo cambia la deducción natural con estos cuantificadores? El cambio es pequeño, y aunque parezca un tanto automático, tiene mucho que ver, de nuevo, con esa palabra algo prohibida aquí: la intuición.

Partimos de un ejemplo.
\textbf{Ejemplo:} Demuestra por deducción natural la consecuencia lógica de
\begin{equation*}
  \forall x.\phi(x) \rightarrow \exists x.\phi(x)
\end{equation*}

La intuición nos dice que si algo se cumple para toda $x$ es obvio que existe alguna $x$ para la que se cumple. Pero no debemos guiarnos sólo por la intuición (aunque es algo que nos puede ayudar y en ocasiones jugarnos en contra).

Hacemos la deducción natural como acostumbramos con los cuadros anidados:

\[
\boxed{
  \begin{aligned}
    &\forall x.\phi(x)\ \text{(Hipótesis)}\\
    &\phi(x)\ \text{ Eliminamos $\forall$ de la línea anterior}\\
    &\exists x.\phi(x)\ \text{Insertamos $\exists$ en la línea anterior}
  \end{aligned}
}
\]
$\forall x.\phi(x) \rightarrow \exists x.\phi(x)$

Como pueden ver hay unas reglas más o menos directas para introducir o eliminar los cuantificadores, para verlas en detalle podemos escribirlas como:

\begin{align*}
  &\frac{A(x)}{\forall x.A(x)}\ \text{ I $\forall$.} \hspace{3cm} \frac{\forall x.A(x)}{A(x)}\ \text{ E $\forall$}\\
  &\frac{A(x)}{\exists x.A(x)}\ \text{ I $\exists$.} \hspace{3cm} \frac{\exists x.\begin{bmatrix}
           A(x) \\
           \vdots \\
           B
         \end{bmatrix}}{B}\ \text{ E $\exists$}
\end{align*}

Tiene sentido poder introducir gratuitamente el $\forall$, si $A(x)$ es cierto es claro que lo estamos diciendo que es cierto para toda $x$. De igual manera si decimos que es cierto $A(x)$ podemos dejar un poco la generalidad y asegurar completamente que al menos existe una $x$ para a cual se cumple, es decir $\exists x.A(x)$.

Veamos algunos ejemplos más.

\textbf{Ejemplo:} Demuestra por deducción natural la consecuencia lógica
\begin{equation*}
  \forall x.A(x), \forall x.B(x) \rightarrow \forall x.(A(x)\wedge B(x))
\end{equation*}

\textbf{Deducción natural}:

\[
\boxed{
  \begin{aligned}
    &\forall x.A(x), \forall x.B(x)\ \text{ (Hip.)}\\
    &\hspace{ 3mm}\boxed{
      \begin{aligned}
        &\forall x.A(x)\ \text{ (Hip.)}\\
        & A(x)\ \text{ (E $\forall$)}\\
      \end{aligned}
    }\\
    & A(x)\\
    &\hspace{ 3mm}\boxed{
      \begin{aligned}
        &\forall x.B(x)\ \text{ (Hip.)}\\
        & B(x)\ \text{ (E $\forall$)}\\
      \end{aligned}
    }\\
    & B(x)\\
    & A(x)\wedge B(x)\ \text{ (I $\wedge$)}\\
    & \forall x.(A(x)\wedge B(x))\ \text{ (I $\forall$)}\\
    & \forall x.A(x), \forall x.B(x) \rightarrow \forall x.(A(x)\wedge B(x))\ \text{ (I $\rightarrow$)}
  \end{aligned}
}
\]

\textbf{Ejemplo:} Demuestra por deducción natural la consecuencia lógica de:

\begin{equation*}
  \exists x.(A(x)\wedge B(x))\rightarrow \exists x.A(x)
\end{equation*}

\textbf{Reaspueta:}

\[
\boxed{
  \begin{aligned}
    & \exists x.(A(x)\wedge B(x))\ \text{ (Hip.)}\\
    & A(x)\wedge B(x)\ \text{ (E $\exists$)}\\
    &\hspace{3 mm}\boxed{
      \begin{aligned}
        & A(x)\ \text{ (E $\wedge$)}\\
        & \exists x.A(x)\\
      \end{aligned}
    }\\
    &\exists x.A(x)\\
    & \exists x.(A(x)\wedge B(x)) \rightarrow \exists x.A(x)\ \text{ (I $\rightarrow$)}
  \end{aligned}
}
\]

\textbf{Ejemplo:} Demuestra por deducción natural la consecuencia lógica de:

\begin{equation*}
  \forall x.(A(x)\rightarrow \neg B(x)) \rightarrow \neg\exists x.(A(x)\wedge B(x))
\end{equation*}

\textbf{Respuesta:}

\[
\boxed{
  \begin{aligned}
    &\forall x.(A(x)\rightarrow \neg B(x))\ \text{ (Hip.)}\\
    & A(x)\rightarrow \neg B(x)\ \text{ (E $\forall$)}\\
    &\hspace{3 mm}\boxed{
      \begin{aligned}
        & \exists x.(A(x)\wedge B(x))\ \text{( Hip.)}\\
        & A(x)\wedge B(x)\ \text{ (E $\exists$)}\\
        & A(x)\ \text{E $\wedge$}\\
        & \neg B(x)\ \text{ (Hip.)}\\
        & \bot\ \text{ (Reducción al absurdo)}\\
      \end{aligned}
    }\\
    & \neg \exists x.(A(x)\wedge B(x))\\
    & \forall x.(A(x)\rightarrow \neg B(x)) \rightarrow \neg \exists x.(A(x)\wedge B(x))\ \text{ (I $\rightarrow$)}\\
  \end{aligned}
}
\]

\begin{thebibliography}{10}
  \bibitem{Metakides1996} Metakides, G. y Nerode, A. ``Principles of Logic and Logic Programming''. Elsevier, Amsterdam (1996).
  \bibitem{Reeves1990} Reeves, S. y Clarke, M. ``Logic for computer science'' Addison-Wesley Publishers Ltd. (1990) 
\end{thebibliography}

\end{document}