## Not signed in

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

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorDavid_Corfield
• CommentTimeDec 16th 2017
• (edited Dec 16th 2017)

There’s a great deal of discussion in philosophy about the relationship between knowledge and belief. One position has maintained that knowledge of a proposition amounts to belief in the proposition + the truth of the proposition + justification in believing it. Others look for greater divergence, e.g., Zeno Vendler claimed that knowledge is of facts and belief of propositions.

Our language sometimes appears to favour the former view:

• I know that there is milk in the fridge.
• I believe that there is milk in the fridge.

But taking a wider view, we find divergence:

• I know who you are.
• I believe who you are.

• I know the date of the wedding.

• I believe the date of the wedding.

It seems that we have to revert to propositions to converge again:

• I know (that) the date of the wedding is 5 March.
• I believe (that) the date of the wedding is 5 March.

Other divergences include that after knowledge claims, we can ask ’How do you know (that)?’, but we can’t ask similarly ’How do you believe (that)?’

Can we approach this array of linguistic usage type theoretically? I was led close to this territory in my ’the structure of’ paper, where to allow ’the introduction’ for a true proposition, I employed ’Fact that P’ as my type, and ’the fact that P’ as unique term.

What if Vendler’s right in that know and believe take different kinds of objects? Where the latter seems to apply to propositions, so a certain kind of type, ’know’ perhaps involves a term or element as well.

In a context $X: Person, P: Prop, p: P$, ’$X$ knows $P$’ would seem to have $X$ in some relation to $p$, whereas ’$X$ believes $P$’ only involves $P$.

Is this why when we have multiple elements, we can only use ’know’?

• I know the dates of our meetings.
• I believe the dates of our meetings.

Has Martin-Löf or any follower written on this?

• CommentRowNumber2.
• CommentAuthorDavid_Corfield
• CommentTimeDec 16th 2017

Instead of ’facts’ in mathematics, we speak of ’theorems’, etc.

We will confine ourselves to the logician’s usage, according to which a proposition is a statement susceptible to proof, whereas a theorem (or “lemma” or “corollary”) is such a statement that has been proven. (HoTT book, p. 17)

So,

• I believe (the mere proposition expressed by) the Poincaré conjecture (to be true).
• I know (a proof of) Pythagoras’ theorem (is true).

Maybe also this element/type distinction makes sense of knowledge/belief concerning sets.

• I know (of) (some) angels.
• I believe in angels.

Perhaps the latter is ’I believe $\vert \vert Angel \vert \vert$’, a proposition again.

• CommentRowNumber3.
• CommentAuthorDavid_Corfield
• CommentTimeDec 16th 2017

Ah, Tannaka et al. have come to a similar conclusion in Factivity and Presupposition in Dependent Type Semantics:

An advantage of dependent type theory is that it is equipped with proofs as first-class objects and thus enables us to analyze the factive verb know as a predicate over a proof (evidence) of a proposition…the notion of facts is not taken as primitive but analyzed in terms of the notion of evidence of a proposition.

They distinguish this ’know’ by evidence from a ’know’ by acquaintance. That seems to be the difference between:

• I know (the fact that) P.
• I know of (am acquainted with) the proposition P.
• CommentRowNumber4.
• CommentAuthorMike Shulman
• CommentTimeDec 17th 2017

Other divergences include that after knowledge claims, we can ask ’How do you know (that)?’, but we can’t ask similarly ’How do you believe (that)?’

That seems to me like just a random idiosyncracy of English; the grammatical way to ask the question is “Why do you believe (that)?”.

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeDec 17th 2017

The question/issue that Mike responded to might best be addressed to linguists.

• CommentRowNumber6.
• CommentAuthorDavid_Corfield
• CommentTimeDec 17th 2017
• (edited Dec 17th 2017)

Since the ’linguistic turn’, this is squarely in philosophical territory, and indeed much of the early work that linguists turn to has been carried out by philosophers: Ryle, Grice, Vendler, Austin, Reichenbach, Davidson,… Some have worried that their treatments are too local to English, but then the idea was only to map out particular conceptual landscapes, and if other peoples do things differently, then that just provides new material to chart.

I wonder how the why/how difference carries over to other languages. Perhaps in German

• Woher weiss du das?
• Warum glaubst du das?

Of course, German brings the interesting wissen/kennen distinction, along the lines of the end of #3.

But the main reason to raise this phenomenon here is whether we find something to which a type theoretic outlook is sensitive, here dependence on proof/evidence.

