#LyX 2.3 created this file. For more info see http://www.lyx.org/
\lyxformat 544
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass book
\use_default_options true
\maintain_unincluded_children false
\language spanish
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "default"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts false
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\use_microtype false
\use_dash_ligatures true
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing single
\use_hyperref false
\papersize default
\use_geometry false
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification true
\use_refstyle 1
\use_minted 0
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\paragraph_indentation default
\is_math_indent 0
\math_numbering_side default
\quotes_style swiss
\dynamic_quotes 0
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Section
Relaciones
\end_layout

\begin_layout Standard
La lógica de primer orden (L1) extiende la lógica categórica permitiendo
 expresar relaciones fuera de las formas normales y relaciones de varios
 objetos.
 Podemos distinguir:
\end_layout

\begin_layout Itemize

\series bold
Categorías:
\series default
 
\begin_inset Quotes cld
\end_inset


\begin_inset Formula $x$
\end_inset

 es 
\begin_inset Formula $P$
\end_inset


\begin_inset Quotes crd
\end_inset

, 
\begin_inset Formula $x\in P$
\end_inset

, 
\begin_inset Formula $P(r)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Relaciones binarias:
\series default
 
\begin_inset Quotes cld
\end_inset


\begin_inset Formula $x$
\end_inset

 e 
\begin_inset Formula $y$
\end_inset

 son 
\begin_inset Formula $R$
\end_inset


\begin_inset Quotes crd
\end_inset

, 
\begin_inset Quotes cld
\end_inset


\begin_inset Formula $x$
\end_inset

 se relaciona con 
\begin_inset Formula $y$
\end_inset


\begin_inset Quotes crd
\end_inset

, 
\begin_inset Formula $(x,y)\in R$
\end_inset

, 
\begin_inset Formula $R(x,y)$
\end_inset

, 
\begin_inset Formula $xRy$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Relaciones
\series default
 de cualquier orden: 
\begin_inset Formula $(x_{1},\dots,x_{n})\in S$
\end_inset

, 
\begin_inset Formula $S(x_{1},\dots,x_{n})$
\end_inset

.
 Se dice que 
\begin_inset Formula $S$
\end_inset

 tiene 
\series bold
aridad
\series default
 
\begin_inset Formula $n$
\end_inset

, o que es una relación 
\series bold

\begin_inset Formula $n$
\end_inset

-aria
\series default
, lo que se representa por 
\begin_inset Formula $S/n$
\end_inset

.
 En general, 
\begin_inset Formula $Q$
\end_inset

 es una relación 
\begin_inset Formula $n$
\end_inset

-aria entre 
\begin_inset Formula $A_{1},\dots,A_{n}$
\end_inset

 si 
\begin_inset Formula $Q\subseteq\prod_{i=1}^{n}A_{i}$
\end_inset

.
 Si 
\begin_inset Formula $\forall i,A_{i}=A$
\end_inset

, entonces 
\begin_inset Formula $\prod_{i=1}^{n}A_{i}=A^{n}$
\end_inset

.
\end_layout

\begin_layout Standard
En relaciones con aridad 
\begin_inset Formula $n\geq2$
\end_inset

, se define el 
\series bold
dominio
\series default
 como 
\begin_inset Formula $\text{Dom}(R)=\{(x_{1},\dots,x_{n-1})|\exists x_{n}\mid (x_{1},\dots,x_{n})\in R\}$
\end_inset

 (si la aridad es 
\begin_inset Formula $2$
\end_inset

, entonces 
\begin_inset Formula $\text{Dom}(R)=\{x|\exists y\mid xRy\}$
\end_inset

), y el 
\series bold
rango
\series default
 como 
