propositional_logic.lean

import data.set.basic
import data.set.finite
import order.closure
import order.zorn
import tactic.by_contra

inductive prop (L : Type)
| prim : L → prop
| false : prop
| impl : prop → prop → prop

open prop

local infixr ` ⇒ `:70 := prop.impl
notation `⊥` := prop.false
-- set_option pp.parens true

variables {L : Type}

@[pp_nodot, reducible] def negate (p : prop L) : prop L := p ⇒ ⊥
local prefix `¬`:80 := negate

@[pp_nodot] def prop_and : prop L → prop L → prop L := λ p q, ¬ (p ⇒ ¬ q)
local infix `∧'`:40 := prop_and

@[pp_nodot] def prop_or : prop L → prop L → prop L := λ p q, (¬ p ⇒ q)
local infix `∨'`:40 := prop_or

inductive proves (S : set (prop L)) : prop L → Prop
| assump (x) : x ∈ S → proves x
| mp (x y : prop L) : proves (x ⇒ y) → proves x → proves y
| ax1 (x y : prop L) : proves (x ⇒ (y ⇒ x))
| ax2 (x y z : prop L) : proves ((x ⇒ (y ⇒ z)) ⇒ ((x ⇒ y) ⇒ (x ⇒ z)))
| ax3 (x : prop L) : proves (¬¬x ⇒ x)

local infix ` ⊢ `:60 := proves

open proves

lemma proves.weaken {S₁ S₂ : set (prop L)} (h : S₁ ⊆ S₂) {p : prop L} : S₁ ⊢ p → S₂ ⊢ p :=
sorry

lemma empty_proves_id {p : prop L} : ∅ ⊢ (p ⇒ p) :=
sorry

lemma composition {p q r : prop L} : {p ⇒ q, q ⇒ r} ⊢ (p ⇒ r) :=
sorry

lemma deduction_easy {S : set (prop L)} (p q : prop L) (h : S ⊢ p ⇒ q) : S.insert p ⊢ q :=
sorry

lemma deduction_hard {S : set (prop L)} (p q : prop L) (h : S.insert p ⊢ q) : S ⊢ p ⇒ q :=
sorry

theorem deduction {S : set (prop L)} (p q : prop L) : S ⊢ p ⇒ q ↔ S.insert p ⊢ q :=
sorry

/-- The principle of explosion. Of course we can prove this without the deduction theorem, but it is
convenient with it. -/
lemma explosion (p : prop L) : ∅ ⊢ (⊥ : prop L) ⇒ p :=
sorry

/--
A function on propositions is a *valuation* if it is false at false, and behaves sensibly on
implication.
-/
def is_valuation (v : prop L → bool) : Prop :=
v ⊥ = ff ∧ ∀ p q : prop L, v (p ⇒ q) = cond (v p) (v q) tt

variables {v v₁ v₂ : prop L → bool}

lemma is_valuation.impl_eq_ff {p q : prop L} (hv : is_valuation v) :
  v (p ⇒ q) = ff ↔ v p = tt ∧ v q = ff :=
sorry

@[simp] lemma is_valuation.neg {p : prop L} (hv : is_valuation v) :
  v (¬p) = !v p :=
sorry

lemma is_valuation.ax1 {p q : prop L} (hv : is_valuation v) :
  v (p ⇒ (q ⇒ p)) = tt :=
sorry

lemma is_valuation.ax2 {p q r : prop L} (hv : is_valuation v) :
  v ((p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r))) = tt :=
sorry

lemma is_valuation.ax3 {p : prop L} (hv : is_valuation v) : v (¬¬p ⇒ p) = tt :=
sorry

/-- The set of propositions `S` *entails* `t` if every valuation which returns true on all of `S`
also returns true on `t`. -/
def entails (S : set (prop L)) (t : prop L) : Prop :=
∀ v, is_valuation v → (∀ s ∈ S, v s = tt) → v t = tt

local infix ` ⊨ `:30 := entails

lemma composition_entails {p q r : prop L} : {p ⇒ q, q ⇒ r} ⊨ (p ⇒ r) :=
sorry

theorem soundness {S : set (prop L)} {p : prop L} :
  S ⊢ p → S ⊨ p :=
sorry

def consistent (S : set (prop L)) : Prop := not (S ⊢ ⊥)

lemma proves.insert_consistent {S : set (prop L)} {p : prop L} (hS : consistent S) (hp : S ⊢ p) :
  consistent (S.insert p) :=
sorry

lemma proves.exists_finite_subset {S : set (prop L)} {p : prop L} (hneg : S ⊢ p) :
  ∃ S', S' ⊆ S ∧ S'.finite ∧ S' ⊢ p :=
sorry

lemma my_thing' {α : Type*} {c : set (set α)} (hc : directed_on (⊆) c) (hc' : c.nonempty)
  (S : set α) (hS₁ : S ⊆ ⋃₀ c) (hS₂ : S.finite) : ∃ T ∈ c, S ⊆ T :=
sorry

lemma model_existence {S : set (prop L)} : S ⊨ ⊥ → S ⊢ ⊥ :=
sorry

theorem adequacy {S : set (prop L)} {t : prop L} : S ⊨ t → S ⊢ t :=
sorry

theorem completeness {S : set (prop L)} {t : prop L} : S ⊢ t ↔ S ⊨ t := ⟨soundness, adequacy⟩