Menu Close

Autor: José A. Alonso

ForMatUS: Pruebas en Lean de ¬Q → ¬P ⊢ P → ¬¬Q

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 15 pruebas en Lean de

¬Q → ¬P ⊢ P → ¬¬Q

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Pruebas de ¬Q → ¬P ⊢ P → ¬¬Q
-- ============================
 
-- Ej. 1. Demostrar
--    ¬Q → ¬P ⊢ P → ¬¬Q
 
import tactic
 
variables (P Q : Prop)
 
-- 1ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P,
have h3 : ¬¬P,
  from not_not_intro h2,
show ¬¬Q, 
  from mt h1 h3
 
-- 2ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P,
have h3 : ¬¬P := not_not_intro h2,
show ¬¬Q, 
  from mt h1 h3
 
-- 3ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P,
show ¬¬Q, 
  from mt h1 (not_not_intro h2)
 
-- 4ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P, mt h1 (not_not_intro h2)
 
-- 5ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
λ h2, mt h1 (not_not_intro h2)
 
-- 6ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
imp_not_comm.mp h1
 
-- 7ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  apply mt h1,
  apply not_not_intro,
  exact h2,
end
 
-- 8ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  apply mt h1,
  exact not_not_intro h2,
end
 
-- 9ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  exact mt h1 (not_not_intro h2),
end
 
-- 10ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
λ h2, mt h1 (not_not_intro h2)
 
-- 11ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  intro h3,
  have h4 : ¬P := h1 h3,
  exact h4 h2,
end
 
-- 12ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intros h2 h3,
  exact (h1 h3) h2,
end
 
-- 13ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
λ h2 h3, (h1 h3) h2
 
-- 14ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
by tauto
 
-- 15ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
by finish
Seguir leyendo →

ForMatUS: Pruebas en Lean de P → (Q → R), P, ¬R ⊢ ¬Q

José A. Alonso--

He añadido a la lista Lógica con Lean un vídeo en el que se se comentan 9 prueba en Lean de

P → (Q → R), P, ¬R ⊢ ¬Q

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Pruebas de P → (Q → R), P, ¬R ⊢ ¬Q
-- ==================================
 
-- Ej. 1. Demostrar
--    Pruebas de P → (Q → R), P, ¬R ⊢ ¬Q 
 
import tactic
 
variables (P Q R : Prop)
 
-- 1ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
have h4 : Q → R,
  from h1 h2,
show ¬Q,
  from mt h4 h3  
 
-- 2ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
have h4 : Q → R := h1 h2,
show ¬Q,
  from mt h4 h3  
 
-- 3ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
show ¬Q,
  from mt (h1 h2) h3  
 
-- 4ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
mt (h1 h2) h3
 
-- 5ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
begin
  intro h4,
  apply h3,
  apply (h1 h2),
  exact h4,
end
 
-- 6ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
begin
  intro h4,
  apply h3,
  exact (h1 h2) h4,
end
 
-- 7ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
begin
  intro h4,
  exact h3 ((h1 h2) h4),
end
 
-- 8ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
λ h4, h3 ((h1 h2) h4)
 
-- 9ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
by finish
Seguir leyendo →

ForMatUS: Pruebas en Lean de la regla de introducción de la doble negación

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de la regla de introducción de la doble negación

P ⊢ ¬¬P

en el que se comentan 9 pruebas en Lean de la regla de introducción de la doble negación usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Regla de introducción de la doble negación
-- ==========================================
 
-- Ej. 1. Demostrar
--    P ⊢ ¬¬P
 
import tactic
variable (P : Prop)
 
-- 1ª demostración
example
  (h1 : P)
  : ¬¬P :=
not.intro 
  ( assume h2: ¬P,
    show false, 
      from h2 h1)
 
-- 2ª demostración
example
  (h1 : P)
  : ¬¬P :=
assume h2: ¬P,
show false,
  from h2 h1
 
-- 3ª demostración
example
  (h1 : P)
  : ¬¬P :=
assume h2: ¬P, h2 h1
 
-- 4ª demostración
example
  (h1 : P)
  : ¬¬P :=
λ h2, h2 h1
 
-- 5ª demostración
example
  (h1 : P)
  : ¬¬P :=
not_not.mpr h1
 
-- 6ª demostración
example
  (h1 : P)
  : ¬¬P :=
not_not_intro h1
 
-- 7ª demostración
example
  (h1 : P)
  : ¬¬P :=
begin
  intro h2,
  exact h2 h1,
end
 
-- 8ª demostración
example
  (h1 : P)
  : ¬¬P :=
by tauto
 
-- 9ª demostración
example
  (h1 : P)
  : ¬¬P :=
by finish
Seguir leyendo →

ForMatUS: Pruebas en Lean de P → Q ⊢ ¬Q → ¬P

José A. Alonso--

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 12 pruebas en Lean de la propiedad

P → Q ⊢ ¬Q → ¬P

A continuación, se muestra el vídeo

y el código de la teoría utilizada

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

ForMatUS: Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R en el que se comentan 5 pruebas en Lean de

P, P → Q, P → (Q → R) ⊢ R

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Pruebas de P, P → Q, P → (Q → R) ⊢ R
-- ====================================
 
-- Ej 1. Demostrar que
--    P, P → Q, P → (Q → R) ⊢ R
 
import tactic
 
variables (P Q R : Prop)
 
-- 1ª demostración
example
  (h1 : P)
  (h2 : P → Q)
  (h3 : P → (Q → R))
  : R :=
have h4 : Q,
  from h2 h1,
have h5 : Q → R,
  from h3 h1,
show R,
  from h5 h4    
 
-- 2ª demostración
example
  (h1 : P)
  (h2 : P → Q)
  (h3 : P → (Q → R))
  : R :=
have h4 : Q     := h2 h1,
have h5 : Q → R := h3 h1,
show R, from h5 h4    
 
-- 3ª demostración
example
  (h1 : P)
  (h2 : P → Q)
  (h3 : P → (Q → R))
  : R :=
show R, from (h3 h1) (h2 h1)    
 
-- 4ª demostración
example
  (h1 : P)
  (h2 : P → Q)
  (h3 : P → (Q → R))
  : R :=
(h3 h1) (h2 h1)    
 
-- 5ª demostración
example
  (h1 : P)
  (h2 : P → Q)
  (h3 : P → (Q → R))
  : R :=
by finish
Seguir leyendo →

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

José A. Alonso--

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)
Seguir leyendo →

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

José A. Alonso--

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
Seguir leyendo →

ForMatUS: Pruebas en Lean de P → Q, P → ¬Q ⊢ ¬P

José A. Alonso--

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

Seguir leyendo →

ForMatUS: Reglas de la negación en Lean

José A. Alonso--

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

Seguir leyendo →

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

José A. Alonso--

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

Seguir leyendo →