4. The law of the excluded middle

17/10/22

Logic of evidence & proof	Intuitionistic logic
Logic of truth	Classical Logic

Excluded Middle

Every propositions is either true or false $P \vee ¬P$

Intuitionistic logic is constructive (compatible) Classical logic may not be compatible Intuitionistic logic is weaker than classical

em (P) - Proves it classically. Allows you to 'spawn' in a variable

Code

variables P Q R : Prop

open classical
#check em P

theorem dMorgan2 : ¬(P ∧ Q) ↔ ¬ P ∨ ¬ Q :=
begin
  constructor,
  assume npq,
  have pnp : P ∨ ¬ P,
  apply em,
  cases pnp with p np,
  right,
  assume q,
  apply npq,
  constructor,
  exact p,
  exact q,

  left,
  exact np,

  assume h,
  cases h,
  assume pq,
  cases pq with p q,
  apply h,
  exact p,
  assume pq,
  cases pq with p q,
  apply h,
  exact q,

end

-- indirect proof
-- to prove P assume ¬ P and desrive False
-- reductio ad absurdum

theorem raa : ¬ ¬ P → P :=
begin
  assume nnp,
  have pnp : P ∨ ¬P,
  apply em,
  cases pnp with p np,
  exact p,
  have f : false,
  apply nnp,
  exact np,
  cases f,
end

example : P → ¬ ¬ P :=
begin
  assume p np,
  apply np,
  exact p,
end

theorem nnem : ¬ ¬ (P ∨ ¬ P) :=
begin
  assume np,
  apply np,
  right,
  assume p,
  apply np,
  left,
  exact p,

end


theorem em_from_raa : P ∨ ¬ P :=
begin
  apply raa,
  apply  nnem,
end

Wills Way

have pnp: P ∨ ¬P,
apply em,
cases pnp with p np,
exact p,

is same as

cases (em P) with p np,
exact p