Tannaka et al. note an interesting feature of Japanese

• John-wa Mary-ga kita koto-o sitteiru.
• John-TOP Mary-NOM came COMP-ACC know.
• ‘John knows (the fact) that Mary came.’

Whereas for belief

• John-wa Mary-ga kita to sinziteiru.
• John-TOP Mary-NOM came COMP believe.
• ‘John believes that Mary came.’

In general, koto-clauses trigger factive presupposition, while to-clauses do not. This contrast can be captured by assuming that a factive verb like sitteiru takes as its object a proof (evidence) of the proposition expressed by a koto-clause, while a non-factive verb selects a proposition denoted by a to-clause.

• CommentRowNumber7.
• CommentAuthorMike Shulman
• CommentTimeDec 18th 2017

Then there is Wittgenstein’s

If there were a verb meaning “to believe falsely,” it would not have any significant first person, present indicative.

which makes one wonder what difference there can be between “I know” and “I believe”. In ordinary language, usually the latter simply conveys less certainty.

• CommentRowNumber8.
• CommentAuthorDavid_Corfield
• CommentTimeDec 18th 2017

In ordinary language, usually the latter simply conveys less certainty.

Right. After stating $P$, you may clarify your certainty by ’I believe/think that $P$’ or ’I know/am certain that $P$’.

One important tradition in philosophy looks to analyse ’knowledge’ in terms of ’belief + conditions’, e.g., knowledge is justified true belief. But rival positions take knowledge to be irreducible and not a kind of super-belief.

The first-person case that Wittgenstein is treating raises new issues, why we happily say ’He falsely believes $P$’ but not ’I falsely believe $P$’. Perhaps if type theory could point to a difference, it might be that the symbol $\vdash$ is involved in a subject’s judgments. Whereas ’he’ is used to refer to an individual, ’I’ is playing a performative role as expressing a locus of epistemic (and moral) responsibility. There’s a direct judgment of $P$ prior to ’I know that $P$’, but not in the case of ’he’.

Ah yes, we spoke about ’I’ and $\vdash$ in the first comments of Science of Logic, up to #9 (and then #12).

• CommentRowNumber9.
• CommentAuthorTim_Porter
• CommentTimeDec 19th 2017

I did a search for the corresponding discussion in French and found:

Croire, du latin credere, ”ajouter foi”. C’est une certitude sans preuve. La croyance a une portée psychologique, et non logique. Elle correspond à tous les degrés de probabilité, de l’opinion la plus vague à la vérité scientifique inscrite dans la mentalité commune (tout le monde “croit” aujourd’hui que la Terre est ronde) en passant par l’affirmation d’une transcendance dont l’existence est rationnellement indécidable (croyances religieuses).

Savoir, du latin sapere, ’avoir de la saveur’,’de la pénétration’, ’comprendre’. Le savoir, c’est la connaissance en général. C’est disposer de connaissances précises et solides dont on est en mesure de justifier le bien fondé et que l’on peut transmettre à d’autres. La philosophie est l’amour du savoir, synonyme de sagesse, les deux mots étant étroitement associés dans la tradition grecque.

Croire que l’on sait est source de dogmatisme, voire de fanatisme. Celui qui croit savoir ne cherche pas. Celui qui sait sait qu’il ne sait pas, tel Socrate, se met en quête de la vérité. Savoir s’oppose à ignorer mais non à douter. Il existe une ignorance qui ne doute de rien, et une ignorance qui cherche à savoir et parcourt le chemin du doute, tel Descartes. Même la science n’a de savoirs que provisoires, puisque «toute vérité est une erreur rectifiée», comme l’a souligné Bachelard.

This, thus, underlines the points made by David in #8. I especially like the discussion of Ignorance (which may have importance in today’s world of ‘fake news’ of various types.) The webpage link was here. This is fairly low level prepared for the Bacalaureat but other sites eg here show that in French, both in Philosophic discussion and linguistic ones the distinction is very similar to the Greek one and to that in English.

A good point may be in the quote:

dont on est en mesure de justifier le bien fondé et que l’on peut transmettre à d’autres.

In other words, knowledge can be transmitted to others as there is ’justification’ to back it up, but belief is not so easy to transmit. (I could be getting into deep water here so will not go on, leaving it up to others to comment if they so wish, but this does seem to me to be related to homotopy theory (and perhaps HoTT) with the idea that I know x and y are equivalent because of a path / homotopy, whilst I believe x and y to be equivalent is weaker (weak equivalence).)

