Definition var := nat.
Inductive form : Type :=
| Var : var → form
| Imp : form → form → form
| Fal : form.
Definition Not s := Imp s Fal.
Instance form_eq_dec : ∀ s t:form, dec (s = t).
Fixpoint vars (s : form) : list var :=
match s with
| Var x ⇒ [x]
| Imp s t ⇒ vars s ++ vars t
| Fal ⇒ nil
end.
Definition assn := var → bool.
Fixpoint satis (f : assn) (s : form) : Prop :=
match s with
| Var x ⇒ f x = true
| Imp s1 s2 ⇒ satis f s1 → satis f s2
| Fal ⇒ False
end.
Instance satis_dec : ∀ f s, dec (satis f s).
Section F.
Variable F:Type.
(*** E is an entailment relation ***)
Variable E:list F → F → Prop.
(*** Structural Properties ***)
Definition Monotonicity : Prop :=
∀ A A' s, A <<= A' → E A s → E A' s.
Definition Reflexivity : Prop :=
∀ A s, s el A → E A s.
Definition Cut : Prop :=
∀ A s t, E A s → E (s::A) t → E A t.
Definition Consistency : Prop :=
∃ s:F, ¬E nil s.
End F.
Fixpoint andlist (A:list Prop) : Prop :=
match A with
| P::A' ⇒ P ∧ andlist A'
| nil ⇒ True
end.
Lemma andlistEq (A:list Prop) : andlist A ↔ ∀ s, s el A → s.
Goal
let E : list Prop → Prop → Prop := fun A s ⇒ andlist A → s in
Reflexivity E ∧ Monotonicity E ∧ Cut E ∧ Consistency E.
(*** Entailment Relations for form ***)
Definition context := list form.
(*** Logical Properties ***)
Definition CharImp (E:context → form → Prop) : Prop :=
∀ A s t, E A (Imp s t) ↔ E (s::A) t.
Definition CharFal (E:context → form → Prop) : Prop :=
∀ A, E A Fal ↔ ∀ s, E A s.
Definition bsc A s : Prop := ∀ f, (∀ u, u el A → satis f u) → satis f s.
Fixpoint subst (sigma : var → form) (s : form) : form :=
match s with
| Var x ⇒ sigma x
| Imp s t ⇒ Imp (subst sigma s) (subst sigma t)
| Fal ⇒ Fal
end.
Definition Substitution (E:context → form → Prop) :=
∀ A s sigma, E A s → E (map (subst sigma) A) (subst sigma s).
Definition EntailRelAllProps (E:context → form → Prop) :=
Reflexivity E ∧ Monotonicity E ∧ Cut E ∧ Consistency E
∧ CharImp E ∧ CharFal E ∧ Substitution E.
Variable F:Type.
(*** E is an entailment relation ***)
Variable E:list F → F → Prop.
(*** Structural Properties ***)
Definition Monotonicity : Prop :=
∀ A A' s, A <<= A' → E A s → E A' s.
Definition Reflexivity : Prop :=
∀ A s, s el A → E A s.
Definition Cut : Prop :=
∀ A s t, E A s → E (s::A) t → E A t.
Definition Consistency : Prop :=
∃ s:F, ¬E nil s.
End F.
Fixpoint andlist (A:list Prop) : Prop :=
match A with
| P::A' ⇒ P ∧ andlist A'
| nil ⇒ True
end.
Lemma andlistEq (A:list Prop) : andlist A ↔ ∀ s, s el A → s.
Goal
let E : list Prop → Prop → Prop := fun A s ⇒ andlist A → s in
Reflexivity E ∧ Monotonicity E ∧ Cut E ∧ Consistency E.
(*** Entailment Relations for form ***)
Definition context := list form.
(*** Logical Properties ***)
Definition CharImp (E:context → form → Prop) : Prop :=
∀ A s t, E A (Imp s t) ↔ E (s::A) t.
Definition CharFal (E:context → form → Prop) : Prop :=
∀ A, E A Fal ↔ ∀ s, E A s.
Definition bsc A s : Prop := ∀ f, (∀ u, u el A → satis f u) → satis f s.
Fixpoint subst (sigma : var → form) (s : form) : form :=
match s with
| Var x ⇒ sigma x
| Imp s t ⇒ Imp (subst sigma s) (subst sigma t)
| Fal ⇒ Fal
end.
Definition Substitution (E:context → form → Prop) :=
∀ A s sigma, E A s → E (map (subst sigma) A) (subst sigma s).
Definition EntailRelAllProps (E:context → form → Prop) :=
Reflexivity E ∧ Monotonicity E ∧ Cut E ∧ Consistency E
∧ CharImp E ∧ CharFal E ∧ Substitution E.
Inductive nd : context → form → Prop :=
| ndA A s : s el A → nd A s
| ndII A s t : nd (s::A) t → nd A (Imp s t)
| ndIE A s t : nd A (Imp s t) → nd A s → nd A t
| ndE A s : nd A Fal → nd A s.
Goal ∀ A s t, nd A (Imp s (Imp (Not s) t)).
Goal ∀ A s t, nd A (Imp s (Imp (Not s) t)).
Lemma ndapp A s u :
Imp s u el A → nd A s → nd A u.
Lemma ndapp1 A s u :
nd (Imp s u :: A) s → nd (Imp s u :: A) u.
Lemma ndapp2 A s t u :
nd (t :: Imp s u :: A) s → nd (t :: Imp s u :: A) u.
Lemma ndapp3 A s t u v :
nd (t :: v :: Imp s u :: A) s → nd (t :: v :: Imp s u :: A) u.
Lemma nd_weak A A' s :
A <<= A' → nd A s → nd A' s.
Lemma ndW A s t :
nd A s → nd (t::A) s.
Lemma ndIE_weak A B s t :
nd B (Imp s t) → B <<= A → nd A s → nd A t.
Lemma ndDN A s :
nd A s → nd A (Not (Not s)).
Lemma nd_bool_sound A s :
nd A s → bsc A s.
Lemma nd_con : ¬ nd nil Fal.
Lemma nd_subst A s sigma : nd A s → nd (map (subst sigma) A) (subst sigma s).
Inductive ndc : context → form → Prop :=
| ndcA A s : s el A → ndc A s
| ndcII A s t : ndc (s::A) t → ndc A (Imp s t)
| ndcIE A s t : ndc A (Imp s t) → ndc A s → ndc A t
| ndcC A s : ndc (Not s :: A) Fal → ndc A s.
Lemma ndc_weak A A' s :
A <<= A' → ndc A s → ndc A' s.
Lemma ndcW A s t :
ndc A s → ndc (t::A) s.
Lemma ndcE A s :
ndc A Fal → ndc A s.
Lemma nd_ndc A s :
nd A s → ndc A s.
Lemma ndc_refute A s :
ndc A s ↔ ndc (Not s :: A) Fal.
(*** Exercise ***)
Goal ∀ A s, ndc A (Imp (Not (Not s)) s).
Glivenko's theorem
- (s → ~~ t) → ~~ (s → t)
- ~~ (s → t) → ~~ s → ~~ t
Lemma Glivenko A s :
ndc A s → nd A (Not (Not s)).
Corollary Glivenko_refute A :
nd A Fal ↔ ndc A Fal.
Corollary nd_embeds_ndc A s :
ndc A s ↔ nd (Not s :: A) Fal.
Intuitionistic Hilbert system
- K : s → t → s
- S : (s → t → u) → (s → t) → s → u
- E : Fal → s
Definition FK (s t : form) : form :=
Imp s (Imp t s).
Definition FS (s t u : form) : form :=
(Imp (Imp s (Imp t u))
(Imp (Imp s t)
(Imp s u))).
Inductive hil (A : context) : form → Prop :=
| hilA s : s el A → hil A s
| hilK s t : hil A (FK s t)
| hilS s t u : hil A (FS s t u)
| hilE s : hil A (Imp Fal s)
| hilMP s t : hil A (Imp s t) → hil A s → hil A t.
Lemma hil_nd A s :
hil A s → nd A s.
Lemma hilAK A s t :
hil A s → hil A (Imp t s).
Lemma hilAS A s t u :
hil A (Imp s (Imp t u)) → hil A (Imp s t) → hil A (Imp s u).
Lemma hilI A s :
hil A (Imp s s).
Lemma hilD s A t :
hil (s::A) t → hil A (Imp s t).
Lemma nd_hil A s :
nd A s → hil A s.
Theorem hil_iff_nd A s :
hil A s ↔ nd A s.