Type Theory and Propositions
Posted by David Corfield
One of the things that philosophers will take a lot of getting used to, if HoTT is to be taken up as a new logic for philosophy, is the idea of propositions as a kind of types. We are very used to treating propositions with propositional logic, and then sets very differently, with first-order logic and some set axioms. This results in different issues arising for the latter, as when a philosopher worries about the ontological commitments of a simple piece of applied set theory or even applied arithmetic. It appears that speaking of two apples on my desk, I’m referring to some abstract entity . Then I’m to worry what kind of entity this number is, and how I can know about it. Applying logic by itself to the world is generally taken not to incur any such ontological debt.
Now, we are beginning to hear in analytic philosophy the idea that propositions are types, for instance, in the work of Hanks and Soames that propositions are types of predicative acts, as when we predicate wisdom of Socrates in ‘Socrates is wise’.
From the HoTT perspective, we will often have
where from we can then form . And we can think of this type as predicating of . But propositions may arise by other routes, such as for a set and two of its elements, e.g., is it the case that the tallest person in the room and the youngest person in the room coincide. Another form of proposition is generated as for a type . The latter is known as the bracket type where any elements of are identified. The proposition will be true when is inhabited. So if, say, is the type of occurrences of Kim drinking coffee yesterday, corresponds to the proposition whether Kim drank coffee yesterday.
Judging a proposition to be true is to judge the type to be inhabited. Propositions are just those kind of types which are subsingletons, or subterminal objects. Establishing that Kim drank coffee yesterday it doesn’t matter if you tell me about her morning espresso or her afternoon latte, they correspond to necessarily equal elements, and , in the mere proposition. We might be interested in the mere proposition rather than the set when all we care about is whether she drank any coffee that day (maybe it’s going to react with some medication) rather than a list of occurrences.
Taking propositions as subterminal objects makes sense of another conception of propositions that one encounters in the philosophical literature, namely, as the set of possible worlds (para. 6) in which they hold. This derives from a tradition which has looked to understand modal logic in terms of possible worlds. We can understand this viewpoint as concerning operations in a category varying over an object of worlds , what we call the slice category or over category. Then a subterminal object here corresponds to a monomorphism into , or in other words a subset of worlds for a set .
Something to be gained by HoTT is uniform type formation, so that, e.g., is set product for sets and conjunction for propositions, while is the set of functions for sets and is implication, , for propositions. This explains all those analogies between logic and arithmetic, which otherwise seem to be mere coincidences, such as
is True if and only if is True,
These are each generated by a single adjunction.
[I’ll leave as an exercise how to understand and as resulting from counting sets occurring in two adjunctions, and what the logical analogues amount to.]
But what about the philosophers’ disanalogy in ontological commitment between logic and arithmetic?
When we say of a proposition that it is true, we’re saying that the type is equivalent to the type . When we say ‘ is false’, we’re saying that the type is equivalent to the type . , the empty type, is defined in HoTT inductively as the type with no constructors. The unit type, , is the type with a unique term, or the product type with no factors. We can also produce as , with its sole element, . These are both propositions.
HoTT allows us to form the type of natural numbers inductively, and then also inductively , a set with elements. is equivalent to , and is equivalent to . When we say there are two apples on the table, we are saying that there is an equivalence between the type of apples on the table and .
We may take and to be part of the syntax, no more ontologically committing than is as product or conjunction. Or perhaps it might be argued that reference is being made to some ‘pure types’. Either way, there should be parity of treatment between applying logic and applying arithmetic/set theory if you adopt HoTT.
Re: Type Theory and Propositions
I am a little confused. Lets say I can form the type (apples on the table) : Type. Then to say that there are two apples on the table is to give a term
(there are two apples on the table) : ||(apples on the table) = Fin(2)||
It seems I have two types on hand – (apples on the table) and a type Fin(2) inductively defined to have exactly two instances – and I am relating these two types (via the relation of mere equivalence). How do I pass from this to any sort of ontological commitment. When is a type said to be a type of real existing entities, so that one may say that I am committing to the apples but not the abstract inductive type. Or am I to commit to both or neither?
I’m not sure what having an ontological commitment is supposed to mean: perhaps I have a model (reality) of reality and a fixed relationship between (apples on the table) and (reality) but not a fixed relationship between Fin(2) and (reality). I commit to those things that have a relationship with reality. But knowing that (there are two apples on the table) only merely gives me a relationship between Fin(2) and (reality), so I should only merely make such a commitment – in other words, I have made some commitment but not a particular commitment.