Abstract sequent semantics
Correctness of simplified some_neg_dep semantics I
This is the dependent version for nonempty sequentsSection Some_neg_dep_form.
Variable V : Type.
Variable L : modal_operators.
Variable form_prop : lambda_formula V L → Prop.
Variable P : ∀(f : lambda_formula V L), form_prop f → Prop.
Definition sequent_prop(s : sequent V L) : Prop := a_list_prop form_prop s.
First hypothesis: well-formedness of formulas is closed under
disjunction.
Hypothesis form_prop_or :
∀(f1 f2 : lambda_formula V L),
form_prop f1 → form_prop f2 → form_prop (lambda_or f1 f2).
∀(f1 f2 : lambda_formula V L),
form_prop f1 → form_prop f2 → form_prop (lambda_or f1 f2).
This is more a parameter than an hypothesis. It declares the
function that converts a proof for the well-formedness of a
sequent into the well-formdness of its disjunction. This
function is needed for the main statement below and will get
instantiated.
Hypothesis form_prop_or_formula_of_sequent_iter :
∀(f : lambda_formula V L)(s : sequent V L),
sequent_prop (f :: s) →
form_prop (or_formula_of_sequent_iter f s).
∀(f : lambda_formula V L)(s : sequent V L),
sequent_prop (f :: s) →
form_prop (or_formula_of_sequent_iter f s).
Second hypothesis: The well-formedness argument is irrelevant
for the formula semantics.
Third hypothesis: The formula semantics is closed under
disjunction.
Hypothesis P_or_formula :
∀(f1 f2 : lambda_formula V L)(tf1 : form_prop f1)(tf2 : form_prop f2),
P (lambda_or f1 f2) (form_prop_or f1 f2 tf1 tf2)
↔ ~(~P f1 tf1 ∧ ¬P f2 tf2).
Lemma a_list_prop_first_or :
∀(f1 f2 f3 : lambda_formula V L)(s : sequent V L),
sequent_prop (f1 :: f2 :: f3 :: s) →
sequent_prop ((lambda_or f1 f2) :: f3 :: s).
Lemma p_or_formula_of_sequent_iter :
∀(s : sequent V L)(f1 f2 : lambda_formula V L)
(t_f_s : sequent_prop (f1 :: f2 :: s)),
P (or_formula_of_sequent_iter f1 (f2 :: s))
(form_prop_or_formula_of_sequent_iter f1 (f2 :: s) t_f_s)
↔
~(~P f1 (a_list_prop_head t_f_s) ∧
¬P (or_formula_of_sequent_iter f2 s)
(form_prop_or_formula_of_sequent_iter f2 s
(a_list_prop_tail t_f_s))).
Lemma some_neg_dep_cons_correct :
∀(s : sequent V L)(f : lambda_formula V L)
(dep_s : sequent_prop (f :: s)),
some_neg_dep form_prop P (f :: s) dep_s ↔
P (or_formula_of_sequent_iter f s)
(form_prop_or_formula_of_sequent_iter f s dep_s).
End Some_neg_dep_form.
Implicit Arguments sequent_prop [V L].
∀(f1 f2 : lambda_formula V L)(tf1 : form_prop f1)(tf2 : form_prop f2),
P (lambda_or f1 f2) (form_prop_or f1 f2 tf1 tf2)
↔ ~(~P f1 tf1 ∧ ¬P f2 tf2).
Lemma a_list_prop_first_or :
∀(f1 f2 f3 : lambda_formula V L)(s : sequent V L),
sequent_prop (f1 :: f2 :: f3 :: s) →
sequent_prop ((lambda_or f1 f2) :: f3 :: s).
Lemma p_or_formula_of_sequent_iter :
∀(s : sequent V L)(f1 f2 : lambda_formula V L)
(t_f_s : sequent_prop (f1 :: f2 :: s)),
P (or_formula_of_sequent_iter f1 (f2 :: s))
(form_prop_or_formula_of_sequent_iter f1 (f2 :: s) t_f_s)
↔
~(~P f1 (a_list_prop_head t_f_s) ∧
¬P (or_formula_of_sequent_iter f2 s)
(form_prop_or_formula_of_sequent_iter f2 s
(a_list_prop_tail t_f_s))).
Lemma some_neg_dep_cons_correct :
∀(s : sequent V L)(f : lambda_formula V L)
(dep_s : sequent_prop (f :: s)),
some_neg_dep form_prop P (f :: s) dep_s ↔
P (or_formula_of_sequent_iter f s)
(form_prop_or_formula_of_sequent_iter f s dep_s).
End Some_neg_dep_form.
Implicit Arguments sequent_prop [V L].
Correctness of simplified some_neg_dep semantics II
This is the dependent version for possibly empty sequentsSection Some_neg_dep_form_2.
Variable V : Type.
Variable L : modal_operators.
Variable form_prop : lambda_formula V L → Prop.
Variable P : ∀(f : lambda_formula V L), form_prop f → Prop.
first hypothesis
Hypothesis form_prop_or :
∀(f1 f2 : lambda_formula V L),
form_prop f1 → form_prop f2 → form_prop (lambda_or f1 f2).
∀(f1 f2 : lambda_formula V L),
form_prop f1 → form_prop f2 → form_prop (lambda_or f1 f2).
Declaration of the well-formedness proof conversion function
Hypothesis form_prop_or_formula_of_sequent :
∀(nonempty_v : V)(s : sequent V L),
sequent_prop form_prop s →
form_prop (or_formula_of_sequent s nonempty_v).
∀(nonempty_v : V)(s : sequent V L),
sequent_prop form_prop s →
form_prop (or_formula_of_sequent s nonempty_v).
second hypothesis
third hypothesis
Hypothesis P_or_formula :
∀(f1 f2 : lambda_formula V L)(tf1 : form_prop f1)(tf2 : form_prop f2),
P (lambda_or f1 f2) (form_prop_or f1 f2 tf1 tf2)
↔ ~(~P f1 tf1 ∧ ¬P f2 tf2).
∀(f1 f2 : lambda_formula V L)(tf1 : form_prop f1)(tf2 : form_prop f2),
P (lambda_or f1 f2) (form_prop_or f1 f2 tf1 tf2)
↔ ~(~P f1 tf1 ∧ ¬P f2 tf2).
Fourth hypothesis: The formula semantics is false for false.
Hypothesis P_false :
∀(nonempty_v : V)(t_false : form_prop (lambda_false nonempty_v)),
P (lambda_false nonempty_v) t_false → False.
Lemma form_prop_or_formula_of_sequent_iter :
∀(nonempty_v : V)(f : lambda_formula V L)(s : sequent V L),
sequent_prop form_prop (f :: s) →
form_prop (or_formula_of_sequent_iter f s).
Lemma some_neg_dep_correct :
∀(nonempty_v : V)(s : sequent V L)(dep_s : sequent_prop form_prop s),
some_neg_dep form_prop P s dep_s ↔
P (or_formula_of_sequent s nonempty_v)
(form_prop_or_formula_of_sequent nonempty_v s dep_s).
End Some_neg_dep_form_2.
Section Some_neg_form.
∀(nonempty_v : V)(t_false : form_prop (lambda_false nonempty_v)),
P (lambda_false nonempty_v) t_false → False.
Lemma form_prop_or_formula_of_sequent_iter :
∀(nonempty_v : V)(f : lambda_formula V L)(s : sequent V L),
sequent_prop form_prop (f :: s) →
form_prop (or_formula_of_sequent_iter f s).
Lemma some_neg_dep_correct :
∀(nonempty_v : V)(s : sequent V L)(dep_s : sequent_prop form_prop s),
some_neg_dep form_prop P s dep_s ↔
P (or_formula_of_sequent s nonempty_v)
(form_prop_or_formula_of_sequent nonempty_v s dep_s).
End Some_neg_dep_form_2.
Section Some_neg_form.
Correctness of simplified some_neg semantics
This is the simple (non-dependent) version for arbitrary sequents.
There remain only two hypothesis for the simple version.
Hypothesis P_false :
∀(nonempty_v : V),
P (lambda_false nonempty_v) → False.
Hypothesis P_or_formula : ∀(f1 f2 : lambda_formula V L),
P (lambda_or f1 f2) ↔ ~(~P f1 ∧ ¬P f2).
Lemma noprop_or : ∀(f1 f2 : lambda_formula V L),
noprop (lambda_formula V L) f1 →
noprop (lambda_formula V L) f2 →
noprop (lambda_formula V L) (lambda_or f1 f2).
Lemma noprop_or_formula_of_sequnet :
∀(nonempty_v : V)(s : sequent V L),
a_list_prop (noprop (lambda_formula V L)) s →
noprop (lambda_formula V L) (or_formula_of_sequent s nonempty_v).
Lemma some_neg_correct :
∀(nonempty_v : V)(s : sequent V L),
some_neg P s ↔ P (or_formula_of_sequent s nonempty_v).
End Some_neg_form.
∀(nonempty_v : V),
P (lambda_false nonempty_v) → False.
Hypothesis P_or_formula : ∀(f1 f2 : lambda_formula V L),
P (lambda_or f1 f2) ↔ ~(~P f1 ∧ ¬P f2).
Lemma noprop_or : ∀(f1 f2 : lambda_formula V L),
noprop (lambda_formula V L) f1 →
noprop (lambda_formula V L) f2 →
noprop (lambda_formula V L) (lambda_or f1 f2).
Lemma noprop_or_formula_of_sequnet :
∀(nonempty_v : V)(s : sequent V L),
a_list_prop (noprop (lambda_formula V L)) s →
noprop (lambda_formula V L) (or_formula_of_sequent s nonempty_v).
Lemma some_neg_correct :
∀(nonempty_v : V)(s : sequent V L),
some_neg P s ↔ P (or_formula_of_sequent s nonempty_v).
End Some_neg_form.