\begin_inset Formula $\text{Ran}(R)=\{x_{n}|\exists(x_{1},\dots,x_{n-1})\mid (x_{1},\dots,x_{n})\in R\}$
\end_inset

 (si la aridad es 
\begin_inset Formula $2$
\end_inset

, entonces 
\begin_inset Formula $\text{Ran}(R)=\{y|\exists x\mid xRy\}$
\end_inset

.
 El 
\series bold
campo
\series default
 de 
\begin_inset Formula $R$
\end_inset

 se define como 
\begin_inset Formula $\text{Campo}(R)=\text{Dom}(R)\cup\text{Ran}(R)$
\end_inset

.
 Representaciones:
\end_layout

\begin_layout Itemize

\series bold
Cartesiana:
\series default
 Similar a una función, con el conjunto inicial en el eje horizontal.
 Se marcan los puntos que están en 
\begin_inset Formula $R$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Tabular:
\series default
 Como la cartesiana pero en una tabla.
 En cada celda se pone un 
\begin_inset Formula $1$
\end_inset

 si el producto de tipos está en 
\begin_inset Formula $R$
\end_inset

, un 
\begin_inset Formula $0$
\end_inset

 si no está y se deja en blanco si no lo sabemos.
\end_layout

\begin_layout Itemize

\series bold
Mediante digrafo:
\series default
 Se representa a la izquierda el conjunto inicial y a la derecha el final,
 y las relaciones se representan con flechas entre elementos de cada.
\end_layout

\begin_layout Itemize

\series bold
Grafo dirigido:
\series default
 Se representa 
\begin_inset Formula ${\cal U}$
\end_inset

 y se indican las relaciones binarias con flechas.
\end_layout

\begin_layout Standard
Una relación 
\begin_inset Formula $n$
\end_inset

-aria 
\begin_inset Formula $f$
\end_inset

 es una 
\series bold
función
\series default
 si y sólo si para cada elemento 
\begin_inset Formula $x\in\text{Dom}(f)$
\end_inset

 existe un único 
\begin_inset Formula $y\in\text{Ran}(f)$
\end_inset

 que se relacione con él.
 Se escribe 
\begin_inset Formula $f(x)=y$
\end_inset

, y la función se representa como 
\begin_inset Formula $f:\prod_{i=1}^{n-1}A_{i}\rightarrow A_{n}$
\end_inset

.
 Es 
\series bold
inyectiva
\series default
 si 
\begin_inset Formula $f(x)=f(x')\implies x=x'$
\end_inset

, 
\series bold
suprayectiva
\series default
 si 
\begin_inset Formula $\text{Ran}(f)=A_{n}$
\end_inset

 y 
\series bold
biyectiva
\series default
 si es inyectiva y suprayectiva.
 Definimos la aridad de 
\begin_inset Formula $f$
\end_inset

 como función como 
\begin_inset Formula $n-1$
\end_inset

.
\end_layout

\begin_layout Standard
\begin_inset Note Comment
status open

\begin_layout Plain Layout
Tipos de relaciones:
\end_layout

\begin_layout Itemize

\series bold
Reflexiva:
\series default
 
\begin_inset Formula $\forall a\in A,aRa$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Irreflexiva:
\series default
 
\begin_inset Formula $\forall a\in A,a\not Ra$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Serial:
\series default
 
\begin_inset Formula $\forall a\in A,\exists b\in A:aRb$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Simétrica:
\series default
 
\begin_inset Formula $\forall a,b\in A,(aRb\implies bRa)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Asimétrica:
\series default
 
\begin_inset Formula $\forall a,b\in A,(aRb\implies b\not Ra)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Antisimétrica:
\series default
 
\begin_inset Formula $\forall a,b\in A,(aRb\land bRa\implies a=b)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Transitiva:
\series default
 
\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies aRc)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Intransitiva:
\series default
 
\begin_inset Formula $\forall a,b,c\in A,(aRb\land bRc\implies a\not Rc)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Negativamente transitiva:
\series default
 
\begin_inset Formula $\forall a,b,c\in A,(a\not Rb\land b\not Rc\implies a\not Rc)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Completa:
\series default
 
\begin_inset Formula $\forall a,b\in A,(aRb\lor bRa)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Euclídea:
\series default
 
\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies bRc)$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Incestuosa:
\series default
 
\begin_inset Formula $\forall a,b,c\in A,(aRb\land aRc\implies\exists d\in A:(bRd\land cRd))$
\end_inset

.
\end_layout

\begin_layout Plain Layout
Dada 
\begin_inset Formula $R\subseteq A\times B$
\end_inset

, su 
\series bold
relación inversa
\series default
 es 
\begin_inset Formula $R^{-1}$
\end_inset

 con 
\begin_inset Formula $xR^{-1}y:\iff yRx$
\end_inset

.
 Dada 
\begin_inset Formula $R\subseteq A\times A$
\end_inset

:
\end_layout

\begin_layout Itemize
Su 
\series bold
relación complementaria
\series default
 es 
\begin_inset Formula $R^{\complement}$
\end_inset

 con 
\begin_inset Formula $xR^{\complement}y:\iff x\not Ry$
\end_inset

.
\end_layout

\begin_layout Itemize
Su 
\series bold
relación simétrica
\series default
 es 
