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 definitions 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 nlab noncommutative noncommutative-geometry number-theory object 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).

Atrium > Mathematics, Physics & Philosophy: Favonia's thesis

Bottom of Page

1 to 16 of 16

  1.  
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 30th 2017

    Added reference at Favonia to his thesis, Higher-Dimensional Types in the Mechanization of Homotopy Theory.

    There’s even a section ’Buddhism in Martin-Löf Type Theory’.

    • CommentRowNumber2.
    • CommentAuthorTim_Porter
    • CommentTimeMar 31st 2017

    That looks fun.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMar 31st 2017

    The statement that he actually proves in that section with Buddhism in the title, that statement has an established name in logic, doesn’t it. I forget the technical term, but people here will readily know: It’s the statement that two things are equal precisely if there is no proposition distinguishing between them.

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeMar 31st 2017

    Leibniz equality.

    • CommentRowNumber5.
    • CommentAuthorMatt Earnshaw
    • CommentTimeMar 31st 2017
    • (edited Mar 31st 2017)

    principle of identity of indiscernibles — but I think the statement in the thesis has a distinct content, or is at least intended as such. Something like, if a concept is equivalent on its fibres over all objects then it ultimately has no content, is-non-dual is a proposition about a concept, not two inhabitants of a type. According to the proof here, identification of any two objects “at an ultimate level” (induced by recognition of the interdependence of all things, the realization that a concept and its antithesis are in complete continuity, supposedly) is necessary and sufficient for demonstration of the “non-duality” or ultimate emptiness of a concept, which doesn’t seem too surprising.

    This results really in a severe form of scepticism or quietism, intended to quell our philosophical anxieties. There is a literature on the relation between Pyrrhonian scepticism and Madhyamaka Buddhism, which are useful parallels (eg. Garfield 1990). Disastrous for many reasons, although there is no better stimulus to the formulation of alternatives: the presuppositionless structure of the Science of Logic is very much designed as the ultimate bulwark against Pyrrhonism (Trisokkas 2012).

    Incidentally I see that (Ladyman & Presnell 2016) has an appendix formulating no fewer than 4 forms of the PII in HoTT. I will add this material to the PII page in due course.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMar 31st 2017
    • (edited Mar 31st 2017)

    Leibniz equality

    and

    identity of indiscernibles

    Thanks! That’s it.

    I have put a pointer to Favonia’s formalization there. (Though this probably was formalized elsewhere before?)

    but I think the statement in the thesis has a distinct content, or is at least intended as such.

    It may be intended differently, but clearly this is exactly what it says.

    On another note, I am not convinced by the quote by John Baez on that page. It was added by Colin Zwanziger when the page was created in revision 1. I vote for removing this.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2017

    Strangely the HoTT book only has it in reverse (and misspelled). In Section 1.12 there is ’Indiscernability of identicals’.

    I am not convinced by the quote by John Baez on that page.

    Yes, not very helpful.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMar 31st 2017

    The HoTT book “has it in reverse” because it’s actually talking there about the reverse implication: the eliminator for the identity type is the indiscernibility of identicals. Identity of indiscernibles is the opposite. In the presence of an identity type, identity of indiscernibles is trivial because of haecceities; but extensionality principles like function extensionality, propositional extensionality, and univalence (“typal extensionality”) are indeed naturally regarded as a stronger form of identity of indiscernibles. In particular, the consistency of univalence means that in MLTT without univalence, one cannot define any predicate that provably distinguishes isomorphic types; thus isomorphic types are “externally indiscernible”, and univalence incarnates that principle internally by making them identical.

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 31st 2017

    I didn’t write ’strangely’ because I thought you had the direction wrong, but because you only give an account of the far less frequent of the two ways.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 31st 2017

    Less frequent to the philosopher, perhaps, but I would say that to a mathematician that’s the more important direction.

    • CommentRowNumber11.
    • CommentAuthorTobyBartels
    • CommentTimeApr 1st 2017
    • (edited Apr 1st 2017)

    I assumed that that phrase was chosen as something in the way of a play on words.

    ETA: Here is somebody who thinks that Leibniz’s principle is properly understood as including both directions: http://www.oberlin.edu/faculty/mwallace/LeibnizsLaw.html.

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeApr 1st 2017

    Function extensionality, univalence, etc are forms of Leibniz’s principle, but applied after making a judgement about what predicates one is allowed to apply to a function, type, etc. Leibniz’s principle by itself, while still important, is also trivial when you have identity predicates, as Mike said. To get function extensionality (for example) as well, you first say that there are some basic predicates about functions that generate all of the predicates, so that if two functions have those predicates (which are the values of the function, or rather their haecceities1) in common, then they have all predicates in common (and so, pace Leibniz, are equal).

    1. I thank Mike for teaching me this word. For our purposes, the haecceity of xx is the predicate −=x- = x. ↩

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeApr 1st 2017

    It doesn't seem to me that Appendix B of Favonia’s thesis actually contains a formulation of the identity of indiscernibles. The statement that they1 prove is not that two things are identical iff no properties distinguish them; it is that all things are identical iff no properties distinguish anything.

    That is, they did not prove2

    ∀o 1,∀o 2,(o 1=o 2↔∀P,P(o 1)↔P(o 2)); \forall\, o_1,\; \forall\, o_2,\; \bigl(o_1 = o_2 \;\leftrightarrow\; \forall\, P,\; P(o_1) \;\leftrightarrow\; P(o_2)\bigr) ;

    rather, they proved

    (∀o 1,∀o 2,o 1=o 2)↔(∀o 1,∀o 2,∀P,P(o 1)↔P(o 2)). (\forall\, o_1,\; \forall\, o_2,\; o_1 = o_2) \;\leftrightarrow\; \bigl(\forall\, o_1,\; \forall\, o_2,\; \forall\, P,\; P(o_1) \;\leftrightarrow\; P(o_2)\bigr) .

    Of course, the second statement follows from the first, so there is that.

    1. ‘I prefer singular they but people often choose he because of my perceived gender.’ ―https://www.cs.cmu.edu/~kuenbanh/#pronoun ↩

    2. That this was in HoTT rather than FOL didn’t seem to add anything, and Favonia even said that their statements omitted some truncations, so I just truncated everything here. ↩

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeApr 1st 2017

    Toby #12 that’s another good way to describe it. For function extensionality it is easy to say what predicates we are interested in, namely those that involve evaluating the function. But it’s less clear to me how to say what predicates we are interested in for univalence; what would you say?

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 1st 2017

    The haeccity business comes into play in discussions emanating from Max Black’s discussion of a universe containing only two identical spheres. The debate considers whether one can say that there are two objects if there is no property which distinguishes one sphere from another. It hinges on whether you allow naming a ball, aa, and then a predicate, −=a-=a.

    In my Structurepaper, I suggest that viewing the situation via an equivariant context BS 2\mathbf{B} S_2 is useful. In that context there are two things. In the empty context, the dependent product gives us nothing, and the dependent sum a singleton.

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2017
    • (edited Apr 1st 2017)

    Thanks, Mike, that makes sense. I have added that to the entry here. And also to the Idea-section at univalence.

1 to 16 of 16

  1.