Skip to content

Latest commit

 

History

History
218 lines (185 loc) · 4.16 KB

Implicacion_mediante_disyuncion_y_negacion.md

File metadata and controls

218 lines (185 loc) · 4.16 KB
Raw
Título Autor
(P → Q) ↔ ¬P ∨ Q.
José A. Alonso

[mathjax]

Demostrar con Lean4 que [ (P → Q) ↔ ¬P ∨ Q ]

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic
variable (P Q : Prop)

example
  : (P → Q) ↔ ¬P ∨ Q :=
by sorry

1. Demostración en lenguaje natural

Demostraremos cada una de las implicaciones.

(==>) Supongamos que (P → Q). Distinguimos dos subcasos según el valor de (P).

Primer subcaso: suponemos (P). Entonces, tenemos (Q) (porque (P → Q)) y. por tanto, (¬P ∨ Q).

Segundo subcaso: suponemos (¬P). Entonces. tenemos (¬P ∨ Q).

(<==) Supongamos que (¬P ∨ Q) y (P) y tenemos que demostrar (Q). Distinguimos dos subcasos según (¬P ∨ Q).

Primer subcaso: Suponemos (¬P). Entonces tenemos una contradicción con (P).

Segundo subcaso: Suponemos (Q), que es lo que tenemos que demostrar.

2. Demostraciones con Lean4

import Mathlib.Tactic
variable (P Q : Prop)

-- 1ª demostración
-- ===============

example
  : (P → Q) ↔ ¬P ∨ Q :=
by
  constructor
  . -- ⊢ (P → Q) → ¬P ∨ Q
    intro h1
    -- h1 : P → Q
    -- ⊢ ¬P ∨ Q
    by_cases h2 : P
    . -- h2 : P
      right
      -- ⊢ Q
      apply h1
      -- ⊢ P
      exact h2
    . -- h2 : ¬P
      left
      -- ⊢ ¬P
      exact h2
  . -- ⊢ ¬P ∨ Q → P → Q
    intros h3 h4
    -- h3 : ¬P ∨ Q
    -- h4 : P
    -- ⊢ Q
    rcases h3 with h3a | h3b
    . -- h : ¬P
      exact absurd h4 h3a
    . -- h : Q
      exact h3b
  done

-- 2ª demostración
-- ===============

example
  : (P → Q) ↔ ¬P ∨ Q :=
by
  constructor
  . -- ⊢ (P → Q) → ¬P ∨ Q
    intro h1
    -- h1 : P → Q
    -- ⊢ ¬P ∨ Q
    by_cases h2: P
    . -- h2 : P
      right
      -- ⊢ Q
      exact h1 h2
    . -- h2 : ¬P
      left
      -- ⊢ ¬P
      exact h2
  . -- ⊢ ¬P ∨ Q → P → Q
    intros h3 h4
    -- h3 : ¬P ∨ Q
    -- h4 : P
    -- ⊢ Q
    cases h3
    . -- h : ¬P
      contradiction
    . -- h : Q
      assumption
  done

-- 3ª demostración
-- ===============

example
  (P Q : Prop)
  : (P → Q) ↔ ¬P ∨ Q :=
imp_iff_not_or

-- 4ª demostración
-- ===============

example
  (P Q : Prop)
  : (P → Q) ↔ ¬P ∨ Q :=
by tauto

Demostraciones interactivas

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

Referencias

3. Demostraciones con Isabelle/HOL

theory Implicacion_mediante_disyuncion_y_negacion
imports Main
begin

(* 1ª demostración *)
lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)"
proof
  assume "P ⟶ Q"
  show "¬P ∨ Q"
  proof -
    have "¬P ∨ P" by (rule excluded_middle)
    then show "¬P ∨ Q"
    proof (rule disjE)
      assume "¬P"
      then show "¬P ∨ Q" by (rule disjI1)
    next
      assume 2: "P"
      with `P ⟶ Q` have "Q" by (rule mp)
      then show "¬P ∨ Q" by (rule disjI2)
    qed
  qed
next
  assume "¬P ∨ Q"
  show "P ⟶ Q"
  proof
    assume "P"
    note `¬P ∨ Q`
    then show "Q"
    proof (rule disjE)
      assume "¬P"
      then show Q using `P` by (rule notE)
    next
      assume "Q"
      then show "Q" by this
    qed
  qed
qed

(* 2ª demostración *)
lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)"
proof
  assume "P ⟶ Q"
  show "¬P ∨ Q"
  proof -
    have "¬P ∨ P" by (rule excluded_middle)
    then show "¬P ∨ Q"
    proof
      assume "¬P"
      then show "¬P ∨ Q" ..
    next
      assume 2: "P"
      with `P ⟶ Q` have "Q" ..
      then show "¬P ∨ Q" ..
    qed
  qed
next
  assume "¬P ∨ Q"
  show "P ⟶ Q"
  proof
    assume "P"
    note `¬P ∨ Q`
    then show "Q"
    proof
      assume "¬P"
      then show Q using `P` ..
    next
      assume "Q"
      then show "Q" .
    qed
  qed
qed

(* 3ª demostración *)
lemma "(P ⟶ Q) ⟷ (¬P ∨ Q)"
  by simp

end