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 bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive constructive-mathematics cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration 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 lie-theory limit limits linear linear-algebra locale localization logic manifolds 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 simplicial space spin-geometry stable-homotopy-theory stack string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2015
    • (edited Apr 1st 2015)

    To me it seems like there is an evident interpretation of Aristotle’s logic in type theory, and I am wondering if there is any literature that discusses it this way.

    The Aristotlean “all AA are BB” is clearly to be interpreted as a function between types ABA \to B. According to taste demand that this function is mono, and feel invited to do so for all the ones mentioned in the following.

    The variant “some AA are BB” is a function out of a subtype of AA. Then “not every AA is BB” means that while there may be such functions out of subtypes, there is none out of AA itself and finally “no AA is BB” means that there is no function for no subtype. Similarly the Aristotlean “a is A” is a a global term a:*Aa \colon \ast \to A.

    Syllogisms then are nothing but function compositon.

    That seems clear enough. What would be a source that puts it this way and then expands on it?

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 1st 2015

    As a general point, some people in the ’Hegelian revival’ within analytic philosophy have been wondering whether something may have been lost in the passage to first-order logic. For example, Paul Redding in Analytic Philosophy and the Return of Hegelian Thought argues that there was a more expressive range of ways of negating in Aristotelian term logic.

    So the classic ’All men are mortal, Socrates is a man,…’ you want to want to represent as the composition of

    *Man \ast \to Man


    ManMortalBeing Man \to Mortal Being

    I guess one thing to say is that this interpretation is made manifest in the Venn diagram approach.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2015
    • (edited Apr 1st 2015)

    Thanks. I will have to finally look at that text by Redding. But so he doesn’t mention type theory either, does he?

    It seems hard not to see that Aristotle is speaking of the type of all mortals etc. . Somebody must have said this?

    Well, that article (Pagnan 13) which Thomas Holder had kindly pointed out a while back of course sort of does. I gather it includes precisely that idea of reading “all AA are BB” as functions between types ABA \to B. But then it has all this non-standard add-on to deal with the other classes of sentences, and while I can see where it is getting at, it strikes me as missing the opportunity of first making some very simple identifications, as in #1 above.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 1st 2015

    No, Redding doesn’t mention type theory.

    So how to think about these things? The story my colleagues would tell themselves is that syllogistic logic, which Kant claimed was little changed from Aristotle and unlikely to change in the future, was replaced by propositional and predicate logic. ’All me are mortal’ is now x(Man(x)Mortal(x))\forall x(Man(x) \to Mortal(x)).

    Recently, dependent type theory comes along and says, No, that statement is an inhabited dependent product x:ManMortal(x)\sum_{x: Man} Mortal(x). There is the question of where Mortal(x)Mortal(x) comes from. ManMan might be a subtype of some larger type on which mortality is a predicate. Then maybe by coercion that’s OK to speak of men as candidates for mortality.

    While I have two seconds, to remind myself later, how does Peirce’s diagrams feature. If the alpha graphs deal with propositional logic, and the beta graphs deal with predicate logic (recall that this gave Mike the diagrams for indexed monoidal categories), where do the Venn diagrams of the syllogism fit. Perice must have spoken of this as he knew mediaeval logic so well.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2015
    • (edited Apr 1st 2015)

    Why dependent types here? Sure, we know how to be much more sophisticated than Aristotle, but he considered something that is simplistic nowadays, so we should say it as simply as it is: “all AA are BB” is a function of types

    AB. A \longrightarrow B \,.

    And if you insist on inserting the mythical-sounding examples then it’s

    ManMortal. Man \longrightarrow Mortal \,.
    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 1st 2015
    • (edited Apr 1st 2015)

    Not good for a conversation when one has snatched moments, but I suppose in a least some cases of ’All Xs are Y’, the ’Y’ seems to be a predicate, and one might be less inclined to think of it as a type of ’Y things’. ’Everyone is preposterous’, PersonPreposterousThingPerson \to Preposterous Thing.

    I never got to think about the difference between Venn diagrams and Euler diagrams

  1. Re #1:

    The Aristotlean “all A are B” is clearly to be interpreted as a function between types A→B. According to taste demand that this function is mono, and feel invited to do so for all the ones mentioned in the following.

    This is similar to what you are saying, but another way of describing this is that a subtyping relationship holds between the types A and B seen as properties of some underlying domain (i.e., the “inclusion interpretation” of subtyping described at coercion).

    The variant “some A are B” is a function out of a subtype of A.

    I’m not sure about this: in general it is possible for A to have empty subtypes.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeApr 1st 2015
    • (edited Apr 1st 2015)

    @David, it would seem to me helpful not to consider those example that allude to complex real-world structures. Just as in set theory it helps to not talk about apples and oranges. I suggest to consider just those four sentences of the form “all AA are BB”, “some AA are BB”, etc.

    @Noam, so I should have said “non-empty subtype” then, but I suppose you get the idea anyway. There are clearly variants to consider, but the basic idea should be obvious enough.

    So is there anyone who discusses the inclusion interpretation of subtyping explicitly as something that in particular formalizes Aristotle’s logic?

    I am just looking for a reference that one could point to. I am not actually interested in developing a formalization of Aristotle’s logic, I think it’s pretty trivial. But I like the idea of “hey, look, what he did was really a kind of type theory” and I’d enjoy knowing a reference that would say so and expand on it a little, such that one could point people to it.

    Or if such a reference doesn’t exist yet, maybe you feel inspired to write one yourself! :-)

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2015
    • (edited Apr 3rd 2015)

    How outrageous would you find the following, in a context of informal exposition to an audience consisting of philosophers interested in mathematics and mathematicians interested in philosophy:

    If XX is a concept, a type, then the judgement x:Xx \colon X says that xx is an instance of the concept XX, or that xx is a term of type XX.

    A function A:XYA \colon X \longrightarrow Y takes instances/terms of XX to instances/terms of YY. If this is a monomorphism A:XYA \colon X \hookrightarrow Y then this says in words that AA wittnesses the fact that

    All instances of XX are instances of YY.

    or for short just

    All XX are YY.

    There is the unit type *\ast of which there is a unique instance. As a concept, this may be regarded as the concept of pure being: since any two instance of the concept just purely are, there is no distinction and hence there is a unique instance.

    Hence a function of the form I:*XI \colon \ast \longrightarrow X is equivalently an instance/term xx of XX. In words this says that

    Some xx is an instance of XX.

    of for short just

    Some xx is XX.

    Functions may be composed. Given I:*XI \colon \ast \to X and A:XYA \colon X \to Y, their composite is a function AI:*BA I \colon \ast \to B. In type theory this is an example of natural deduction, in words this is a syllogism

    All XX are YY.

    Some xx is XX.


    Some xx is YY.

    In summary

    Aristotle’s logic type theory
    All XX are YY. A:XYA \colon X \hookrightarrow Y .
    Some xx is XX. I:*XI \colon \ast \to X.
    syllogism natural deduction
    Some xx are YY. AI:*X A I \colon \ast \to X.
    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2015

    Some xx is XX.

    If you’re looking at Aristotelian syllogisms, they typically involve combinations of the forms:

    All S are P – universal affirmatives: All humans are mortal.

    No S are P – universal negatives: No humans are perfect.

    Some S are P – particular affirmatives: Some humans are healthy.

    Some S are not P – particular negatives: Some humans are not clever.

    There’s a question of what to do with a singular term, such as Socrates, and the idea that ’Socrates is a man’ is to be rendered ’All things identical to Socrates are men’

    To our ear, there’s something odd about universal affirmatives implying existence. So,

    All squares are rectangles. (MaP)

    All squares are rhombuses. (MaS)

    ∴ Some rhombuses are rectangles. (SiP)

    doesn’t work for us unless we know there’s a square.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2015
    • (edited Apr 3rd 2015)

    Ah, I see that Thomas Holder has secretly been adding the kind of references that I was asking for above. Thanks!

    And I am relieved to see that on p.46 of PalmeReyes-Macnamara-Reyes 94 at least some of what I suggested above is said (and attributed to Lawvere).

    (Relieved because I was losing faith in humanity that with all the erudition thrown at this, something so obvious would never have been mentioned.)

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2015
    • (edited Apr 3rd 2015)

    David, almost missed your message, we overlapped in #10, #11.

    I have to admit that I have trouble following the suggestions that it’s all very subtle in Aristotle’s logic. I think it’s all rather simplistic, but a bit imprecise at some points. A few millennia later, we are not to build epicycles that capture the imprecision, we are to highlight the precise elegant theory that we see is intended.

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2015

    But he never says

    Some xx is XX,

    and nor does anyone else, as far as I know, unless perhaps when we come to the weird untyped world of predicate logic where they write

    There is/exists xx which is XX.

    In a way that’s the larger point of my comment before: for Aristotle, categories presuppose membership, hence we can do things like go from ’All As are B’ to ’Some A is B’. So you really never need to say ’Some xx is XX’ in Aristotelian logic. This isn’t epicycles, it’s a core feature of the system.

    From #12, perhaps you’re not doing Aristotelian logic but then I’m lost as to who you think would want to say ’Some xx is XX’.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2015

    Oh, in ’Some xx is XX’ perhaps you mean a named individual, such as ’Socrates is a man’.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeApr 7th 2015
    • (edited Apr 7th 2015)

    Sorry for the delay, somehow I missed the further replies.

    I am thinking that the case of an individual is a degenerate case of the “all BB are AA” statement for the case that BB is a concept with an single individual instance. For what it’s worth, in Hegel’s “Science of Logic”, which seems to mean to be commenting on Aristotle, this “E-B-A”-figure with an individual (EE) being a particular (BB) which in turn are generals (AA) is the main case that is considered.

    Sorry if the “epicycles” came across badly, I just meant to express that one shouldn’t make this more complicated than it is. We should capture the intention of Aristotle’s logic with modern hindsight, and when there is a subtlety or imprecision in Aristotle then this shouldn’t make us introduce unnatural case distinctions, but we should observe that from a modern perspective it all sorts itself out neatly. From a modern perspective, we have no trouble with a type that has a single inhabitant.

    I have expanded a bit more on how I see the Aristotlean judgements “Some B are A”, “Individual E is B” and “Some B1 is B2” here. I think their evident formalization nicely matches respectively, existence of function types, unit type, and product types (all in context) hence matches neatly to the structure dependent type theory / in a locally Cartesian closed category.

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 8th 2015

    If “Some A is B” is to be taken in a context C, then when we carry out the syllogism with “All B are D” to conclude “Some A is D”, then we’d need to have that D in the context C too, so that we can form the fiber product A × C\times_C D, right?

    You just wrote “(all in context)”, so I guess so.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeApr 9th 2015
    • (edited Apr 9th 2015)

    Yes, I would say that

    Some B 1B_1 is B 2B_2.

    All B 2B_2 is AA.

    Some B 1B_1 is AA.

    is well thought of as having categorical semantics by top horizontal composites in diagrams of the form

    B 1×CB 2 B 2 A B 1 C \array{ B_1 \underset{C}{\times} B_2 &\longrightarrow& B_2 &\longrightarrow& A \\ \downarrow && \downarrow & \swarrow \\ B_1 &\longrightarrow& C }

    By the way, on a somewhat different note: do any of the ancients, or anyone for that matter, explore a logic that knows about statements of the form “XX is similar to YY”?

    As I mentioned to you in Bristol, it occurs to me that this is the right natural language rendering of

    X=Y \bigcirc X \;=\; \bigcirc Y

    for a modality/moment \bigcirc. The modality projects out some details and retains only some pure quality, hence two types may be different but similar with respect to \bigcirc if after coarse-graining away all details except their pure \bigcirc-aspect, then they become equal.

    For instance S 1S^1 is similar to S 1×(ε,ε)S^1 \times (-\epsilon,\epsilon) in that they differ, but have the same shape.

    (For what it’s worth, this is what the section “The difference” in the Science of Logic is all about. For instance §906 is the remark that all XX and YY whatsoever are similar, in that they are at all. This is formalized as similarity in the above sense, with respect to the *\ast-modality. )

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 9th 2015


    B 1×CB 2 B 2 A B 1 C \array{ B_1 \underset{C}{\times} B_2 &\longrightarrow& B_2 &\longrightarrow& A \\ \downarrow && \downarrow & \swarrow \\ B_1 &\longrightarrow& C }

    I guess we should pass to

    B 1×CA A B 1 C \array{ B_1 \underset{C}{\times} A &\longrightarrow& A \\ \downarrow && \downarrow \\ B_1 &\longrightarrow& C }

    I never heard of a logic of similarity. It’s normally raised as a relation which is not transitive, but here I guess we don’t want that.

    Well I suppose really the issue is that we may have X and Y similar by projecting according to one modality, and Y and Z similar through another, but there might no substantial modality to allow comparison of X and Z. By choosing ’orthogonal’ modalities, one could see this phenomenon maximally.

    Non-transitivity of similarity with respect to the ’same’ standard is often discussed. In there’s some kind of proximity relation between terms, x may be near y and y near to z, but x not near z.

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 9th 2015

    We haven’t covered negative varieties of syllogism, such as

    No flowers are animals.

    All flowers are plants.

    ∴ Some plants are not animals.

    Best left alone, or should we give it a try?

    E.g., ’No B 1B_1 is B 2B_2’ could be expressed via a map from B 1×CB 2B_1 \underset{C}{\times} B_2 to 00.

    Speaking of negation, it occurred to me the other day that we might treat the Raven’s Paradox. This is the idea that it is incompatible to hold all four of

    1. ’All ravens are black’ is logically equivalent to ’All non-black things are non-ravens’.
    2. ’All ravens are black’ receives no evidential support from the observation of a white tennis shoe.
    3. ’All non-black things are non-ravens’ receives evidential support from the observation of a white tennis shoe.
    4. Logically equivalent statements receive equal support from the same evidence.

    I was going to question whether ’All non-black things are non-ravens’ is well-formed, but working in a context maybe that’s not right. So then in the context of ThingThing there is an arrow RavensBlackthingsRavens \to Black things, and I guess we could have an arrow the other way between complements.

    I see Wikipedia has a large page on the paradox.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeApr 9th 2015
    • (edited Apr 9th 2015)

    Regarding Aristotlean negation:

    E.g., ’No B 1B_1 is B 2B_2’ could be expressed via a map from B 1×CB 2B_1 \underset{C}{\times} B_2 to 00.

    Yes, that would be my suggestion, too.

    Regarding the raven paradox: this reminds me of the ongiong discussion of whether or not we have seen evidential support for the non-existence of supersymmetry.

    • CommentRowNumber21.
    • CommentAuthorTim_Porter
    • CommentTimeApr 10th 2015

    Within AI there are similarity logics related to concept analsysis and data processing. (I did a Google search on similarity logic as I remembered seeing something that might be relevant years ago!) It also relates, apparently, to probabilistic logic.

    As to the ravens, what is to be the definition of ‘evidential support’?

    • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 10th 2015

    As to the ravens, what is to be the definition of ‘evidential support’?

    The original motivation was one where it was seen as broadly accepted that any incidence of an A that is B counts as evidence for ’All As are B’. But then any non-B thing which is non-A ends up counting as evidence for ’All non-Bs are non-A’ which is logically equivalent to ’All As are B’.

    Spelling it out a little more, the Bayesians might cash support out as the condition that evidence ee has this feature with respect to hypothesis hh, plausibility increases: P(h|e)>P(h)P(h|e) \gt P(h).

    You can work with this formula to say that the white tennis shoe does provide a modicum of support for All Ravens are black in that glimpsing a white thing, it was a potential falsifier. On finding it is a tennis shoe, the threat is over, so you should feel more confident in the rule.

    You can see that something like this in the context of a class you have where you wonder is it the case that ’All right-handers are taller than 1.6m’. It’s a reasonable strategy to check out those under 1.6m, and any one you find who is left-handed should boost your hypothesis.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 10th 2015

    Re #19: there’s something missing, namely existence of a flower.

    No unicorns are seen without a horn.

    All unicorns are equines.

    Hence some equines are seen with a horn.

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 10th 2015

    Re #23, yes I mentioned in #10 another appearance of what to us is the oddity of taking a universal to imply existence. I wonder if there’s any way to see a kind of motivation for this.

    I have a feeling, and you’d be well placed to help us Todd, we should spend some time on Peirce. He must have had interesting things to say on the syllogism.

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 10th 2015

    Just in case I need it, would you say that syllogism of #19 is Bocardo?

    • CommentRowNumber26.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 10th 2015

    I took it from wikipedia where they calls it Felapton.

    Bocardo is

    Some cats have no tails.

    All cats are mammals.

    ∴ Some mammals have no tails.

    • CommentRowNumber27.
    • CommentAuthorTim_Porter
    • CommentTimeApr 10th 2015

    I learnt one famous syllogism early on when a teenager, and it is mentioned in the Wikipedia page on Arisotelianim:

    Bertrand Russell criticizes Aristotle’s logic on the following points:[29]

    The Aristotelian system allows formal defects leading to “bad metaphysics”. For example, the following syllogism is permitted: “All golden mountains are mountains, all golden mountains are golden, therefore some mountains are golden”, which insinuates the existence of at least one golden mountain.[30] Furthermore, according to Russell, a predicate of a predicate can be a predicate of the original subject, which blurs the distinction between names and predicates with disastrous consequences; for example, a class with only one member is erroneously identified with that one member, making impossible to have a correct theory of the number one.[31]

    The syllogism is overvalued in comparison to other forms of deduction. For example, syllogisms are not employed in mathematics since they are less convenient.[31]

    The golden mountains example trips people up still. I have tried it in talks etc in ‘popularisation’ contexts.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeApr 10th 2015

    Regarding that criticisms by Russell:

    on the off-chance that anyone cares I may re-iterate my opinion that I find such nit-picking on evident and foremost simple and easily fixed inaccuracies in the otherwise insightful thinking of an ancestor from millennia ago, poor intellectual practice. Maybe it’s my physics background, maybe in the history of physics one is more used to insight being approximate and proceeding gradually; an analogy that comes to my mind is dismissing, say, Leonardo DaVinci’s insights on the ground that he didn’t draw the trajectories of cannonballs quite realistically. Doing so would be a narrow-mindedness on our part that would reflect worse on us than on Da Vinci.

    For Russell I would hope that his criticism originates in the desire to boast his own brilliancy rather than in the actual intellectual failure of recognizing the little implicit assumption that one has to grant Aristotle left implict, and be it unconciously.

    The claim that syllogisms are not very useful in mathematics is maybe usefully reflected on after reading Martin-Löf’s 1996 lectures (pdf) and asking how many colleagues outside type theory one would find who could readily agree that the verbose aguments therein of the sort that “to judge that A and B we are to judge that A and that B” would be useful to them. Indeed, it seems indulging in the tautological, and yet we know now that to get to the bottom of it in logic, it pays to identify that which is trivially trivial.

    This brings me back to the beginning of this thread. I find it surprising that apparently almost nobody has articulated Aristotlean’s logic for what it’s achievement is: a primitive logic of types, including, I would say, at least function types and intersection of types. I imagine Aristotle and Martin-Löf would have had a good time chatting.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeApr 10th 2015

    One actually still finds logicians nowadays who implicitly assume that all domains of quantification are nonempty.

    • CommentRowNumber30.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 12th 2015
    • (edited Apr 12th 2015)

    Added a quote from Aristotle giving a definition of a syllogism

    A ‘syllogismos’ is an argument (logos) in which, (i) certain things being posited (tethentôn), (ii) something other than what was laid down (keimenôn) (iii) results by necessity (eks anagkês sumbainei)(iv) because these things are so. By ‘because these things are so’ I mean that it results through these, and by ‘resulting through these’ I mean that no term is required from outside for the necessity to come about.

    • CommentRowNumber31.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 13th 2015

    Re #30, great. I’ll use that in next year’s slides for Intro to Logic.

    Reminding ourselves of the dominance of Aristotle’s views in logic for over 2000 might go a little way to explaining Russell’s criticisms (#28). Kant had said that little had changed up to his day, and it was unlikely to do so in the future. So it must have seemed exhilarating to think you were going to usher in a new way of doing things:

    The old logic put thought in fetters, while the new logic gives it wings. It has, in my opinion, introduced the same kind of advance into philosophy as Galileo introduced into physics, making it possible at last to see what kinds of problems may be capable of solution, and what kinds are beyond human powers. And where a solution appears possible, the new logic provides a method which enables us to obtain results that do not merely embody personal idiosyncrasies, but must command the assent of all who are competent to form an opinion. (Bertrand Russell, ‘Logic As The Essence Of Philosophy’, 1914)

    It seems it was the most recent philosophical use made of the old logic that Russell really objected to.

    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeApr 13th 2015
    • (edited Apr 13th 2015)

    re #31, yes, I can see that people were stuck, and it’s a shame that for over 2000 years nobody recognized that there remains something to be fixed with and something to be added to Aristotle’s logic.

    Still, it feels like somebody of Russell’s stature missed a chance here. Imagine where we could be now had he said back then:

    Ah, okay, so this idea of having some types is really good, it helps to prevent paradoxes. Let’s just be careful that in Aristotle’s examples many of these types are secretly in some implicit context. I suggest we make this explicit by introducing types depending on other types. Then the naive “All AA are BB” I suggest should be refined by an operation which I suggest to denote by AB\prod_A B. Also, we should make explicit that as Aristotle moves a type from subject to predicate, he is once looking at, say “Mortal” as the type of all mortals, and once as the proposition that somebody is mortal. This conflation seems really deep, I suggest we call it “propositions as types”, but it is worth making it a bit more explicit, too.

    And so forth.

    But then, I suppose the spirit has to take all these detours to work itself out. It’s a slow process. ;-)

    • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 13th 2015

    There’s something of a split between those who think change will happen anyway (Die List der Vernunft) in its own time, and those who think it needs a little encouragement. This was true also of Hegelian-inspired Marxism.