Intuitionistic Propositional Calculus in the Extended Framework with Modal Operator. Part I

Takao Inoue

The Iida Technical High School, Nagano

Summary.

In this paper, we develop intuitionistic propositional calculus IPC in the extended language with single modal operator. The formulation that we adopt in this paper is very useful not only to formalize the calculus but also to do a number of logics with essentially propositional character. In addition, it is much simpler than the past formalization for modal logic. In the first section, we give the mentioned formulation which the author heavily owes to the formalism of Adam Grabowski's [4]. After the theoretical development of the logic, we prove a number of valid formulas of IPC in the sections 2-4. The last two sections are devoted to present classical propositional calculus and modal calculus S4 in our framework, as a preparation for future study. In the forthcoming Part II of this paper, we shall prove, among others, a number of intuitionistically valid formulas with negation.

MML Identifier: INTPRO_1

Contents (PDF format)

1. Intuitionistic Propositional Calculus IPC in the Extended Language with Modal Operator
2. Formulas Provable in IPC: Implication
3. Formulas Provable in IPC: Conjunction
4. Formulas Provable in IPC: Disjunction
5. Classical Propositional Calculus CPC
6. Modal Calculus S4

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[4] Adam Grabowski. Hilbert positive propositional calculus. Journal of Formalized Mathematics, 11, 1999.

[5] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[6] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[7] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[8] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.