Different subsets of formulas and sequents

This module defines
  • simple modal formulas/sequents, S(Lambda(V)), possibly negated modal formulas with variables as arguments only
  • prop_modal_prop, Prop(Lambda(V)), propositional formulas over modalities with variables as arguments only
  • prop_modal formulas/sequents, Prop(Lambda(S)), propositional formulas over modalities with arbitrary arguments
  • top_modal formulas/sequents, S(Lambda(S)), possibly negated modalities with arbitrary arguments

Require Export substitution.

Section Modal_formulas.

  Variable V : Type.
  Variable L : modal_operators.

need a decidable equality on propositional constants for some results
  Variable v_eq : eq_type V.

Simple modal sequents


  Definition simple_modal_form(f : lambda_formula V L) : Prop :=
    match f with
      | lf_modal op argsevery_nth prop_form (list_of_counted_list args)
      | _False
    end.

  Definition simple_modal_sequent(s : sequent V L) : Prop :=
    every_nth (neg_form_maybe simple_modal_form) s.

  Lemma simple_modal_sequent_empty : simple_modal_sequent [].

  Lemma simple_modal_sequent_append :
    (s1 s2 : sequent V L),
      simple_modal_sequent s1
      simple_modal_sequent s2
        simple_modal_sequent (s1 ++ s2).

  Lemma simple_modal_sequent_append_left :
    (s1 s2 : sequent V L),
      simple_modal_sequent (s1 ++ s2) → simple_modal_sequent s1.

  Lemma simple_modal_sequent_append_right :
    (s1 s2 : sequent V L),
      simple_modal_sequent (s1 ++ s2) → simple_modal_sequent s2.

  Lemma simple_modal_sequent_cons :
    (f : lambda_formula V L)(s : sequent V L),
      neg_form_maybe simple_modal_form f
      simple_modal_sequent s
        simple_modal_sequent (f :: s).

  Lemma simple_modal_sequent_head :
    (f : lambda_formula V L)(s : sequent V L),
      simple_modal_sequent (f :: s) → neg_form_maybe simple_modal_form f.

  Lemma simple_modal_sequent_tail :
    (f : lambda_formula V L)(s : sequent V L),
      simple_modal_sequent (f :: s) → simple_modal_sequent s.

  Lemma simple_modal_sequent_list_reorder : (s1 s2 : sequent V L),
    list_reorder s1 s2
    simple_modal_sequent s1
      simple_modal_sequent s2.

  Lemma simple_modal_sequent_cutout_nth : (s : sequent V L)(n : nat),
    simple_modal_sequent ssimple_modal_sequent (cutout_nth s n).

Rank of simple modal formulas/sequents


  Lemma rank_formula_simple_modal_form :
    (f : lambda_formula V L),
      simple_modal_form f
        rank_formula 2 f.

  Lemma rank_simple_modal_sequent : (s : sequent V L),
    simple_modal_sequent srank_sequent 2 s.

  Lemma minimal_rank_simple_modal_sequent :
    (n : nat)(s : sequent V L),
      s []
      simple_modal_sequent s
      rank_sequent n s
        1 < n.

  Lemma rank_sequent_subst_simple_modal_sequent :
    (s : sequent V L)(sigma : lambda_subst V L)(n : nat),
      simple_modal_sequent s
      1 < n
      rank_subst (pred n) sigma
        rank_sequent n (subst_sequent sigma s).

  Lemma rank_subst_limit_simple_modal_form :
    (n : nat)(v : V)(sigma : lambda_subst V L)(f : lambda_formula V L),
      neg_form_maybe simple_modal_form f
      In v (prop_var_formula f) →
      rank_formula n (subst_form sigma f) →
        rank_formula (pred n) (sigma v).

  Lemma rank_subst_limit_subst_rule :
    (n : nat)(s : sequent V L)(sigma : lambda_subst V L),
      s []
      simple_modal_sequent s
      rank_sequent n (subst_sequent sigma s) →
        rank_subst (pred n) (limit_subst v_eq (prop_var_sequent s) sigma).

