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 continuación, se muestra el vídeo

ForMatUS: Pruebas en Lean de P ∧ Q → Q ∧ P

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P ∧ Q → Q ∧ P en el que se comentan 13 pruebas en Lean de la fórmula (P ∧ Q → Q ∧ P) en distintos estilos (declarativo, aplicativo con tácticas, funcional con término de prueba y automático).

Los enlaces correspondientes son:

A continuación, se muestra el vídeo