Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’ve been reading some of the work of the philosopher Mark Wilson of late. He’s unusual for giving detailed accounts of the messiness of applied mathematics and engineering’s treatment of meso-scale properties, such as hardness. This gives him grounds to reject the overly neat ambitions of philosophers of science taking theories to be syntactic entities, cast in first-order logic, physical models as logical models of the theories, etc. One example he mentions in a chapter of Scientific Metaphysics is Sturm’s treatment of the resonances of a vibrating plate. Wilson’s thought is that logician’s constructions cannot be of help here when we have Sturm locating
…his ’hidden’ qualities through a strategically informed series of contractive mappings from one covering manifold yo another, not by locating a preexisting ’kind term’ for any of them.
Rather than just logic,
we generally rely upon our prior sense of mathematical behavior with a set-theoretic vein in order to flesh out a tolerable sense of the quantities contained in the world based upon a starting knowledge of its governing differential equations and side conditions.
Ok, so now the question, in the extended ’logic’ that is cohesive HoTT can we formulate the reasoning going on when extracting normal modes etc. in Sturm-like situations?
Maybe this is not so far from Urs’s request that someone code Stoke’s theorem, perhaps along the lines of the abstract formulation. On the other hand, maybe that’s not so much requiring the production of ’qualities’ not contained in the original expression of the problem.
Stokes’s theorem is a general abstract property of differential equations, while Sturm-Liouville theory concerns a class of concrete particulars. I’d think that pure logic and metaphysics has a chance to inform us about the former, but not about the latter.That is the beauty of how a rich world emerges out of the abstract: complex exceptional particulars appear endlessly out of eternal general abstracts, and there is no telling from first principles what marvels they will realize.
That distinction has always confused me a little. I mean to anything there is a generality as well as a particularity. The HoTT version of the fundamental group of the circle as HIT is abstract, but it concerns a particular HIT.
Hearing the sound of a drum as the study of the spectrum of Laplace operators on Riemannian manifolds is sufficiently abstract to appear in our page Science of Logic. I know this is meant more abstractly than a particular choice of Laplacian applied with the particular boundary conditions of a given shape.
Is it really possible to separate out the abstract and the particular in completely principled fashion?
At the very least there is the syntactic distance from the origin that serves to distinguish these.
Buy a copy of ModalHoTT 2.0, install it on your computer, fire up the user interface. You’ll get a black screen with a green cursor blinking in the top left corner, waiting for your input.
Now you write code that constructs a certain term, then you prove a theorem about that term.
The longer the code is that you need to construct that term, the less general abstract and the more particular it is.
In cohesive HoTT, Stokes’ theorem is just a few lines above the absolute zero of the foundations. To encode Sturm-Liouville-type differential equations one will need considerably more code, and so reasoning about them will be a lot more specialized than reasoning about Stokes’ theorem.
My impression is that the point where philosophy in the guise of “objective logic” really helps is down there in the abyss close to absolute zero. The further we climb out of that into the complexity of the world, the less it will help.
1 to 4 of 4