- 19 Downloads
For simple type theory with λ-conversion, extensionality and classical, intuitionistic or minimal predicate logic together with M-, Br-, S4- or S5-modalities as examples it is shown that it is possible to obtain Skolemnormalforms only by applying transpositions, i.e. replacements of equivalent subformulae. In this way one gets in classical type theory without modalities a provable equivalent normalform with prefix and with S5-modalities a deductive equivalent prenex normalform of the form. The axiom of choice allows further simplifications: for example in classical simple type theory a provable equivalent normalform with prefix.
Unable to display preview. Download preview PDF.
© Springer-Verlag 1969