Completeness for propositional logic
Require Export classic propositional_sound build_prop_proof.
Section Propositional_Completeness.
Variable V : Type.
Variable L : modal_operators.
need a decidable equality on propositional constants for
the proof construction
Lemma simple_tautology_cons_append :
∀(v : V)(f g : lambda_formula V L)(s1 s2 : sequent V L),
(f = lf_prop v ∧ g = lf_neg (lf_prop v)) ∨
(f = lf_neg (lf_prop v) ∧ g = lf_prop v) →
simple_tautology (f :: s1 ++ g :: s2).
Definition prop_hyp_oracle :
hypotheses_oracle_type V L (empty_sequent_set V L) :=
fun _ ⇒ None.
Definition prop_build_proof(s : sequent V L) :
(proof (G_set V L) (empty_sequent_set V L) s) + (sequent V L) :=
build_proof (S (sequent_measure s))
prop_hyp_oracle (prop_G_oracle v_eq) s.
Definition prop_build_proof_prop_type(s : sequent V L) : Type :=
propositional_sequent s → prop_proof_type s.
Fixpoint apply_propositional_subproofs(sl : list (sequent V L))
(cond_subproofs : dep_list (sequent V L) prop_build_proof_prop_type sl)
(prop_subproofs : every_nth propositional_sequent sl)
: dep_list (sequent V L) prop_proof_type sl :=
match cond_subproofs
in dep_list _ _ sl
return every_nth propositional_sequent sl →
dep_list (sequent V L) prop_proof_type sl
with
| dep_nil ⇒ fun _ ⇒ dep_nil
| dep_cons s rsl prop_fun_s r_prop_funs ⇒
fun(prop_s_rsl : every_nth propositional_sequent (s :: rsl)) ⇒
dep_cons s rsl (prop_fun_s (every_nth_head _ _ _ prop_s_rsl))
(apply_propositional_subproofs rsl r_prop_funs
(every_nth_tail _ _ _ prop_s_rsl))
end prop_subproofs.
Definition prop_build_proof_prop(s : sequent V L)
(p : proof (G_set V L) (empty_sequent_set V L) s) :
prop_build_proof_prop_type s :=
proof_rect V L (G_set V L) (empty_sequent_set V L)
prop_build_proof_prop_type
(fun(gamma : sequent V L)(in_hyp : empty_sequent_set V L gamma) _ ⇒
assume (prop_G_set V L) (empty_sequent_set V L) gamma in_hyp)
(fun(r : sequent_rule V L)(in_G : G_set V L r)
(subproofs : dep_list (sequent V L)
prop_build_proof_prop_type
(assumptions r))
(prop_concl : propositional_sequent (conclusion r))
⇒
rule (prop_G_set V L) (empty_sequent_set V L) r
(G_set_prop_set r in_G prop_concl)
(apply_propositional_subproofs (assumptions r) subproofs
(const_rank_G_set 1 r in_G prop_concl)))
s p.
Definition all_true_model : prop_model V := fun _ ⇒ True.
Definition formula_counter_model(f : lambda_formula V L)
(m : prop_model V) : prop_model V :=
match f with
| lf_prop v ⇒ function_update v_eq m v False
| lf_neg (lf_prop v) ⇒ function_update v_eq m v True
| _ ⇒ m
end.
Fixpoint build_counter_model(l : sequent V L)(m : prop_model V)
: prop_model V :=
match l with
| [] ⇒ m
| f :: r ⇒ build_counter_model r (formula_counter_model f m)
end.
Lemma build_counter_model_const_v_ind :
∀(s1 s2 : sequent V L)(f : lambda_formula V L)
(m : prop_model V)(v : V),
(f = lf_prop v ∨ f = lf_neg (lf_prop v)) →
not (simple_tautology (f :: (s1 ++ s2))) →
(formula_counter_model f m v = m v) →
((build_counter_model s2 m v) = (m v)).
Lemma build_counter_model_const_v :
∀(s : sequent V L)(f : lambda_formula V L)(m : prop_model V)(v : V),
(f = lf_prop v ∨ f = lf_neg (lf_prop v)) →
not (simple_tautology (f :: s)) →
(formula_counter_model f m v = m v) →
((build_counter_model s m v) = (m v)).
Lemma formula_counter_model_correct :
∀(m : prop_model V)(f : lambda_formula V L)
(prop_f : propositional f)(s : sequent V L),
neg_form_maybe prop_form f →
¬ simple_tautology (f :: s) →
¬ is_prop_model (build_counter_model s (formula_counter_model f m))
f prop_f.
Lemma build_counter_model_correct :
∀(s : sequent V L)(prop_s : propositional_sequent s)(m : prop_model V),
prop_sequent s →
(not (simple_tautology s)) →
not (prop_sequent_interpretation (build_counter_model s m) s prop_s).
Definition prop_correct(m : prop_model V)(s : sequent V L) : Prop :=
prop_s # propositional_sequent s /#\ prop_sequent_interpretation m s prop_s.
Lemma prop_correct_propositional :
∀(m : prop_model V)(s : sequent V L),
prop_correct m s → propositional_sequent s.
Definition upward_correct_rule(r : sequent_rule V L) : Prop :=
∀(m : prop_model V),
prop_correct m (conclusion r) →
every_nth (prop_correct m) (assumptions r).
Lemma upward_correct_context :
∀(r : sequent_rule V L)(sl sr : sequent V L),
every_nth propositional_sequent (assumptions r) →
every_nth (fun a ⇒ a ≠ []) (assumptions r) →
upward_correct_rule r →
upward_correct_rule (rule_add_context sl sr r).
Lemma upward_propositional_bare_and_left :
∀(f1 f2 : lambda_formula V L),
propositional_sequent [lf_and f1 f2] → propositional_sequent [f1].
Lemma upward_propositional_bare_and_right :
∀(f1 f2 : lambda_formula V L),
propositional_sequent [lf_and f1 f2] → propositional_sequent [f2].
Lemma upward_propositional_bare_and :
∀(f1 f2 : lambda_formula V L),
propositional_sequent (conclusion (bare_and_rule f1 f2)) →
every_nth propositional_sequent
(assumptions (bare_and_rule f1 f2)).
Lemma upward_correct_and : ∀(r : sequent_rule V L),
is_and_rule r → upward_correct_rule r.
Lemma upward_propositional_bare_neg_and_sequent :
∀(f1 f2 : lambda_formula V L),
propositional_sequent [lf_neg (lf_and f1 f2)] →
propositional_sequent [lf_neg f1; lf_neg f2].
Lemma upward_propositional_bare_neg_and :
∀(f1 f2 : lambda_formula V L),
propositional_sequent (conclusion (bare_neg_and_rule f1 f2)) →
every_nth propositional_sequent
(assumptions (bare_neg_and_rule f1 f2)).
Lemma upward_correct_neg_and : ∀(r : sequent_rule V L),
is_neg_and_rule r →
upward_correct_rule r.
Lemma upward_propositional_bare_neg_neg_sequent :
∀(f : lambda_formula V L),
propositional_sequent [lf_neg (lf_neg f)] →
propositional_sequent [f].
Lemma upward_propositional_bare_neg_neg :
∀(f : lambda_formula V L),
propositional_sequent (conclusion (bare_neg_neg_rule f)) →
every_nth propositional_sequent
(assumptions (bare_neg_neg_rule f)).
Lemma upward_correct_neg_neg : ∀(r : sequent_rule V L),
classical_logic →
is_neg_neg_rule r →
upward_correct_rule r.
Lemma correct_rule_inductive_G : ∀(m : prop_model V),
classical_logic →
rule_inductive (G_set V L) (prop_correct m).
Lemma propositional_complete_G :
∀(nonempty_v : V)(s : sequent V L)
(prop_s : propositional_sequent s),
classical_logic →
prop_valid_sequent nonempty_v s prop_s →
provable (prop_G_set V L) (empty_sequent_set V L) s.
Theorem prop_3_2_1 :
∀(nonempty_v : V)(s : sequent V L)(prop_s : propositional_sequent s),
classical_logic →
(prop_valid_sequent nonempty_v s prop_s
↔
provable (prop_G_set V L) (empty_sequent_set V L) s).
End Propositional_Completeness.
Implicit Arguments build_counter_model_correct [V L].