## February 20, 2013

### Have You Left Off Beating Your Wife?

#### Posted by David Corfield

Continuing the series of what type theory can do for philosophy, let us take a look at the infamous question of the title. To forestall criticism, let me say straight away that I’m not proposing in these posts that dependent type theory is the last word in the analysis of these puzzles. I’m merely exploring some issues for my own sake. If I manage to elicit comments such as Neel’s and Mike’s response on self-reference, I shall be very content.

So,

Have you left off beating your wife yet?

Where Bertrand Russell would take a belief as more complex than its surface structure might suggest, still he took it to concern a proposition, the kind of thing which is either true or false. As discussed before

The present king of France is bald

is really a composite:

There is something which is presently king of France, anything else which is presently king of France is the same as that thing, and it is bald.

Asked whether you believe ‘The present king of France is bald?’, you would say “No”, perhaps adding helpfully “There isn’t one.”

On the other hand, we saw that the type theoretic approach suggests that a proposition may depend on a number of presuppositions which are denoted in the ‘context’. So I cannot even form ‘the present King of France’ without first presupposing that there is presently a unique king of France.

A strand of British philosophers were not convinced by the new logic-driven philosophy of Russell, which arose in the early decades of the twentieth century. For R. G. Collingwood, propositions are answers to questions, and questions themselves rely on presuppositions, which are the answers to further questions. Collingwood gives the wife-beating question as an instance of the ‘fallacy of many questions’ to explain this idea. By “disentangling such knots” he resolves this question into a new set of four correctly ordered questions:

Have you left off beating your wife yet?

1. Have you a wife?
2. Were you ever in the habit of beating her?
3. Do you intend to manage in the future without doing so?
4. Have you begun carrying out that intention?

(An Essay on Metaphysics, p. 38)

Is the resemblance to building up a context sequentially in dependent type theory a coincidence? Collingwood gives no indication that he sought a new formalism, one better adapted than Russellian logic to account for the structure of our beliefs. But if such a formalism existed, there would surely be good reason to try out a Martin-Löf style type theory.

To form the type of the proposition ‘Punch has left off beating his wife’, we would need to form Punch as a person, establish that he has a wife, establish that he was in the habit of beating her, establish that he formed an intention to stop this habit, and then establish that he has successfully begun to carry out this intention.

There would have to be many kinds of dependent type formation operator involved here, such as perhaps

$x: Person, y: Action \vdash intend(x, y): Type$

$y: Action \vdash stop(y): Action.$

We would also need to make reference to the temporal aspect to deal with habits, forming an intention in the past, and continuing to act on it. Chapter 5 of Aarne Ranta’s book should help us here.

For Collingwood, presuppositions could be traced yet further back until a level he called the ‘constellation of absolute presuppositions’. These are a nebulous collection of generally unexpressed commitments, which we know we have reached when certain lines of enquiry upset our interlocutor.

Def. 6. An absolute presupposition is one which stands, relatively to all questions to which it is related, as a presupposition, never as an answer.

Thus if you were talking to a pathologist about a certain disease and asked him ‘What is the cause of the event $E$ which you say sometimes happens in this disease?’ he will reply ‘The cause of $E$ is $C$’; and if he were in a communicative mood he might go on to say ‘That was established by So-and-so, in a piece of research that is now regarded as classical.’ You might go on to ask: ‘I suppose before So-and-so found out what the cause of $E$ was, he was quite sure it had a cause?’ The answer would be ‘Quite sure, of course.’ If you now say ‘Why?’ he will probably answer ‘Because everything that happens has a cause.’ If you are importunate enough to ask ‘But how do you know that everything that happens has a cause?’ he will probably blow up right in your face, because you have put your finger on one of his absolute presuppositions, and people are apt to be ticklish in their absolute presuppositions. But if he keeps his temper and gives you a civil and candid answer, it will be to the following effect. ‘That is a thing we take for granted in my job. We don’t question it. We don’t try to verify it. It isn’t a thing anybody has discovered, like microbes or the circulation of the blood. It is a thing we just take for granted.’

He is telling you that it is an absolute presupposition of the science he pursues; and I have made him a pathologist because this absolute presupposition about all events having causes, which a hundred years ago was made in every branch of natural science, has now ceased to be made in some branches, but medicine is one of those in which it is still made.

Absolute presuppositions are not verifiable. This does not mean that we should like to verify them but are not able to; it means that the idea of verification is an idea which does not apply to them, because, as I have already said, to speak of verifying a presupposition involves supposing that it is a relative presupposition. If anybody says ‘Then they can’t be of much use in science’, the answer is that their use in science is their logical efficacy, and that the logical efficacy of a supposition does not depend on its being verifiable, because it does not depend on its being true: it depends only its being supposed (prop. 3).

In the case before us, clearly we have more digging to do. The question

Have you a wife?

