Abstract

In formal semantics based on modern type theories, some sentences may be interpreted as judgements and some as logical propositions. When interpreting composite sentences, one may want to turn a judgemental interpretation or an ill-typed semantic interpretation into a proposition in order to obtain an intended semantics. For instance, an incorrect judgement $$a:A$$ may be turned into its propositional form $$\textsc {is}(A,a)$$ and an ill-typed application p(a) into $$\textsc {do}(p,a)$$, so that the propositional forms can take part in logical compositions that interpret composite sentences, especially those that involve negations and conditionals.In this paper, we propose an operator not that facilitates such a transformation. Introducing not axiomatically, with five axiomatic laws to govern its behaviour, we shall use it to define $$\textsc {is}$$ and $$\textsc {do}$$ and give examples to illustrate its use in semantic interpretation. The introduction of not into type theories is logically consistent – this is justified by showing that not can be defined by means of the heterogeneous equality $$\textrm{JMeq}$$ so that all of the axiomatic laws for not become provable. Therefore, since the extension with $$\textrm{JMeq}$$ preserves logical consistency, so does the extension with not. We shall also study conditions under which $$\textsc {is}$$ and $$\textsc {do}$$ operators can be used safely without the risk of over-generation.