Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology 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

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.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 5th 2016

    I’ve wondered in the past about the aptness of calling (1)(-1)-truncated types in HoTT ’mere propositions’. A proposition is something proposed, something that can be believed or not believed. A fact is something that is the case irrespective of belief.

    Take a proposition, P(x)P(x), dependent on a type A. Say, I believe P(a)P(a), then if we have a definitional equality aba \equiv b, it should then also be the case that I believe P(b)P(b). But if cc is another element of AA, and in fact id A(a,c)id_A(a, c) is inhabited, but this is as yet unknown, then we wouldn’t expect ’I believe P(c)’. There’s an opacity operating here, see de re and de dicto.

    Propositional extensionality, a case of univalence, reinforces the non-opacity:

    (P=Q)(PQ). (P=Q) \simeq (P\leftrightarrow Q) \,.

    When I was thinking up a way to apply generalized the to mere propositions, I thought that since a true proposition is contractible, there should be the same kind of ’the’ formation rule for it. However, ’the P’ is not something we say as we do ’the cat’, ’the product of two sets’, etc. However, we do say ’the fact that P’. I proposed then the type should be termed ’fact that P’, with ’the fact that P’ its unique term.

    Now I recently came across a philosopher, Zeno Vendler, who argues that if we are working up to the abstraction of what above is ’propositional extension’, then we should call these things ’facts’. Working up to definitional equality, he want to call propositions.

    So then, why not call the (1)(-1)-truncated types ’facts’, and then speak of ’factual extensionality’. I guess this has much to do with the tradition in mathematics of speaking of propositions as theorems, or even as axioms, e.g., in the case of Euclidean geometry.

    • CommentRowNumber2.
    • CommentAuthorUlrik
    • CommentTimeNov 5th 2016

    Just a quick thought: to me, a fact is something that is in fact true, so to speak, whereas I’ve gotten used to the idea that a proposition may or may not be true.

    Of course, in ordinary mathematics we mostly use “Proposition” the same way we use “Theorem”, as something that is provable. So perhaps that doesn’t matter so much.

    Some time ago there was a discussion on the HoTT list about whether “truth values” would serve better as a term for “propositions modulo typal equality” when we want “proposition” to preserve its intensional aspect. See this thread (and perhaps an earlier one).

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2016

    Yes, I would be pretty uncomfortable talking about “the fact that 0=10=1”.

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 6th 2016

    Well in the set up ’the fact that 0 = 1’ would be a putative term of type ’Fact that 0 = 1’. But of course the latter is empty so no ’the formation’ is possible.

    Maybe this isn’t quite how we speak but then I don’t think the public including philosophers think of propositions as in a family with sets. I don’t propose/believe/assert/deny a set, such as Sheep.

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 6th 2016

    Of course, in ordinary mathematics we mostly use “Proposition” …

    well, it is a proposition, and then the following proof constructs an inhabitant of that proposition, so it is actually a fact.

    @David C - makes me think to my back-burner project to think about the Tractatus via internal logic of a category (W talking about ’facts’ and ’what is the case’ and so on made the link to this)

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2016
    • (edited Nov 7th 2016)

    Wait, there’s a difference between calling the elements of (-1)-types “facts” and calling the (-1)-types themselves “facts”. The former seems much more defensible to me.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 7th 2016
    • (edited Nov 7th 2016)

    The idea was that just as we name a type by its elements, e.g., Dolly: Sheep, so we would have a type ’Fact that P’ with at most one element, and if P happened to be true, then precisely one element ’the fact that P: Fact that P’.

    So the type Sheep is not a sheep, and the type ’Fact that P’ is not a fact. ’The fact that P’ is a sole element if P is true, just as ’the sheep on the hill’ is a sole element of ’Sheep on the hill’ if that is a singleton.

    On the other hand, I can see that people tend not leave facts up in the air this way. A little scouting around the literature has suggested states of affairs, which many allow possibly not to obtain. If we pursue my trick, we might want

    the state of affairs that P: State of affairs that P.

    The SEP article points out that like facts, states of affairs resolve the opacity issue (#1):

    The state of affairs Marilyn Monroe’s being an actress and the state of affairs Norma Jean Baker’s being an actress, contain, in some sense, the same objects and properties as constituents in the same order. They are the same state of affairs under different names. However, I can believe that Marilyn Monroe is an actress while doubting that Norma Jean Baker is an actress. Hence, if there are states of affairs, they are not the content of propositional attitudes like belief; thoughts are.

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 7th 2016

    I knew this rang a bell, David R. having brought up the Tractatus. There are a couple of well-known translations which you can compare here.

    2 Was der Fall ist, die Tatsache, ist das Bestehen von Sachverhalten

    (a): What is the case, the fact, is the existence of atomic facts

    (b): What is the case—a fact—is the existence of states of affairs.

    Some prefer

    (c): What is the case—a fact—is the obtaining of states of affairs.

    That first translation (a) surely sounds awkward.

    • CommentRowNumber9.
    • CommentAuthorDaniel Luckhardt
    • CommentTimeNov 7th 2016
    • (edited Nov 7th 2016)

    The similarities are striking indeed. Here a diagram that connects some important terms from the Tractatus:

    Tatsache 2 Sachverhalte=2.01Verbindung von Gegenständen. (Sachen, Dingen) Form 2.033Möglichkeit der Struktur 2.034 Struktur \array{ & & Tatsache & \underset{2}{\ni} & Sachverhalte \mathrlap{\scriptsize{\underset{2.01}{=}\text{Verbindung von Gegenständen. (Sachen, Dingen)}} } \\ & & \downarrow & & \downarrow \\ Form & \underoverset{2.033}{\text{Möglichkeit der}}{\to} & Struktur & \underset{2.034}{\ni} & Struktur }

    and in Pears/McGuinness translation

    facts 2 states of affairs=2.01combination of objects (things) Form 2.033possibility of structure 2.034 structure \array{ & & facts & \underset{2}{\ni} & \text{states of affairs} \mathrlap{\scriptsize{\underset{2.01}{=}\text{combination of objects (things)}} } \\ & & \downarrow & & \downarrow \\ Form & \underoverset{2.033}{\text{possibility of}}{\to} & structure & \underset{2.034}{\ni} & structure }
    • CommentRowNumber10.
    • CommentAuthorDaniel Luckhardt
    • CommentTimeNov 7th 2016
    • (edited Nov 7th 2016)

    To understand the meaning of “fact” in the Tractatus the following passage from a letter from Wittgenstein to Russell from August 19, 1919 might be useful

    Ein Sachverhalt ist, was einem Elementarsatz entspricht, falls es wahr ist. Eine Tatsache ist, was dem logischen Produkt von Elementarsätzen entspricht, falls dieses Produkt wahr ist.

    (my own translation: A state of affairs is what corresponds to an elementary proposition, if it is true. A fact is what corresponds to the logical product of elementary propositions, if this product is true.)

    • CommentRowNumber11.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 7th 2016

    So in the truth table framework, columns correspond to atomic/elementary propositions which picture states of affairs. A row corresponds to a logical product which if it is true will collect all the corresponding states of affairs which make up a fact.

    Of course, those ’atoms’ proved hard to find, and so the story goes, one of the reasons for W. giving up on the Tractatus account was not seeing a way to decompose ’This is green all over’ and ’This is red all over’ to show their logical dependence.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2016

    I have a hard time thinking of any type in mathematics that we name by its elements; that seems to be mostly a CS thing.

    • CommentRowNumber13.
    • CommentAuthorDaniel Luckhardt
    • CommentTimeNov 7th 2016
    • (edited Nov 7th 2016)

    @David C

    Wittgenstein formulated this point in a letter to Waismann

    Viel gefährlicher ist ein anderer Irrtum, der auch mein ganzes Buch durchzieht, das ist die Auffassung, als gäbe es Fragen, auf die man später einmal eine Antwort finden werde. So habe ich z. B. geglaubt, daß es die Aufgabe der logischen Analyse ist, die Elementarsätze aufzufinden. Ich schrieb: über die Form der Elementarsätze kann man keine Angabe machen, und das war auch ganz richtig. Mir war klar, daß es hier jedenfalls keine Hypothesen gibt und daß man bei diesen Fragen nicht etwa so vorgehen kann wie Carnap, indem man von vornherein annimmt, die Elementarsätze sollten aus zweistelligen Relationen bestehen etc. Aber ich meinte doch, daß man später einmal die Elementarsätze würde angeben können.

    Probably I have to read the details again, but I am asking myself how W. could think that one could state (some day) the elementary propositions while one can not state the form of elementary propositions.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 7th 2016

    Mike #12, is your ambition limited to taking over mathematics?

    Outside computer science, there is physics, Quantization via Linear homotopy types:

    It should be plausible that using types instead of (just) propositons as the fundamental logical substrate suits formalization of fundamental physics, for here we are clearly concerned with talking not just about propositions, but about “things”, notably when talking about some type of fields, which we generically write

    FieldsHFields \in \mathbf{H} – a moduli space of fields.

    By the way,

    I have a hard time thinking of any type in mathematics that we name by its elements

    does this mean you don’t count ,,,...\mathbb{N}, \mathbb{Q}, \mathbb{R},... as shorthand for ’Natural numbers’, etc.?

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeNov 7th 2016

    I would consider \mathbb{N} as shorthand for “the set of natural numbers”. And I’m happy to similarly call the empty set “the set of facts that 0=1”.

    Of course there is more to the world than mathematics, but since mathematics is where we study logic and proofs, it seems appropriate to consider its sensibilities seriously when talking about propositions.

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 7th 2016

    Ok, I guess if HoTT for philosophy gets going we’ll just have some explaining to do.

    • CommentRowNumber17.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 7th 2016

    To my mind, W’s truth tables are just trying to grasp at the idea of subobject classifiers, and I think they are really just objects in the slice E/ΩE/\Omega. Certainly

    ’This is green all over’ and ’This is red all over’

    makes me think of local truth of a statement. I’ve raised the oddity of one of the early statements of Tractatus before (1.21), that seems to be an overly strong statement of classical logic:

    1.2 The world divides into facts.

    1.21 Any one can either be the case or not be the case, and everything else remain the same.

    I do wonder if this would be more meaningful in an internal/local sense (and of course allowing for non-classical logic!)

    • CommentRowNumber18.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 7th 2016

    I have a hard time thinking of any type in mathematics that we name by its elements; that seems to be mostly a CS thing.

    SetSet, VectVect, BoolBool, … Unless you don’t want to think of categories as types (I guess in some directed type theory they might be)

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeNov 8th 2016

    Right, I was thinking of sets, not categories. But even for categories, I would say SetSet is more of a notation like \mathbb{N} which stands for “the category of sets” like “the set of natural numbers”.

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 8th 2016
    • (edited Nov 8th 2016)

    Hmm, is that so different from SheepSheep is the type of sheep, FieldField is the type of fields, TypeType is the type of (small) types? Aren’t we thinking of types as concepts and elements as instances of those concepts?

    HITs don’t work that way. CircleCircle is not inhabited by circles.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 8th 2016

    Re #17, it’s a rather static picture. Presumably we’re to think of some atomic states of affairs (atomic facts in some translations) as saying how things are at particular time and place. I don’t think we’re to see properties as varying over time and space and then perhaps locally true or locally false.

    As for

    1.2 The world divides into facts

    and the earlier

    1.1 The world is the totality of facts, not of things,

    I know this has been criticised for saying of facts that are about the world, that they are in the world. A fact about a book in my room is not in my room.

    • CommentRowNumber22.
    • CommentAuthorDavidRoberts
    • CommentTimeNov 8th 2016

    I can’t remember if I said it before, but I expect the Yoneda embedding to play an important rôle in understanding some of what W was talking about. Thus

    A fact about a book in my room is not in my room.

    really reflects the fact that we are looking at your book in relation to all other things, including for instance ’being the colour of the leaves of the tree outside’.

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 8th 2016

    Yoneda and the idea of something’s nature being determined by its relations with other things puts me more in mind of the British idealists, such as Bradley and his theory of ’Internal relations’ Wikipedia. Russell and Moore were keen to refute this doctrine, arguing that destruction of an object Y related by relation R to a given object X need not affect X – R is external to X and Y.

    At this stage in W’s career he certainly see facts as possessing independence:

    1.2.1 Each item can be the case or not the case while everything else remains the same.

    Objects seem more complicated (2.01 etc.).

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeNov 8th 2016

    Re #20, maybe not so different. So maybe I should be okay with a notation like Fact 0=1Fact_{0=1} for the empty type. I would still want to pronounce it as “the type of facts that 0=10=1” rather than just “fact that 0=10=1”, though, just like I say “the set of real numbers” rather than “real number” for \mathbb{R}.