\begin_inset Formula $\overline{R}=R^{-1}$
\end_inset

 con 
\begin_inset Formula $x\overline{R}y:\iff yRx$
\end_inset

.
\end_layout

\begin_layout Itemize
Su 
\series bold
relación dual
\series default
 es 
\begin_inset Formula $R^{d}$
\end_inset

 con 
\begin_inset Formula $aR^{d}b:\iff b\not Ra$
\end_inset

.
\end_layout

\begin_layout Plain Layout
Una relación de equivalencia es aquella reflexiva, simétrica y transitiva.
 Sea 
\begin_inset Formula $(A,\sim)$
\end_inset

 de equivalencia, podemos definir la clase de equivalencia de 
\begin_inset Formula $x$
\end_inset

, 
\begin_inset Formula $[x]$
\end_inset

, como el conjunto de todos los elementos que se relacionan con 
\begin_inset Formula $[x]$
\end_inset

.
 
\begin_inset Formula $y\in[x]\implies[y]=[x]$
\end_inset

, y decimos que 
\begin_inset Formula $y$
\end_inset

 es un representante de la clase.
 El conjunto cociente es el formado por todas las clases de equivalencia,
 y se escribe 
\begin_inset Formula $A/\sim=\{[x]|x\in A\}$
\end_inset

.
\end_layout

\end_inset


\end_layout

\begin_layout Section
Sintaxis
\end_layout

\begin_layout Itemize

\series bold
Proposición atómica:
\series default
 
\begin_inset Formula $V$
\end_inset

, 
\begin_inset Formula $F$
\end_inset

 o un predicado.
\end_layout

\begin_layout Itemize

\series bold
Predicado:
\series default
 Secuencia de letras latinas que representa una relación, seguida de una
 serie de términos: 
\begin_inset Formula $R(t_{1},\dots,t_{n})$
\end_inset

.
\end_layout

\begin_layout Itemize

\series bold
Término:
\series default
 Constante que representa un objeto definido, variable o función.
\end_layout

\begin_layout Itemize

\series bold
Constante:
\series default
 Secuencia de letras latinas que representa a un objeto definido (salvo
 
\begin_inset Formula $V$
\end_inset

 y 
\begin_inset Formula $F$
\end_inset

).
\end_layout

\begin_layout Itemize

\series bold
Variable:
\series default
 Secuencia de letras latinas que representa a un objeto indefinido.
 Puede estar 
\series bold
ligada
\series default
 a un cuantificador, y entonces es igual al resto de variables ligadas al
 mismo, o 
\series bold
libre
\series default
, en cuyo caso puede representar cualquier cosa.
\end_layout

\begin_layout Itemize

\series bold
Función:
\series default
 Secuencia de letras latinas que representa una función, seguida de una
 serie de términos: 
\begin_inset Formula $f(t_{1},\dots,t_{n})$
\end_inset

.
\end_layout

\begin_layout Standard
La construcción de f.b.f es igual que en L0, pero cambiando la forma de las
 proposiciones atómicas y añadiendo que si 
\begin_inset Formula $\alpha$
\end_inset

 es f.b.f.
 también lo son 
\begin_inset Formula $(\forall x\alpha)$
\end_inset

 y 
\begin_inset Formula $(\exists x\alpha)$
\end_inset

.
 Una f.b.f.
 es 
\series bold
cerrada
\series default
 si todas las variables están ligadas y 
\series bold
abierta
\series default
 en otro caso.
\end_layout

\begin_layout Section
Interpretación y asignación
\end_layout

\begin_layout Standard
Una 
\series bold
interpretación
\series default
 de 
\begin_inset Formula $\alpha$
\end_inset

 en un 
\series bold
mundo
\series default
 
\begin_inset Formula $\mathbb{M}$
\end_inset

 es una cuaterna 
\begin_inset Formula ${\cal I}_{\alpha}=(\mathbb{D},{\cal C}_{\mathbb{D}},{\cal F}_{\mathbb{D}},{\cal R}_{\mathbb{D}})$
\end_inset

 donde 
\begin_inset Formula $\mathbb{D}$
\end_inset

 es un conjunto no vacío de objetos, llamado dominio, 
