Skip to content

Latest commit

 

History

History
613 lines (442 loc) · 60.2 KB

README.org

File metadata and controls

613 lines (442 loc) · 60.2 KB
Raw

Lógica con Lean

1 Introducción

El objetivo de este trabajo es presentar una introducción a la Lógica usando Lean para usarla en las clases de la asignatura de Razonamiento automático del Máster Universitario en Lógica, Computación e Inteligencia Artificial de la Universidad de Sevilla. Por tanto, el único prerrequisito es, como en el Máster, cierta madurez matemática como la que deben tener los alumnos de los Grados de Matemática y de Informática.

El trabajo se basa fundamentalmente en

La exposición se hará mediante una colección de ejercicios. En cada ejercicios se mostrarán distintas pruebas del mismo resultado y se comentan las tácticas conforme se van usando y los lemas utilizados en las demostraciones.

Además, en cada ejercicio hay tres enlaces: uno al código, otro que al pulsarlo abre el ejercicio en Lean Web (en una sesión del navegador) de forma que se puede navegar por las pruebas y editar otras alternativas, y el tercero es un enlace a un vídeo explicando las soluciones del ejercicio.

El trabajo se desarrolla como un proyecto en GitHub que contiene libro en PDF. Además, los vídeos correspondientes a cada uno de los ejercicios se encuentran en YouTube.

#

2 Lógica proposicional

2.1 Reglas del condicional

2.1.1 Regla de eliminación del condicional en P → Q, P ⊢ Q

2.1.2 Pruebas de P, P → Q, P → (Q → R) ⊢ R

2.1.3 Regla de introducción del condicional en P → P

2.1.4 Pruebas de P → (Q → P)

2.1.5 Pruebas del silogismo hipotético: P → Q, Q → R ⊢ P → R

2.2 Reglas de la conjunción

2.2.1 Reglas de la conjunción en P ∧ Q, R ⊢ Q ∧ R

2.2.2 Pruebas de P ∧ Q → Q ∧ P

2.3 Reglas de la negación

2.3.1 Reglas de la negación con (⊥ ⊢ P), (P, ¬P ⊢ ⊥) y ¬(P ∧ ¬P)

2.3.2 Pruebas de P → Q, P → ¬Q ⊢ ¬P

2.3.3 Pruebas del modus tollens: P → Q, ¬Q ⊢ ¬P

2.3.4 Pruebas de P → (Q → R), P, ¬R ⊢ ¬Q

2.3.5 Pruebas de P → Q ⊢ ¬Q → ¬P

2.3.6 Regla de introducción de la doble negación: P ⊢ ¬¬P

2.3.7 Pruebas de ¬Q → ¬P ⊢ P → ¬¬Q

2.4 Reglas de la disyunción

2.4.1 Reglas de introducción de la disyunción

2.4.2 Regla de eliminación de la disyunción

2.4.3 Pruebas de P ∨ Q ⊢ Q ∨ P

2.4.4 Pruebas de Q → R ⊢ P ∨ Q → P ∨ R

2.4.5 Pruebas de ¬P ∨ Q ⊢ P → Q

2.5 Reglas del bicondicional

2.5.1 Regla de introducción del bicondicional en P ∧ Q ↔ Q ∧ P

2.5.2 Reglas de eliminación del bicondicional en P ↔ Q, P ∨ Q ⊢ P ∧ Q

2.6 Reglas de la lógica clásica

2.6.1 Pruebas de la regla de reducción al absurdo

2.6.2 Pruebas de la eliminación de la doble negación

2.6.3 Pruebas del principio del tercio excluso

2.6.4 Pruebas de P → Q ⊢ ¬P ∨ Q

2.6.5 Pruebas de P, ¬¬(Q ∧ R) ⊢ ¬¬P ∧ R

2.6.6 Pruebas de ¬P → Q, ¬Q ⊢ P

2.6.7 Pruebas de (Q → R) → ((¬Q → ¬P) → (P → R))

