(* Paradoxe du barbier. Dans un village, un barbier rase tous les habitants qui ne se rasent pas eux-mêmes, et seulement ceux-ci. 1) Montrer qu'en logique classique, cette hypothèse mêne à une contradiction. *) Section Paradoxe_du_Barbier_version_classique. Variable Habitants : Set. Variable Rase : Habitants -> Habitants -> Prop. Variable barbier : Habitants. Hypothesis barbier_1 : forall h:Habitants, ~ Rase h h -> Rase barbier h. Hypothesis barbier_2 : forall h: Habitants, Rase barbier h -> ~ Rase h h. Hypothesis classic : forall P:Prop, P \/ ~P. (* usage : elim (classic A) où A est une proposition *) Lemma paradoxe : False. Proof. Admitted. End Section Paradoxe_du_Barbier_version_classique. (* En fait, l'utilisation de la logique classique et du tiers exclu relève de la paresse intellectuelle. Compléter le développement suivant : *) Section Paradoxe_du_Barbier_version_intuitionniste. Variable Habitants : Set. Variable Rase : Habitants -> Habitants -> Prop. Variable barbier : Habitants. Hypothesis barbier_1 : forall h:Habitants, ~ Rase h h -> Rase barbier h. Hypothesis barbier_2 : forall h: Habitants, Rase barbier h -> ~ Rase h h. Lemma paradoxe' : False. Proof. Admitted. End Paradoxe_du_Barbier_version_intuitionniste.