Type theoretic existential introduction and proof with subtypes

Question

I'm working through a book[1], on type theory and categorial grammar (for linguistic applications). Sadly, I ran into problems pretty early on. I'd be very grateful if someone could

1. Explain the type theoretic $\exists$-introduction to me, which goes as follows: $\frac{\beta \ \sqsubseteq \ \alpha}{A \ \sqsubseteq \ (\exists x \ \sqsubseteq \ \alpha \ A(\frac{X}{\beta}))}$,

where $A$ is any type expression with an occurence of $\beta$ and $\sqsubseteq$ the subtyping relation.

$ \ \ $2.How to prove:

$\exists x \ \sqsubseteq \ \mathrm{e} (x \rightarrow \mathrm{t})$

using '$\mathrm{p} \rightarrow \mathrm t$' and the $\exists$-introduction, where $e, p$, and $t$ are types and $p \rightarrow t$ is a functional type. Furthermore $p \sqsubseteq e$ and $e \rightarrow t$.

Ad1: I think I have a problem with the notation. While I'm not very familiar with type theory, I do what $\exists$-intros are supposed to express. The use of $A$ and its relation to $\alpha$ and $\beta$ escape me at the moment. Maybe just rephrasing what the rule states in verbose may be enough.

Ad2: Hinges on question (1), but having both would probably be very useful to understand either one.

---

[1] Asher, N.. 2011. Lexical Meaning in Context: A Web of Words.

Answer 1

I'm not an expert, but the part :

$(\exists x \ \sqsubseteq \ \alpha \ A(\frac{X}{\beta}))$,

looks like the standard first-order logic expression :

$\exists x A[x / \beta]$

which can be "translated" as :

• take a formula $A$ ( a well-formed expression, according to the "grammar" of the language) which contains an expression $\beta$

• replace $\beta$ with the variable $x$

• quantify it with $\exists$.

We can try to explain it with an example :

• let $A :=$ "Plato is a philosopher" and let $\beta :=$ "Plato"

• replace $\beta$ with $x$, to get : "$x$ is a philosopher"

• quantify it, to get : "$\exists x (x$ is a philosopher)".

What we have done is to start with :

"Plato is a philosopher"

and turn it into :

"There is something which is a philosopher".

The rule states the type of the resulting expression, according to the "type restrictions" :

$x \ \sqsubseteq \ \alpha$ and $\beta \ \sqsubseteq \ \alpha$.

We can understand them following our example : in standard first-order logic, we interpret a formula defining a universe for the interpretation. This universe is the "place" where the variables and the terms (i.e. "names") take their denotation.

In a "typed" logic, the universe is organized into not-overlapping "categories" and we have type-restrictions to be matched.

Thus, in our example, we have that Plato must belong to some type, e.g. philosopher which is a sub-type of, e.g. : man. I.e. :

philosopher $\sqsubseteq$ man.

Thus, the type-restrictions included in the rule force us to replace the term of type $\beta \sqsubseteq \alpha$ contained into expression $A$ with a variable $x$ (which is also a term) of type $\sqsubseteq \alpha$ and the resulting expression : $\exists x A[x]$ will satisfy the ordering relation between types : $A \sqsubseteq \exists x A[x]$.

Again, using the example, the variable $x$ must be of a sub-type of the type man.

---

In first-order logic, we have the so called $\exists$-introduction rule :

$$\frac {\varphi(t)} {\exists x \varphi[x / t] }$$

which works in this way :

• from a formula $\varphi$ containing a term (a "name") $t$, we can infer : $\exists x \varphi(x)$, where we have replaced the term $t$ with the variable $x$.

This is exactly the inference rule which licences us to infer :

"There is something which is a philosopher"

from :

"Plato is a philosopher".

---

Added

If the above explanation is correct, we can rewrite your rule (omitting type-restrictions) as :

$$\frac {A(\beta)} {\exists x A[x / \beta] }$$

If so, we can apply it with :

• $A := p \rightarrow t$

and

• $\beta := p$

to get :

$$\frac {p \rightarrow t} {\exists x (x \rightarrow t) }$$

For type restrictions, we must use $e$ as $\alpha$; in this way we must have :

• $p, x \sqsubseteq \ e$.