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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeApr 1st 2015
   • (edited Apr 1st 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexTo me it seems like there is an evident interpretation of [Aristotle's logic](http://ncatlab.org/nlab/show/syllogism#SEP) in type theory, and I am wondering if there is any literature that discusses it this way. The Aristotlean "all $A$ are $B$" is clearly to be interpreted as a function between types $A \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 $A$ are $B$" is a function out of a subtype of $A$. Then "not every $A$ is $B$" means that while there may be such functions out of subtypes, there is none out of $A$ itself and finally "no $A$ is $B$" means that there is no function for no subtype. Similarly the Aristotlean "a is A" is a a global term $a \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?

   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 $A$ are $B$” is clearly to be interpreted as a function between types $A \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 $A$ are $B$” is a function out of a subtype of $A$. Then “not every $A$ is $B$” means that while there may be such functions out of subtypes, there is none out of $A$ itself and finally “no $A$ is $B$” means that there is no function for no subtype. Similarly the Aristotlean “a is A” is a a global term $a \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?

2. • CommentRowNumber2.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 1st 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexAs 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 $$ \ast \to Man $$ and $$ Man \to Mortal Being $$ I guess one thing to say is that this interpretation is made manifest in the [Venn diagram](http://philosophy.lander.edu/logic/syll_venn.html) approach.

   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

   $$\ast \to Man$$

   and

   $$Man \to Mortal Being$$

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

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeApr 1st 2015
   • (edited Apr 1st 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexThanks. 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](http://ncatlab.org/nlab/show/syllogism#Pagnan13)) 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 $A$ are $B$" as functions between types $A \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.

   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 $A$ are $B$” as functions between types $A \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.

4. • CommentRowNumber4.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 1st 2015
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexNo, 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 $\forall x(Man(x) \to Mortal(x))$. Recently, dependent type theory comes along and says, No, that statement is an inhabited dependent product $\sum_{x: Man} Mortal(x)$. There is the question of where $Mortal(x)$ comes from. $Man$ 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.

   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 $\forall x(Man(x) \to Mortal(x))$.

   Recently, dependent type theory comes along and says, No, that statement is an inhabited dependent product $\sum_{x: Man} Mortal(x)$. There is the question of where $Mortal(x)$ comes from. $Man$ 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.

5. • CommentRowNumber5.
   • CommentAuthorUrs
   • CommentTimeApr 1st 2015
   • (edited Apr 1st 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexWhy 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 $A$ are $B$" is a function of types $$ A \longrightarrow B \,. $$ And if you insist on inserting the mythical-sounding examples then it's $$ Man \longrightarrow Mortal \,. $$

   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 $A$ are $B$” is a function of types

   $$A \longrightarrow B \,.$$

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

   $$Man \longrightarrow Mortal \,.$$
6. • CommentRowNumber6.
   • CommentAuthorDavid_Corfield
   • CommentTimeApr 1st 2015
   • (edited Apr 1st 2015)
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexNot 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', $Person \to Preposterous Thing$. I never got to think about the difference between Venn diagrams and [Euler diagrams](http://en.wikipedia.org/wiki/Euler_diagram)

   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’, $Person \to Preposterous Thing$.

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

7. • CommentRowNumber7.
   • CommentAuthorNoam_Zeilberger
   • CommentTimeApr 1st 2015
   • PermaLink
   Author: Noam_Zeilberger
   Format: MarkdownItexRe #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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorUrs
   • CommentTimeApr 1st 2015
   • (edited Apr 1st 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItex@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 $A$ are $B$", "some $A$ are $B$", 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! :-)

   @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 $A$ are $B$”, “some $A$ are $B$”, 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! :-)

9. • CommentRowNumber9.
   • CommentAuthorUrs
   • CommentTimeApr 3rd 2015
   • (edited Apr 3rd 2015)
   • PermaLink
   Author: Urs
   Format: MarkdownItexHow 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 $X$ is a concept, a type, then the [[judgement]] $x \colon X$ says that $x$ is an instance of the concept $X$, or that $x$ is a [[term]] of type $X$. A [[function]] $A \colon X \longrightarrow Y$ takes instances/terms of $X$ to instances/terms of $Y$. If this is a [[monomorphism]] $A \colon X \hookrightarrow Y$ then this says in words that $A$ wittnesses the fact that > All instances of $X$ are instances of $Y$. or for short just > All $X$ are $Y$. 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 \colon \ast \longrightarrow X$ is equivalently an instance/term $x$ of $X$. In words this says that > Some $x$ is an instance of $X$. of for short just > Some $x$ is $X$. Functions may be composed. Given $I \colon \ast \to X$ and $A \colon X \to Y$, their composite is a function $A I \colon \ast \to B$. In type theory this is an example of [[natural deduction]], in words this is a [[syllogism]] > All $X$ are $Y$. > Some $x$ is $X$. Hence > Some $x$ is $Y$. In summary | [[Aristotle's logic]] | [[type theory]] | |----------------------------|----------------------| | All $X$ are $Y$. | $A \colon X \hookrightarrow Y $. | | Some $x$ is $X$. | $I \colon \ast \to X$. | | [[syllogism]] | [[natural deduction]] | | Some $x$ are $Y$. | $ A I \colon \ast \to X$. |

   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 $X$ is a concept, a type, then the judgement $x \colon X$ says that $x$ is an instance of the concept $X$, or that $x$ is a term of type $X$.

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

   All instances of $X$ are instances of $Y$.

   or for short just

   All $X$ are $Y$.

   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 \colon \ast \longrightarrow X$ is equivalently an instance/term $x$ of $X$. In words this says that

   Some $x$ is an instance of $X$.

   of for short just

   Some $x$ is $X$.

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

   All $X$ are $Y$.

   Some $x$ is $X$.

   Hence

   Some $x$ is $Y$.

   In summary

   Aristotle’s logic	type theory
   All $X$ are $Y$.	$A \colon X \hookrightarrow Y$.
   Some $x$ is $X$.	$I \colon \ast \to X$.
   syllogism	natural deduction
   Some $x$ are $Y$.	$A I \colon \ast \to X$.

10. • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex>Some $x$ is $X$. If you're looking at Aristotelian [syllogisms](http://en.wikipedia.org/wiki/Syllogism), 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.

    Some $x$ is $X$.

    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.

11. • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2015
    • (edited Apr 3rd 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexAh, 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](http://ncatlab.org/nlab/show/syllogism#PalmeReyesMacnamaraReyes94) 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.)

    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.)

12. • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeApr 3rd 2015
    • (edited Apr 3rd 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexDavid, 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.

    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.

13. • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexBut he never says >Some $x$ is $X$, 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 $x$ which is $X$. 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 $x$ is $X$' 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 $x$ is $X$'.

    But he never says

    Some $x$ is $X$,

    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 $x$ which is $X$.

    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 $x$ is $X$’ 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 $x$ is $X$’.

14. • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 3rd 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexOh, in 'Some $x$ is $X$' perhaps you mean a named individual, such as 'Socrates is a man'.

    Oh, in ’Some $x$ is $X$’ perhaps you mean a named individual, such as ’Socrates is a man’.

15. • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeApr 7th 2015
    • (edited Apr 7th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexSorry 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 $B$ are $A$" statement for the case that $B$ 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 ($E$) being a particular ($B$) which in turn are generals ($A$) 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](http://ncatlab.org/nlab/show/Science+of+Logic#JudgementInFormalization). 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.

    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 $B$ are $A$” statement for the case that $B$ 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 ($E$) being a particular ($B$) which in turn are generals ($A$) 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.

16. • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 8th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexIf "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 $\times_C$ D, right? You just wrote "(all in context)", so I guess so.

    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 $\times_C$ D, right?

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

17. • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeApr 9th 2015
    • (edited Apr 9th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexYes, I would say that > Some $B_1$ is $B_2$. > All $B_2$ is $A$. > *** > Some $B_1$ is $A$. is well thought of as having categorical semantics by top horizontal composites in diagrams of the form $$ \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 "$X$ is similar to $Y$"? As I mentioned to you in Bristol, it occurs to me that this is the right natural language rendering of $$ \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^1$ is similar to $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](http://ncatlab.org/nlab/show/Science+of+Logic#906) is the remark that all $X$ and $Y$ whatsoever are similar, in that they are at all. This is formalized as similarity in the above sense, with respect to the $\ast$-modality. )

    Yes, I would say that

    Some $B_1$ is $B_2$.

    All $B_2$ is $A$.

    ---

    Some $B_1$ is $A$.

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

    $$\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 “$X$ is similar to $Y$”?

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

    $$\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^1$ is similar to $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 $X$ and $Y$ whatsoever are similar, in that they are at all. This is formalized as similarity in the above sense, with respect to the $\ast$-modality. )

18. • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 9th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexFrom $$ \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 $$ \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.

    From

    $$\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

    $$\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.

19. • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 9th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexWe 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_1$ is $B_2$' could be expressed via a map from $B_1 \underset{C}{\times} B_2$ to $0$. 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'. 1. 'All ravens are black' receives no evidential support from the observation of a white tennis shoe. 1. 'All non-black things are non-ravens' receives evidential support from the observation of a white tennis shoe. 1. 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 $Thing$ there is an arrow $Ravens \to Black things$, and I guess we could have an arrow the other way between complements. I see [Wikipedia](http://en.wikipedia.org/wiki/Raven_paradox) has a large page on the paradox.

    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_1$ is $B_2$’ could be expressed via a map from $B_1 \underset{C}{\times} B_2$ to $0$.

    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 $Thing$ there is an arrow $Ravens \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.

20. • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeApr 9th 2015
    • (edited Apr 9th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexRegarding Aristotlean negation: > E.g., 'No $B_1$ is $B_2$' could be expressed via a map from $B_1 \underset{C}{\times} B_2$ to $0$. 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.

    Regarding Aristotlean negation:

    E.g., ’No $B_1$ is $B_2$’ could be expressed via a map from $B_1 \underset{C}{\times} B_2$ to $0$.

    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.

21. • CommentRowNumber21.
    • CommentAuthorTim_Porter
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: Tim_Porter
    Format: MarkdownItexWithin 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'?

    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’?

22. • CommentRowNumber22.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItex>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 $e$ has this feature with respect to hypothesis $h$, plausibility increases: $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.

    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 $e$ has this feature with respect to hypothesis $h$, plausibility increases: $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.

23. • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexRe #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.

    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.

24. • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe #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.

    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.

25. • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexJust in case I need it, would you say that syllogism of #19 is [Bocardo](http://en.wikipedia.org/wiki/Syllogism#Bocardo_.28OAO-3.29)?

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

26. • CommentRowNumber26.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexI took it from [wikipedia](http://en.wikipedia.org/wiki/Syllogism) where they calls it Felapton. Bocardo is >Some cats have no tails. >All cats are mammals. >∴ Some mammals have no tails.

    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.

27. • CommentRowNumber27.
    • CommentAuthorTim_Porter
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: Tim_Porter
    Format: MarkdownItexI 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.

    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.

28. • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: Urs
    Format: MarkdownItexRegarding 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](http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.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.

    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.

29. • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeApr 10th 2015
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOne actually still finds logicians nowadays who implicitly assume that all domains of quantification are nonempty.

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

30. • CommentRowNumber30.
    • CommentAuthorDavidRoberts
    • CommentTimeApr 12th 2015
    • (edited Apr 12th 2015)
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexAdded 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.

    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.

31. • CommentRowNumber31.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 13th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexRe #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.

    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.

32. • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeApr 13th 2015
    • (edited Apr 13th 2015)
    • PermaLink
    Author: Urs
    Format: MarkdownItexre #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 $A$ are $B$" I suggest should be refined by an operation which I suggest to denote by $\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. ;-)

    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 $A$ are $B$” I suggest should be refined by an operation which I suggest to denote by $\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. ;-)

33. • CommentRowNumber33.
    • CommentAuthorDavid_Corfield
    • CommentTimeApr 13th 2015
    • PermaLink
    Author: David_Corfield
    Format: MarkdownItexThere'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.

    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.