The n-Category Café

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.)

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.
Admitted.

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”.

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?

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.

“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).