Ejercicios_de_LPO_con_Lean.org

Ejercicios de lógica de primer orden con Lean

1 Introducción

Este libro es una colección de soluciones de ejercicios de lógica de primer orden (LPO) formalizadas con Lean que complementa el libro de Lógica con Lean y es continuación del libro Ejercicios de lógica proposicional con Lean.

Para cada uno de los ejercicios se formalizan las soluciones en distintos estilos:

• aplicativo usando tácticas con razonamiento hacia atrás,
• declarativo (o estructurado) con razonamiento hacia adelante,
• funcional con términos del tipo especificado y
• automático.

Las demostraciones funcionales se obtienen mediante una sucesión de transformaciones de una aplicativa (o declarativa) eliminando elementos no esenciales.

Además, al final de cada ejercicio se encuentra un enlace al código y otro a una sesión de Lean en la Web que contiene la solución del ejercicio.

2 Ejercicios sobre cuantificadores

2.1 ∀x, P x ⟶ Q x ⊢ (∀x, P x) ⟶ (∀x, Q x)

Enlaces al código y a la sesión en Lean Web.

2.1.1 ∃ x, ¬(P x) ⊢ ¬(∀ x, P x)

Enlaces al código y a la sesión en Lean Web.

2.2 ∀ x, P x ⊢ ∀ y, P y

Enlaces al código y a la sesión en Lean Web.

2.3 ∀ x, P x → Q x ⊢ (∀ x, ¬(Q x)) → (∀ x, ¬(P x))

Enlaces al código y a la sesión en Lean Web.

2.4 ∀ x, P x → ¬(Q x) ⊢ ¬(∃ x, P x ∧ Q x)

Enlaces al código y a la sesión en Lean Web.

2.5 ∀ x y, P x y ⊢ ∀ u v, P u v

Enlaces al código y a la sesión en Lean Web.

2.6 ∃ x y, P x y ⊢ ∃ u v, P u v

Enlaces al código y a la sesión en Lean Web.

2.7 ∃ x, ∀ y, P x y ⊢ ∀ y, ∃ x, P x y

Enlaces al código y a la sesión en Lean Web.

2.8 ∃x, P a → Q x ⊢ P a → (∃ x, Q x)

Enlaces al código y a la sesión en Lean Web.

2.9 P a → (∃ x, Q x) ⊢ ∃ x, P a → Q x

Enlaces al código y a la sesión en Lean Web.

2.10 P a → (∃ x, Q x) ⊢ ∃ x, P a → Q x

Enlaces al código y a la sesión en Lean Web.

2.11 (∃ x, P x) → Q a ⊢ ∀ x, P x → Q a

Enlaces al código y a la sesión en Lean Web.

2.12 ∀ x, P x → Q a ⊢ ∃ x, P x → Q a

Enlaces al código y a la sesión en Lean Web.

2.13 (∀ x, P x) ∨ (∀ x, Q x) ⊢ ∀ x, P x ∨ Q x

Enlaces al código y a la sesión en Lean Web.

2.14 ∃ x, P x ∧ Q x ⊢ (∃ x, P x) ∧ (∃ x, Q x)

Enlaces al código y a la sesión en Lean Web.

2.15 ∀ x y, P y → Q x ⊢ (∃ y, P y) → (∀ x, Q x)

Enlaces al código y a la sesión en Lean Web.

2.16 ¬(∀ x, ¬(P x)) ⊢ ∃ x, P x

Enlaces al código y a la sesión en Lean Web.

2.17 ∀ x, ¬(P x) ⊢ ¬(∃ x, P x)

Enlaces al código y a la sesión en Lean Web.

2.18 ∃ x, P x ⊢ ¬(∀ x, ¬(P x))

Enlaces al código y a la sesión en Lean Web.

2.19 P a → (∀ x, Q x) ⊢ ∀ x, P a → Q x

Enlaces al código y a la sesión en Lean Web.

2.20 ∀ x y z, R x y ∧ R y z → R x z; ∀ x, ¬(R x x) ⊢ ∀ x y, R x y → ¬(R y x)

Enlaces al código y a la sesión en Lean Web.

2.21 ∀x, P x ∨ Q x; ∃x, ¬Q x, ∀ x, R x → ¬P x ⊢ ∃x, ¬R x

Enlaces al código y a la sesión en Lean Web.

2.22 ∀x, P x → Q x ∨ R x; ¬∃x, P x ∧ R x ⊢ ∀x, P x → Q x

Enlaces al código y a la sesión en Lean Web.

2.23 ∃ x y, R x y ∨ R y x ⊢ ∃ x y, R x y

Enlaces al código y a la sesión en Lean Web.

2.24 (∃x, ∀y, P x y) → (∀y, ∃x, P x y)

Enlaces al código y a la sesión en Lean Web.

2.25 (∀ x, P x → Q) ⟷ ((∃x, P x) → Q)

Enlaces al código y a la sesión en Lean Web.

2.26 ((∀x, P x) ∧ (∀x, Q x)) ⟷ (∀x, P x ∧ Q x)

Enlaces al código y a la sesión en Lean Web.

2.27 ((∃x, P x) ∨ (∃x, Q x)) ⟷ (∃x, P x ∨ Q x)

Enlaces al código y a la sesión en Lean Web.

2.28 (¬(∀ x, P x)) ⟷ (∃x, ¬P x)

Enlaces al código y a la sesión en Lean Web.

3 Ejercicios sobre igualdad y funciones

3.1 P a ⊢ ∀ x, x = a → P x

Enlaces al código y a la sesión en Lean Web.

3.2 ∃x y, R x y ∨ R y x; ¬∃x, R x x ⊢ ∃x y, x ≠ y

Enlaces al código y a la sesión en Lean Web.

3.3 ∀x, P a x x; ∀xyz, P x y z → P (f x) y (f z) ⊢ P (f a) a (f a)

Enlaces al código y a la sesión en Lean Web.

3.4 ∀x, P a x x; ∀xyz, P x y z → P (f x) y (f z) ⊢ ∃z, P (f a) z (f (f a))

Enlaces al código y a la sesión en Lean Web.

3.5 ∀y, Q a y; ∀xy, Q x y → Q (s x) (s y) ⊢ ∃z, Qa z ∧ Q z (s (s a))

Enlaces al código y a la sesión en Lean Web.

3.6 x = f x; P (f x) ⊢ P x

Enlaces al código y a la sesión en Lean Web.

3.7 x = f x, triple (f x) (f x) x ⊢ triple x x x

Enlaces al código y a la sesión en Lean Web.

4 Bibliografía

• Deducción natural en lógica de primer orden. ~ J.A. Alonso, A. Cordón, M.J. Hidalgo.
• Lógica con Lean ~ J.A. Alonso.
  • Cap. 2: Lógica proposicional.
• Logic and proof. ~ J. Avigad, R.Y. Lewis, F. van Doorn.
  • Cap. 4: Propositional Logic in Lean.
• Logic in Computer Science. ~ M. Huth, M. Ryan.
  • Cap. 1.2: Propositional logic. Natural deduction.
• Theorem proving in Lean. ~ J. Avigad, L. de Moura, S. Kong.
  • Cap. 3: Propositions and proofs.