The Coq mailing list

[Jose Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Dear Andrej,

I’m not an internet TROLL, LOL. If you read my papers in number theory, there is always a reference to the Hilbert scheme of n points. My motivation to learn HoTT is to check topological constructions related to number theory in Coq. HoTT is wonderful for synthetics topology. Indeed, I watched your lectures about Coq and HoTT during my learning process. I’m not from an arrogant position, I just try to understand the significance of Russell O’Connor PhD Thesis in a non-dogmatic way.

My initial arguments were from Voevodsky’s lectures and I quoted the sources for the other students in this mailing list interested to watch him to learn UniMath from his creator: https://www.math.ias.edu/vladimir/Lectures 

I quoted from Voevodsky that:

• Peano arithmetics is inconsistent (his conjecture) https://video.ias.edu/voevodsky-80th
• CiC is wrong foundational speaking https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/VTS_01_2.mp4

Sincerely, I was confused trying to follow Voevodsky’s ideas. So, I asked to the experts in this mailing list, using the example of O’Connor, because I read his paper before. I learned here that the idea of the inconsistency of Peano arithmetic comes from Edward Nelson and his arguments.

If I well understood, my impoliteness was to claim that: "Russell O'Connor did not prove in Coq that PA is consistent”.

First, I sincerely apology with Russell O’Connor if this statement triggered him. If someone tell me that the main theorem of my paper (published this month in Finite Fields and their Applications, Elsevier)

https://www.sciencedirect.com/science/article/pii/S1071579718300169

is wrong, I will not be triggered, but curious (maybe there is something deep to learn). If this person gives me an invalid argument, I will explain him/her if I have enough time, otherwise, I will ignore him, because a wrong refutation cannot destroy the reputation of a true mathematician.

Second, what I really meant was that Russell O'Connor did not prove that PA is consistent in a meta-mathematical sense, following Hilbert standards (I think that we all agree). The phrase “in Coq” means that Coq cannot be used to do meta-mathematics following Hilbert standards (I though that it was clear from the context of foundation of mathematics). On the other hand, I accept that relevant arithmetics  R#  (Peano axioms with first-order relevant logic in place of the classical one) is consistent, because this proof follows Hilbert standards.

Sincerely Yours,

José M.

On  May 3, 2018, at 3:32 PM, Andrej Bauer <andrej.bauer AT andrej.com> wrote:

"Russell O'Connor did not prove in Coq that PA is consistent",