Require Export LFS.

Natural deduction for propositional logic

Formulas and contexts

Definition var := nat.

Inductive form : Type :=
| Var : var → form
| Imp : form → form → form
| Fal : form.

Definition Not s := Imp s Fal.

Definition context := list form.

(*** This could be an exercise without decide equality. ***)
Instance form_eq_dec : ∀ s t:form, dec (s = t).

Intuitionistic system

Inductive nd (A : context) : form → Prop :=
| ndA s : s el A → nd A s
| ndII s t : nd (s ::A) t → nd A (Imp s t)
| ndIE s t : nd A (Imp s t) → nd A s → nd A t
| ndE s : nd A Fal → nd A s.

Goal ∀ A s t, nd A (Imp (Not s) (Imp s t)).

Lemma ndA1 A s :
nd (s :: A) s.

Lemma ndA2 A s t :
nd (t :: s :: A) s.

Lemma ndA3 A s t u :
nd (u :: t :: s :: A) s.

Check (nd_ind :
  ∀ p : context → form → Prop,
    (∀ (A : context) (s : form), s el A → p A s) →
    (∀ (A : context) (s t : form), nd (s :: A) t → p (s :: A) t → p A (Imp s t)) →
    (∀ (A : context) (s t : form), nd A (Imp s t) → p A (Imp s t) → nd A s → p A s → p A t) →
    (∀ (A : context) (s : form), nd A Fal → p A Fal → p A s) →
    ∀ (A : context) (s : form), nd A s → p A s).

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 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 ndDN A s :
  nd A s → nd A (Not (Not s)).

Classic system

Inductive ndc (A : context) : form → Prop :=
| ndcA s : s el A → ndc A s
| ndcII s t : ndc (s ::A) t → ndc A (Imp s t)
| ndcIE s t : ndc A (Imp s t) → ndc A s → ndc A t
| ndcC s : ndc (Not s :: A) Fal → ndc A s.

Lemma ndcA1 A s :
ndc (s :: 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.

Glivenko's theorem

says that from a classical proof of a formula one can obtain an intuitionistic proof of the double negation of the formula. It follows that intuitionistic and classical refutation coincide. The proof is by induction on ndc. For each case one has to show an intuitionistic tautology. Proving the tautologies first in Coq is very helpful. The two more involved tautologies are:

(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

The Hilbert system consists of Modus Ponens and the axioms

K : s → t → s
S : (s → t → u) → (s → t) → s → u
E : Fal → s

We show that Hilbert derivability agrees with ND derivability. The easy direction is from Hilbert to ND. For the other direction we use the deduction theorem hilD.

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.

Check hil_ind.

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.

Fixpoint valb (s:form) (p:var → bool) : bool :=
match s with
| Var x ⇒ p x
| Fal ⇒ false
| Imp s t ⇒ implb (valb s p) (valb t p)
end.

Lemma ndc_valb_sound A s p :
ndc A s → (∀ t, t el A → valb t p = true) → valb s p = true.

Lemma ndc_con : ¬ ndc nil Fal.

Lemma nd_con : ¬ nd nil Fal.

Fixpoint subst (theta : var → form) (s : form) : form :=
match s with
| Var x ⇒ theta x
| Imp s t ⇒ Imp (subst theta s) (subst theta t)
| Fal ⇒ Fal
end.

(*** Properties of Proof Systems. ***)
Definition Assumption (p:context → form → Prop) :=
∀ A s, s el A → p A s.

Definition ModusPonens (p:context → form → Prop) :=
∀ A s t, p A (Imp s t) → p A s → p A t.

Definition Deductivity (p:context → form → Prop) :=
∀ A s t, p (s ::A) t → p A (Imp s t).

Definition Explosivity (p:context → form → Prop) :=
∀ A s, p A Fal → p A s.

Definition Weakening (p:context → form → Prop) :=
∀ A A' s, A <<= A' → p A s → p A' s.

Definition Substitutivity (p:context → form → Prop) :=
∀ A s theta, p A s → p (map (subst theta) A) (subst theta s).

Definition Consistency (p:context → form → Prop) :=
¬p nil Fal.

Definition ProvPred (p:context → form → Prop) :=
Assumption p ∧ ModusPonens p ∧ Deductivity p ∧ Explosivity p
∧ Weakening p ∧ Substitutivity p ∧ Consistency p.