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.
We hope that this exercise will warn you against the danger of
putting axioms in your theories. If you don't leave your Coq session
immediately, please type the following command :
to get a consistent environment.
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