Some bad inference rules

Among many logical mistakes, we often meet bad inference rules, the use of which can lead to inconsistencies. For instance, let us consider implication dyslexia (confusion between P->Q and Q->P) and dyslexic contraposition :
Definition dyslexic_imp := forall P Q:Prop, (P->Q)->Q->P.

Definition dyslexic_contrap :=forall P Q:Prop,(P->Q)->~P->~Q.
Show that if one or the other of the preceding types was inhabited, one could prove False, hence any proposition.

Solution

Look at file dyslexia.v


Going home
Pierre Castéran