My philosophical post on the circularity of mathematics implies that formal logic must rest ultimately on an informal foundation. In this post, I discuss what that means for our definition of mathematical rigor, which will be an important reference for future philosophical discussions.
The circularity of mathematics discussion shows that we cannot base all truth off of purely formal logic. Thus, mathematical rigor cannot be defined to consist solely of formal validity. Instead, we must accept certain concepts, like numbers, shapes, functions, and sets, as informal primitives. So what does that mean for our definition of what is sufficiently rigorous in math?
Well, as part of the acceptance of informal primitives, we would accept non-formal “proofs” or demonstrations with them too. These can include the kinds of demonstrations featured on Art of Problem Solving’s “proofs without words” page. We can call these “physical proofs” and/or “geometric proofs” (but we need to be careful to contrast the latter with formal proofs done in the subject of geometry.)
For such proofs to be sufficiently rigorous, it is imperative that the diagrams/depictions/etc. showing them are generalizable, and care must be taken to ensure this. But if that is satisfied, then we can consider such proofs to be rigorous for our purposes, and we can thus consider the statements they prove to be valid. Then, we can define math to consist of physically proven statements and statements proven by formal proofs on top of physical proven statements.
As a consequence, we can define the scope of math to be primitives, such as numbers, shapes, sets, and functions, plus concepts derived from these, such as derived objects and logical systems (which are defined by sets of logical statements which are interpreted as axioms that the systems must satisfy.)
—
EDIT (sometime later, not sure when I first came up with this point): the distinction between primitives like integers and formal systems is even deeper than just validity: no formal system in general can capture all the properties of primitives. Off the bat, the notion of “capturing all the properties of an informal primitive” is not formalizable, so such a statement can’t be proven. However, the notion of capturing all the properties of an informal primitive of a certain form, involving a certain subset of primitive operations, relations, and so forth, can in fact be formalized with completeness of a formal system in a particular logic, given that philosophically we accept that any statement about a primitive must primitively have a truth value (be either true or false), regardless of whether or not such a value is derivable from a particular formal system. For example, for the integers, we accept that any statement about the integers must be true or false, regardless of whether not a certain subset of the properties of integers can formally prove such a statement. Then, it actually turns out that it can be proven that any effectively axiomatizable formal system capturing enough properties of say the integers must be necessarily incomplete — this is the statement of Godel’s First Incompleteness Theorem. Thus, it can be rigorously proven that in general “practical” formal systems can’t capture all the properties of primitives, and in fact this is true for the specific primitive of a counting number (nonnegative integer.)
