Completeness and semantic cut elimination, Section 4

Non-decomposable formulas

In the proof of 4.13, there appears a set of formulas that cannot be decomposed by the propositional rules. These formulas are either possibly negated propsitional variables or possibly negated modal formulas. Note the similarity with plain_prop_mod.

Require Export dsets build_prop_proof.

Section Prop_mod.

  Variable V : Type.
  Variable L : modal_operators.

Need a decidable equality on propositional constants for the properties on the proof built oracle.
  Variable v_eq : eq_type V.

non-decomposable formulas

See also neg_form for the Prop version.
  Definition dneg_form_maybe(F : dset (lambda_formula V L))
                                                : dset (lambda_formula V L) :=
    fun(f : lambda_formula V L) ⇒
      match f with
        | lf_neg fF f
        | _F f

  Definition dprop_or_mod_formula : dset (lambda_formula V L) :=
    dunion (dneg_form_maybe is_prop) (dneg_form_maybe is_modal).

  Definition dprop_or_mod_sequent : dset (sequent V L) :=
    forallb dprop_or_mod_formula.

As Prop sets

Prop oracle properties

Partition prop-mod sequents

  Lemma prop_or_mod_partition : (s : sequent V L),
    prop_or_mod_sequent s
      (prop_s mod_s : sequent V L),
        prop_sequent prop_s
        top_modal_sequent mod_s
        list_reorder s (mod_s ++ prop_s).

End Prop_mod.

Implicit Arguments dprop_or_mod_sequent [V L].
Implicit Arguments prop_or_mod_sequent_prop [V L].
Implicit Arguments prop_or_mod_partition [V L].