Admissible 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).
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 r → admissible 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).
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 rs → admissible_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].