3 ms·
I think every mathematician are aware of both of those perspectives, and uses whichever is more convenient at the moment.
by im3w1l 2y ago
I think every mathematician are aware of both of those perspectives, and uses whichever is more convenient at the moment.
- auggierose 2y agoYes, but in a software like a theorem prover you must make the conscious decision whether you want your prover to be able to assume ℕ ⊂ ℤ or not. All the type theory based ones say "not". That is not very convenient.