Comment by xtal_freq
5 days ago
I wonder what the ultrafinist argument against theorems about the natural numbers as defined in Coq would be.
5 days ago
I wonder what the ultrafinist argument against theorems about the natural numbers as defined in Coq would be.
They would say the theorems are meaningless.
The classical mathematician would respond that the theorems are clearly meaningful and you can easily test them against any natural numbers you care about to see empirically they are meaningful.
The ultrafinitist would respond that they are only coincidentally correct, in the same way that pre-modern mathematical reasoning was often very sloppy, featured regular abuse of notation, and had no coherent foundations, but nonetheless still often arrived at correct conclusions by "coincidence."
The classical mathematician might then go over how strong the intuition of something like "there exists a number that..." is and how it is an easily empirically validated statement...
And so the debate would keep going.