Citations of:
Higherorder semantics and extensionality
Journal of Symbolic Logic 69 (4):10271088 (2004)
Add citations
You must login to add citations.


The paper shows how ideas that explain the sense of an expression as a method or algorithm for finding its reference, preshadowed in Frege’s dictum that sense is the way in which a referent is given, can be formalized on the basis of the ideas in Thomason (1980). To this end, the function that sends propositions to truth values or sets of possible worlds in Thomason (1980) must be replaced by a relation and the meaning postulates governing the behaviour of (...) 

A logic is called higher order if it allows for quantiﬁcation over higher order objects, such as functions of individuals, relations between individuals, functions of functions, relations between functions, etc. Higher order logic began with Frege, was formalized in Russell [46] and Whitehead and Russell [52] early in the previous century, and received its canonical formulation in Church [14].1 While classical type theory has since long been overshadowed by set theory as a foundation of mathematics, recent decades have shown remarkable (...) 

Standard approaches to proper names, based on Kripke's views, hold that the semantic values of expressions are (settheoretic) functions from possible worlds to extensions and that names are rigid designators, i.e.\ that their values are \emph{constant} functions from worlds to entities. The difficulties with these approaches are wellknown and in this paper we develop an alternative. Based on earlier work on a higher order logic that is \emph{truly intensional} in the sense that it does not validate the axiom scheme of (...) 

In this paper we define intensional models for the classical theory of types, thus arriving at an intensional type logic ITL. Intensional models generalize Henkin's general models and have a natural definition. As a class they do not validate the axiom of Extensionality. We give a cutfree sequent calculus for type theory and show completeness of this calculus with respect to the class of intensional models via a model existence theorem. After this we turn our attention to applications. Firstly, it (...) 





We explore the view that Frege's puzzle is a source of straightforward counterexamples to Leibniz's law. Taking this seriously requires us to revise the classical logic of quantifiers and identity; we work out the options, in the context of higherorder logic. The logics we arrive at provide the resources for a straightforward semantics of attitude reports that is consistent with the Millian thesis that the meaning of a name is just the thing it stands for. We provide models to show (...) 

We study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various nonclassical logics. We report some experiments using the higherorder automated theorem prover LEOII. 

Even though OpenMath has been around for more than 10 years, there is still confusion about the “semantics of OpenMath”. As the upcoming MathML3 recommendation will semantically base Content MathML on OpenMath Objects, this question becomes more pressing. One source of confusions about OpenMath semantics is that it is given on two levels: a very weak algebraic semantics for expression trees, which.. 

