Admissible rules

This module defines the concept of an admissible rule and generlizes it to sets of rules.

Require Export rules.

Section Admissibility.

  Variable V : Type.
  Variable L : modal_operators.

  Variable rules : set (sequent_rule V L).
  Variable hypotheses : set (sequent V L).

admissibility, not depth preserving

  Definition admissible(r : sequent_rule V L) : Prop :=
    every_nth (provable rules hypotheses) (assumptions r) →
      provable rules hypotheses (conclusion r).

  Definition admissible_rule_set(rs : set (sequent_rule V L)) : Prop :=
    (r : sequent_rule V L), rs radmissible r.

  Lemma admissible_prop :
    (rs : set (sequent_rule V L))(s : sequent V L),
      admissible_rule_set rs
        (provable rules hypotheses s
           provable (union rs rules) hypotheses s).

admissibility, depth preserving

  Definition depth_preserving_admissible(r : sequent_rule V L) : Prop :=
    (n : nat),
      every_nth (provable_at_depth rules hypotheses n) (assumptions r) →
        provable_at_depth rules hypotheses n (conclusion r).

  Definition depth_preserving_admissible_rule_set
                                       (rs : set (sequent_rule V L)) : Prop :=
    (r : sequent_rule V L), rs r
      depth_preserving_admissible r.

  Lemma admissible_depth_preserving_admissible :
    (rs : set (sequent_rule V L)),
      depth_preserving_admissible_rule_set rsadmissible_rule_set rs.

  Lemma delete_depth_admissible_rule :
    (r : sequent_rule V L)(n : nat)(s : sequent V L),
      depth_preserving_admissible r
      provable_at_depth (add r rules) hypotheses n s
        provable_at_depth rules hypotheses n s.

  Lemma depth_admissible_prop :
    (r : sequent_rule V L)(s : sequent V L)(n : nat),
      depth_preserving_admissible r
        (provable_at_depth rules hypotheses n s
           provable_at_depth (add r rules) hypotheses n s).

End Admissibility.

Implicit Arguments admissible [V L].
Implicit Arguments admissible_rule_set [V L].
Implicit Arguments depth_preserving_admissible [V L].
Implicit Arguments depth_preserving_admissible_rule_set [V L].