ForMatUS: Reglas de la negación en Lean
He añadido a la lista Lógica con Lean el vídeo Reglas de la negación en Lean en el que se comentan las reglas de Lean para la eliminación del falso, para la eliminación de la negación y para la introducción de la negación. Para 1ª se muestran 6 pruebas de (⊥ ⊢ P); para la 2ª, se muestran 2 pruebas de (P, ¬P ⊢ ⊥) y para la 3ª, 11 pruebas de ¬(P ∧ ¬P).
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