There are, of course, other uses of ’know’ in English, e.g. to know a person (I know Ronnie Brown’ but I do not necessarily ‘believe’ him! ), which do not occur in French as there is a distinct term of knowing a person which does not exist in English to the same extent.

I am not sure that one would never say ’I believe falsely’ as I may know that belief is more easily duped than knowledge. Although all the evidence tells me otherwise I may believe the world is flat, it is just that I do not want to admit that I am wrong, and so do not accept the truth of what seems evident to others. From that perspective, ’person A falsely believes P’ has not that different a meaning as it is saying that the speaker/writer, (person B) believes that P is not true but the other (here ’A’} believes it false. (… and this is getting very near the situation of today’s society in several different parts of the world, especially with regard to ideas such as ‘global warming’, oh dear!!!)

• CommentRowNumber10.
• CommentAuthorDavid_Corfield
• CommentTimeDec 19th 2017
• (edited Dec 19th 2017)

(A knows that P) is a type in a context which must contain something like:

• $A: Person, P: Prop, x:P \vdash (A\;knows\;that P)(x): Type,$

whereas for belief

• $A: Person, P: Prop \vdash A\;believes\; that P: Type.$

But then how to represent the inference from ’A knows P’ to ’A believes P’? I guess either we have defined ’know’ in such a way that we extract the belief as a component through a projection, or else we could have a dedicated inferential function:

• $k: (A\;knows\;that \;P)(x) \vdash f(k): A\; believes\; that\;P.$

This brings to mind another issue in the literature, the difference between presupposition and consequence. In the Collingwood case, ’X has left off beating his wife’, this was taken to presuppose that X is married, that he was in the habit of beating his wife, that he formed an intention to stop, that he has since acted on this intention, and so on. If on hearing the statement we say ’So X is married then’, it seems to be a passage backwards to the implicit presuppositions, rather than an inference forward to new conclusions. Is there a difference type theoretically?

I suppose that if we have

• $\Gamma \vdash x: P$

then the object corresponding to $\Gamma$ is terminal in the slice over $\Gamma$, so there’s always a map from any object in the slice to it.

So maybe I have a statement $P$, and then build up a context in which it makes sense:

• $x_1:A_1,x_2:A_2, \ldots ,x_n:A_n \vdash P:Type$

and then since

• $x_1:A_1,x_2:A_2, \ldots ,x_n:A_n \vdash x_j: A_j, for 1 \leq j \leq n$

we have trivially

• $x_1:A_1,x_2:A_2, \ldots ,x_n:A_n, y: P \vdash x_j: A_j,$

at which point we forget the context and think we have an entailment

• $y: P \vdash x_j: A_j.$

This is to be contrasted with the case when we have the means in a context to derive a new proposition. Does that make any sense?

• CommentRowNumber11.
• CommentAuthorRichard Williamson
• CommentTimeDec 19th 2017
• (edited Dec 20th 2017)

There are, of course, other uses of ’know’ in English, e.g. to know a person (I know Ronnie Brown’ but I do not necessarily ‘believe’ him! ), which do not occur in French as there is a distinct term of knowing a person which does not exist in English to the same extent.

This is also true in Norwegian: å vite (used about knowing something) is rather different from å kjenne (used about knowing somebody). In many contexts, å kjenne is more like “to be familiar with”, but also can be used like “to feel”. Definitely I think these distinctions are relevant to the discussion here.

There is also a quite subtle distinction in English (and Norwegian) between the use of ’to believe’ and the use of ’to think’. Often one uses them interchangeably, especially when followed by ’that’. The distinction comes more, for instance, in ’believe in’ something. In Norwegian, one uses å tro (to believe) very commonly, in many places where one would use ’to think’ in English. “Å tenke” in Norwegian, ’to think’, is used much more restrictively. Moreover, Norwegian has a rather subtle distinction when it comes to expressing an opinion: “I think” in English can be ’jeg synes’ or ’jeg mener’ when one is offering an opinion, and one is never allowed to use ’jeg tror’ (“I believe”) when offering an opinion. ’Jeg mener’ is used when you have some kind of grounds for your opinion, e.g. if you are an expert on something or have experience of it. All of this is relevant, I feel.

• CommentRowNumber12.
• CommentAuthorDavid_Corfield
• CommentTimeDec 20th 2017

