About the danger of axioms
Consider the following definition
of positive rational numbers, including an axiom stating
that if ad=bc, then a/b=c/d.
Show that this theory is unconsistent.
Solution
Notes
We hope that this exercise will warn you against the danger of
putting axioms in your theories. Please exit from your Coq session
before doing any serious job.
A possible way to get a theory of rational numbers is to replace Coq's
equality by an equivalence relation. Please look at Setoids in
Coq's documentation, and
this tutorial