Menu Close

Día: 14 septiembre, 2020

ForMatUS: Pruebas en Lean del modus tollens: P → Q, ¬Q ⊢ ¬P

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean del modus tollens en el que se se comentan 11 pruebas en Lean del modus tollens:

P → Q, ¬Q ⊢ ¬P

Se comienza con pruebas declarativas, con razonamiento hacia adelante, que se reducen a funcionales; a continuación, se hacen pruebas aplicativas, con razonamiento hacia atrás, que también se reducen a funcionales y, finalmente, se buscan las pruebas automáticas.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Pruebas del modus tollens
-- =========================
 
-- Ej. 1. Demostrar
--    P → Q, ¬Q ⊢ ¬P
 
import tactic
 
variables (P Q : Prop)
 
-- 1ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
assume h3 : P,
have h4 : Q,
  from h1 h3,
show false, 
  from h2 h4
 
-- 2ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
assume h3 : P,
have h4 : Q := h1 h3,
show false, 
  from h2 h4
 
-- 3ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
assume h3 : P,
show false, 
  from h2 (h1 h3)
 
-- 4ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
assume h3 : P, h2 (h1 h3)
 
-- 5ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
λ h, h2 (h1 h)
 
-- 6ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
h2  h1
 
-- 7ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
mt h1 h2
 
-- 8ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
by tauto
 
-- 9ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
by finish
 
-- 10ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
begin
  intro h,
  apply h2,
  apply h1,
  exact h,
end
 
-- 11ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
begin
  intro h,
  exact h2 (h1 h),
end
 
-- 12ª demostración
example 
  (h1 : P  Q)
  (h2 : ¬Q)
  : ¬P :=
λ h, h2 (h1 h)

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

He añadido a la lista Lógica con Lean el vídeo Pruebas del silogismo hipotético en el que se se comentan 11 pruebas en Lean del silogismo hipotético

P → Q, Q → R ⊢ P → R.

Se comienza con pruebas declarativas, con razonamiento hacia adelante, que se reducen a funcionales; a continuación, se hacen pruebas aplicativas, con razonamiento hacia atrás, que también se reducen a funcionales y, finalmente, se buscan las pruebas automáticas.

A continuación, se muestra el vídeo

El código es

-- Pruebas del silogismo hipotético
-- --------------------------------
 
import tactic
 
variables (P Q R : Prop)
 
-- Ej. 1. Demostrar que
--    P → Q, Q → R ⊢ P → R
 
-- 1º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
assume h : P,
have h3 : Q,
  from h1 h,
show R, 
  from h2 h3
 
-- 2º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
assume h : P,
have h3 : Q := h1 h,
show R, 
  from h2 h3
 
-- 3º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
assume h : P,
show R, 
  from h2 (h1 h)
 
-- 4º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
assume h : P, h2 (h1 h)
 
-- 5º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
λ h, h2 (h1 h)
 
-- 6º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
h2  h1
 
-- 7º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
begin
  intro h,
  apply h2, 
  apply h1,
  exact h,
end
 
-- 8º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
begin
  intro h,
  apply h2, 
  exact h1 h,
end
 
-- 9º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
begin
  intro h,
  exact h2 (h1 h),
end
 
-- 10º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
λ h, h2 (h1 h)
 
-- 11º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
h2  h1
 
-- 12º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
by tauto
 
-- 13º demostración
example 
  (h1 : P  Q)
  (h2 : Q  R)
  : P  R :=
by finish

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