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.
Does the rheonomic modality have a characterization as $loc$ of anything?
Not that I know of.
I was just thinking of the pattern of NW and SE corners of the upper and lower sqaures of opposition. So $\sharp$, $\int$ and $\rightrightarrows$ are all $loc$ something.
EDIT: Maybe your comment on the other thread about co-localization changes this.
I corrected some typos a few days, but now they seem to be back. Is this a problem through copying from ’Modern Physics formalized in Modal Homotopy Type Theory’ which I didn’t correct?
civen ; wittnesses ; dependend ; truncated morphisms ; of the general concept A. (B) ; defn 2, H in bold ; prop 3 bar on square ; thouhgt ; productdahsvinternal twice ; loc≠¬ ; termimal ; quanitatively ; dash ; (♭⊣) ; this are ; an factorization ; concep ; RdashbI ; The negative Re¯¯¯¯- ; righsquigarrow
Talking of typos, I saw in ’Quantization via Linear Homotopy Types’ you have in Definition 2.7. fiber and cofiber wrong way around.
Ah, thanks and sorry for that. Yes, those paragraphs I have been editing separately on my private web and then copied them back in with their whole subsection. Sorry for this being somewhat counterproductive. I am editing in now the fix of the typos that you just provided.
regarding #101:
I was being stupid. It is indeed the rheonomy modality which is localization at $\mathbb{R}^{0\vert 1}$ in super formal smooth stacks.
Just as in the proof that $\mathbb{R}^1$-localization of the $\infty$-topos over $CartSp$ is given on representables by contracting away the powers of $\mathbb{R}^1$, so the $\mathbb{R}^{0\vert 1}$-localization contracts away powers of $\mathbb{R}^{0\vert 1}$.
This is really obvious, but I managed to get myself mixed up in variances. Anyway, better late than never.
The argument to take the $\mathbb{Z}/2\mathbb{Z}$ case in Science of Logic: solid substance is just that its simplest (and that we have discovered fermions)?
This means that the grading is not by a free group, but for instance by a finite cyclic group $\mathbb{Z}/n \mathbb{Z}$-grading. The minimal choice is $\mathbb{Z}/2\mathbb{Z}$-grading.
So what would happen with other gradings, such as happens with anyons? I see John Baez was interested in this many years ago,
And recently Covolo et al. look at $(\mathbb{Z}/2\mathbb{Z})^n$-gradings,
Classical Supersymmetry and Supergeometry are not sufficient to suit the current needs. In Physics, $\mathbb{Z}^n_2$-gradings, $n \ge 2$, are used in string theory and in parastatistics
and refer to John
…interesting to observe the parallelism of our extension with Baez’ suggestion of a common generalization – under the name of r-Geometry – of superalgebras and Clifford algebras with the goal to incorporate, besides bosons and fermions, also anyons into the picture [Bae92].
Is this kind of work just fishing for possible useful extensions? What happens to a paper like Z2 x Z2 graded superconformal algebra of parafermionic type?
Anyway, if there is something special about the super geometry/solid cohesion case, it would good to know what it is.
Thanks for coming back to this, this is a question that I would like myself to understand better.
Non-degenerate models for $\rightrightarrows \dashv \rightsquigarrow \dashv Rh$ should be provided by the toposes over sites of formal Cartesian spaces whose function algebras are further extended by $A$-graded pieces, for $A$ a cyclic group or products of such.
Maybe it’s good to have this generality, for some applications such as suggested by the texts you link to. But I am not sure if there is a compelling case made there. Maybe, I haven’t really thought about it enough.
But in any case it would seem good to know if there are axioms that would further narrow in on the supergeometric model.
One of them, and this might need more highlighting in the entry, is the Aufhebung $\stackrel{\rightsquigarrow}{\Im X} \simeq\Im X$. As the proof of prop. 15 in the entry shows, in the supergeometric model this holds because the even part $C^\infty(\mathbb{R}^{0\vert q})_{even}$ of the algebra of functions on a superpoint is nilpotent. This is a straight consequence of the crucial super sign rule $\theta_1 \theta_2 = - \theta_2 \theta_1$. In a more generally graded algebra, this sign rule is not present, and hence models based on more generally graded algebras would tend to violate this Aufhebungs-condition. But I haven’t systematically thought about if there are other kinds of graded algebras that, while not having the super-sign rule, would still satisfy the above Aufhebung. That would be good to think about.
There’s no way to make relevant to the Aufhebung story the claim that
In higher geometry/higher algebra supergeometry/superalgebra is intrinsic, canonically given
as truncation of sphere spectrum grading, is there?
Can we even see from the superalgebra truncation story why there should be a cohesion-elastic-solid pathway to supergeometry?
The idea that super-grading is a truncation of sphere-spectrum grading might still fit in. I haven’t thought this through yet, should do so at some point. But it could work. The main problem is maybe first still the one to realize that idea itself in a natural way, before even seeing how it connects to solid cohesion. The closest that I have come to this is, as you know, the paragraphs on $E_\infty$-arithmetic geometry here, with its parenthetical remark on supergeometry. But this supergeometric relation needs to be filled with more life.
Can we even see from the superalgebra truncation story why there should be a cohesion-elastic-solid pathway to supergeometry?
These three stages capture the three partial aspects of supergeometry
cohesion $\leftrightarrow$ smooth geometry;
elasticity $\leftrightarrow$ infinitesimal thickenings;
solidity $\leftrightarrow$ graded infinitesimals.
Conversely, this way supergeometry ended up beign the path by which I finally came to see the “solidity”-adjoints.
So I think this works out rather naturally and pleasingly.
By the way, I see I had a brief comment on the grading inssue in the subsection Formalization – Objective logic – Solid substance – Super, but it was maybe too brief to be intelligible. I have now expanded it a little more. It’s still terse though. (When you feel like editing anything in the entry, let me know, then I stop syncing it with the subsections that I keep copying over from my private web.)
These three stages capture the three partial aspects of supergeometry
cohesion $\leftrightarrow$ smooth geometry;
elasticity $\leftrightarrow$ infinitesimal thickenings;
solidity $\leftrightarrow$ graded infinitesimals.
Conversely, this way supergeometry ended up beign the path by which I finally came to see the “solidity”-adjoints.
Right, but there’s no way to break down $\pi_2(\mathbb{S}) \simeq \mathbb{Z}_2$ into such parts, is there?
Oh, I see, that’s what you mean.
But there is. So the key is that the $\mathbb{Z}_2$-grading is not any old $\mathbb{Z}_2$-grading, but goes along with $\mathbb{Z}_2$-graded commutativity, hence with the rule $\theta_1 \theta_2 = -\theta_2 \theta_1$ (which need not hold in a general $\mathbb{Z}_2$-graded algebra!). This in turn means that there is not just grading, but also infinitesimals, in a compatible way. Hence whenever we have $\mathbb{Z}_2$-graded geometry which is “graded commutative”, then we do have these three aspects: the underlying even geometry, its even infinitesimal thickening, and finally the graded infinitesimals.
Yes, but what does what you just wrote have to do with
$a \otimes b = (-1)^{deg(a) deg(b)} b \otimes a$The crucial super-grading rule (the “Koszul sign rule”)
in the symmetric monoidal category of Z-graded vector spaces is induced from the subcategory which is the abelian 2-group of metric graded lines. This in turn is the free abelian 2-group (groupal symmetric monoidal category) on a single generator.
What’s to stop there being a $\pi_3(\mathbb{S}) \simeq \mathbb{Z}_{24}$ form of cohesion with a similar Aufhebung story?
Maybe we should disentangle the idea with the $\mathbb{S}$-grading from the question of whether graded algebra other than superalgebra would give
$\stackrel{\rightsquigarrow}{\Im X} \simeq \Im X \,.$Because when you speak of the higher homotopy groups of $\mathbb{S}$, these will affect grading of some higher homotopies in derived function rings, and it is not clear to me if or how that affects the above relation.
Regarding ordinary graded algebra then the issue is that with a $\mathbb{Z}_k$-graded algebra with some sign rule such as, probably, given by factors of roots of unity $\exp(\frac{2\pi}{k} i)$, then it seems unclear that it follows that the non-0-graded part of the algebra is nilpotent (while it is this nilpotency that is needed for the above Aufhebung-condition).
Igor Khavkine was interested in that question in the comment section here. But I don’t know what kind of stable conclusion is reached there.
I added a few lines to the presentation of Aristotelian logic from “or rather,…” just above The method(absolute Idea).
Mostly this is just to add that we can represent “No A is B” by an arrow to $0$, and use this in a syllogism.
Was going to edit a little more, but it keeps freezing on me.
saw this hegel/physics related image on facebook and thought it was absolutely hilarious: http://asset-7.soupcdn.com/asset/16063/5715_7e47_520.jpeg
There’s no definition on the page of the negative of a monadic moment. Def. 1.13 just concerns comonadic moments. But it is needed shortly afterwards in the hexagon diagram, and then later for $\sharp$ in the comment on extensive quantities (which was really what I was trying to understand).
Elsewhere def 6.3, you give it as the fiber of the unit. So then how to add this to Science of Logic? The flow of the discussion there at 1.13 is all about what’s left of $\Box$ in the negative. So can one just run a parallel story about $\bigcirc$ and its relation to its negative?
So now to understand this:
objects which have purely the negative moment of continuity $\overline{\sharp}$ are codomains for “functions” which vanish on points and receive their contribution only from regions that extend beyond a single point
So I’m looking at those $Y$ which are equal to $\overline{\sharp} Y$? The latter is the homotopy fiber of the unit $Y \to \sharp Y$, so I must be working with a pointed object?
If I can make sense of this, I’d introduce it into intensive or extensive quantity, which does mention any modalities.
Does Hegel have a means of thinking cases where history progresses in one direction, but then it is later found that you can also branch off at a point in the past (which was previously marginal, but is now very important) into a different parallel history? If not (& I’m assuming that’s the case), would be interesting to think about how to formulate an idea of history that can embrace both of these views, & what the logic of such history would be.
(Thought about this after reading the last section (4.4) of Mochizuki’s latest paper, a philosophical section on the type of historical development I mentioned http://www.kurims.kyoto-u.ac.jp/~motizuki/Alien%20Copies,%20Gaussians,%20and%20Inter-universal%20Teichmuller%20Theory.pdf).
Sociological aspects aside, I think any kind of proof relevant logic goes some way towards warding off what Mochizuki calls the ’linear model’, since the essential content of past judgments is faithfully recorded by proof terms, not discarded — continuing the metaphors we might say that proof terms are like buds or potentialities dwelling in the historical ledger. So perhaps the latent injunction here to be aware of the life of the “dead” (not so much “read the masters”) will in the future just be the knowledge that eg. new proofs might automatically compose with old terms of a relevant type, etc. (?)
Near the quote given at proof relevance#prehistory we have some further related comments, in the context of a critique of extant mathematical reasoning as Hegel saw it:
[the necessity of a mathematical demontration] does not issue from the Concept of the theorem; rather it is commanded, and one must blindly obey the command to draw precisely these lines instead of an indefinite number of others, not because one knows anything but merely in the good faith that this will turn out to be expedient for the conduct of the demonstration. Afterwards this expediency does indeed become manifest, but it is an external expediency because it manifests itself only after the demonstration … As it proceeds, these determinations and relations are taken up while others are ignored, although one does not by any means see immediately according to what necessity. An external purpose rules this movement.
Thus demonstrations on this model appear as no more than self-fulfilling prophecies. He goes on to suggest such a model has no place in philosophy — but as we know, it needn’t in maths either.
proof relevance does help, but then you also have things like mochizuki’s frobenioids which were developed for IUT / proving the abc conjecture, but were only partially used towards that end. mochizuki gives frobenioids in their full depth (which would not be recovered from proof relevant logic alone, since they’re not fully involved in the proof of the abc or even IUT at large) as an example of something that is marginal now but could - who knows - be resurrected as central in a new development.
It turns out that editing the entry Science of Logic works again! (In the last months the system used to stall when saving further edits to the entry).
I have added one more reference (Asher 11) to my list of texts which argue the point that “type” in “type theory” is usefully read as a formalization of “concept”.
Thanks to David Corfield for pointing out this reference (here)!
Thanks to David Roberts
But $Id_{People}(David Roberts, David Corfield)$ is an uninhabited concept.
David, I am sorry. This is so embarrasing for me. I have fixed it now. Sorry again.
No worries! It was on my G+ post :-)
Another one. I’ve added:
where it says on page 129:
Types are general concepts: This statement represents the main conceptual basis of the whole idea of using CTT [constructive type theory] as a language to formalize knowledge processes.
Excellent! Thanks.
I’m getting closer to an explicit ’types are concepts’ claim. I’ve added
- Per Martin-Löf, Philosophical aspects of intuitionistic type theory, unpublished lectures given at the Faculteit der Wijsbegeerte, Rijksuniversiteit, Leiden, Sept-Dec 1993,
where he was recorded as saying
There is no question of talking of an object of type $\alpha$ unless $\alpha$ is a type, so the $\alpha$, the type, must come before $a$, come before the object, in this conceptual order. As $\alpha$ here is the universal general concept under which $a$, the object $a$, falls, the conclusion is that in the conceptual order the general concept, the universale, is prior to the object which falls under it. (Cited in P. Boldini, Des catégories aux types : un itinéraire en mathématiques appliquées, pdf)
Thanks, David. Now that’s of course the best we could hope for here, to have the statement made by Martin-Löf himself. Since he is quite philosophically minded, it makes me wonder whether he ever paused to notice that concept logic has been highlighted long before…
concept logic has been highlighted long before…
He would probably say ’Yes, by Aristotle’, but he’d prefer to retain the word ’category’:
Given how basic the very idea of type is, it is of course unthinkable that there shouldn’t be a word already in the tradition for what we here call types. You will all know that the traditional word for what I here call type is category. It was introduced by Aristotle and heavily used by Kant. I will show that the traditional use of the word coincides with the way I am using it here. What I call here the doctrine of types, the idea that an object is always an object of a certain type, really goes back to Aristotle.
Then he laments Mac Lane taking the word ’category’ for another purpose. (This is all in that Boldini article cited above. It’s a shame we can’t have access to notes from the lectures he’s given over the years.)
If you were hoping for mention of Hegel, I think this is unlikely. He strikes me as someone who follows other lines out of Kant. And yet, how close is the relationship between a type theorist’s types and Kant’s twelve categories?
concept logic has been highlighted long before…
He would probably say ’Yes, by Aristotle’,
Good, that’s just what is argued for in the Science of Logic article here: the sentences in Aristotle’s logic are typing judgements. And that’s the jumping-off point for Hegel’s “concept logic”.
Then he laments Mac Lane taking the word ’category’ for another purpose.
Luckily we now know that it is in fact the same purpose, just generalized to allow for “directedness”.
There is some net progress even in philosophy.
Our entry category (philosophy), being the stub that it is, lacks any mentioning of Aristotle. I don’t feel qualified. Could you maybe add a few lines to provide a minimum of substance for the entry? And then we should add that quote by Martin-Löf which you found!
how do we square the idea of “types are concepts” with “propositions as types”? I take it we don’t want to lump all 3 together, and even following propositions as some types, propositions would appear as a species of concept, which seems wrong…
how do we square the idea of “types are concepts” with “propositions as types”?
That’s immdiate. Proposition “X is blue”, Concept of blueness.
There’s something for now. Hopefully more later. The idea of an exhaustive list of categories seems lost to us (even Martin-Löf). But it’s interesting to reflect on whether there are basic types. One of the ways, I guess, is to think about joining implicit inclusions (join of maps). If you can’t quite see something, you say can say “it’s either a rabbit or a rock”, presumably as they’re both included in some basic kind of discrete, middle-sized entity. But we don’t go across the categories and say something is “cold, being beaten or an elephant”.
Thanks. I have added a line relating to Eilenberg-MacLane. Noticed that we didn’t even have that reference listed at category, so I put in there (Eilenberg-MacLane 45). One day maybe somebody finds the energy to bring our basic category-theoretic entries into better shape…
#136: yes, from Kant/Frege we have the relation — whose precise nature is another matter — between concepts and predicates, as in “concepts are predicates for a possible judgment” (KrV A69/B94). Now, a predicate is a dependent type, but I don’t see how propositions are concepts even if they involve the latter. Frege puts this in terms of the necessarily “unsaturated” nature of concepts, which I take to mean that specifically nullary predicates cannot count as concepts:
I regard it as essential for a concept that the question whether something falls under it have a sense. Thus I would call ‘Christianity’ a concept only in the sense in which it is used in the proposition ‘this (this way of acting) is Christianity’, but not in the proposition ‘Christianity continues to spread’. A concept is unsaturated in that it requires something to fall under it; hence it cannot exist on its own. That an individual falls under the concept is a judgeable content, and here the concept appears as predicative and is always predicative. In this case, where the subject is an individual, the relation of subject to predicate is not a third thing added to the two, but it belongs to the content of the predicate, which is what makes the predicate unsatisfied.
Perhaps I am just missing something very basic here.
Presumably we are to take the whole of ‘Christianity continues to spread’ as a type/concept, one whose warrants/instances are rather complicated. In long hand, it says something like ’over a time interval stretching some way into the past, the geographical range in which Christian acts (of sufficient frequency) were performed has expanded in (more or less) monotone fashion up to today’. We may imagine a series of maps purporting to display the truth of such a claim.
So predication is taking place concerning time series of areas.
“concepts are predicates for a possible judgment” (KrV A69/B94)
Now that”s excellent, I didn’t know about this statement from KrV. Thanks for highlighting this! I have now added a pointer to the Science of Logic entry here.
I was always puzzled by how hard it is to find authors who recognize Aristotelian logic as a kind of type theory. But combining Kant with Martin-Löf, then it’s right there.
The remaining issue you seem to have with predicates versus propositions seems to be independent of these considerations, and entirely covered by Curry-Howard and clarified by propositional truncation.
Curious to ask since I saw an interesting book coming out soon* which “convincingly sets out the philosophical kernel of Hegel’s view, reconstructing and updating it in such a way that it becomes a ‘live’ philosophical option for contemporary audiences” & addresses the highly socio-politically valuable question of whether or not we can make moral judgement and how to best do so:
“For many liberals, the question “Do others live rightly?” feels inappropriate. Liberalism seems to demand a follow-up question: “Who am I to judge?” Peaceful coexistence, in this view, is predicated on restraint from morally evaluating our peers. But Rahel Jaeggi sees the situation differently. Criticizing is not only valid but also useful, she argues. Moral judgment is no error; the error lies in how we go about judging.
One way to judge is external, based on universal standards derived from ideas about God or human nature. The other is internal, relying on standards peculiar to a given society. Both approaches have serious flaws and detractors. In Critique of Forms of Life, Jaeggi offers a third way, which she calls “immanent” critique. Inspired by Hegelian social philosophy and engaged with Anglo-American theorists such as John Dewey, Michael Walzer, and Alasdair MacIntyre, immanent critique begins with the recognition that ways of life are inherently normative because they assert their own goodness and rightness. They also have a consistent purpose: to solve basic social problems and advance social goods, most of which are common across cultures. Jaeggi argues that we can judge the validity of a society’s moral claims by evaluating how well the society adapts to crisis—whether it is able to overcome contradictions that arise from within and continue to fulfill its purpose.
Jaeggi enlivens her ideas through concrete, contemporary examples. Against both relativistic and absolutist accounts, she shows that rational social critique is possible.”
http://www.hup.harvard.edu/catalog.php?isbn=9780674737754
If we’re formalizing Hegel here… do people here ever envision it being possible to contribute something non-trivial to matters like those Jaeggi is concerned with? On the face of it category/type theory and moral judgement seem such radically different spheres that a non-trivial contribution would be absurd…. but, I nevertheless thought the question was worth asking.
And if the answer is negative - then what are the implications for a project like this of formalizing Hegel? Does it really capture Hegel if it can’t contribute to matters like these that Hegel can contribute to?
I should add that I’m glad this project exists …. just a collision of realms this different is difficult to wrap my head around.
*in english. it was published in german in 2014 as “Kritik von Lebensformen”
As you may observe, we have nothing on Grundlinien der Philosophie des Rechts (Elements of the Philosophy of Right). Perhaps if one took the Encyclopedia of the Philosophical Sciences seriously as a unified work, then any writing here on the Science of Logic as an expanded version of the shorter logic of the first part of the Encyclopedia, and on its realisation in Nature as described in the second part of the Encyclopedia, could form the basis for something to say on the third part – The Philosophy of Mind. The Philosophy of Right is seen as a development of this third part.
Quite a stretch, but something to note reading almost any of Hegel is the appearance of his key logical terms, such as universal, individual, particular. On the other hand, most present-day revivers of Hegel don’t take the logical aspects too seriously, and look rather to the spirit of his work rather than the details.
As for details, I don’t suppose we’ll be trying to reproduce the following any time soon:
The difference in the physical characteristics of the two sexes has a rational basis and consequently acquires an intellectual and ethical significance. This significance is determined by the difference into which the ethical substantiality, as the concept, internally sunders itself in order that its vitality may become a concrete unity consequent upon this difference. Thus one sex is mind in its self-diremption into explicit personal self-subsistence and the knowledge and volition of free universality, i.e. the self-consciousness of conceptual thought and the volition of the objective final end. The other sex is mind maintaining itself in unity as knowledge and volition of the substantive, but knowledge and volition in the form of concrete individuality and feeling. In relation to externality, the former is powerful and active, the latter passive and subjective. It follows that man has his actual substantive life in the state, in learning, and so forth, as well as in labour and struggle with the external world and with himself so that it is only out of his diremption that he fights his way to self-subsistent unity with himself. In the family he has a tranquil intuition of this unity, and there he lives a subjective ethical life on the plane of feeling. Woman, on the other hand, has her substantive destiny in the family, and to be imbued with family piety is her ethical frame of mind. (165-166, Philosophy of Right)