5 ms·
Formal systems (like formal axiomatic set theory) are more in the domain of logic than mathematics (although there are things like model theory that lie at the
by pron 8y ago
Formal systems (like formal axiomatic set theory) are more in the domain of logic than mathematics (although there are things like model theory that lie at the intersection of the two). From their very early conception, they were designed to serve two roles: 1. Serve as completely precise languages, where no ambiguity is possible, and 2. allow for mechanical reasoning. As role 1 is often in service of role 2, I think it's fair to generalize and say that the role of formal systems is mechanical reasoning.
If mechanical reasoning is not something that interests you, you have little use for these pedantic systems. Mechanical reasoning has two current uses: 1. mechanical verification of mathematical proofs and assistance in such proofs -- this application is very rarely used in practice, and is commonly the domain of a few enthusiasts who hold high hopes for improvements that would make it more mainstream. 2. Mechanical verification of software, including static analysis, model checkers, type systems and other software-relevant proof systems.
- antidesitter 8y agoAxiomatic set theory isn't just for "pedantry" and mechanical reasoning, though that's an important application. It's also like a telescope array that allows us to see ever further into Cantor's paradise and the universe (multiverse?) of mathematics. The upper levels of transfinite set theory are especially breathtaking and somewhat scary [1]. Hugh Woodin spoke a little bit about this in a presentation on the Ultimate L conjecture: "There's the other possibility: set theory is completely irrelevant to physics... That's almost more interesting because if this conjecture is true, we've argued there's truth here for set theory, and it's a truth that's not about the physical universe. To me that's almost more remarkable, that there could be some conception of truth that transcends truth that we see around us." The presentation is called The Continuum Hypothesis and the search for Mathematical Infinity [2]. [1] http://cantorsattic.info/Cantor's_Attic http://cantorsattic.info/Cantor's_Attic [2] https://www.youtube.com/watch?v=nVF4N1Ix5WI https://www.youtube.com/watch?v=nVF4N1Ix5WI.
- fnrslvr 8y agoFormal systems aren't just about mechanizing mathematical work to make it a subject of software engineering. (Though this is a useful and probably underdeveloped outcome.) They also turn mathematical work itself into mathematical objects which one can reason about, which opens the door to metamathematics, i.e. the ability to reason mathematically about aspects of mathematics itself.