intuitionistic-logic.v

Section BHK_interpretable.

Hypotheses P Q R:Prop.

Theorem bot_to_p: False -> P.
Proof. intros. contradiction. Qed.

Theorem neglect_Q: P -> Q -> P.
Proof. intros. assumption. Qed.

Theorem pqr: (P -> Q -> R) -> (P -> Q) -> P -> R.
Proof. intros. auto. Qed.

Theorem doub_neg: P -> ~~P.
Proof. unfold not. intros. apply H0 in H. assumption. Qed.

Theorem doub_neg_elim: ~~~P -> ~P.
Proof. unfold not. intros. apply H. intros. apply H1 in H0. assumption. Qed.

Theorem contra_imp:(P -> Q) -> (~Q -> ~P).
Proof. unfold not. intros. apply H0. apply H in H1. assumption. Qed.

Theorem vee_distr: ~(P \/ Q) <->  (~P /\ ~Q).
Proof. split; unfold not.
    - intros. split. 
        + intros. destruct H. left. assumption.
        + intros. destruct H. right. assumption.
    - intros. destruct H. destruct H0.
        + apply H. assumption.
        + apply H1. assumption.
Qed.

Theorem sum_arrow:((P /\ Q) -> R) <-> (P -> (Q -> R)).
Proof. split; intros; tauto. Qed.

Theorem ex_mid_doub_neg: ~~(P \/ ~P).
Proof. unfold not. intro. apply H. right. intro. apply H. left. assumption. Qed.

Theorem ex_mid_impl: (P \/ ~P) -> ~~P -> P.
Proof. unfold not. intros.  destruct H.
    - assumption.
    - apply H0 in H. contradiction.
Qed.

End BHK_interpretable.