What do semi-formal proofs that use objects from different areas mathematics look like when completely formalized?
For example:
- Using graphs and planarity to show that circles cannot be used to draw n-Venn diagrams for n grater than or equal to 4.
or
- Using properties of recursion and combinatorics to prove a lower bound on the time complexity of algorithms solving the Towers of Hanoi problem.
It seems like, at some point in the formalization of these proofs, there must be a statement in first-order logic that says something along the lines of, “because of such an such, deductions regarding properties of these objects over here (i.e. planarity of graphs or recursion over the natural numbers) allow us to make statements about properties of these objects over here (i.e. drawing circles on a plane or the time-complexity of Algorithms).”
Although I’m not completely confident in my understanding of these technical concepts, here is my attempt to make my question at least a little more well defined:
When a semi-formal proof uses ideas associated with two areas of mathematics that are founded on different non-logical axioms, (any time the natural numbers show up in proofs of geometry for example), how do the statements regarding these two models logically “interface” with each other?