There must be quite a range of subtle distinctions marked by different languages. It seems that

“Turkish grammar requires speakers to indicate if an assertion is based on first hand knowledge or non-first hand knowledge (hearsay or inference).”

Back to Martin-Löf, I can’t find him distinguishing belief and knowledge. He speaks extensively about the latter as what arises from having judged in ’On the Meanings of the Logical Constants and the Justification of Logical Laws’.

• CommentRowNumber13.
• CommentAuthorTim_Porter
• CommentTimeDec 20th 2017
• (edited Dec 20th 2017)

Slightly aside from the main thread, David, are there subtle differences that could be made in the modal versions of knowledge i.e. in the epistemic logics? That turkish example, for instance, might suggest a direct knowledge operator, but then some version of the common knowledge idea but with the different chains of direct knowledge links being part of the history of the knowledge. I ask because years ago I discussed with a ’now-ex’ colleague the possible use of epistemic knowledge in AI using search in a network and that might be of relevance here as an interpretation.

(To partially answer my own question I found this)

• CommentRowNumber14.
• CommentAuthorDavid_Corfield
• CommentTimeDec 23rd 2017

Tim, I’m hoping we can find a role for the proof-relevance of the type-theoretic approach. There’s certainly room for some modal type theory around here.

Back with the presupposition/consequence distinction from #10, from an article by Ranta ’Constructive Type Theory’, he has

• $B$ presupposes $A$ meaning $x: A \vdash B(x): Type$.
• $A$ semantically entails $B$ meaning $x: A \vdash b(x): B$.
• CommentRowNumber15.
• CommentAuthorUrs
• CommentTimeDec 23rd 2017
• (edited Dec 23rd 2017)

There is one popular mathematical formalization of “belief”, that’s Bayesian inference.

But of course you are aware of this (your book is the first citation in our entry here! :-), so maybe what you are after here is something different?

There is an actual scientific issue still open here: What does it mean that our most fundamental theory of nature yields (only) something that looks like probabilities for events, hence which looks like belief, not like knowledge.

Physicists and and mathematicians haven’t been making any progress on this, except for producing speculations. Maybe a clever mathematical philosopher could help.

• CommentRowNumber16.
• CommentAuthorMike Shulman
• CommentTimeDec 24th 2017

FWIW, I think I’ve changed my mind about #4. A “why” question asks for a reason that something happened, or a reason that a person chose to do a certain thing as opposed to an alternative, whereas a “how” question asks for a process by which something occurred, or a method by which a person accomplished some desired goal. Comparing “why did you become a mathematician” to “how did you become a mathematician” the contrast is clear, and I can detect something of a similar contrast between “why do you believe X” and “how do you know X”. In fact, “how do you believe X” is not meaningless; I can imagine it being asked with a meaning like “I would like to believe that, but how do I convince myself of it?”. I can also imagine “why do you know X” being asked instead of “how do you know X”, notably in a context where the speaker already knows X but is surprised that the addressee does too – “how do you know X” carries more of a connotation that the speaker didn’t know X and needs to be convinced.

Of course this is probably old hat to philosophers of language. And I haven’t thought of anything intelligent to say related to type theory.

• CommentRowNumber17.
• CommentAuthorDavid_Corfield
• CommentTimeDec 24th 2017

Re #15, certainly something I intend to explore. If above I was contrasting knowledge as depending on an element of a proposition-type, and belief not, of course the Bayesian tradition has degrees of belief assigned according to the strength of the evidence, something less than proof. Then it would be a matter of relating to different strengths of evidence.

Since type theory became all the rage around these parts, I was wondering whether it might be possible to use it to understand the Raven paradox, which we spoke about once, namely the inconsistency of the set of propositions:

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.

To define ’black(x)’ we would need to know the type which it is depending upon.

Perhaps we need a probabilistic type theory. I know there are attempts, e.g., Probabilistic Type Theory and Natural Language Semantics.

• CommentRowNumber18.
• CommentAuthorDavid_Corfield
• CommentTimeDec 24th 2017

Re #16,

I can imagine it being asked with a meaning like “I would like to believe that, but how do I convince myself of it?”

Not surprising then to find it in a religious context. There’s a book by Pierre Teilhard de Chardin called Comment je crois, which looks to resolve the difficulty of integrating evolutionary theory with Christianity.

• CommentRowNumber19.
• CommentAuthorTim_Porter
• CommentTimeDec 24th 2017
• (edited Dec 24th 2017)

