A General Theory of Completeness Proofs
Sh ocirc ji MAEHARA · Annals of the Japan Association for Philosophy of Science · 1970
1.4.2.Intuitionistic propositional and predicate logic.The calculus LJ introduced by Gentzen [1] does not satisfy the condition 2) of 1.3.But we can introduce an admitted calculus which is essentially equivalent to LJ, by regarding the provability of sequent as the LJ-provability of the sequent The new calculus is obtained from LK by restricting the use of the following three rules of inference within the case where © is empty (cf.Maehara [4]): 1.4.4.Some of the modal logics.For example, an admitted calculus expressing Lewis' system S 4 is obtained from LK, if we introduce a new logical symbol • and we admit, as rules of in ference, the use of 5.1.The intuitionistic nrediThe calculus LEJ is the system obtained from LJ by adjoining the axiom schemata But, in LEJ, the rules of inference