Is this right?

The semantics of a simple type-theoretic language

 

The language for predicate logic contains this: connectives (∨, ∧, → etc.), quantifiers (∀ and ∃), individual constants (a, b, c, d etc.) and variables (x, y, z etc.), and predicate constants (W, B, H etc.). These have their prowess as well as their limits. In predicate logic, you can only say something about entities (the properties they have) and the relation of entities to other entities. Logicians and linguists alike felt the need to add more structure to this language when faced with sentences like:

(a) If Winnie the Pooh is a mammal, then there is at least one thing he has in common with Lady Gaga
(b) Mary is yelling furiously
(c) Jumbo is a terribly small elephant

And, mind you, these are not terribly complicated sentences. For instance, (a) feels like quantifying over properties, saying that there is a property such that both Winnie and Lady Gaga share, so we need to introduce a variable for predicates that renders it into (a’) below. That would already upgrade our first-order predicate logic into second-order predicate logic. But consider (b). It feels like attributing the property of being furious to the property of yelling – the latter in turn being attributed to Mary. For that, we would need a representation on the lines of (b’) below, where the scripts are expressions of a third-order. Needless to add, (c’) is even more elaborate, with terribly modifying small elephant, and small being applied to elephant, and elephant to Jumbo.

(a’) Mp → ∃X(Xl ∧ Xp)
(b’) (Y)(m)

The theory of types is a very handy tool which linguists (some, not all) use to operate on these natural language sentences. It is good to note that type theory did not arise out of this need, but the purely logical one of overcoming the paradoxes discovered in set-theory (Russell’s paradox, more precisely). We will come back to this later. Let us proceed by defining the set of all types. As we’ve mentioned before, types are labels for categories of expressions. What’s really nice is that we can go along with just two basic types (e – for entities, and t – for formulas^[1]) and build up from there. So let’s start:

Definition 1:
T, the set of types, is the smallest set such that:
(i) e, t ∈ T
(ii) if a, b ∈ T, then <a, b> ∈ T

The notation <a, b> is what stands for the so-called derived types and should be read as follows. An expression of the type <a, b> combines with an expression of the type “a” and results in an expression of the type “b”. Let α be an expression of the type <a, b> and β an expression of the type “a”. This means that if we combine α with β, we get α(β), which we know will be of the type “b”. This process of applying expressions to other expressions is called “functional application of α of type <a, b> to β of type a”. I guess you know where we’re going with this. Predicates will be of the type <e, t>, because they combine with individuals (which are of the type e) and result in truth values (t). We will say then that the predicate walks is of the type <e, t> because it combines with John and gives the formula W(j) – which we know, and which is true or false.

Not all types can be identified in natural language (and this is quite normal). But some are. Expressions of the type <<e, t>, t>, for instance, combine with predicates (<e, t>) and give truth values (t) – which is just what we want for second-order predicates in sentences like “Walking is healthy”. Expressions of the type <<e, t>, <e, t>> combine with one place predicates and give one-place predicates. In natural language, adverbs and relative adjectives correspond to expressions of this type. Now what would two-place predicates look like? Let’s look at the sentence:

(1) Paepaenoy loves Zmika

What loves does in (1) is it combines with Zmika (an expression of the type e) and gives loves Zmika, which applied to Paepaenoy results in a formula. Thus, two-place predicates will be of the type <e, <e, t>>.

We can now give the syntax of our type-theoretic language in a very precise form:

(i) If α is a variable or a constant of type a in L, then α is an expression of type a in L
(ii) If α is an expression of a type <a, b> in L, and β is an expression of the type a, then α(β) is an expression of the type β in L
(iii) If ψ and ϕ are expressions of type t in L (i.e. formulas), then so are (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), (ϕ ↔ ψ).
(iv) If ϕ is an expression of type t in L, and v is a variable (of any type), then ∀xϕ and ∃xϕ are expressions of type t in L.
(v) If α and β are expressions that belong to the same arbitrary type, then (α = β) is an expression of type t in L.
(vi) Every expression in L is to be constructed by means of (i)-(v) in a finite number of steps

Given this, we can have a notation for “all well-formed expressions of type a”. Because of HTML constraints, I will note that as WE_[a/L], but fortunately one never notes the name of the language, so I will use WE_a – e.g. WE_t for the set of all formulas. Another thing that will change in our talk, due to these upgrades, is that we will not talk about sets any more, not normally, but of the “characteristic function of sets”. These two ways of speaking are interchangeable, but the latter gives a better picture of what’s going on: a one-place predicate like “walks” is not, strictly speaking, the same as “the set of all walkers” – although saying this is not wrong, in the set-view of expressions – but “a function from individual to truth values”, namely, that function which maps walkers to 1 and non-walkers to 0. This is called the functional view and goes hand in hand with the functional application of types. The notation also changes – although some authors prefer not to introduce a different notation for something which is in the end pretty similar. Thus, if

B = {1, 2}, and D = {x | x is a natural number}, then the characteristic function of B can be written as f_B(1) = f_B(2) = 1 and f_B(3) = f_B(4) = f_B(5) = … f_B(n) = 0. The domain of f_B is D, and the range is {1, 0} – which goes hand in hand with the fact that something like B will be of the type <e, t>.

With this we arrive at the basis of the semantics for our language, for one-place predicates will be interpreted as the characteristic functions of subsets of the domain. As we move up the ladder of types of expressions, an expression of the type <a, b> is treated as a function from “type a things” to “type b things”. It is useful now to remember the general notation X^Y which stands for “all functions that map Y into Z”. Thus, the set of all one-place predicates will be {0, 1}^D and the set of all two-place predicates will be ({0, 1}^D)^D. These are functions that “spill out” other functions.

Since more complex types are constructed by means of two simple types, we will be able to specify the domain of their characteristic functions in the same way. Thus, with the notation D_{a, D} standing for “the domain of interpretation of expressions of type a_, given a domain D”, we will naturally have:

Definition 3:

(i) D_{e, D} = D (i.e. the domain of interpretation of WE_e is D, the set of individuals)
(ii) D_{t, D} = {1, 0} (i.e. the domain of interpretation of WE_t is {1, 0}, the set of truth values)
(ii) D_{<a, b>, D} = (D_b)^{D a} (i.e. the set of functions from D_a to D_b)

So, the domain of interpretation of a one place predicate will be (D_t)^{D e}, which is the same as {1, 0}^D; for two-place predicates, (D_t^{D e})^{D e}, which is ({1, 0}^D)^D. What we just did is specify the domains of the interpretation functions for each type (simple or derivate). We now have a model M for our language L, consisting of a non-empty domain D and an interpretation function I as specified in definition 3. This function I assigns to each constant an element from the domain which corresponds to the type of the constant. Within WE_a, then, we can differentiate between CON_a and VAR_a – that is, between constants of type a and variables of type a.

 

 

 

 

 

 

 

 

 

The best thing to do now is some exercises. I’ll come back with that.

---

[1] Be very careful not to mix up the meta-languages when we discuss types. “e” is a type, but <a, b> is not a type, but a notation for the type that combines with “a” and results in “b”. So <a, b> stands for all types which have an “a” and a “b” as types, namely <e, t>, <<e, t>, t>, <<e, t>, <e, t>>, etc.