David: I do not see why ’All ravens are black’ receives no evidential support from the observation of a white tennis shoe.’ I would reject it because of the other statements. In this context perhaps ’little evidential support’ is exactly what one is looking for.

• CommentRowNumber20.
• CommentAuthorDavid_Corfield
• CommentTimeDec 24th 2017

Tim, yes, that’s one resolution of the paradox. And if you imagine glimpsing a white thing through your binoculars in a distant copse, it provides a potential falsifier. So when it turns out not to be a raven, that one fewer falsifier.

On the other hand, it would certainly be strange to look about your room for non-black things to check on whether they’re non-ravens. So it seems that it matters how we go about collecting our information.

• CommentRowNumber21.
• CommentAuthorTim_Porter
• CommentTimeDec 25th 2017
• (edited Dec 25th 2017)

BTW (and Happy Christmas to all reading this) White (albino) ravens exist (but are rare!) On Anglesey we have one of the highest concentrations of ravens in the UK (I regularly see several ravens flying over our house) but I have never seen a white one. (Newborough forest is called by some bird watchers the Ibiza of Ravendom as the young birds go there it seems to meet birds of the opposite gender!!! They seem to have a ‘right old time’, especially towards dusk!)

That is as may be but what is perhaps interesting from a philosophical viewpoint is that we seem to filter information a lot so prejudge the relevance of observations and so looking about the room as you suggest has low relevance unless you know there is a possibility of ravens in the room.

We thus have to work with partial models of ’reality’ and ’truth’. This is perhaps a type of ’possible worlds’ model but looking at the usual stuff on Possible worlds I do not think they go far enough. In Ai and data analysis they use mutiscale models for observational analysis and perhaps we should use a multifilter model for knowledge. (Is knowledge supposed to be absolute or can it be more nuanced?)

Have you every looked at the implications (if there are any) of the sort of ideas coming from Topological Data Analysis? There one looks for knowledge of the structure of a data cloud and one searches for persistent phenomena (measured topologically as it so happens) over different filter ’sizes’. (I can explain more if you think it might be interesting.)

• CommentRowNumber22.
• CommentAuthorMike Shulman
• CommentTimeDec 25th 2017

I think an important aspect of the raven paradox has to do with the fact that the statement “an instance of a hypothesis gives evidentiary support to that hypothesis” is not universally true but depends on the prior. There’s a classic example of a prior for which the observation of a black raven decreases the posterior probability that all ravens are black. This example is admittedly fairly contrived, but it seems reasonably likely to me that one could construct a sensible prior for which “’All ravens are black” (or its equivalent “all non-black objects are not ravens”) does receive evidentiary support from the observation of a black raven but not from the observation of a white shoe.

• CommentRowNumber23.
• CommentAuthorDavid_Corfield
• CommentTimeJan 13th 2018

Putting

• $A: Person, P: Prop, x:P \vdash (A\;knows\;that P)(x): Type,$
• $A: Person, P: Prop \vdash A\;believes\; that P: Type,$
• $k: (A\;knows\;that \;P)(x) \vdash f(k): A\; believes\; that\;P,$

together with Ranta’s

• $B$ presupposes $A$ meaning $x: A \vdash B(x): Type,$
• $A$ semantically entails $B$ meaning $x: A \vdash b(x): B,$

would suggest that knowledge entails belief, neither presupposes the other, and knowledge of a proposition presupposes its truth. This is a position that some hold.

• CommentRowNumber24.
• CommentAuthorDavid_Corfield
• CommentTimeJan 13th 2018
• (edited Feb 3rd 2018)

My student informs me that the exact correspondence in Modern Greek is:

• πιστεύω “believe something”
• ξέρω “know someone”
• γνωρίζω “recognize something as true/false”

I wonder how one signals true or false in the last case.

1. Re #7

Then there is Wittgenstein’s

If there were a verb meaning “to believe falsely,” it would not have any significant first person, present indicative.


Mandarin has a verb “yiwei” which means something quite like “to believe falsely”.

It’s attracted some detailed study recently (pdf). When used in the present first person, it’s interpreted as roughly “am under the possibly false impression that”, so it doesn’t contradict Wittgenstein’s point (and indeed provides evidence for it).

• CommentRowNumber26.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 3rd 2018

Thanks! I meant to look into the literature on context and presupposition. Now there’s also ’postsupposition’ to deal with. Of course, type theoretic versions of context are the way to go.

