septiembre 2020 – Página 5

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

PorJosé A. Alonso 14 septiembre 2020

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)

100

101

102

103

104

105

106

107

108

109

110

-- 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

PorJosé A. Alonso 14 septiembre 202014 septiembre 2020

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.

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

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

-- 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

PorJosé A. Alonso 14 septiembre 2020

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

ForMatUS: Reglas de la negación en Lean

PorJosé A. Alonso 13 septiembre 2020

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

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

PorJosé A. Alonso 13 septiembre 202013 septiembre 2020

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 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