GRC Properties 3.14 - 3.15
Require Export admissibility rule_sets.
Section Cut_properties.
Variable V : Type.
Variable L : modal_operators.
Towards the substitution Lemma 3.14
Lemma generic_substitution_lemma :
∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
(sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
subst_closed_rule_set rules →
rank_sequent_set n hypothesis →
rank_subst (S k) sigma →
provable (rank_rules n (union is_ax_rule rules)) hypothesis gamma →
provable (rank_rules (n + k) (union is_ax_rule rules))
(union (subst_Ax_n_set sigma (n + k))
(subst_sequent_set sigma hypothesis))
(subst_sequent sigma gamma).
Lemma GRC_n_substitution_lemma :
∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
(sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
one_step_rule_set rules →
rank_sequent_set n hypothesis →
rank_subst (S k) sigma →
provable (GRC_n_set rules n) hypothesis gamma →
provable (GRC_n_set rules (n + k))
(union (subst_Ax_n_set sigma (n + k))
(subst_sequent_set sigma hypothesis))
(subst_sequent sigma gamma).
∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
(sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
one_step_rule_set rules →
rank_sequent_set n hypothesis →
rank_subst (S k) sigma →
provable (GRC_n_set rules n) hypothesis gamma →
provable (GRC_n_set rules (n + k))
(union (subst_Ax_n_set sigma (n + k))
(subst_sequent_set sigma hypothesis))
(subst_sequent sigma gamma).
Lemma GR_n_substitution_lemma :
∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
(sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
one_step_rule_set rules →
rank_sequent_set n hypothesis →
rank_subst (S k) sigma →
provable (GR_n_set rules n) hypothesis gamma →
provable (GR_n_set rules (n + k))
(union (subst_Ax_n_set sigma (n + k))
(subst_sequent_set sigma hypothesis))
(subst_sequent sigma gamma).
∀(rules : set (sequent_rule V L))(hypothesis : set (sequent V L))
(sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
one_step_rule_set rules →
rank_sequent_set n hypothesis →
rank_subst (S k) sigma →
provable (GR_n_set rules n) hypothesis gamma →
provable (GR_n_set rules (n + k))
(union (subst_Ax_n_set sigma (n + k))
(subst_sequent_set sigma hypothesis))
(subst_sequent sigma gamma).
And the variant for empty hypothesis
Lemma GR_n_substitution_lemma_empty_hyp :
∀(rules : set (sequent_rule V L))
(sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
one_step_rule_set rules →
rank_subst (S k) sigma →
provable (GR_n_set rules n) (empty_sequent_set V L) gamma →
provable (GR_n_set rules (n + k))
(subst_Ax_n_set sigma (n + k))
(subst_sequent sigma gamma).
∀(rules : set (sequent_rule V L))
(sigma : lambda_subst V L)(n k : nat)(gamma : sequent V L),
one_step_rule_set rules →
rank_subst (S k) sigma →
provable (GR_n_set rules n) (empty_sequent_set V L) gamma →
provable (GR_n_set rules (n + k))
(subst_Ax_n_set sigma (n + k))
(subst_sequent sigma gamma).
Lemma proof_minimal_proof_rank :
∀(rules : set (sequent_rule V L))(s : sequent V L)(n : nat),
∀(p : proof rules (empty_sequent_set V L) s),
minimal_proof_rank p ≤ n →
provable (rank_rules n rules) (empty_sequent_set V L) s.
Lemma rank_proof_GRC :
∀(rules : set (sequent_rule V L))(s : sequent V L),
provable (GRC_set rules) (empty_sequent_set V L) s
↔
∃(n : nat),
provable (GRC_n_set rules n) (empty_sequent_set V L) s.
∀(rules : set (sequent_rule V L))(s : sequent V L),
provable (GRC_set rules) (empty_sequent_set V L) s
↔
∃(n : nat),
provable (GRC_n_set rules n) (empty_sequent_set V L) s.