Lift injective substitutions to simple modal formulas


  Lemma injective_subst_prop_form :
    (sigma : lambda_subst V L)(f1 f2 : lambda_formula V L),
      injective sigma
      prop_form f1
      prop_form f2
      subst_form sigma f1 = subst_form sigma f2
        f1 = f2.

  Lemma injective_subst_simple_modal :
    (sigma : lambda_subst V L)(f1 f2 : lambda_formula V L),
      injective sigma
      simple_modal_form f1
      simple_modal_form f2
      subst_form sigma f1 = subst_form sigma f2
        f1 = f2.

  Lemma injective_subst_neg_simple_modal :
    (sigma : lambda_subst V L)(f1 f2 : lambda_formula V L),
      injective sigma
      neg_form_maybe simple_modal_form f1
      neg_form_maybe simple_modal_form f2
      subst_form sigma f1 = subst_form sigma f2
        f1 = f2.

Separete negated and unnegated formulas in simple modal sequents

This is needed for one-step-completeness of K.

  Lemma simple_modal_sequent_partition : (s : sequent V L),
    simple_modal_sequent s
    (ms ns : sequent V L),
      every_nth neg_form ns
      every_nth simple_modal_form ms
      list_reorder s (ms ++ ns).

Prop(Lambda(V))


  Definition prop_modal_prop(f : lambda_formula V L) : Prop :=
    neg_and_over simple_modal_form f.

  Lemma prop_modal_prop_lambda_or :
    (f1 f2 : lambda_formula V L),
      prop_modal_prop f1
      prop_modal_prop f2
        prop_modal_prop (lambda_or f1 f2).

  Lemma prop_modal_prop_tcc_prop : {X : Type}(v : V),
    prop_modal_prop (lf_prop v) → X.

  Lemma prop_modal_prop_tcc_neg : (f : lambda_formula V L),
    prop_modal_prop (lf_neg f) → prop_modal_prop f.

  Lemma prop_modal_prop_tcc_and_1 : (f1 f2 : lambda_formula V L),
    prop_modal_prop (lf_and f1 f2) → prop_modal_prop f1.

  Lemma prop_modal_prop_tcc_and_2 : (f1 f2 : lambda_formula V L),
    prop_modal_prop (lf_and f1 f2) → prop_modal_prop f2.

  Lemma prop_modal_prop_tcc_modal :
    (op : operator L)
          (args : counted_list (lambda_formula V L) (arity L op)),
      prop_modal_prop (lf_modal op args) →
        every_nth prop_form (list_of_counted_list args).

  Lemma rank_formula_prop_modal_prop : (f : lambda_formula V L),
    prop_modal_prop f
      rank_formula 2 f.

  Lemma simple_modal_form_is_prop_modal_prop :
    (f : lambda_formula V L),
      neg_form_maybe simple_modal_form fprop_modal_prop f.

  Definition prop_modal_prop_sequent(s : sequent V L) : Prop :=
    every_nth prop_modal_prop s.

  Lemma prop_modal_prop_sequent_append_left :
    (s1 s2 : sequent V L),
      prop_modal_prop_sequent (s1 ++ s2) → prop_modal_prop_sequent s1.

  Lemma prop_modal_prop_sequent_append_right :
    (s1 s2 : sequent V L),
      prop_modal_prop_sequent (s1 ++ s2) → prop_modal_prop_sequent s2.

  Lemma prop_modal_prop_sequent_cons :
    (f : lambda_formula V L)(s : sequent V L),
      prop_modal_prop f
      prop_modal_prop_sequent s
        prop_modal_prop_sequent (f :: s).

  Lemma prop_modal_prop_sequent_head :
    (f : lambda_formula V L)(s : sequent V L),
      prop_modal_prop_sequent (f :: s) → prop_modal_prop f.

  Lemma prop_modal_prop_sequent_tail :
    (f : lambda_formula V L)(s : sequent V L),
      prop_modal_prop_sequent (f :: s) → prop_modal_prop_sequent s.

  Lemma prop_modal_prop_or_formula_iter :
    (f : lambda_formula V L)(s : sequent V L),
      prop_modal_prop_sequent (f :: s) →
        prop_modal_prop (or_formula_of_sequent_iter f s).

  Lemma prop_modal_prop_or_formula :
    (s : sequent V L)(nonempty_s : s []),
      prop_modal_prop_sequent s
        prop_modal_prop (or_formula_of_ne_sequent s nonempty_s).

  Lemma simple_modal_sequent_is_prop_modal_prop :
    (s : sequent V L),
      simple_modal_sequent sprop_modal_prop_sequent s.

  Lemma rank_sequent_prop_modal_prop_sequent :
    (s : sequent V L),
      prop_modal_prop_sequent s
        rank_sequent 2 s.

