What is the difference between intensional and extensional logic?

Question

Homotopy type theory talks is conjectured to be the internal language of (infinity,1)-toposes; it comes in two flavours: extensional and intensional - these aren't notions that I've come across before in logic.

How are these terms defined and what do they mean?

A set can be defined in two ways: either by a predicate or by a simple listing. The first I take it is intensional, and the second extensional; This tallies with the axiom of extensionality in ZF. Is this it or are there further subtleties? It seems to me that definition by predicate can either be syntactical or semantic, whereas the second can only be syntactical - is this right?

Are they also meaningful terms in propositional logic? That is outside of Set theory proper. And how does one conceptualise them in type theory? Say in the lambda calculus?

Answer 1

The difference between an intension and an extension in contemporary logic comes from Frege, who distinguishes a concept's Sinn (sense) from its Bedeutung (reference).

The easiest way to illustrate the difference between sense and reference is through cases. The predicates "having a kidney" and "having a heart" clearly have different senses, but as a matter of contingent fact everything that has a kidney has a heart: hence we case the two terms are co-referential. The set of the renates = the set of the cordates, because set membership is extensional. First order logics, including set theory are all extensional in this sense. It doesn't matter whether we are talking about the set of the renates or the set of the cordates, because they are the same set, and we know they're the same set, because we define a set extensionally--i.e. purely by the reference of the terms. We don't need to know what the terms "renate" and "cordate" really mean, we just need to know which things they refer to.

An intensional logic, however we do need to know what the terms mean, because we want to ask not just about which things do, as a matter of contingent fact, happen to fall under those terms. For instance, modal logic is an intensional logic. Take the set of all things that have hearts. The sentence, "every renate is a cordate" can be checked by examining every item in the domain and checking that all the things that actually have kidneys also actually have hearts. But, "Necessarily, every renate is a cordate" can't be checked this way. Even if it is the case that all renates are actually cordates, this is just a contingent fact. So to establish the truth or falsity of the modal sentence requires me to have some kind of model that isn't just looking at the referents of the terms "renate" and "cordate", it's going to have to have something to do with knowing the meaning of the terms, etc.

It is because modal logic isn't extensional that lots of people in the first half of the 20th century were suspicious of it. (Think of Quine here.) That's the neat thing about Kripke style model theory for modal logic. It provides something that looks a lot like extensional semantic theory for an intensional logic. It doesn't make modal logic extensional, but it does open up the possibility of using nice model theoretical techniques that were designed for extensional logics on modal logic as well. Since getting access to those techniques, we can prove consistency, and some other metalogical results for some modal logics, which have led to renewed interest in these logics among philosophers.

There are other intensional logics as well. Modal logic is just one prominent example.

Answer 2

In Martin-Löf type theory, for any two terms x,y:A one can form the identity type x=y. A term of this type can be seen as a "reason" for x and y to be equal. In (propositionally) extensional type theory one demands these types to be propositions, that is, they are required to admit at most one term. Intensional type theory does not have this restriction. This makes it a suitable base for homotopy type theory, where terms are interpreted as points of a type/space and the identity type is interpreted as the space of paths between two points. In general, there is more than one path (up to homotopy) between two points, it would thus be unnatural to demand the identity type to be a proposition.

Note that, there is also the concept of function extensionality, which states that two functions are equal, if their values at every argument are equal. Both extensional and intensional type theories can satisfy function extensionality but do not have to.

Answer 3

At least for the German language, the notions Extension und Intension come from the context of Aristotelian logic and where established by the Port-Royal Logic:

Das Begriffspaar stammt aus dem Umfeld der aristotelischen Logik und wurde als 'étendue de l’idee' und 'comprehension de l’idée' durch die Logik von Port-Royal etabliert.

This small clip from the wikipedia indicates that extension and intension might be false friends for German speakers, because the French original talked of étendue and comprehension instead. But I see from the SEP entry on Intensional Logic that due to Carnap, this terminology is no longer completely wrong:

The Port-Royal Logic used terminology that translates as “comprehension” and “denotation” for this. John Stuart Mill used “connotation” and “denotation.” Frege famously used “Sinn” and “Bedeutung,” often left untranslated, but when translated, these usually become “sense” and “reference.” Carnap settled on “intension” and “extension.” However expressed, and with variation from author to author, the essential dichotomy is that between what a term means, and what it denotes.

So extension can be translated as 'étendue de l’idee', 'denotation', "denotation", 'Bedeutung', 'reference', or 'to denote'. And intension can be translated as 'comprehension de l’idée', 'comprehension', "connotation", 'Sinn', 'sense', or 'to mean'. The problem for me as German speaker comes probably from the word 'comprehension', because it doesn't seem to imply anything related to 'intention' to me, but what I want to express is an intended meaning. Probably "connotation" would have been the closest English word for this.

Answer 4

The distinction being asked about can be stripped down to the following question of type theory.

Suppose that f and g are functions X→Y with the property that, for all x∈X, f(x)=g(x).

Do we have the property that f=g?

"Function extensionality" is the property that the answer is always "yes". Extensional type theory takes this as an axiom.

Note that the extensionality in set theory is directly analogous: the axiom of extensionality of ZFC states:

Suppose S and T are two sets with the property that for all x, x∈S if and only if x∈T. Then S=T.