• CommentRowNumber27.
• CommentAuthorMike Shulman
• CommentTimeFeb 3rd 2018

Yes, thanks! However, the paper you linked to seems to me to be saying that “yiwei” doesn’t really mean “to believe falsely” even in the third person, but rather something like “to believe probably falsely” or “to believe without good reason”:

non-first-person yiwei strongly suggests that the speaker views the reported belief with skepticism. Sometimes, yiwei conveys that the speaker rejects the reported belief; but other times, the speaker simply finds it questionable or unwarranted.

• CommentRowNumber28.
• CommentAuthorColin Zwanziger
• CommentTimeFeb 3rd 2018
• (edited Feb 3rd 2018)

I think the traditional lexicography includes the definition “to mistakenly believe” (as Wiktionary does), but the paper indeed concludes it doesn’t quite mean that, and that may very well be.

Nevertheless there are some Wittgensteinian effects noted in the paper. For instance, it notes that if you say

wo renwei jintian you ge jiangzuo

I think today have Classifier talk

it can mean “I think there is a talk today” or “I thought there was a talk today”. But if you say

wo yiwei jintian you ge jiangzuo

I yiwei today have Classifier talk

it typically forces a past-tense interpretation. And it certainly can’t be interpreted as “I mistakenly think there is a talk today”!

• CommentRowNumber29.
• CommentAuthorMike Shulman
• CommentTimeFeb 4th 2018

So maybe a more linguistically realistic version of Wittgenstein’s comment would end with “its first-person present indicative would mean something else”.

• CommentRowNumber30.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 4th 2018

In that paper that Colin mentions, there’s talk of ’pragmatic inference’. There’s quite a debate in philosophy of language as to how sharp is the semantic/pragmatic distinction. I guess you might think of attempts to codify contexts into a logic with the richer range of constructions of a dependent type theory as playing down the split.

Continuing the line of #23, in a song that many poor parents in the UK have to suffer, we hear

If you’re happy and you know it, clap your hands.

So what is the ’it’ referring to there? Not the proposition ’You’re happy’, but its element ’the fact that you are happy’. When ’You’re happy’ is a true proposition, then it’s contractible, hence allowing ’the’ introduction, glossed as ’the fact that…’

We’re not going to have

If you’re happy and you believe it, clap your hands.

On the other hand, if we have been discussing a proposition $P$, and I say

If you believe it, then act accordingly.

The ’it’ there is referring to ’the proposition’ = $P$.

• CommentRowNumber31.
• CommentAuthorMike Shulman
• CommentTimeFeb 6th 2018

Not the proposition ’You’re happy’, but its element ’the fact that you are happy’.

Hmm… I would say “if you know that you’re happy” or “if you know you’re happy” but not “if you know the fact that you’re happy”.

(That song is plenty common in the US too.)

• CommentRowNumber32.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 6th 2018
• (edited Feb 6th 2018)

Or “if you know it to be the case that you’re happy”.

However one says it, I still like the idea that’s there’s a dependence on the element which marks the truth of the proposition. If we have

$X: Person, P: Prop, x: P \vdash Know(X, P, x): Type$

maybe the corresponding ’it’ refers to the pair $(P, x)$.

By the way, some slides on a talk I just gave arguing that ’and’ is covered better by dependent sum.

• CommentRowNumber33.
• CommentAuthorRichard Williamson
• CommentTimeFeb 6th 2018
• (edited Feb 6th 2018)

Hi David, I think you know Ranta’s work, so I suppose you are aware that the same view of ’and’ as a special case of dependent sum is in his book? He discusses many of the same kind of examples, e.g. ones that he refers to as ’progressive conjunctions’.

Nice talk, by the way!

• CommentRowNumber34.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 7th 2018

Yes, sure, I’m very in debt to Ranta.

2. Is your plan to make use of HoTT to refine Ranta’s picture? I would have thought that would definitely be new.

• CommentRowNumber36.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 7th 2018

Yes, that’s certainly part of the plan. My treatment of ’the’ as associated to a contractible type looks like it makes sense for groupoids and higher ones, and also in contexts such as equivariance under a group.

I haven’t looked much at ’and’ away from basic situations. A proposition like

• He used to lie in the sun and play cards

is really quite complicated. There must be a series of time intervals in which he lay in the sun, and for some reasonable number and length of subintervals of these intervals he played cards.

