Systems of logic for necessity

takeuti is.sci. toho-u.ac.jp Abstract: This paper discusses atheory of modal predicate logic, which is based on S5. This paper gives four ways to define this theory. The first way is to define asystem which tells whether acontext supports aformula or not. In this way we evaluate a formula with not amodel but acontext. This theory distinguish occasional equality from necessary equality, as is discussed with the problem of referentially opaque context. The aim of this paper is to observe the mathematical properties of this theory. The second way is aderivation system of Hirbert-style, which is given by adding new axiom schemata to the rules of S5. The third is aderivation system of Gentzen-style, where asequent is not asequence of formulae but atable of formulae, his system satisfies cut elimination. The fourth is akind of possible-world semantics. In the fourth way, aformula is valid when the formula is true in each partial abstraction models. This paper shows the equivalence of these four ways, that is, these four ways define the same theory