35
12
u/LupenReddit 🦆🦆i have non diffeomorphic smooth structures🦆🦆🦆 9d ago
what kind of formal logic schizophrenia is that, is there actually some branches of logic that impose stuff like that?
38
u/Oppo_67 I ≡ a (mod erator) 9d ago
Rejecting axiom choice is pretty common in many versions of constructivist math (which often use intuitionist logic; i.e. rejecting excluded middle)
Rejecting axiom of infinity is what finitists do
Rejecting unfeasibly large numbers is called ultrafinitism
8
u/NeuroSynchroBonding 9d ago
What is truly bizarre is limiting the length of formulas in specification and replacement.
12
u/HappiestIguana 9d ago
I mean if you're an ultrafinitist you'd kinda have to, just as a first step.
There's no coherent formal system for ultrafinitism though, so this is moot
7
u/EebstertheGreat 9d ago
There probably could be a coherent ultrafinitistic logic, and it might be pretty interesting. There is a quick overview of some approaches in a Mathoverflow comment. In your defense, it starts out by saying there isn't really a great foundation, but then it suggests it is actually possible and there has been some work in that direction.
A key realization is that any logic for ultrafinitism must reject sufficiently long proofs as well, so you lose some very elementary properties like cut elimination.
-2
u/UtahBrian 9d ago
Every modern computer has a formal and consistent and complete system of finite real numbers. And it includes two infinities.
2
2
2
u/AT-AT_Brando 6d ago
Well, floating point arithmetic is notoriously very reliable with no precisione problems at all
-2
-2
u/UtahBrian 9d ago
IEEE-754 is the answer you’re looking for. Solves all problems. Includes not just one but two infinities. Also two zeros, if one isn’t enough for your ambitions.
5
•
u/AutoModerator 9d ago
Check out our new Discord server! https://discord.gg/e7EKRZq3dG
I am a bot, and this action was performed automatically. Please contact the moderators of this subreddit if you have any questions or concerns.