Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 6th 2015

    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.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeAug 6th 2015
    • (edited Aug 6th 2015)

    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.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 6th 2015
    • (edited Aug 6th 2015)

    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?

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeAug 6th 2015
    • (edited Aug 6th 2015)

    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.