The calculus was created before the innovation of formal systems in the 20th century. Mathematical reasoning might be capable of being represented by a formal system, but it is not identical with a formal system. If by “axiom system” you mean formal system, then in a very precise way there is no axiom system for the calculus and one has never been used. Any formal system that accurately modeled the calculus (regardless of its completeness or consistency) would be so much more austere and cluttered than the calculus itself, that it would be of no practical use.
The proofs in the calculus are not proofs in a completely syntactic system, the axioms and theorems require some degree of interpretation. Likewise, we don’t actually use PA to prove most statements about the natural numbers, we use the basic agreements we all have about what numbers act like and about what happens when you combine them by certain operators.
The calculus was created before the innovation of formal systems in the 20th century.
So was arithmetic. That is irrelevant to the possibility of formalising them.
Mathematical reasoning might be capable of being represented by a formal system, but it is not identical with a formal system. If by “axiom system” you mean formal system, then in a very precise way there is no axiom system for the calculus and one has never been used.
Can you elucidate this precise sense? Calculus is just as formalisable as every other branch of mathematics.
The proofs in the calculus are not proofs in a completely syntactic system, the axioms and theorems require some degree of interpretation.
What do you mean? I can prove d(x^2)/dx = 2x in as exhaustively complete detail as you want. So can these people and they probably have the proof online somewhere (the web site makes it very difficult to actually read their repository of formalised mathematics). Here’s a road map, starting from Peano arithmetic.
Construct the negative integers as equivalence classes of pairs of Peano integers: (a,b) and (c,d) are equivalent if a+d=b+c.
Do a similar extension to get the rational numbers.
I am not arguing about the possibility of formalizing the calculus, I am talking about the necessity. There have been proofs without formal systems and there will continue to be. All of these proofs might be formalize-able, but they were proofs before they were shown to be such.
What I meant by “there is a very formal sense in which the calculus cannot be formalized.” is that you can’t have a complete and consistent axiomatization of the reals. I apologize for the ambiguity. But unlike finitism, frst order logic, boolean arithmetic, category theory, and I’m sure many more, calculus and arithmetic cannot be completely and consistently axiomatized.
I am not arguing about the possibility of formalizing the calculus, I am talking about the necessity. There have been proofs without formal systems and there will continue to be. All of these proofs might be formalize-able, but they were proofs before they were shown to be such.
People built buildings before mechanics and materials science, but at some point in the development of the technology, you need those to get any further. It’s the same with mathematics. The formal apparatus isn’t what people do mathematics in, but it’s a necessary foundation. Without it you get informal arguments that no-one is quite sure are really valid, as was the case for calculus before the epsilon-delta definition of a limit was worked out. (It was more than a century later before someone was able to make rigorous the original talk of infinitesimals.)
The calculus was created before the innovation of formal systems in the 20th century. Mathematical reasoning might be capable of being represented by a formal system, but it is not identical with a formal system. If by “axiom system” you mean formal system, then in a very precise way there is no axiom system for the calculus and one has never been used. Any formal system that accurately modeled the calculus (regardless of its completeness or consistency) would be so much more austere and cluttered than the calculus itself, that it would be of no practical use.
The proofs in the calculus are not proofs in a completely syntactic system, the axioms and theorems require some degree of interpretation. Likewise, we don’t actually use PA to prove most statements about the natural numbers, we use the basic agreements we all have about what numbers act like and about what happens when you combine them by certain operators.
So was arithmetic. That is irrelevant to the possibility of formalising them.
Can you elucidate this precise sense? Calculus is just as formalisable as every other branch of mathematics.
What do you mean? I can prove d(x^2)/dx = 2x in as exhaustively complete detail as you want. So can these people and they probably have the proof online somewhere (the web site makes it very difficult to actually read their repository of formalised mathematics). Here’s a road map, starting from Peano arithmetic.
Construct the negative integers as equivalence classes of pairs of Peano integers: (a,b) and (c,d) are equivalent if a+d=b+c.
Do a similar extension to get the rational numbers.
Use Dedekind cuts to define real numbers.
Use epsilon-delta definitions to define limits.
With limits, define derivatives.
Calculate d(x^2)/dx: ((x+delta)^2 - x^2)/delta = 2x + x*delta --> 2x as delta --> 0. QED.
I am not arguing about the possibility of formalizing the calculus, I am talking about the necessity. There have been proofs without formal systems and there will continue to be. All of these proofs might be formalize-able, but they were proofs before they were shown to be such.
What I meant by “there is a very formal sense in which the calculus cannot be formalized.” is that you can’t have a complete and consistent axiomatization of the reals. I apologize for the ambiguity. But unlike finitism, frst order logic, boolean arithmetic, category theory, and I’m sure many more, calculus and arithmetic cannot be completely and consistently axiomatized.
People built buildings before mechanics and materials science, but at some point in the development of the technology, you need those to get any further. It’s the same with mathematics. The formal apparatus isn’t what people do mathematics in, but it’s a necessary foundation. Without it you get informal arguments that no-one is quite sure are really valid, as was the case for calculus before the epsilon-delta definition of a limit was worked out. (It was more than a century later before someone was able to make rigorous the original talk of infinitesimals.)