\begin_inset Formula ${\cal C}_{\mathbb{D}}$
\end_inset

 es un conjunto de objetos concretos (
\begin_inset Formula ${\cal C_{\alpha}\mapsto{\cal C}_{\mathbb{D}}}$
\end_inset

), 
\begin_inset Formula ${\cal F}_{\mathbb{D}}$
\end_inset

 de funciones concretas (
\begin_inset Formula $f_{\alpha}\mapsto f_{\mathbb{D}}$
\end_inset

) y 
\begin_inset Formula ${\cal R}_{\mathbb{D}}$
\end_inset

 de relaciones concretas (
\begin_inset Formula $R_{\alpha}\mapsto R_{\mathbb{D}}$
\end_inset

).
 La 
\series bold
signatura
\series default
 es el conjunto de todos los predicados y funciones, indicando su aridad.
\end_layout

\begin_layout Standard
Una asignación de variables es una función 
\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}:{\cal V}\rightarrow\mathbb{D}$
\end_inset

 que relaciona cada variable de 
\begin_inset Formula $\alpha$
\end_inset

 con un elemento del dominio, y definimos 
\begin_inset Formula $\sigma_{{\cal I}_{\alpha}|x\looparrowright d}$
\end_inset

 a la asignación definida igual que 
\begin_inset Formula $\sigma_{{\cal I}_{\alpha}}$
\end_inset

 pero asignando a 
\begin_inset Formula $x$
\end_inset

 el objeto 
\begin_inset Formula $d$
\end_inset

.
\end_layout

\begin_layout Standard
Una 
\series bold
asignación de valores de verdad
\series default
 
\begin_inset Formula $v_{\sigma_{{\cal I}_{\alpha}}}:{\cal P_{\alpha}\rightarrow\mathbb{B}}$
\end_inset

 asigna un valor de verdad a cada elemento atómico de 
\begin_inset Formula $\alpha$
\end_inset

.
 Así, 
\begin_inset Formula $v(R_{\alpha}(t_{1},\dots,t_{n}))=V\iff(d_{1},\dots,d_{n})\in R_{\mathbb{D}}$
\end_inset

, donde si 
\begin_inset Formula $t_{i}$
\end_inset

 es constante entonces 
\begin_inset Formula $d_{i}=t_{i}$
\end_inset

, si 
\begin_inset Formula $t_{i}=f(x_{1},\dots,x_{n})$
\end_inset

 entonces 
\begin_inset Formula $d_{i}$
\end_inset

 es el único 
\begin_inset Formula $y$
\end_inset

 tal que 
\begin_inset Formula $(x_{1},\dots,x_{n},y)\in f$
\end_inset

, y si es variable entonces depende de la 
\series bold
asignación
\series default
.
\end_layout

\begin_layout Standard
La 
\series bold
evaluación
\series default
 de una oración 
\begin_inset Formula $\alpha$
\end_inset

 se hace igual que en LC, pero partiendo de esta asignación de valores de
 verdad.
 También se puede hacer mediante tablas de verdad, que en L1 sólo evalúan
 una interpretación a la vez:
\end_layout

\begin_layout Enumerate
Se introduce una columna por variable, dividida en una fila por cada valor
 del dominio.
 Puede ser necesario considerar aquí todas las posibles combinaciones de
 variables.
\end_layout

\begin_layout Enumerate
Se introduce una columna por cada función que aparece en la oración, y se
 evalúa de acuerdo al valor de la variable dado.
\end_layout

\begin_layout Enumerate
Se introducen las filas correspondientes a la fórmula, indicando el orden
 de evaluación.
 Un cuantificador que no está dentro de otro ocupa la fila completa, pero
 su contenido se divide en una fila por cada posible asignación de la variable.
 Una vez se conoce el valor del cuantificador no es necesario evaluar el
 resto de asignaciones, pero es importante justificar los valores de verdad
 de los predicados (ejemplos: 
\begin_inset Formula $V:(a,b)\in P_{{\cal M}}$
\end_inset

; 
\begin_inset Formula $F:(c,a)\notin Q_{{\cal M}}$
\end_inset

).
\end_layout

\begin_layout Standard
Este método es impráctico, por lo que no se usa.
\end_layout

\begin_layout Section
Sustituciones
\end_layout

\begin_layout Standard
Una 
\series bold
sustitución
\series default
 es una expresión 
\begin_inset Formula $s=\{t_{1}/v_{1},\dots,t_{n}/v_{n}\}$
\end_inset

 que indica que toda ocurrencia de cada 
\begin_inset Formula $v_{i}$
\end_inset

 se debe sustituir por el término 
\begin_inset Formula $t_{i}$
\end_inset

.
 Todas las sustituciones se hacen simultáneamente.
