Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’ve wondered in the past about the aptness of calling -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, , dependent on a type A. Say, I believe , then if we have a definitional equality , it should then also be the case that I believe . But if is another element of , and in fact 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:
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 -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.
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).
Yes, I would be pretty uncomfortable talking about “the fact that ”.
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.
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)
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.
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.
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.
The similarities are striking indeed. Here a diagram that connects some important terms from the Tractatus:
and in Pears/McGuinness translation
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.)
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.
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.
@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.
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
• – 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 as shorthand for ’Natural numbers’, etc.?
I would consider 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.
Ok, I guess if HoTT for philosophy gets going we’ll just have some explaining to do.
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 . 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!)
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.
, , , … Unless you don’t want to think of categories as types (I guess in some directed type theory they might be)
Right, I was thinking of sets, not categories. But even for categories, I would say is more of a notation like which stands for “the category of sets” like “the set of natural numbers”.
Hmm, is that so different from is the type of sheep, is the type of fields, 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. is not inhabited by circles.
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.
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’.
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.).
Re #20, maybe not so different. So maybe I should be okay with a notation like for the empty type. I would still want to pronounce it as “the type of facts that ” rather than just “fact that ”, though, just like I say “the set of real numbers” rather than “real number” for .
1 to 24 of 24