Markus.v

From Coq Require Import List Utf8 Bool.


Section Propositional.

  Inductive Formula : Type :=
  | atom : nat -> Formula
  | imp : Formula -> Formula -> Formula
  | bot : Formula. 


  Definition neg (f : Formula) : Formula := imp f bot.
  Definition True : Formula := neg bot. 
  Definition disj (fa fb : Formula) : Formula := imp (neg fa) fb.
  Definition conj (fa fb : Formula) : Formula := neg (disj (neg fa) (neg fb)).
  Definition biimp (fa fb : Formula) : Formula := conj (imp fa fb) (imp fb fa).


  Fixpoint eval_formula (m : nat -> bool) (f : Formula) : bool :=
  match f with 
  | atom i => m i
  | imp fa fb => orb (negb (eval_formula m fa)) (eval_formula m fb)
  | bot => false 
  end. 



  Inductive hilbert_axiom : Formula -> Prop :=
  | hilbert_axiom_I {P} : hilbert_axiom (imp P P)  (* Identity: P -> P *)
  | hilbert_axiom_K {P Q} : hilbert_axiom (imp P (imp Q P))  (* K axiom: P -> Q -> P *)
  | hilbert_axiom_S {P Q R} : hilbert_axiom (imp (imp P (imp Q R)) (imp (imp P Q) (imp P R)))  (* S axiom *)
  | hilbert_axiom_bot_elim {P} : hilbert_axiom (imp bot P)  (* Bottom elimination: ⊥ -> P *)
  | hilbert_axiom_top_intro : hilbert_axiom True  (* Top introduction: ⊤ *)
  | hilbert_axiom_and_intro {P Q} : hilbert_axiom (imp P (imp Q (conj P Q)))  (* And introduction: P -> Q -> P ∧ Q *)
  | hilbert_axiom_and_elim {P Q R} : hilbert_axiom (imp (imp P (imp Q R)) (imp (conj P Q) R))  (* And elimination *)
  | hilbert_axiom_or_introl {P Q} : hilbert_axiom (imp P (disj P Q))  (* Or introduction (left): P -> P ∨ Q *)
  | hilbert_axiom_or_intror {P Q} : hilbert_axiom (imp Q (disj P Q))  (* Or introduction (right): Q -> P ∨ Q *)
  | hilbert_axiom_or_elim {P Q R} : hilbert_axiom (imp (imp P R) (imp (imp Q R) (imp (disj P Q) R))).  (* Or elimination *)

  Inductive Provable : Formula -> Prop :=
  | Ax : forall P, hilbert_axiom P -> Provable P
  | MP : forall P Q, Provable (imp P Q) -> Provable P -> Provable Q.




  Lemma soundness : forall P, Provable P -> forall m, eval_formula m P = true.
  Proof.
    intros P Hprov.
    induction Hprov as [P Hax | P Q HimpP IHimpP HP IHP].
    - (* Case: P is an axiom *)
      induction Hax; intro m.
      + (* Identity axiom: P ⊃ P *)
        simpl; destruct P; simpl; try reflexivity.
        ++ eapply orb_negb_l.
        ++ destruct (eval_formula m P1);
             destruct (eval_formula m P2);
             reflexivity.
      + (* K axiom: P ⊃ Q ⊃ P *)
        simpl. intros.
        destruct (eval_formula m P); destruct (eval_formula m Q);
          reflexivity.
      + (* S axiom: (P ⊃ Q ⊃ R) ⊃ (P ⊃ Q) ⊃ P ⊃ R *)
        simpl. intros.
        destruct (eval_formula m P); simpl;
          destruct (eval_formula m Q); simpl;
          destruct (eval_formula m R); simpl; reflexivity.
      + (* Bottom elimination axiom: ⊥ ⊃ P *)
        simpl. reflexivity.
      + (* Top introduction axiom: ⊤ *)
        simpl. reflexivity.
      + (* And introduction axiom: P ⊃ Q ⊃ P ∧ Q *)
        simpl. intros.
        destruct (eval_formula m P); simpl;
          destruct (eval_formula m Q); simpl; reflexivity.
      + (* And elimination axiom: (P ⊃ Q ⊃ R) ⊃ P ∧ Q ⊃ R *)
        simpl. intros.
        destruct (eval_formula m P); simpl;
          destruct (eval_formula m Q); simpl;
          destruct (eval_formula m R); simpl; reflexivity.
      + (* Or introduction (left): P ⊃ P ∨ Q *)
        simpl. intros.
        destruct (eval_formula m P); destruct (eval_formula m Q);
          reflexivity.
      + (* Or introduction (right): Q ⊃ P ∨ Q *)
        simpl. intros.  destruct (eval_formula m P); destruct (eval_formula m Q); reflexivity.
      + (* Or elimination: (P ⊃ R) ⊃ (Q ⊃ R) ⊃ P ∨ Q ⊃ R *)
        simpl. intros.
        destruct (eval_formula m P); simpl;
          destruct (eval_formula m Q); simpl;
          destruct (eval_formula m R); simpl; reflexivity.
    - (* Case: Modus Ponens *)
      intro m.
      specialize (IHimpP m).
      specialize (IHP m).
      cbn in IHimpP.
      destruct (eval_formula m P) eqn:Ha.
      ++
        simpl in IHimpP.
        assumption.
      ++
        congruence.
  Qed.


  Theorem completeness : forall P m, eval_formula m P = true -> Provable P.
  Proof.
    (* This one is a bit involved *)
  Admitted.

End Propositional.