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