One of the many roles of linguistics is to address the semantics of natural languages, that is, the meaning of sentences in natural languages. An important part of the meaning of sentences can be characterized by stating the conditions that need to hold fo

,or equivalently,

There seems to be a discrepancy among the logical contributions of the subjects in the above sentences.There is a

distinction in thefirst-order logic translation of these sentences that is not expressed by their grammatical form.

It turns out that there is a way to solve those problems,by looking at an extension offirst-order logic,known as higher-order logic[3].Let us give enough theory of higher-order logic to see how it can be used to assign semantics

to(a subset of)a natural language.This presentation presupposes a familiarity with bothfirst-order logic and the -calculus[5].1There is a slight difference in our approach tofirst-order logic and our approach to higher-order logic. In the former,formulas,which represents properties of the world and its individuals,are the basic units of the logic.In

higher-order logics,terms are the basic units,including constants and functions,with formulas explicitly represented

as boolean-valued functions.

We start by defining a set of types that will be used to characterize the well-formedness of formulas,as well as

derive the models.We assume a set of basic types,where is the type of boolean values, and is the type of individuals.(Infirst-order logic,the type is not made explicit.)The set of types is the smallest set such that,and if.A type of the form is a functional(or higher-order)type,the elements of which map objects of type to objects of type.

The syntax of higher-order logic is defined as follows.Assume for each type a set of variables and

a set of constants of that type.The set of terms of type is defined as the smallest set such that:

,

,

if and,and

if,,and.

What are we doing here?We are defining a term language.First-order logic introduces special syntax for its logical

connectives(,,,).It turns out,for higher-order logic,that we do not need to do that,we can simply define constants for those operators.(We will call these logical constants,because they will have the same interpretation in all models.)We will assume the following constants,at the following types:a constant of type and a constant of type,the interpretation of which should be clear,a family of constants each of type,which checks for equality of two elements of type,and a family of constants

each of type,used to capture universal quantification.The idea is that quantifies over objects of type.Infirst-order logic,is true if for every possible individual,replacing by in yields a true formula.Note that binds the variable infirst-order logic.In higher-order logic,where there is only as a binder, we write the above as,which is true if is true for all objects of type.

This defines the syntax of higher-order logic.The models of higher-order logic are generalizations of the relational

structures used to modelfirst-order logic.A(standard)frame for higher-order logic is specified by giving for each basic type a domain of values of that type.These extend to functional types inductively:for a type ,,that is,the set of all functions from elements of

to elements of.Let.We also need to given an interpretation for all the constants,via a function assigning to every constant of type an object of type.(We simply write when the type is clear from the context.)Hence,a model for higher-order logic is of the form.We extend the interpretation to all the terms of the language.To deal with variables,we define an assignment to be a function such that if.We denote the assignment that maps to and

to.We define the denotation of the term with respect to the model and assignment as:

if,

if,

,and

such that.