Syntactic properties of propositional logic
Require Export propositional_rules generic_cut inversion.
Section Propositional_properties.
Variable V : Type.
Variable L : modal_operators.
Lemma G_non_atomic_axiom_head :
∀(hyp : set (sequent V L))(f : lambda_formula V L)(s : sequent V L),
sequent_multiset hyp →
propositional f →
propositional_sequent s →
provable (prop_G_set V L) hyp (f :: lf_neg f :: s).
Definition head_contraction_closed(ss : set (sequent V L)) : Prop :=
∀(f : lambda_formula V L)(s : sequent V L),
ss (f :: f :: s) → ss (f :: s).
Lemma head_contraction_closed_empty :
head_contraction_closed (empty_sequent_set V L).
Lemma G_n_contraction_head_ax :
∀(hyp : set (sequent V L))
(n d : nat)(f : lambda_formula V L)(s : sequent V L),
simple_tautology (f :: f :: s) →
rank_sequent n (f :: f :: s) →
provable_at_depth (G_n_set V L n) hyp (S d) (f :: s).
Lemma G_n_contraction_and_assumptions_head :
∀(hyp : set (sequent V L))(n d : nat)(f g1 g2 : lambda_formula V L)
(s : sequent V L)(br : sequent_rule V L)
(subproofs : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
(map (add_context [f] s) (assumptions br))),
conj_head_inversion_closed hyp →
(∀(s : sequent V L),
provable_at_depth (G_n_set V L n) hyp d s →
∀(s_tl : sequent V L)(f : lambda_formula V L),
s = f :: f :: s_tl →
provable_at_depth (G_n_set V L n) hyp d (f :: s_tl)) →
br = bare_and_rule g1 g2 →
[f] = conclusion br →
every_dep_nth
(fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
proof_depth p ≤ d)
(map (add_context [f] s) (assumptions br))
subproofs →
every_nth (provable_at_depth (G_n_set V L n) hyp d)
(map (add_context [] s) (assumptions br)).
Lemma G_n_contraction_neg_and_assumptions_head :
∀(hyp : set (sequent V L))(n d : nat)(f g1 g2 : lambda_formula V L)
(s : sequent V L)(br : sequent_rule V L)
(subproofs : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
(map (add_context [f] s) (assumptions br))),
sequent_multiset hyp →
disj_head_inversion_closed hyp →
(∀(s : sequent V L),
provable_at_depth (G_n_set V L n) hyp d s →
∀(s_tl : sequent V L)(f : lambda_formula V L),
s = f :: f :: s_tl →
provable_at_depth (G_n_set V L n) hyp d (f :: s_tl)) →
br = bare_neg_and_rule g1 g2 →
[f] = conclusion br →
every_dep_nth
(fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
proof_depth p ≤ d)
(map (add_context [f] s) (assumptions br)) subproofs →
every_nth (provable_at_depth (G_n_set V L n) hyp d)
(map (add_context [] s) (assumptions br)).
Lemma G_n_contraction_neg_neg_assumptions_head :
∀(hyp : set (sequent V L))(n d : nat)(f g : lambda_formula V L)
(s : sequent V L)(br : sequent_rule V L)
(subproofs : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
(map (add_context [f] s) (assumptions br))),
neg_head_inversion_closed hyp →
(∀(s : sequent V L),
provable_at_depth (G_n_set V L n) hyp d s →
∀(s_tl : sequent V L)(f : lambda_formula V L),
s = f :: f :: s_tl →
provable_at_depth (G_n_set V L n) hyp d (f :: s_tl)) →
br = bare_neg_neg_rule g →
[f] = conclusion br →
every_dep_nth
(fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
proof_depth p ≤ d)
(map (add_context [f] s) (assumptions br)) subproofs →
every_nth (provable_at_depth (G_n_set V L n) hyp d)
(map (add_context [] s) (assumptions br)).
Lemma G_n_contraction_head :
∀(hyp : set (sequent V L))(n : nat)
(f : lambda_formula V L)(s : sequent V L),
sequent_multiset hyp →
head_inversion_closed hyp →
head_contraction_closed hyp →
provable (G_n_set V L n) hyp (f :: f :: s) →
provable (G_n_set V L n) hyp (f :: s).
Lemma prop_contraction_head :
∀(f : lambda_formula V L)(s : sequent V L),
provable (prop_G_set V L) (empty_sequent_set V L) (f :: f :: s) →
provable (prop_G_set V L) (empty_sequent_set V L) (f :: s).
Lemma G_n_hyp_list_contraction_left :
∀(n : nat)(hyp : set (sequent V L))(r s : sequent V L),
sequent_multiset hyp →
head_inversion_closed hyp →
head_contraction_closed hyp →
provable (G_n_set V L n) hyp (r ++ r ++ s) →
provable (G_n_set V L n) hyp (r ++ s).
Lemma G_n_cut_elim_head_ax :
∀(n : nat)(hyp : set (sequent V L))
(f : lambda_formula V L)(q r : sequent V L),
rank_sequent_set n hyp →
sequent_multiset hyp →
bounded_weakening_closed n hyp →
neg_head_inversion_closed hyp →
rank_sequent n q →
simple_tautology (f :: q) →
provable (G_n_set V L n) hyp ((lf_neg f) :: r) →
provable (G_n_set V L n) hyp (q ++ r).
Lemma G_n_cut_elim_head_and_inside :
∀(n m d : nat)(hyp : set (sequent V L))
(f g1 g2 : lambda_formula V L)(r q : sequent V L)
(brule : sequent_rule V L),
sequent_multiset hyp →
head_inversion_closed hyp →
head_contraction_closed hyp →
(∀(f : lambda_formula V L)(q r : sequent V L),
formula_measure f < m →
provable (G_n_set V L n) hyp (f :: q) →
provable (G_n_set V L n) hyp (lf_neg f :: r) →
provable (G_n_set V L n) hyp (q ++ r)) →
formula_measure f < S m →
provable (G_n_set V L n) hyp (lf_neg f :: r) →
every_nth (provable (G_n_set V L n) hyp)
(map (add_context [] q) (assumptions brule)) →
brule = bare_and_rule g1 g2 →
[f] = conclusion brule →
provable (G_n_set V L n) hyp (q ++ r).
Lemma G_n_cut_elim_head_neg_and_inside :
∀(n m : nat)(hyp : set (sequent V L))
(f g1 g2 : lambda_formula V L)(r q : sequent V L)
(brule : sequent_rule V L),
sequent_multiset hyp →
head_inversion_closed hyp →
(∀(f : lambda_formula V L)(q r : sequent V L),
formula_measure f < m →
provable (G_n_set V L n) hyp (f :: q) →
provable (G_n_set V L n) hyp (lf_neg f :: r) →
provable (G_n_set V L n) hyp (q ++ r)) →
formula_measure f < S m →
provable (G_n_set V L n) hyp (f :: q) →
provable (G_n_set V L n) hyp (lf_neg f :: r) →
brule = bare_neg_and_rule g1 g2 →
[f] = conclusion brule →
provable (G_n_set V L n) hyp (q ++ r).
Lemma G_n_cut_elim_head_neg_neg_inside :
∀(n m : nat)(hyp : set (sequent V L))
(f : lambda_formula V L)(r q : sequent V L),
sequent_multiset hyp →
head_inversion_closed hyp →
(∀(f : lambda_formula V L)(q r : sequent V L),
formula_measure f < m →
provable (G_n_set V L n) hyp (f :: q) →
provable (G_n_set V L n) hyp (lf_neg f :: r) →
provable (G_n_set V L n) hyp (q ++ r)) →
formula_measure (lf_neg f) < S m →
provable (G_n_set V L n) hyp (lf_neg f :: q) →
provable (G_n_set V L n) hyp (lf_neg (lf_neg f) :: r) →
provable (G_n_set V L n) hyp (q ++ r).
Lemma G_n_cut_elim_head_and_outside :
∀(n d : nat)(hyp : set (sequent V L))
(f1 f2 g1 g2 : lambda_formula V L)(sl sr r : sequent V L)
(brule : sequent_rule V L),
(∀(q : sequent V L),
provable_at_depth (G_n_set V L n) hyp d (f1 :: q) →
provable (G_n_set V L n) hyp (q ++ r)) →
provable (G_n_set V L n) hyp (f2 :: r) →
every_nth (provable_at_depth (G_n_set V L n) hyp d)
(map (add_context (f1 :: sl) sr) (assumptions brule)) →
brule = bare_and_rule g1 g2 →
every_nth (provable (G_n_set V L n) hyp)
(map (add_context sl (sr ++ r)) (assumptions brule)).
Lemma G_n_cut_elim_head_neg_and_outside :
∀(n d : nat)(hyp : set (sequent V L))
(f1 f2 g1 g2 : lambda_formula V L)(sl sr r : sequent V L)
(brule : sequent_rule V L),
(∀(q : sequent V L),
provable_at_depth (G_n_set V L n) hyp d (f1 :: q) →
provable (G_n_set V L n) hyp (q ++ r)) →
provable (G_n_set V L n) hyp (f2 :: r) →
every_nth (provable_at_depth (G_n_set V L n) hyp d)
(map (add_context (f1 :: sl) sr) (assumptions brule)) →
brule = bare_neg_and_rule g1 g2 →
every_nth (provable (G_n_set V L n) hyp)
(map (add_context sl (sr ++ r)) (assumptions brule)).
Lemma G_n_cut_elim_head_neg_neg_outside :
∀(n d : nat)(hyp : set (sequent V L))
(f1 f2 g : lambda_formula V L)(sl sr r : sequent V L)
(brule : sequent_rule V L),
(∀(q : sequent V L),
provable_at_depth (G_n_set V L n) hyp d (f1 :: q) →
provable (G_n_set V L n) hyp (q ++ r)) →
provable (G_n_set V L n) hyp (f2 :: r) →
every_nth (provable_at_depth (G_n_set V L n) hyp d)
(map (add_context (f1 :: sl) sr) (assumptions brule)) →
brule = bare_neg_neg_rule g →
every_nth (provable (G_n_set V L n) hyp)
(map (add_context sl (sr ++ r)) (assumptions brule)).
Lemma prop_G_cut_elim_head_ind :
∀(n : nat)(f : lambda_formula V L)(q r : sequent V L),
formula_measure f < n →
provable (prop_G_set V L) (empty_sequent_set V L) (f :: q) →
provable (prop_G_set V L) (empty_sequent_set V L) ((lf_neg f) :: r) →
provable (prop_G_set V L) (empty_sequent_set V L) (q ++ r).
Lemma prop_G_cut_elim_head :
∀(f : lambda_formula V L)(q r : sequent V L),
provable (prop_G_set V L) (empty_sequent_set V L) (f :: q) →
provable (prop_G_set V L) (empty_sequent_set V L) ((lf_neg f) :: r) →
provable (prop_G_set V L) (empty_sequent_set V L) (q ++ r).
Lemma admissible_bounded_cut_prop_G :
admissible_rule_set (prop_G_set V L) (empty_sequent_set V L)
(bounded_cut_rules V L 1).
Lemma provable_GC_1_G_1 : ∀(s : sequent V L),
provable (GC_n_set V L 1) (empty_sequent_set V L) s →
provable (G_n_set V L 1) (empty_sequent_set V L) s.
Lemma provable_GRC_1_GR_1 :
∀(rules : set (sequent_rule V L))(s : sequent V L),
one_step_rule_set rules →
provable (GRC_n_set rules 1) (empty_sequent_set V L) s →
provable (GR_n_set rules 1) (empty_sequent_set V L) s.
Lemma propositional_cut_contraction_weakening :
∀(hyp : set (sequent V L))(os cs : sequent V L),
sequent_multiset hyp →
rank_sequent_set 1 hyp →
incl os cs →
os ≠ [] →
propositional_sequent cs →
provable (prop_GC_set V L) hyp os →
provable (prop_GC_set V L) hyp cs.
End Propositional_properties.
Implicit Arguments head_contraction_closed [V L].