November 9, 2020

Posted by David Corfield

The British philosopher R. G. Collingwood wrote

…whenever anybody states a thought in words, there are a great many more thoughts in his mind than there are expressed in his statement. Among these there are some which stand in a peculiar relation to the thought he has stated; they are not merely its context, they are its presuppositions. (An Essay on Metaphysics, 1940, pp. 21-22)

In my book I proposed that dependent type theory is well-suited to represent such presuppositions, largely via the device of its notion of ‘context’ (pp. 57-58, 92). Ideas for this thesis came in part from discussions at the Café, including that generated by this post, concerning Collingwood’s treatment of the presuppositions of a complex question. Something perhaps worth developing then is a dependent type-theoretic treatment of questions.

Collingwood writes in his Autobiography:

…a logic in which the answers are attended and the questions neglected is a false logic. (Autobiography, 1939, p. 31)

What is ordinarily meant when a proposition is called ‘true’, I thought, was this: (a) the proposition belongs to a question-and-answer complex which as a whole is ‘true’ in the proper sense of the word; (b) within this complex it is an answer to a certain question; (c) the question is what we ordinarily call a sensible or intelligent question, not a silly one, or in my terminology it ‘arises’; (d) the proposition is the ‘right’ answer to that question. (R.G. Collingwood, Autobiography, p. 38)

What do we have then on the logical treatment of questions? Well the Stanford Encylopedia of Philosophy is a natural starting point. And consulting SEP: Questions, we find the briefest mention of a couple of type-theoretic approaches, but nothing on dependent types:

• Ciardelli, I., F. Roelofsen and N. Theiler, 2017. Composing alternatives, Linguistics and Philosophy, 40 (1): 1-36.
• Cooper R., Ginzburg J. 2012. Negative Inquisitiveness and Alternatives-Based Negation. In: Aloni M., Kimmelman V., Roelofsen F., Sassoon G.W., Schulz K., Westera M. (eds) Logic, Language and Meaning. Lecture Notes in Computer Science, vol 7218. Springer, Berlin, Heidelberg. doi

If presuppositions are usefully treated by dependent type theory, then we would expect this logic to account well for questions. This is a task Aarne Ranta begins in his Type-Theoretic Grammar (OUP, 1994, pp. 137-142), which I’ll look to expand somewhat here. If anyone knows of a place where this section of his book is developed, then please let me know.

A first distinction is between questions where it is presupposed that there is precisely one answer, and those where there may be any number of answers.

• ‘Who was in the bar last night?’ is likely to have multiple answers.
• ‘Which King of England reigned in 1507?’ has one.

Let’s just consider single-answer ones, for which Ranta mentions the following question types:

(1) $P$?, for $P$ a proposition.

(2) $P$ or $Q$?, which one?

(3) Who, when, what $X$, which $X$, whither, whence, whose, how, how much/many/ long: to be understood as $(Wh\; x: A)B(x)?$, for a proposition $B(x)$ depending on $A$.

(4) Iterated question: Who read which book? Who did what to whom? This is $(Wh\; x:A)(Wh\; y:B)R(x,y)$?, etc.

Notes:

• (2) isn’t quite $(P$ or $Q)$?, even constructively, as it’s not expected that you say ‘Neither’. It seems to be presupposed that precisely one is true.

• Ranta sees (1) as a case of (2), i.e., ‘$P$?’ is really ‘$P$ or not $P$?’.

• (3) should include requesting an element of a type, say a canonical term given a non-canonical term, What is 2 + 2? as $(Wh\; x: N)(x = 2+2)$?.

• Perhaps (2) $P$ or $Q$? could be taken as a case of (3) $(Wh\; x: A)B(x)$? in the sense that ‘$P(0)$ or $P(1)$?’ is $(Wh\;x: \mathbf{2})P(x)$?

Ranta doesn’t mention ‘why’ specifically, but I think it deserves special treatment.

(5) Why $P$? This is highly dependent on the nature of $P$, and the way the type that is $P$ has been generated by type formation rules and generators.

