(********************************************************************************)
(*                              axioms.v                                    	*)
(*                                                                          	*)
(*                             Pierre Lescanne                              	*)
(*                                                                          	*)
(*		       LIP (ENS-Lyon, CNRS, INRIA) 				*)
(*                                                                          	*)
(*                                                                          	*)
(* Developed in V7.4       January 2001  --   March 2004                        *)
(********************************************************************************)

Section Connector_quantifier_modality.

Require PolyList.

(* The connectives *)

Inductive proposition: Set :=
    Imp    :  proposition -> proposition -> proposition | (* p => q *)
    Forall :  (A:Set) (A -> proposition) -> proposition | 
    K      :  nat -> proposition -> proposition         |  (* K_i p  *)
    C      :  (list nat) -> proposition -> proposition. 

Infix RIGHTA 7 "=>" Imp.
Notation "\-/ p" := (Forall ? p) (at level 5, right associativity).

Inductive theorem: proposition -> Prop :=

(* ------------------------- Propositional calculus ------------------------- *)

(* Hilbert axioms for intuitionistic propositional logic *)
    Hilbert_K: (p,q:proposition) (theorem p => q => p)      |

    Hilbert_S: (p,q,r:proposition) (theorem (p => q => r) => (p => q) => p => r) |

(* Modus Ponens *)                            (* p => q , p |- q *)
     MP: (p,q:proposition) (theorem p => q) -> (theorem p) -> (theorem q)        |

(* --------------------------- Predicate   calculus --------------------------- *)

(* Forall 1 *) 
    Forall1: (A: Set)(P:A -> proposition)(a:A) (theorem \-/ P => (P a))  |

(* Forall 2 *) (* x not in FV(q)  (\-/x (q => (P x))) => q => (\-/x(P x)) *)
    Forall2: (A: Set)(P:A -> proposition)(q:proposition) 
        (theorem (\-/[x:A](q => (P x))) => q => \-/ P)	        |

(* Forall rule *) 
    ForallRule: (A: Set)(P:A->proposition)
	((x:A)(theorem (P x))) -> (theorem \-/ P). 


End Connector_quantifier_modality.