3 Lógica de primer orden

3.1 Reglas del cuantificador universal

3.1.1 Regla de eliminación del cuantificador universal

3.1.2 Regla de introducción del cuantificador universal

3.2 Reglas del cuantificador existencial

3.2.1 Regla de introducción del cuantificador existencial

3.2.2 Regla de eliminación del cuantificador existencial

3.3 Ejercicios sobre cuantificadores

3.3.1 Pruebas de ¬∀x P(x) ↔ ∃x ¬P(x)

3.3.2 Pruebas de ∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)

3.3.3 Pruebas de ∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)

3.3.4 Pruebas de ∃x∃y P(x,y) ↔ ∃y∃x P(x,y)

3.4 Reglas de la igualdad

3.4.1 Regla de eliminación de la igualdad

3.4.2 Pruebas de la transitividad de la igualdad

3.4.3 Regla de introducción de la igualdad

3.4.4 Pruebas de y = x → y = z → x = z

3.4.5 Pruebas de (x + y) + z = (x + z) + y

3.4.6 Pruebas de desarrollo de producto de sumas

4 Conjuntos

4.1 Elementos básicos sobre conjuntos

4.1.1 Pruebas de la reflexividad de la inclusión de conjuntos

4.1.2 Pruebas de la antisimetría de la inclusión de conjuntos

4.1.3 Introducción de la intersección

4.1.4 Introducción de la unión

4.1.5 El conjunto vacío

4.1.6 Diferencia de conjuntos: A \ B ⊆ A

4.1.7 Complementario de un conjunto: Pruebas de A \ B ⊆ Bᶜ

4.1.8 Pruebas de la conmutatividad de la intersección

4.2 Identidades conjuntistas

4.2.1 Pruebas de la propiedad distributiva de la intersección sobre la unión.

4.2.2 Pruebas de (A ∩ Bᶜ) ∪ B = A ∪ B

4.3 Familias de conjuntos

4.3.1 Unión e intersección de familias de conjuntos

4.3.2 Pertenencia a uniones e intersecciones de familias

4.3.3 Pruebas de la distributiva de la intersección general sobre la intersección

4.3.4 Reglas de la intersección general

4.3.5 Reglas de la unión general

4.3.6 Pruebas de intersección sobre unión general

4.3.7 Pruebas de (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)

4.4 Conjunto potencia

4.4.1 Definición del conjunto potencia

4.4.2 Pruebas de A ∈ 𝒫 (A ∪ B)

4.4.3 Monotonía del conjunto potencia: 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B

5 Relaciones

5.1 Relaciones de orden

5.1.1 Las irreflexivas y transitivas son asimétricas

5.1.2 Las partes estrictas son irreflexivas

5.1.3 Las partes estrictas de los órdenes parciales son transitivas

5.1.4 Las partes simétricas de las reflexivas son reflexivas

5.1.5 Las partes simétricas son simétricas

5.2 Órdenes sobre números

5.2.1 Pruebas de n + 1 ≤ m ⊢ n < m + 1

5.3 Relaciones de equivalencia

5.3.1 Las equivalencias son preórdenes simétricos

5.3.2 Las relaciones reflexivas y euclídeas son de equivalencia

6 Funciones

6.1 Funciones en Lean

6.1.1 Definición de la composición de funciones

6.1.2 Definición de la función identidad

6.1.3 Extensionalidad funcional

6.1.4 Propiedades de la composición de funciones (elemento neutro y asociatividad)

6.1.5 Funciones inyectivas, suprayectivas y biyectivas

6.1.6 La identidad es biyectiva

6.1.7 La composición de funciones inyectivas es inyectiva

6.1.8 La composición de funciones suprayectivas es suprayectiva

6.1.9 La composición de funciones biyectivas es biyectiva

6.1.10 Las composiciones con las inversas son la identidad

6.1.11 Las funciones con inversa por la izquierda son inyectivas