Prop(Lambda(S))


  Definition modal_form(f : lambda_formula V L) : Prop :=
    match f with
      | lf_modal _ _True
      | _False
    end.

  Definition prop_modal(f : lambda_formula V L) : Prop :=
    neg_and_over modal_form f.

  Definition prop_modal_sequent(s : sequent V L) : Prop :=
    every_nth prop_modal s.

  Lemma prop_modal_sequent_cons :
    (f : lambda_formula V L)(s : sequent V L),
      prop_modal f
      prop_modal_sequent s
        prop_modal_sequent (f :: s).

  Lemma prop_modal_sequent_head :
    (f : lambda_formula V L)(s : sequent V L),
      prop_modal_sequent (f :: s) → prop_modal f.

  Lemma prop_modal_sequent_tail :
    (f : lambda_formula V L)(s : sequent V L),
      prop_modal_sequent (f :: s) → prop_modal_sequent s.

Top modal sequents


  Definition top_modal_form(f : lambda_formula V L) : Prop :=
    neg_form_maybe modal_form f.

  Lemma top_modal_is_prop_modal : (f : lambda_formula V L),
    top_modal_form fprop_modal f.

  Lemma top_modal_form_lf_neg : (f : lambda_formula V L),
    top_modal_form (lf_neg f) → top_modal_form f.

  Lemma top_modal_not_neg_prop : (f : lambda_formula V L),
    top_modal_form f¬ neg_form_maybe prop_form f.

  Lemma top_modal_not_prop : (f : lambda_formula V L),
    top_modal_form f¬ prop_form f.

  Definition top_modal_sequent(s : sequent V L) : Prop :=
    every_nth top_modal_form s.

  Lemma top_modal_sequent_list_reorder : (s1 s2 : sequent V L),
    list_reorder s1 s2
    top_modal_sequent s2
      top_modal_sequent s1.

  Lemma top_modal_is_prop_modal_sequent : (s : sequent V L),
    top_modal_sequent sprop_modal_sequent s.

  Lemma top_modal_sequent_tail :
    (f : lambda_formula V L)(s : sequent V L),
      top_modal_sequent (f :: s) → top_modal_sequent s.

  Lemma top_modal_sequent_head :
    (f : lambda_formula V L)(s : sequent V L),
      top_modal_sequent (f :: s) → top_modal_form f.

End Modal_formulas.

Implicit Arguments prop_modal_prop [[V] [L]].
Implicit Arguments prop_modal_prop_lambda_or [V L].
Implicit Arguments prop_modal_prop_tcc_prop [V L X].
Implicit Arguments prop_modal_prop_tcc_neg [V L].
Implicit Arguments prop_modal_prop_tcc_and_1 [V L].
Implicit Arguments prop_modal_prop_tcc_and_2 [V L].
Implicit Arguments prop_modal_prop_tcc_modal [V L].
Implicit Arguments prop_modal_prop_sequent [V L].
Implicit Arguments prop_modal_prop_sequent_append_left [V L].
Implicit Arguments prop_modal_prop_sequent_append_right [V L].
Implicit Arguments prop_modal_prop_sequent_head [V L].
Implicit Arguments prop_modal_prop_sequent_tail [V L].
Implicit Arguments prop_modal_prop_or_formula [V L].
Implicit Arguments simple_modal_sequent_is_prop_modal_prop [V L].
Implicit Arguments modal_form [[V] [L]].
Implicit Arguments prop_modal_sequent [V L].
Implicit Arguments top_modal_form [V L].
Implicit Arguments top_modal_sequent [V L].
Implicit Arguments simple_modal_form [[V] [L]].
Implicit Arguments simple_modal_sequent [V L].
Implicit Arguments simple_modal_sequent_append_left [V L].
Implicit Arguments simple_modal_sequent_append_right [V L].
Implicit Arguments simple_modal_sequent_head [V L].
Implicit Arguments simple_modal_sequent_tail [V L].
Implicit Arguments simple_modal_sequent_list_reorder [V L].
Implicit Arguments injective_subst_neg_simple_modal [V L].