Semantics of PPC

Syntactic Poset

Definition

semantics/PPC_poset.lean

def PPC_eq := @Form_eq PPC_Form PPC_Der

and_eq

semantics/PPC_poset.lean

def and_eq : PPC_eq → PPC_eq → PPC_eq :=
  quot.lift₂ (λ φ ψ, ⦃φ & ψ⦄) and_liftable1 and_liftable2 

notation (name := and_eq) X `&⁼` Y := and_eq X Y

semantics/PPC_poset.lean

lemma and_liftable1 : ∀ φ ψ ψ' : PPC_Form, 
      (ψ ⊣⊢ ψ') → ⦃φ & ψ⦄ = ⦃φ & ψ'⦄ :=
  begin
    assume φ ψ ψ' h,
    apply quotient.sound,
    cases h with ψψ' ψ'ψ,
    constructor,
    -- Proof that φ&ψ ⊢ φ&ψ'
      apply and_intro,
      -- φ&ψ ⊢ φ
      apply and_eliml,
      apply derive_refl, -- φ&ψ ⊢ φ&ψ
      -- φ&ψ ⊢ ψ'
      apply derive_trans,
      apply and_elimr,
      apply derive_refl, -- φ&ψ ⊢ φ&ψ
      exact ψψ',
    -- Proof that φ&ψ' ⊢ φ&ψ
      apply and_intro,
      -- φ&ψ ⊢ φ
      apply and_eliml,
      apply derive_refl, -- φ&ψ' ⊢ φ&ψ'
      -- φ&ψ' ⊢ ψ
      apply derive_trans,
      apply and_elimr,
      apply derive_refl, -- φ&ψ' ⊢ φ&ψ'
      exact ψ'ψ,
  end

lemma and_liftable2 : ∀ φ φ' ψ : PPC_Form, 
      (φ ⊣⊢ φ') → ⦃φ & ψ⦄ = ⦃φ' & ψ⦄ := 
  begin
    assume φ φ' ψ h,
    apply quotient.sound,
    cases h with φφ' φ'φ,
    constructor,
    -- Proof that φ&ψ ⊢ φ'&ψ
      apply and_intro,
      apply derive_trans,
      apply and_eliml,
      apply derive_refl, -- φ&ψ ⊢ φ&ψ
      exact φφ',
      apply and_elimr,
      apply derive_refl, -- φ&ψ ⊢ φ&ψ
    -- Proof that φ'&ψ ⊢ φ&ψ
      apply and_intro,
      apply derive_trans,
      apply and_eliml,
      apply derive_refl, -- φ'&ψ ⊢ φ'&ψ
      exact φ'φ,
      apply and_elimr,
      apply derive_refl, -- φ'&ψ ⊢ φ'&ψ
  end

impl_eq

semantics/PPC_poset.lean

def impl_eq : PPC_eq → PPC_eq → PPC_eq :=
  quot.lift₂ (λ φ ψ, ⦃φ ⊃ ψ⦄) impl_liftable1 impl_liftable2 

notation (name := impl_eq) X `⊃⁼` Y := impl_eq X Y

semantics/PPC_poset.lean

lemma impl_liftable1 : ∀ φ ψ ψ' : PPC_Form, 
      (ψ ⊣⊢ ψ') → ⦃φ ⊃ ψ⦄ = ⦃φ ⊃ ψ'⦄ :=
  begin 
    assume φ ψ ψ' h,
    apply quotient.sound,
    cases h with ψψ' ψ'ψ,
    constructor,
      apply impl_intro,
      apply PPC_derives_x.trans_hyp,
      rw PPC_Hyp_x.insert_is_union_singleton,
      apply PPC_derives_x.modus_ponens,
      exact ψψ',
      apply impl_intro,
      apply PPC_derives_x.trans_hyp,
      rw PPC_Hyp_x.insert_is_union_singleton,
      apply PPC_derives_x.modus_ponens,
      exact ψ'ψ,
  end 

lemma impl_liftable2 : ∀ φ φ' ψ : PPC_Form, 
      (φ ⊣⊢ φ') → ⦃φ ⊃ ψ⦄ = ⦃φ' ⊃ ψ⦄ := 
  begin 
    assume φ φ' ψ h,
    apply quotient.sound,
    cases h with φφ' φ'φ,
    constructor,
      apply impl_elim,
      apply PPC_derives_x.hypo_syll',
      apply impl_intro,
      apply weak,
      exact φ'φ,
      ---
      apply impl_elim,
      apply PPC_derives_x.hypo_syll',
      apply impl_intro,
      apply weak,
      exact φφ',
  end 

Syntactic Category

semantics/PPC_syntacticCat.lean

instance ℂ_PPC : thin_cat PPC_eq := syn_cat

Lifting tactic

semantics/PPC_syntacticCat.lean

namespace ℂ_PPC_tactics

def Form : Type := PPC_Form
def Der : has_derives Form := PPC_Der

meta def lift_derive_ℂ_PPC : tactic unit → tactic unit :=
  @synCat_tactics.lift_derive_syn_cat Form Der

end ℂ_PPC_tactics

Finite-product category

categoryTheory/thin.lean

class thin_cat (C : Type) extends category C :=
  (K : ∀ (X Y : C) (f g : X ⟶ Y), f = g)

semantics/PPC_syntacticCat.lean

instance : FP_cat PPC_eq :=
{
  unit := syn_obj PPC_Form.top,
  term := by lift_derive_ℂ_PPC `[ apply truth ], -- φ ⊢ ⊤
  unit_η := λ X f, by apply thin_cat.K,
  prod := (&⁼),
  pr1 := by lift_derive_ℂ_PPC `[ apply and_eliml ], -- φ & ψ ⊢ φ
  pr2 := by lift_derive_ℂ_PPC `[ apply and_elimr ], -- φ & ψ ⊢ ψ
                -- If θ ⊢ φ and θ ⊢ ψ, then θ ⊢ φ & ψ
  pair := by lift_derive_ℂ_PPC `[ apply and_intro ],
  prod_β1 := λ X Y Z f g, by apply thin_cat.K,
  prod_β2 := λ X Y Z f g, by apply thin_cat.K,
  prod_η :=  λ X Y, by apply thin_cat.K,
}

Cartesian closed category

semantics/PPC_syntacticCat.lean

instance : CC_cat PPC_eq := 
{
  exp := (⊃⁼),
  eval := by lift_derive_ℂ_PPC `[ 
                -- φ⊃ψ & φ ⊢ ψ
                apply PPC_derives_x.union_Hyp_and,
                apply PPC_derives_x.modus_ponens ],
  curry := by lift_derive_ℂ_PPC `[ 
                -- If φ & ψ ⊢ θ, then φ ⊢ ψ ⊃ θ
                apply impl_intro,
                apply PPC_derives_x.and_Hyp_union ],
  curry_β := λ {X Y Z} u, by apply thin_cat.K,
  curry_η := λ {X Y Z} v, by apply thin_cat.K,
}