How to find a term that proves a given proposition?

Question

I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of semantics of an intransitive verb, which is $talk: Human \to Prop$, where $Prop$ is "the internal totality of all logical propositions" (I'm not sure what "internal totality" means, but maybe that's not exactly relevant here), with inference rules as shown below.

Now, if $j: Human$ ($j$ for "John"), then I believe in certain context we can prove that $talk(j): Prop$. But how do I find a term that would prove the proposition $talk(j)$? I'm not sure I understand even what such a term should look like.

Answer 1

OK, so this is painful. I haven't read your book, but it looks like the authors are trying to appropriate Montague Grammar for their examples but they don't quite know what they're doing. So briefly, Montague Grammar is an approach to the semantics of natural languages analogous to Denotational semantics for programming languages. The idea of Montague Grammar is to create a parse tree for a sentence, and then combine the semantics of each word as you go up the tree in a clever sequence of function applications which ultimately combine to form a proposition. So to get to your question, the semantics of $talk(j)$ is just given to you as an axiom from the lexical semantics of "talk". In Montague grammar, you are assured that every word in a sentence has appropriate semantics. It's given in the lexicon, which is assumed to exist before the semantics of any sentence can be evaluated. The axioms you've provided look like barely enough to perform the various function combinations to yield a proposition from the lexical semantics, but don't provide any lexical semantics whatsoever.