\end_layout

\begin_layout Standard
Una 
\series bold
particularización por sustitución
\series default
 consiste en sustituir sus variables por términos.
 Escribimos 
\begin_inset Formula $Ps$
\end_inset

 como la particularización de la expresión 
\begin_inset Formula $P$
\end_inset

 según la sustitución 
\begin_inset Formula $s$
\end_inset

.
\end_layout

\begin_layout Itemize
En una 
\series bold
particularización básica
\series default
, los términos son constantes.
\end_layout

\begin_layout Itemize
En una 
\series bold
particularización alfabética
\series default
, los términos son otras variables.
\end_layout

\begin_layout Standard

\series bold
Composición de sustituciones:
\series default
 Dadas 
\begin_inset Formula $s=\{a_{1}/x_{1},\dots,a_{n}/x_{n}\}$
\end_inset

 y 
\begin_inset Formula $t=\{b_{1}/y_{1},\dots,b_{m}/y_{m}\}$
\end_inset

 con 
\begin_inset Formula $X$
\end_inset

 e 
\begin_inset Formula $Y$
\end_inset

 los conjuntos de variables sustituidas respectivamente según 
\begin_inset Formula $s$
\end_inset

 y 
\begin_inset Formula $t$
\end_inset

, 
\begin_inset Formula $s\cdot t=\{(a_{i}t)/x_{i}|x_{i}\neq a_{i}t\}\cup\{b_{i}/y_{i}|y_{i}\in Y\backslash X\}$
\end_inset

, donde 
\begin_inset Formula $a_{i}t$
\end_inset

 es la particularización de 
\begin_inset Formula $a_{i}$
\end_inset

 según 
\begin_inset Formula $t$
\end_inset

.
\end_layout

\begin_layout Section
Equivalencias
\end_layout

\begin_layout Standard
\align center
\begin_inset Tabular
<lyxtabular version="3" rows="2" columns="2">
<features tabularvalignment="middle">
<column alignment="center" valignment="top">
<column alignment="center" valignment="top">
<row>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\neg\exists x\alpha[x]\equiv\forall x\neg\alpha[x]$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\neg\forall x\alpha[x]\equiv\exists x\neg\alpha[x]$
\end_inset


\end_layout

\end_inset
</cell>
</row>
<row>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\forall x(\alpha[x]\land\beta[x])\equiv\forall x\alpha[x]\land\forall x\beta[x]$
\end_inset


\end_layout

\end_inset
</cell>
<cell alignment="center" valignment="top" topline="true" bottomline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\begin_layout Plain Layout
\begin_inset Formula $\exists x(\alpha[x]\lor\beta[x])\equiv\exists x\alpha[x]\lor\exists x\beta[x]$
\end_inset


\end_layout

\end_inset
</cell>
</row>
</lyxtabular>

\end_inset


\end_layout

\begin_layout Standard
También, tanto en L1 como en LC, podemos sustituir el nombre de una variable
 por otro siempre que lo cambiemos en el cuantificador al que está ligado
 y en todos los símbolos ligados al mismo cuantificador (o bien la variable
 sea libre), y al hacerlo todas las variables de la oración sigan ligadas
 al mismo cuantificador de partida (o sigan libres).
\end_layout

\begin_layout Section
Satisfacibilidad
\end_layout

\begin_layout Standard
Podemos comprobar la satisfacibilidad de una oración mediante tableaux.
 Añadimos dos tipos de reglas:
\end_layout

\begin_layout Itemize
\begin_inset Formula $\gamma$
\end_inset


\series bold
-reglas
\series default
: 
\begin_inset Formula $\forall x\alpha[x]\mapsto\alpha[C],\forall x\alpha[x]$
\end_inset

; 
\begin_inset Formula $\neg\exists x\alpha[x]\mapsto\neg\alpha[C],\neg\exists x\alpha[x]$
\end_inset

.
 La sustitución 
\begin_inset Formula $\{C/x\}$
\end_inset

 se hace sobre una constante 
\begin_inset Formula $C$
\end_inset

 existente.
 Si no existe ninguna, debemos suponer una nueva.
 El 
\begin_inset Formula $\forall x\alpha[x]$
\end_inset

 resultante no hace referencia a 
\begin_inset Formula $C$
\end_inset

, de modo que se debe escribir una lista debajo de cada expresión de este
 tipo (
\begin_inset Formula $L=\{\dots\}$
\end_inset

) con los elementos a los que sí hace referencia.
\end_layout

