Library UniMath.CategoryTheory.Inductives.PropositionalLogic

This file contains a formalization of the syntax of propositional logic as the initial algebra of a functor.
Following Goldblatt's 'Topoi', all of the connectives are treated as primitive. As stated there, they are a priori distinct; their interdefinability is naturally propositional, not definitional.
Written by: Langston Barrett, 2019

Contents

  • Definition of PL syntax as an initial algebra
  • Definition of a PL valuation in bool
  • TODO: Definition of a PL valuation in an (order-theoretic) algebra
    PL_functor Var Rec :=
        Var            (* -- arity 1, sentences *)
      + Rec            (* -- arity 1, ¬ (not) *)
      + (Rec × Rec)    (* -- arity 2, ∧ (and) *)
      + (Rec × Rec)    (* -- arity 2, ∨ (or) *)
      + (Rec × Rec)    (* -- arity 2, → (implies) *)
The following three statements are crucial for performance.
The underlying set of the initial algebra
Definition PL : hSet := alg_carrier _ PL_alg.

Definition PL_type : UU := pr1hSet PL.

Definition PL_var : HSETvars, PL.
  refine (_ · alg_map _ PL_alg).
  intro v; do 4 apply inl; exact v.
Defined.

Definition PL_not : HSETPL, PL.
  refine (_ · alg_map _ PL_alg).
  intro s; do 3 apply inl; apply inr; exact s.
Defined.

Definition PL_and : HSETPL PL, PL.
  refine (_ · alg_map _ PL_alg).
  intro s; do 2 apply inl; apply inr; exact s.
Defined.

Definition PL_and_fun (x : PL_type) (y : PL_type) : PL_type :=
  PL_and (make_dirprod x y).

Definition PL_or : HSETPL PL, PL.
  refine (_ · alg_map _ PL_alg).
  intro s; do 1 apply inl; apply inr; exact s.
Defined.

Definition PL_or_fun (x : PL_type) (y : PL_type) : PL_type :=
  PL_or (make_dirprod x y).

Definition PL_impl : HSETPL PL, PL.
  refine (_ · alg_map _ PL_alg).
  intro s; apply inr; exact s.
Defined.

Definition PL_impl_fun (x : PL_type) (y : PL_type) : PL_type :=
  PL_impl (make_dirprod x y).

Definition PL_iff_fun (x : PL_type) (y : PL_type) : PL_type :=
  PL_and_fun (PL_impl (make_dirprod x y)) (PL_impl (make_dirprod y x)).

Declare Scope PL.
Delimit Scope PL with PL.
Notation "¬" := (PL_not) : PL.
Infix "∧" := (PL_and) : PL.
Infix "∨" := (PL_or) : PL.
Infix "⇒" := (PL_impl) : PL.
Infix "⇔" := (PL_iff_fun) (at level 90) : PL.

Definition make_PL_algebra (X : hSet) (vs : vars -> X) (not : X -> X)
           (and : X -> X -> X) (or : X -> X -> X) (impl : X -> X -> X) :
  algebra_ob PL_functor'.
Show proof.
  exists X.
  cbn; do 5 (try (apply sumofmaps)).
  - assumption.   - exact not.
  - apply (invweq (weqfunfromdirprod _ _ _)); exact and.
  - apply (invweq (weqfunfromdirprod _ _ _)); exact or.
  - apply (invweq (weqfunfromdirprod _ _ _)); exact impl.

The fold, or catamorphism: given the same structure of operations on any other set, we can construct an interpretation of PL in that set.
Definition PL_fold_alg_mor {X : hSet} (vs : vars -> X)
           (not : X -> X) (and : X -> X -> X) (or : X -> X -> X) (impl : X -> X -> X) :
  algebra_mor PL_functor' PL_alg (make_PL_algebra X vs not and or impl).
Show proof.
  apply (InitialArrow PL_functor_initial (make_PL_algebra X vs not and or impl)).

Definition PL_fold {X : hSet} (vs : vars -> X)
           (not : X -> X) (and : X -> X -> X) (or : X -> X -> X) (impl : X -> X -> X) :
  PL -> X := mor_from_algebra_mor _ (PL_fold_alg_mor vs not and or impl).