• In ordinary speech, $P$ will often speak of an event, and for this we need an analysis of the kind I give in II.6 of my book. I’ll talk about this more in a future post. For instance, if $P$ states that an activity is taking place with an intentional agent, then it may be asking for the achievement that will be the culmination of the activity. ‘Why does this state obtain?’ or ‘Why is the activity occurring?’ may request a previous activity or achievement. In a sense, then, this still asks $(Wh\; x: A)B(x)$?, ‘Which achievement does this activity aim for?’, ‘Which state prompted this activity?’, ‘Which activity brought about this state?’

So ‘Why are you running?’ may be answered by: ‘I want to get fit.’; ‘To get away from the fire.’; ‘To reach the shop before it closes’, ‘I was told to’, etc.

Have any kinds of question been missed above?

Let me sign off with another combative quotation from Collingwood:

…[questions] must be asked in the right order. Descartes, one of the three great masters of the Logic of Questioning (the other two being Socrates and Bacon), insisted upon this as a cardinal point in scientific method, but so far as modern works on logic are concerned, Descartes might never have lived. Modern logicians are in a conspiracy to pretend that a scientist’s business is to ‘make judgments’, or ‘assert propositions’, or ‘apprehend facts’, and also to ‘assert’ or ‘apprehend’ the relations between them; suggesting that they have no experience of scientific thinking, and wish to palm off, as an account of scientific thinking, an account of their own haphazard, unsystematic, unscientific consciousness. (The Principles of History, p. 29)

Posted at November 9, 2020 11:06 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3264

Re: Questions about Questions

It might be fun to look into connections between dependent type systems and logic-based query languages.

Some well-known examples of what I mean by logic-based query languages:

These are listed in order of increasing expressiveness, and λProlog is Turing-complete, so may be too different from natural language questions. But λProlog also seems the closest of the 3 to type theory. And I think logic programmers still have something called “queries”. (The goal clauses, I think.) None of these use dependent types.

(I figure the main threat to your program of basing philosophy on dependent type theory is not that it’s not powerful enough, but that it could appear to be an unnecessary complication. In programming languages too, many problems are successfully addressed without dependent types.)

You might try talking to Neel Krishnaswami about this. He has a blog post about a variant of Datalog he worked on, using some type systems ideas. (And he’s a type theorist who’s commented on this blog before.)

Twelf (stubby article on the nLab) is the only example I know of of a tool based on dependent types, and with a focus on logic programming. But other dependent type systems support it, via propositions-as-types and proof search.

Posted by: Matt Oliveri on November 9, 2020 10:33 PM | Permalink | Reply to this

Re: Questions about Questions

Ah yes, thanks. Query languages should be interesting.

I see there are dependently-typed language-integrated query systems (LINQs)

• Gregory Malecha, Ryan Wisnesky, 2015, Using Dependent Types and Tactics to Enable Semantic Optimization of Language-Integrated Queries (pdf)
Posted by: David Corfield on November 10, 2020 8:02 AM | Permalink | Reply to this

Re: Questions about Questions

I often mentally classify questions into yes-or-no questions (which ask for just a truth value), questions whose answer is an element of some well-defined set, and still more open-ended questions.

I like to ask yes-or-no questions, because I hope most people have the patience to at least give me one bit of information. But in practice, most people take these questions as a request for a long rambling discussion. I like answering yes-or-no questions when they’re well-formed. But in practice, they often involve mistaken presuppositions that prevent a simple answer. I suppose these are flip sides of the same coin! It reminds me of Nabokov, who complained of his apartment building where the neighbor downstairs had oversensitive ears and the one upstairs had feet of lead.

At the opposite extreme from a yes-or-no question, I hate getting questions in my email like “how does quantum entanglement work?”, where an answer would require guessing what the questioner knows or can understand.

Posted by: John Baez on November 10, 2020 8:55 PM | Permalink | Reply to this

Re: Questions about Questions

Right, how? is up there with why? in terms of open-endedness when it asks for a method or mechanism.

Ranta has the type-theoretic context play the role of what we assume is jointly accepted in a conversation. Guessing this is far from straightforward.

Then we have the capacity to recognise that others may make assumptions that we don’t share: ‘The ‘tiger’ you see at the bottom of the garden is wagging its tail.’

Posted by: David Corfield on November 11, 2020 8:09 AM | Permalink | Reply to this

