R4

chapter ‹R4: Sintaxis y semántica de la Lógica de primer orden›

theory R4
imports Main 
begin

text ‹------------------------------------------------------------------ 
  Ejercicio 1.
(a) Formalizar el siguiente argumento (ejercicio 5 de LPO de APPLI2),
  verificando la corrección de la solución:

  * Todo aquel que entre en el país y no sea un VIP será cacheado por un
    aduanero.
  * Hay un contrabandista que entra en el país y que solo podrá ser 
    cacheado por contrabandistas.
  * Ningún contrabandista es un VIP.
  * Por lo tanto, algún aduanero es contrabandista.

(b) Escribir la formalización en Isabelle, probando la corrección del
  razonamiento de forma automática o bien obteniendo un contraejemplo.
  ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------ 
  Ejercicio 2.
(a) Formalizar el siguiente argumento  (ejercicio 15 de LPO de APPLI2),
  verificando la corrección de la solución:

  * Todos los robots obedecen a los amigos del programador jefe.
  * Alvaro es amigo del programador jefe.
  * Benito no obedece a Alvaro.
  * Benito no es un robot.

(b) Escribir la formalización en Isabelle, probando la corrección del
  razonamiento de forma automática o bien obteniendo un contraejemplo.
  Para ello, representar la constante Benito mediante el número natural
  1, y la constante Álvaro mediante 2.
  ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------ 
  Ejercicio 3.
(a) Formalizar el siguiente argumento (ejercicio 16 de LPO de APPLI2),
   verificando la corrección de la solución:

  * Hay algún pez x que para cualquier pez y, si el pez x no se come al 
    pez y entonces existe un pez z tal que z es un tiburón o bien z 
    protege al pez y.
  * No hay ningún pez que se coma a todos los demás.
  * Ningún pez protege a ningún otro.
  * Por lo tanto, existe algún tiburón en la pecera.

(b) Escribir la formalización en Isabelle, probando la corrección del
  razonamiento de forma automática o bien obteniendo un contraejemplo.
  ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------ 
  Ejercicio 4.
(a) Formalizar el siguiente argumento (ejercicio 21 de LPO de APPLI2),
  verificando la corrección de la solución:

  * Carlos afeita a todos los habitantes de Las Chinas que no se afeitan 
    a sí mismo y sólo a ellos.  
  * Carlos es un habitante de las Chinas.
  * Por lo tanto, Carlos no afeita a nadie.

(b) Escribir la formalización en Isabelle, probando la corrección del
  razonamiento de forma automática o bien obteniendo un contraejemplo.
 Para ello, representar la constante Carlos mediante el número natural
 1.
  ---------------------------------------------------------------------›


text ‹------------------------------------------------------------------ 
Ejercicio 5.
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. 
Dar un ejemplo de una interpretación en la que F sea verdadera. Y un 
ejemplo de una interpretación en la que F sea falsa.
  ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------ 
Ejercicio 6.
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de 
aridad 1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. 
Sea I = ( U, I ) la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha 
estructura? 
  * P (x) → ∃y Q (y,x) 
  * ∀x Q (f(x),x)
  * Q(f(x),x) → Q(x,x)
  * Q(x,y) → P(x)
  ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------ 
Ejercicio 7.
En el lenguaje con igualdad L = {a, f} , siendo f un símbolo de  función 
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
  * F₁ : = ∀ x [ f(x) ≠ a ] 
  * F₂ : = ∀ x ∀ y [ f(x) = f(y) → x = y ] 
  * F₃ : = ∀ x [ x ≠ a → ∃ y [ f(y) = x ]]

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos 
restantes.
  ---------------------------------------------------------------------›

text ‹------------------------------------------------------------------ 
  Ejercicio 8.
  Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. 
  Generalizarlo a un n cualquiera.
  ---------------------------------------------------------------------›

end