Questions regarding well formed expressions in the Theory of types

169 Views Asked by At

I'm dealing with a question in type theory: Is it possible to assign types to $\alpha$, $\beta$, and $\gamma$ in such a way that both $(\alpha (\beta))(\gamma)$ and $\alpha (\beta (\gamma))$ are well-formed expressions?

Now, I have a couple of questions:

  1. Since the type syntax I'm looking at is constructed out of types of symbols e and t, where e represents an entity and t represents formulas, such that $<e, t>$ represents a one-place 1st order predicate sentence. Should therefore all sentences have an individual expression; an entity e? Could e.g. a verb function as such an expression and in that case, can the theory account for that?

  2. How should I tackle the parentheses? Should it be read as in mathematics? Is $\beta$ a function of $\alpha$, and thus $\alpha(\beta)$ then in turn a function of $\gamma$ in the first sentence? I am trying to understand in what order should I construct the meaning. Is otherwise the sentence constructions done quite independently of the brackets which functions rather as "semantic indicators", pointing to semantic ambiguities e.g?

  3. Do you reckon it is possible?

N.B. I'm quite new to this so help and guidance would be much appreciated. :)

2

There are 2 best solutions below

1
On BEST ANSWER

If both of the expressions in your question are well-formed, then $\beta(\gamma)$ and $\beta$ would have the same type, because they both occur as the argument of $\alpha$. In the type theories I'm acquainted with, such a thing (a function having the same type as its output) is not possible. (Indeed, it would seem to defeat the purpose of having types in the first place.)

0
On

Type $e$ is the type of individual constants or variables : i.e. "names" [I suppose $e$ for $e$ntity].

Type $t$ is the type of sentences, i.e. "boolean" [I suppose $t$ for $t$rue-false].

In general [see Gamut's book, page 79] :

an expression of type $<a,b>$ is an expression which when applied to an expression of type $a$ results in an expression of type $b$. In other words, if $\alpha$ is an expression of type $<a,b>$ and $\beta$ is an expression of type $a$, the $\alpha(\beta)$ is an expression of type $b$. The process of applying an $\alpha$ of type $<a,b>$ to a $\beta$ of type $a$ is called (functional) application of $\alpha$ to $\beta$.

Thus, type $<e,t>$ is the type of (unary) predicate letters : i.e. "properties". You have to think at on "object" of this type as a function that maps a name into a sentence.

Consider the sentence (type $t$) : "Socrates is a philosopher"; we can write it as :

$philosopher(Socrates)$.

$Socrates$ is of type $e$ and $philospher(x)$ is of type $<e,t>$.

With verbs, we can consider the example : "loves". The (binary) predicate $Loves(x,y)$ (translating : "$x$ loves $y$") is of type $<e, <e,t>>$.

We can think at obtaining the sentence "$Loves(John,Mary)$" with the (functional) application of the predicate $Loves(x,y)$ to the object $John$ of type $e$ getting a new object of type $<e,t>$ : $Loves(John,y)$.

Now we apply it to the objcet of type $e$ $Mary$ to get the final sentence of type $t$.

Thus, $Loves(x,y)$ maps objects of type $e$ into objcets of type $<e,t>$, and so is an object of type $<e, <e,t>>$.