\begin_layout Itemize
\begin_inset Formula $\delta$
\end_inset


\series bold
-reglas
\series default
: 
\begin_inset Formula $\exists x\alpha[x]\mapsto\alpha[C]$
\end_inset

; 
\begin_inset Formula $\neg\forall x\alpha[x]\mapsto\neg\alpha[C]$
\end_inset

.
 La sustitución 
\begin_inset Formula $\{C/x\}$
\end_inset

 se hace sobre una constante 
\begin_inset Formula $C$
\end_inset

 nueva, y entonces se debe añadir a las listas de todas las expresiones
 de 
\begin_inset Formula $\gamma$
\end_inset

-reglas dicha constante.
\end_layout

\begin_layout Standard
Al aplicar estas reglas, se debe indicar, por ejemplo: 
\begin_inset Formula $\gamma:\forall x;\{C/x\};C\text{ nueva}$
\end_inset

 (la última parte se incluye siempre en las 
\begin_inset Formula $\delta$
\end_inset

-reglas).
 Las 
\begin_inset Formula $\delta$
\end_inset

-reglas se aplican después de las 
\begin_inset Formula $\beta$
\end_inset

-reglas y antes de las 
\begin_inset Formula $\gamma$
\end_inset

-reglas, y si se llega a un bucle por una rama, se razona que el tableaux
 es abierto.
\end_layout

\begin_layout Standard
Si el tableaux es cerrado (si todas las hojas están cerradas), llegamos
 a una contradicción.
 Sin embargo, si el tableaux es abierto, no sabemos que sea satisfacible
 (salvo si todos los predicados son de aridad 1 o la identidad).
 No obstante, los nodos abiertos pueden servir como ejemplos de interpretaciones
 en las que la oración es satisfacible.
\end_layout

\begin_layout Section
Grafos semánticos
\end_layout

\begin_layout Standard
Son iguales que en L0, pero en los cuantificadores, el nombre de la variable
 se incluye en el nombre del propio nodo junto con el cuantificador.
 Además, debajo de cada predicado (que se escribe completo), se puede indicar
 el f.b.f.
 de términos, que consiste en añadir un nodo hijo por cada término.
 Si el término es una función, se indica simplemente el nombre de la función
 y sus parámetros se escriben como nodos hijo.
\end_layout

\begin_layout Section
Deducción natural
\end_layout

\begin_layout Standard
Se añaden reglas de deducción natural:
\end_layout

\begin_layout Itemize
\begin_inset Formula $E_{\forall}:\frac{\vdash\forall x\alpha[x]}{\vdash\alpha[C]}$
\end_inset

.
 
\begin_inset Formula $C$
\end_inset

 es una constante cualquiera.
 Se debe indicar la sustitución 
\begin_inset Formula $\{C/x\}$
\end_inset

 y, en su caso, si 
\begin_inset Formula $C$
\end_inset

 es nueva o 
\begin_inset Quotes cld
\end_inset

arbitraria
\begin_inset Quotes crd
\end_inset

.
\end_layout

\begin_layout Itemize
\begin_inset Formula $I_{\forall}:\frac{\vdash\alpha[C]}{\vdash\forall x\alpha[x]}$
\end_inset

.
 
\begin_inset Formula $C$
\end_inset

 debe ser 
\begin_inset Quotes cld
\end_inset

arbitraria
\begin_inset Quotes crd
\end_inset

, es decir, no distinguible de cualquier otro individuo por suposiciones,
 derivaciones o premisas anteriores.
 Puede ser obtenida nueva con 
\begin_inset Formula $E_{\forall}$
\end_inset

.
\end_layout

\begin_layout Itemize
\begin_inset Formula $E_{\exists}:\frac{\vdash\exists x\alpha[x]\vdash(\alpha[C]\vdash\beta)}{\vdash\beta}$
\end_inset

.
 No se debe hacer ninguna suposición sobre 
\begin_inset Formula $C$
\end_inset

, y 
\begin_inset Formula $\beta$
\end_inset

 no puede depender de 
\begin_inset Formula $C$
\end_inset

.
\end_layout

\begin_layout Itemize
\begin_inset Formula $I_{\exists}:\frac{\vdash\alpha[C]}{\vdash\exists x\alpha[x]}$
\end_inset

.
 Se pueden cambiar todas las apariciones de 
\begin_inset Formula $C$
\end_inset

 o solo algunas.
\end_layout

\end_body
\end_document