Perhaps for equivariance I could develop my noughts-and-crosses (tic-tac-toe) example. There in the context of the symmetries of the square, one can propose starting in the corner. Then a response might be to fill in an adjacent side square, so dependent on the corner. Maybe since the two adjacent squares to a corner are equivalent, we could use ’the’. (Perhaps a little forced.)

3. Yes, time is very fundamental in the Montague semantics, for instance, where modal logic is used to formalise it.

Do you have a groupoid example to hand?

The equivariance example is interesting. In the following..

Maybe since the two adjacent squares to a corner are equivalent, we could use ’the’

…were you referring to whether one can say ’start in the corner’? I think one can indeed say this in a certain context, e.g. if you are describing what you are doing to someone whilst you are doing it. And then I agree that the equivariance may be relevant to the meaning; one can say it regardless of which corner one chooses. If you meant ’fill in the adjacent side square’, then I’m not sure I agree that one can say it, even in the same kind of context. I am not sure exactly what makes the one meaningful and not the other.

• CommentRowNumber38.
• CommentAuthorRichard Williamson
• CommentTimeFeb 7th 2018
• (edited Feb 7th 2018)

Could it be that when we say ’the corner’, we are implicitly saying so in opposition to another distinct choice, i.e. not in the corner? Whereas with the two adjacent side squares, one has to choose between them, we do not see how to set them up in opposition to one another. In which case, equivariance seems to give a really nice explanation: one has to choose between things which are equivariant (like the two adjacent side squares), but one does not necessarily need to choose within an equivariance class. Was this the kind of thing you had in mind?

• CommentRowNumber39.
• CommentAuthorDavid_Corfield
• CommentTimeFeb 7th 2018
• (edited Feb 8th 2018)

So the idea was that in the equivariant case when I take the type of play squares to be acted on by the grid symmetry group, we have $\ast: \mathbf{B} G \vdash Square(\ast): Type$. So we then form the dependent sum, the orbits of the action, $\vdash \sum_{\ast: \mathbf{B} G} Square(\ast): Type$. Then an element of this type is ’the corner’ orbit. So I may say, “When I start a game, I like to open by playing in the corner”.

Now, one would probably ask “How would you then reply to the opponent’s play in an adjacent square?” rather than “the adjacent square”, even though “Which one?” won’t be asked. Maybe this is because symmetry has been broken, although we’d still have a reflective symmetry left that makes those two adjacent squares fall in the same orbit.

On the other hand, were the game interesting enough to warrant a theory on opening moves, then corner followed by adjacent side would be a single opening which we might call ’the X gambit’ as in chess, and we wouldn’t care which particular pair of squares was chosen.

4. Thanks! I think that the perspective of #38 goes through quite well here too. We can view ’adjacent side squares’ as an orbit, i.e. as an element of your dependent sum, so we can use this orbit as a ’the’, which is what we are doing in ’the X gambit’ (i.e. are using both ’the corner’). But there is no sense in which we can pick out something within the orbit, i.e. a single adjacent side square, and call it ’the’.

Also, I agree that we could regard ’in an adjacent square’ in your second paragraph as a kind of generalised ’the’, or a syntactic sugaring of ’the’, i.e of something like ’play in the next diagonal’.

• CommentRowNumber41.
• CommentAuthorMike Shulman
• CommentTimeFeb 8th 2018

If the grid symmetry group includes reflections, and we only use “the” for elements of contractible types, then it seems to me that we ought to say “respond on the adjacent side” but not “open in the corner”. The type of grids with an X in one corner and an O in an adjacent side is contractible (i.e. the grid symmetry group acts freely and transitively on the set of such grids), but the type of grids with merely an X in one corner is not, because each such grid has a nontrivial automorphism that reflects across the diagonal through that corner (the grid symmetry group acts transitively but not freely). Which makes it very intriguing that we intuitively say “open in the corner” but not “respond on the adjacent side”.

My initial guess would be that our brains aren’t wired to implement reflectional symmetry in the same way that we do rotational symmetry. After all, you can pick up the paper and move it around to implement rotational symmetry, but you can’t do the same with reflectional symmetry.

On the other hand, we do say something like “he poked me in the eye”…

• CommentRowNumber42.
• CommentAuthorMike Shulman
• CommentTimeFeb 8th 2018

I wonder to what extent this sort of “fine structure” of the definite/indefinite article distinction is language-dependent (or even dialect-dependent).