Re: Questions about Questions

I agree that (1) is a case of (2), and that (2) is a case of (3). I also think (4) can be regarded as a case of (3) by combining the questions with tuples, e.g. $(Wh x:A)(Wh y:B) R(x,y)$ should be equivalent to $(Wh p:A\times B) R(p)$.

One might argue that (5) is also reducible to (3) by introducing a “type of reasons”, just as when encoding logic in type theory we represent a proposition by its “type of proofs”.

This general form of question (3) looks similar to the posing of a problem in a programming language: $A$ is the (simple) type of a function and $B$ is the specification it has to satisfy. (Similarly, in mathematics, we might have to define an object that satisfies some desired property.) Defining the function is answering the question; then proving the specification is justifying the answer, which could be considered to be answering a particular kind of “why” question: “why does $x$ have property $B$?”. Of course in a dependently typed language one can do both at once by constructing an element of $\sum_{x:A} B(x)$; I suppose in natural language one might end a wh-question with “and why?”.

Posted by: Mike Shulman on November 12, 2020 8:11 PM | Permalink | Reply to this

Re: Questions about Questions

Thanks.

Bas van Fraassen once gave an account of explanation in terms of contrast, so one is asking why this rather than that: Why did this happen rather than not happen? Why did this thing have that property rather than some other? Why is this happening now rather than later?

Maybe this is type-able.

Posted by: David Corfield on November 25, 2020 5:43 PM | Permalink | Reply to this

Re: Questions about Questions

Programming languages can do these “which?” selections (SQL is designed for them). The theory of relational databases has been a big field in CS since the 70s, and the industry standard language is SQL. As David mentions in his post, there is a subarea overlapping logic, philosophy of language and science, which looks at questions and tries to analyse what they are.

Outside of SQL, in R, one has the which() command, which returns the indices of a given argument vector satisfying the stated condition. (Though I don’t use Python or C++ much, they have similarly functionality.) E.g., if I assign the vector $(0,1,0,1,1,0,1,1,1,0)$ to $A$, like this,

$A \leftarrow c(0,1,0,1,1,0,1,1,1,0)$

then the command

$which(A \text{ == } 1)$

gives the indices,

$\text{2 4 5 7 8 9}$

I wondered if I could embed a function, $B$ to specify the condition:

$A \leftarrow c(0,1,0,1,1,0,1,1,1,0)$

$B \leftarrow function(x) \ \{ \ x \ \text{ == } \ 1 \ \}$

The function $B$ gives $\top$ if the input is 1, and $\bot$ otherwise.

Then the command,

$which(B(A))$

gives the same answer as before (i.e., answers “which (indices for) elements of $A$ satisfy $B$?”).

Posted by: Jeffrey Ketland on November 12, 2020 10:16 PM | Permalink | Reply to this

Re: Questions about Questions

I found your book “Modal Homotopy Type Theory” extremely useful and inspiring for developing the theory for strong AI. My approach is based on combining classical logic-based with deep learning. An interesting insight I got is that Google’s BERT, a deep-learning language model, can actually be viewed as an alternative form of logic via the Curry-Howard correspondence.

Another idea I have is that fuzzy logic may be viewed as a logic living on HoTT’s level 0 (the level of sets), where truth values are not just {0,1} but a real number in [0,1] depending on the ratio of set elements belonging or not belonging to some predicates. This explains why “mere propositions” have binary truth values.

(Sorry about the digressions…)

Re the issue of questions, I think it would be helpful to consider what is the nature of having a “question” in the mind of an intelligent system. Clearly this would be part of the mental “state” of the intelligent agent. Traditionally we think of the AI system’s state as constituted of logic propositions. Perhaps what you need here is to expand the scope to beyond traditional propositions (as “things that can be assigned truth values”). A question would be like a desire or a goal, which suggests the realm of planning and actions. Interestingly, again by the Curry-Howard correspondence, actions may be regarded as side-effects of programming.

Posted by: Yan King Yin on November 25, 2020 12:37 PM | Permalink | Reply to this

Re: Questions about Questions

Regarding the shift to $[0, 1]$ as truth values (or from sets to metric spaces), I was speculating in this direction in the post Summer Meanderings About Enriched Logic.