14 septiembre 2020 – Vestigium

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