Review of Type-Logical Semantics(5)

each of type,used to capture universal quanti?cation.The idea is that quanti?es over objects of type.In?rst-order logic,is true if for every possible individual,replacing by in yields a true formula.Note that binds the variable in?rst-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 de?nes the syntax of higher-order logic.The models of higher-order logic are generalizations of the relational

structures used to model?rst-order logic.A(standard)frame for higher-order logic is speci?ed 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 de?ne an assignment to be a function such that if.We denote the assignment that maps to and

to.We de?ne the denotation of the term with respect to the model and assignment as:

if,

if,

,and

such that.

搜索“diyifanwen.net”或“第一范文网”即可找到本站免费阅读全部范文。收藏本站方便下次阅读，第一范文网，提供最新外语学习Review of Type-Logical Semantics(5)全文阅读和word下载服务。