Some lemmas expressing the computational behavior of PL_fold
Section FoldComputationLemmas.
  Context {X : hSet} (vs : vars -> X)
          (not : X -> X) (and : X -> X -> X) (or : X -> X -> X) (impl : X -> X -> X).

  Let fold := PL_fold vs not and or impl.
  Let mor := PL_fold_alg_mor vs not and or impl.
  Let comm := algebra_mor_commutes _ _ _ mor.

  Lemma PL_fold_var : z, fold (PL_var z) = vs z.
  Show proof.
    reflexivity.

  Lemma PL_fold_not : p, fold (PL_not p) = not (fold p).
  Show proof.
    intro.
    do 3 apply (maponpaths (λ x, (inl : HSET _, BinCoproductsHSET _ _) · x)) in comm.
    apply (maponpaths (λ x, (inr : HSET _, BinCoproductsHSET _ _) · x)) in comm.
    apply eqtohomot in comm.
    specialize (comm p).
    exact comm.

  Lemma PL_fold_and : p q, fold (PL_and (make_dirprod p q)) = and (fold p) (fold q).
  Show proof.
    intros p q.
    do 2 apply (maponpaths (λ x, (inl : HSET _, BinCoproductsHSET _ _) · x)) in comm.
    apply (maponpaths (λ x, (inr : HSET _, BinCoproductsHSET _ _) · x)) in comm.
    apply eqtohomot in comm.
    specialize (comm (make_dirprod p q)).
    exact comm.

  Lemma PL_fold_or : p q, fold (PL_or (make_dirprod p q)) = or (fold p) (fold q).
  Show proof.
    intros p q.
    apply (maponpaths (λ x, (inl : HSET _, BinCoproductsHSET _ _) · x)) in comm.
    apply (maponpaths (λ x, (inr : HSET _, BinCoproductsHSET _ _) · x)) in comm.
    apply eqtohomot in comm.
    specialize (comm (make_dirprod p q)).
    exact comm.

  Lemma PL_fold_impl : p q, fold (PL_impl (make_dirprod p q)) = impl (fold p) (fold q).
  Show proof.
    intros p q.
    apply (maponpaths (λ x, (inr : HSET _, BinCoproductsHSET _ _) · x)) in comm.
    apply eqtohomot in comm.
    specialize (comm (make_dirprod p q)).
    apply comm.
End FoldComputationLemmas.

The induction principle.
Mirrors the proof for lists.
Section PL_ind.

Context {P : PL -> UU} (PhSet : l, isaset (P l)).
Context (P_vars : v : vars, P (PL_var v))
        (P_not : pl, P pl -> P (PL_not pl))
        (P_and : pl1 pl2, P pl1 -> P pl2 -> P (PL_and (make_dirprod pl1 pl2)))
        (P_or : pl1 pl2, P pl1 -> P pl2 -> P (PL_or (make_dirprod pl1 pl2)))
        (P_impl : pl1 pl2, P pl1 -> P pl2 -> P (PL_impl (make_dirprod pl1 pl2))).

Let P' : UU := pl : PL, P pl.
Let P'_vars (v : vars) : P' := (PL_var v,, P_vars v).
Let P'_not (pl : P') : P' := (PL_not (pr1 pl),, P_not _ (pr2 pl)).
Let P'_and (pl1 pl2 : P') : P' :=
  (PL_and (make_dirprod (pr1 pl1) (pr1 pl2)),,
   P_and _ _ (pr2 pl1) (pr2 pl2)).
Let P'_or (pl1 pl2 : P') : P' :=
  (PL_or (make_dirprod (pr1 pl1) (pr1 pl2)),,
   P_or _ _ (pr2 pl1) (pr2 pl2)).
Let P'_impl (pl1 pl2 : P') : P' :=
  (PL_impl (make_dirprod (pr1 pl1) (pr1 pl2)),,
   P_impl _ _ (pr2 pl1) (pr2 pl2)).

Definition P'HSET : HSET.
Show proof.
  use make_hSet.
  - exact P'.
  - abstract (apply (isofhleveltotal2 2); [ apply setproperty | intro x; apply PhSet ]).

Opaque is_omega_cocont_PL_functor'.

Lemma is_algebra_morphism_pr1_PL_fold :
  is_algebra_mor _ PL_alg PL_alg (λ l, pr1 (@PL_fold P'HSET P'_vars P'_not P'_and P'_or P'_impl l)).
Show proof.
apply (BinCoproductArrow_eq_cor _ BinCoproductsHSET).
- apply funextfun; intro x; induction x as [x2 | x3].
  + induction x2 as [x4 | x5].
    * induction x4 as [x6 | x7].
      -- cbn in x6.
Abort.

End PL_ind.

End PL.

A valuation for atomic sentences can be extended to one for all sentences.
Definition bool_valuation {vars : hSet} (V : vars -> bool) : PL vars -> bool.
Proof.
  use (@PL_fold vars boolset).
  - assumption.   - exact negb.
  - exact andb.
  - exact orb.
  - exact implb.