presupposes all kinds of things, including the institution of marriage, the authority of the dignitary who performed the wedding service, etc. Way in the distance lie presuppositions such as the identity of persons.

What am I doing when I write

$Person: Type ?$

There are assumptions to be made as to the nature of personhood, perhaps relating to the metaphysicians’ question whether a person is wholly present at a moment or else is merely a time-slice of their whole trajectory. Then there are issues of moral agency,…

Posted at February 20, 2013 9:59 AM UTC

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

### Re: Have You Left Off Beating Your Wife?

What am I doing when I write Person:Type?

Let me strongly recommend Per Martin-Löf’s Siena lectures, On the Meaning of the Logical Constants and the Justifications of the Logical Laws, for an explanation of what many type theorists think happens when you form hypotheses and give proof terms for judgements.

I also thought Michael Dummett’s The Logical Basis of Metaphysics contained a very good exposition of the relevant issues, especially regarding the connections between anti-realism and proof-theoretic semantics. As a professional philosopher, I expect you will find Dummett’s prose style an easier row to hoe than I did! (Though in all fairness, it’s such an astoundingly good book I found it easy to persevere.)

Posted by: Neel Krishnaswami on February 20, 2013 3:10 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

I certainly remember reading Dummett in the first year of my philosophical studies. I wrote a dissertation on the proof-theoretic and topological semantics of constructive logic. I can’t say I found his row very hoe-able at the time. Perhaps years later I should return to it.

Posted by: David Corfield on February 20, 2013 3:56 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

It seems reasonable to me to regard implicit presuppositions as forming the ‘context’ of a statement in the type-theoretic, as well as the informal, sense.

Recent versions of the Coq proof assistant even have a nifty feature called “implicit generalization”, which basically says that if you refer to a variable that hasn’t been defined yet, then it is automatically added to the context as an additional hypothesis.

This is subject to certain controls to prevent typos from getting out of hand — you have to declare which variables can be implicitly generalized, and use a special backquote syntax in the first place where the variables to be generalized are mentioned. For instance, in the following declaration

Generalizable Variables A B.

Theorem foo (f : A -> B) : bar.


the variables A and B have not been defined when they are referred to, but since they are declared implicitly generalizable and occur first inside a backquoted assumption, they are implicitly added to the context. Their types are inferred from their first occurrence: in this case, both must be types. Thus it is as if we had written

Theorem foo {A B : Type} (f : A -> B) : bar.


It doesn’t seem too implausible to me to interpret Collingwood’s analysis as:

Parameter person : Type.
Parameter has_wife : person -> Type.
Parameter wife_of : forall (X : person) (hw : has_wife X), person.
Parameter action_by : person -> Type.
Parameter beating : forall (X : person), person -> action_by X.
Parameter was_doing : forall (X : person), action_by X -> Type.
Parameter stopped : forall (X : person) (A : action_by X) (wd : was_doing X A), Type.

Generalizable Variables hw wd.

Theorem loaded_question (you : person) : (stopped you (beating you (wife_of you hw)) wd).


Here I’m interpreting the phrase “your wife” as analogous to “the king of France”, which as we discussed last time takes an additional argument witnessing the existence of the object denoted. The Theorem above is not actually valid Coq, since implicit generalization can only happen in hypotheses rather than in conclusions, but this doesn’t seem essential to the philosophical idea. But if we change it to something like

Theorem loaded_question (you : person) (stopped you (beating you (wife_of you hw)) wd) : Type.


then Coq accepts it. Then with the command Check loaded_question we can see that the inferred type:

forall (you : person) (hw : has_wife you)
(wd : was_doing you (beating you (wife_of you hw))),
stopped you (beating you (wife_of you hw)) wd -> Type


has automatically added the implicit assumptions that you have a wife and that you were beating her.

Although after writing all this, it occurs to me that a simpler way to represent Collingwood’s analysis may be just with implicit arguments. If we declare the arguments that are left implicit in everyday speech to be implicit in Coq:

Arguments wife_of X [hw].
Arguments stopped X A [wd].


then if we try to say

Theorem loaded_question2 (you : person) : (stopped you (beating you (wife_of you))).


Coq complains that it “cannot infer the implicit parameter hw of wife_of”. Of course, if we add this argument explicitly:

Theorem loaded_question2 (you : person) (hw: has_wife you)
: (stopped you (beating you (@wife_of you hw))).


