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 comma 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 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.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 12th 2018

    Over at MathOverflow, where the general discussion was on “logical foundations of variable-centric [high-school] calculus”, I had referred to an old nn-Category Café discussion about this, and in my answer wrote

    Categorical models of typed λ\lambda-calculus are cartesian closed categories, and the idea was to contemplate the universal (i.e., initial) cartesian closed category that comes equipped with

    • A commutative ring object RR (finite products suffice to describe what is meant by a commutative ring object),

    • A differentiation operator D:R RR RD\colon R^R \to R^R (here R RR^R is the “function space object” whose existence is given by cartesian closure; the elements of R RR^R correspond to morphisms RRR \to R), satisfying all the formal expected properties of differentiation (product rule, chain rule, etc.).

    This universal cartesian closed category can be constructed syntactically and could be called “the λ\lambda-theory of high school calculus”; I’ll call it Diff\mathit{Diff}.

    In a comment, Michael Bächtold wrote,” ’This universal cartesian closed category can be constructed syntactically’ Do you know if this has been written down somewhere? I just stumbled upon this, hoping to find an answer to my related question.” I don’t know a really good reference to give him. Can anyone help?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeAug 12th 2018

    This would be the standard instance of simply typed λ\lambda-calculus generated by the finite-product theory of a ring object RR together with f:RRD(f):RRf:R\to R \vdash D(f) : R\to R satisfying some axioms, right? So the question is just about where to find a proof that STLC generates free CCC’s?

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeAug 12th 2018

    One reference for the latter is section D4.2 in the Elephant.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 12th 2018

    Thanks, Mike! That seems to be a good reference, but: what is STLC?

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 12th 2018

    Oh, maybe it’s “simply typed lambda calculus”?

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeAug 12th 2018

    Yes, that’s right, sorry for using an unexplained abbreviation.

    • CommentRowNumber7.
    • CommentAuthorMichael_Bachtold
    • CommentTimeAug 13th 2018
    • (edited Aug 13th 2018)

    Thanks Todd and Mike! In the meantime Mike also gave a very useful answer to my original question on MO, which leads me to conclude that STLC was probably not directly what I was looking for. The modal type theory Mike mentions over at MO seems more promising.

    @Mike: in your longer answer at MO you asked me to elaborate what I was hoping to achieve with the example y=x 2y=x^2. You seem to have understood the abuse of notation problem I was trying to explain. So I don’t know if this helps, but my ’original’ motivation for asking that MO question is that I’m dreaming of a proof checker for teaching (high-school) calculus the way it is actually used by physicist and engineers. (With variables, constants, “functions of” and a correct use of the notation dy/dx) This wish was ultimately sparked by your nforum thread “What is a variable?” from a few years ago.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeAug 13th 2018

    I see now that in your answer to the linked MO question you linked to Jason Howald’s question from 6 years ago, to which I today had added an answer essentially along the same lines as what you wrote there (involving a state space).

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeAug 13th 2018

    For a while I dreamed of writing a calculus textbook based on this perspective. But eventually I decided that my calculus students, at least, suffer from much more basic problems than confusion about notation, and I should focus on addressing those to the extent I can.

    I’ll be interested to see what you end up with.

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeAug 13th 2018

    Re #8, you could always direct to the nLab :) chain rule.

    • CommentRowNumber11.
    • CommentAuthorMichael_Bachtold
    • CommentTimeAug 14th 2018
    • (edited Aug 14th 2018)

    I’ll report back if I get anywhere with this.

    Related with the discussion over at MO here’s something I still don’t understand: why is it that the external property “There exists an f:XYf:X\to Y such that y=fxy=f\circ x” is not something that can be expressed with the internal language of a topos/category? Probably I’ll need to study categorical logic and the “internal language of a topos” more thoroughly to understand the answer. I’ve tried reading the appendix in Anders Kock Synthetic differential geometry but had difficulties following it. Would your notes on categorical logic Mike cover the necessary topics to answer my question?

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeAug 14th 2018

    It depends on the representation. If x,y:AXx,y:A\to X are morphisms in a category CC, then the existence of an f:XYf:X\to Y such that fx=yf\circ x = y can be expressed in the internal language of CC itself. But that’s the “analytic” version where the “domain of variation” of a “variable quantity” is made explicit. For the implicit/synthetic version you have to work in a category of sheaves or something that builds in AA, which means that everything you say in its internal language varies over AA. So if x,y:Xx,y:X in the internal language of this category-over-AA, then if you write “there exists an f:XYf:X\to Y such that f(x)=yf(x)=y” in its internal language, you get externally a statement in which ff also varies over AA, i.e. a morphism f:A×XYf:A\times X\to Y, which is not what you want as the expected meaning of “yy is a function of xx”.

    Unfortunately my categorical logic notes don’t get this far yet. I found Part D of the Elephant to be a good place to learn about categorical logic in general, although it’s rather more encyclopedic than you may need. Also you can try the nLab, e.g. internal logic.