Propositional Forms of Judgemental Interpretations

In formal semantics based on modern type theories, some sentences may be inter-preted 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 is(A, a) and an ill-typed application p(a) into 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 is and 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 JMeq so that all of the axiomatic laws for NOT become provable. Therefore, since the extension with JMeq preserves logical consistency, so does the extension with NOT. We shall also study conditions under which is and DO operators can be used safely without the risk of over-generation.