It likewise complains about the missing parameter wd of stopped`.

So perhaps that is the type theorist’s version of the negative MU: “Cannot infer implicit parameter”.

Posted by: Mike Shulman on February 21, 2013 1:54 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

So perhaps we can run through the classics of philosophy now, making sense of them with type theory.

When Descartes writes

I think, therefore I am,

he is observing that to form the proposition ‘I think’, this must rely on a context in which ‘I’ is declared to be a term of a type of existing things. I know that ‘I think’ is a proposition, and indeed a true one, since my wondering about it is a proof of it.

$mw: (I think)$.

Next stop:

Das Nichts selbst nichtet.

Must be something to do with the empty type:

$\not (-) = (-) \to \emptyset$

– the nothing itself negates?

Posted by: David Corfield on February 22, 2013 4:58 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

Hmm, is Heidegger a better dependent type theorist than Carnap?

Most metaphysicians since antiquity have allowed themselves to be seduced into pseudo-statements by the verbal, and therewith the predicative form of the word “to be,” e.g. “I am,” “God is.”

We meet an illustration of this error in Descartes’ “cogito, ergo sum.” Let us disregard here the material objections that have been raised against the premise–viz. whether the sentence “I think” adequately expresses the intended state of affairs or contains perhaps an hypostasis–and consider the two sentences only from the formal logical point of view. We notice at once two essential logical mistakes. The first lies in the conclusion “I am.” The verb “to be” is undoubtedly meant in the sense of existence here; for a copula cannot be used without predicate; indeed, Descartes’ “I am” has always been interpreted in this sense. But in that case this sentence violates the above-mentioned logical rule that existence can be predicated only in conjunction with a predicate, not in conjunction with a name (subject, proper name). An existential statement does not have the form “a exists” (as in “I am,” i.e. “I exist”), but “there exists something of such and such a kind.” The second error lies in the transition from “I think” to “I exist.” If from the statement “P(a)” (“a has the property P”) an existential statement is to be deduced, then the latter can assert existence only with respect to the predicate P, not with respect to the subject a of the premise. What follows from “I am a European” is not “I exist,” but “a European exists.” What follows from “I think” is not “I am” but “there exists something that thinks.” (Carnap, The Elimination of Metaphysics)

Contrast with Heidegger’s analysis:

The formula which the proposition sometime has, “Cogito ergo sum,” suggests the misunderstanding that it is here a question of inference. That is not the case and cannot be so, because this conclusion would have to have as its major premise: Id quod cogitat, est; and the minor premise: cogito; conclusion: ergo sum. However, the major premise would be only a formal generalization of what lies in the proposition: “cogito–sum.” Descartes himself emphasizes that no inference is present. The sum is not a consequence of thinking, but vice versa; it is the ground of thinking, the fundamentum. (Heidegger, Modern Science, Metaphysics, and Mathematics)

Is sum the assertion of a term of a type forming the context for the formation of the type cogito?

Posted by: David Corfield on March 23, 2013 5:04 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

Great breakdown of a question you should never answer if someone asks you. Was this, by chance, inspired by David Stern using this phrase in response to a reporter’s question?

Posted by: Brian on February 25, 2013 5:55 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

David –

Collingwood’s four questions look very much like a set of Critical Questions (CQs) which philosophers in Informal Logic and Argumentation Theory attach to Argument Schemes. The idea there is that a scheme gives a default conclusion, which is accepted unless an answer to one of the CQs suggests otherwise. For example:

Scheme: Expert E in domain D says conclusion C is correct, so we should accept conclusion C.

Critical Questions (for example):

1. Is E actually an expert in domain D ?

2. Do other people in this domain accept E’s expertise in D?

3. Is domain D relevant for conclusion C?

4. Is E disinterested in our acceptance or rejection of the conclusion? (ie, Does E stand to gain anything from our acceptance of C?)

etc.

These ideas have recently found application in AI, because the schemes and CQs provide a basis for non-monotonic reasoning. Indeed, the CQs can usually be readily turned into a formal dialog protocol under which a collection of intelligent agents may jointly interact to decide whether or not to accept the default conclusion.

Posted by: Peter McBurney on March 18, 2013 11:51 AM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

“To form the type of the proposition ‘Punch has left off beating his wife’, we would need to form Punch as a person, establish that he has a wife, establish that he was in the habit of beating her, establish that he formed an intention to stop this habit, and then establish that he has successfully begun to carry out this intention.”

I forgot to add: This sounds like the semantics for human language known as Discourse Representation Theory, which similarly involves the incremental construction of semantics for statements (jointly, by a group of dialogue participants).

Posted by: Peter McBurney on March 18, 2013 12:00 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

Interesting that the Stanford encyclopedia article on Discourse Representation Theory uses the same donkey examples that proponents (Ranta, Sundholm) of Martin-Löf dependent type theory use.

Is there any dialogue between the communities? I have to say that I’d feel reassured to have any formalism I used appear as mathematical well-grounded as the latter.

Posted by: David Corfield on March 18, 2013 1:09 PM | Permalink | Reply to this

### Re: Have You Left Off Beating Your Wife?

Philippe de Groot gave a talk on Type Theory for DRT at ESSLLI 2008, here.

Posted by: Peter McBurney on March 18, 2013 4:37 PM | Permalink | Reply to this

Post a New Comment