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. If you don't leave your Coq session
immediately, please type the following command :
Reset eq_RatPlus.
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
Coq's documentation.
Going home
Pierre Castéran