Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 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 nforum 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

1. • CommentRowNumber1.
   • CommentAuthorDavid_Corfield
   • CommentTimeJul 16th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexA question largely for Urs, but anyone feel free to chip. So, I've been promoting the line recently that dependent type theory presents philosophy with a rather different tool in comparison to the standardly used predicate logic. The latter prompts the user to load all their presuppositions into one long conjunction, while the former has them build up the presuppositions in a tower of contexts. It then occurred to me that this corresponds to a difference in the philosophy of science between the likes of Quine, for whom all knowledge is one large web, and Carnap or Friedman for whom questions only make sense within a given framework. Putting these together, leads me to wonder whether what Carnap or Friedman say might be expressed via dependent type theory. The problem is laid out [here](http://ncatlab.org/davidcorfield/show/Friedman+and+DTT), where you see Friedman criticising Quine for the long symmetrical conjunction picture. Friedman does not employ formal means to characterise his position, but were one to try this, could dependent type theory or HoTT help? Of course, we've been very much exposed to the idea that HoTT captures quantum gauge field theory. Back [here](http://golem.ph.utexas.edu/category/2010/10/cohesive_toposes.html#c035168) I posed to Urs the question of whether Maxwell's electromagnetism needed cohesive $\infty$-toposes. So one question is whether a HoTT rendition of electromagnetism would be very distant from Maxwell's understanding of his own theory. There's quite a difference between thinking of dependent type theory as the best way to represent any contextual body of knowledge, where presuppositions are encoded in a tower of contexts, and thinking of it in the guise of HoTT as being supremely well-adapted to capture modern mathematical physics. In either case, an old theory, say, Newtonian mechanics might be representable by dependent type theory, but this could be so because it is true of any theory, or alternatively because it is possible to understand old theories through the lens of modern physical treatments, which themselves are represented by HoTT. It would be great if Friedman's ideas on the [changing status of principles](http://ncatlab.org/davidcorfield/show/change+in+status+of+principles) could be captured by type theory.

   A question largely for Urs, but anyone feel free to chip. So, I’ve been promoting the line recently that dependent type theory presents philosophy with a rather different tool in comparison to the standardly used predicate logic. The latter prompts the user to load all their presuppositions into one long conjunction, while the former has them build up the presuppositions in a tower of contexts.

   It then occurred to me that this corresponds to a difference in the philosophy of science between the likes of Quine, for whom all knowledge is one large web, and Carnap or Friedman for whom questions only make sense within a given framework. Putting these together, leads me to wonder whether what Carnap or Friedman say might be expressed via dependent type theory.

   The problem is laid out here, where you see Friedman criticising Quine for the long symmetrical conjunction picture. Friedman does not employ formal means to characterise his position, but were one to try this, could dependent type theory or HoTT help? Of course, we’ve been very much exposed to the idea that HoTT captures quantum gauge field theory. Back here I posed to Urs the question of whether Maxwell’s electromagnetism needed cohesive $\infty$-toposes. So one question is whether a HoTT rendition of electromagnetism would be very distant from Maxwell’s understanding of his own theory.

   There’s quite a difference between thinking of dependent type theory as the best way to represent any contextual body of knowledge, where presuppositions are encoded in a tower of contexts, and thinking of it in the guise of HoTT as being supremely well-adapted to capture modern mathematical physics. In either case, an old theory, say, Newtonian mechanics might be representable by dependent type theory, but this could be so because it is true of any theory, or alternatively because it is possible to understand old theories through the lens of modern physical treatments, which themselves are represented by HoTT.

   It would be great if Friedman’s ideas on the changing status of principles could be captured by type theory.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeJul 16th 2013
   • (edited Jul 16th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHi, I just glanced over this. From my first impression, I would certainly agree with you in agreeing with Friedman. Concerning this point here: > There’s quite a difference between thinking of dependent type theory as the best way to represent any contextual body of knowledge, where presuppositions are encoded in a tower of contexts, and thinking of it in the guise of HoTT as being supremely well-adapted to capture modern mathematical physics. Yes, this is what I foud so interesting. On the one hand of course we can say pretty much anything in $\infty$-topos theory. For instance by first going to the h-sets and then proceeding from there pretty much as in any textbook, modulo being careful about intuitionistic reasoning. But it turns out that some statement that the textbooks think of as being very sophisticated because it takes them many pages to formulate and derive, are actually easily expressed in just a few lines if we don't take what is actually a long detour through the 0-truncated theory. So yes, there is this difference, and it can be striking.

   Hi,

   I just glanced over this. From my first impression, I would certainly agree with you in agreeing with Friedman.

   Concerning this point here:

   There’s quite a difference between thinking of dependent type theory as the best way to represent any contextual body of knowledge, where presuppositions are encoded in a tower of contexts, and thinking of it in the guise of HoTT as being supremely well-adapted to capture modern mathematical physics.

   Yes, this is what I foud so interesting. On the one hand of course we can say pretty much anything in $\infty$-topos theory. For instance by first going to the h-sets and then proceeding from there pretty much as in any textbook, modulo being careful about intuitionistic reasoning. But it turns out that some statement that the textbooks think of as being very sophisticated because it takes them many pages to formulate and derive, are actually easily expressed in just a few lines if we don’t take what is actually a long detour through the 0-truncated theory.

   So yes, there is this difference, and it can be striking.

3. • CommentRowNumber3.
   • CommentAuthorDavid_Corfield
   • CommentTimeJul 17th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexThanks. I need to work out how to proceed strategically to handle this difference in writing some of this up for philosophers.

   Thanks. I need to work out how to proceed strategically to handle this difference in writing some of this up for philosophers.

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeJul 17th 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItexBut notice that this difference is as such not a new phenomenon. We see this all through the history of natural sciences, that the gradually one finds better theory and language to express phenomena. You can still these days see this happening in physics departments, that an experimentalist will express "I don't need differential forms, I can do everyhting with matrices". And its true. But the thing is, Maxwell wrote down his equations filling several pages with symbols. Today, with better language, we write half a dozen _symbols_ $$ d \ast d A = J $$ to express the same. And we also realize today that differential form language is actually more fundamental than matrix calculus, not the other way around.

   But notice that this difference is as such not a new phenomenon. We see this all through the history of natural sciences, that the gradually one finds better theory and language to express phenomena.

   You can still these days see this happening in physics departments, that an experimentalist will express “I don’t need differential forms, I can do everyhting with matrices”. And its true. But the thing is, Maxwell wrote down his equations filling several pages with symbols. Today, with better language, we write half a dozen symbols

   $$d \ast d A = J$$

   to express the same.

   And we also realize today that differential form language is actually more fundamental than matrix calculus, not the other way around.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeJul 17th 2013
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexI guess one way to approach this is via the notion of 'internalisation'. Really fundamental concepts ought not to be described via towers of axioms bolted onto a logical foundation, but rather written into the logic itself. A good case in point would be smoothness. Do we learn something when axioms can't be internalised in a type theory? Is it clear which kinds of property and structure lend themselves to forming a '??? homotopy type theory', like 'cohesive' and 'differential'?

   I guess one way to approach this is via the notion of ’internalisation’. Really fundamental concepts ought not to be described via towers of axioms bolted onto a logical foundation, but rather written into the logic itself. A good case in point would be smoothness.

   Do we learn something when axioms can’t be internalised in a type theory? Is it clear which kinds of property and structure lend themselves to forming a ’??? homotopy type theory’, like ’cohesive’ and ’differential’?

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJul 17th 2013
   • (edited Jul 17th 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItex> Really fundamental concepts ought not to be described via towers of axioms bolted onto a logical foundation, but rather written into the logic itself. I also feel that this is so, yes. But I do appreicate that not everybody feels this way. Personally I do feel that the history of the exact sciences is a long list of evidence for this statement, which one might think of as a strengthening of the proverbial "[unreasonable effectivenes of mathematics](https://en.wikipedia.org/wiki/The_Unreasonable_Effectiveness_of_Mathematics_in_the_Natural_Sciences)". But since it's just evidence, not a proof (not yet at least, we are working on it ;-) there is room to feel differently. My favorite antagonistic discussion partner about fundamental mathematical physics, Igor Khavkine, holds something like the opposite point of view: that (in my paraphrase, hope he doesn't mind me saying this here) your formal language should just follow your science like a well-trained dog, not run ahead and lead the way. I feel differently, but I do very much appreciate the critical attention that this point of view holds up, which makes one check to which extent the formalism is possibly running too far ahead and going astray. For instance people with this formalism-critical point of view reject otherwise widely accepted believes about the universe, such as this one: Modern particle physicists are fond of the mechanism of [[spontaneous symmetry breaking]] as a general organizational principle in field theory. In the course of this it is today taken widely for granted that an example is [[electroweak symmetry breaking]]. This is attractive, as it is conceptually beautiful, the formalism leads the way. But apparently there is room to doubt that this is actually what happens in nature, an alternative model is discussed in Andreas Aste, Michael Dütsch, Günter Scharf, _Perturbative gauge invariance: electroweak theory II_ ([arXiv:hep-th/9702053](http://arxiv.org/abs/hep-th/9702053))

   Really fundamental concepts ought not to be described via towers of axioms bolted onto a logical foundation, but rather written into the logic itself.

   I also feel that this is so, yes. But I do appreicate that not everybody feels this way. Personally I do feel that the history of the exact sciences is a long list of evidence for this statement, which one might think of as a strengthening of the proverbial “unreasonable effectivenes of mathematics”. But since it’s just evidence, not a proof (not yet at least, we are working on it ;-) there is room to feel differently.

   My favorite antagonistic discussion partner about fundamental mathematical physics, Igor Khavkine, holds something like the opposite point of view: that (in my paraphrase, hope he doesn’t mind me saying this here) your formal language should just follow your science like a well-trained dog, not run ahead and lead the way.

   I feel differently, but I do very much appreciate the critical attention that this point of view holds up, which makes one check to which extent the formalism is possibly running too far ahead and going astray. For instance people with this formalism-critical point of view reject otherwise widely accepted believes about the universe, such as this one:

   Modern particle physicists are fond of the mechanism of spontaneous symmetry breaking as a general organizational principle in field theory. In the course of this it is today taken widely for granted that an example is electroweak symmetry breaking. This is attractive, as it is conceptually beautiful, the formalism leads the way. But apparently there is room to doubt that this is actually what happens in nature, an alternative model is discussed in

   Andreas Aste, Michael Dütsch, Günter Scharf, Perturbative gauge invariance: electroweak theory II (arXiv:hep-th/9702053)