ForMatUS: Pruebas en Lean de P → Q, P → ¬Q ⊢ ¬P
He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P → Q, P → ¬Q ⊢ ¬P en el que se comentan 11 pruebas en Lean de la siguiente propiedad
P → Q, P → ¬Q ⊢ ¬P
usando las reglas del condicional y de la negación.
Los enlaces correspondientes son:
- a la sesión en Lean Web,
- al código,
- al libro “Lógica con Lean” y
- al repositorio en GitHub “Lógica con Lean”.
A continuación, se muestra el vídeo