6.1.12 Las funciones con inversa por la derecha son suprayectivas

6.2 La función inversa

6.2.1 Las funciones inyectivas tienen inversa por la izquierda

6.3 Funciones y conjuntos

6.3.1 La composición de inyectivas parciales es inyectiva

6.3.2 La composición de suprayectivas parciales es suprayectiva

6.3.3 La imagen de la unión es la unión de las imágenes

7 Números naturales, recursión e inducción

7.1 Definiciones por recursión

7.1.1 Definiciones por recursión sobre los naturales

7.1.2 Operaciones aritméticas definidas

7.2 Recursión e inducción

7.2.1 Prueba por inducción 1: (∀ n ∈ ℕ) 0 + n = n

7.2.2 Prueba por inducción 2: (∀ m n k ∈ ℕ) (m + n) + k = m + (n + k)

7.2.3 Prueba por inducción 3: (∀ m n ∈ ℕ) succ m + n = succ (m + n)

7.2.4 Prueba por inducción 4: (∀ m n ∈ ℕ) m + n = n + m

7.2.5 Prueba por inducción 5: (∀ m n ∈ ℕ) m^(n+1) = m * m^n

7.2.6 Prueba por inducción 6: (∀ m n k ∈ ℕ) m^(n + k) = m^n * m^k

7.2.7 Prueba por inducción 7: (∀ n ∈ ℕ) n ≠ 0 → succ (pred n) = n

8 Razonamiento sobre programas

8.1 Razonamiento ecuacional

8.1.1 Razonamiento ecuacional sobre longitudes de listas

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.1.2 Razonamiento ecuacional sobre intercambio en pares

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.1.3 Razonamiento ecuacional sobre la inversa de listas unitarias

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.2 Razonamiento por inducción sobre los naturales

8.2.1 Pruebas de longitud (repite n x) = n

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.3 Razonamiento por inducción sobre listas

8.3.1 Pruebas de la asociatividad de la concatenación

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.3.2 Pruebas del elemento neutro por la derecha de la concatenación

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.3.3 Pruebas de longitud (conc xs ys) = longitud xs + longitud ys

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.4 Inducción con patrones para funciones recursivas generales

8.4.1 Pruebas de conc (coge n xs) (elimina n xs) = xs

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.5 Razonamiento por casos

8.5.1 Pruebas de esVacia xs = esVacia (conc xs xs)

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.6 Heurística de generalización

8.6.1 Pruebas de equivalencia entre definiciones de inversa (Heurística de generalización)

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.7 Inducción para funciones de orden superior

8.7.1 Pruebas de la relación entre length y map.

Enlaces al código, a la sesión en Lean Web y al vídeo.

8.7.2 Pruebas de la distributiva del producto sobre sumas

Enlaces al código, a la sesión en Lean Web y al vídeo.

9 Tipos inductivos

9.1 Tipos abreviados

9.1.1 Razonamiento con tipos abreviados: Posiciones

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.2 Tipos parametrizados

9.2.1 Razonamiento con tipos parametrizados: Pares

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.3 Tipos enumerados

9.3.1 Razonamiento con tipos enumerados: Direcciones

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.3.2 Razonamiento con tipos enumerados: Movimientos

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.3.3 Razonamiento con tipos enumerados: Los días de la semana

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.3.4 Razonamiento con tipos enumerados con constructores con parámetros

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.4 Tipo inductivo: Números naturales

9.4.1 El tipo de los números naturales

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.5 Tipo inductivo: Listas

9.5.1 El tipo de las listas

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.6 Tipo inductivo: Árboles binarios

9.6.1 Razonamiento sobre árboles binarios: La función espejo es involutiva

Enlaces al código, a la sesión en Lean Web y al vídeo.

9.6.2 Razonamiento sobre arboles binarios: Aplanamiento e imagen especular

Enlaces al código, a la sesión en Lean Web y al vídeo.