<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>This paper is a continuation of Inoué [5]. As already mentioned in the paper, a number of intuitionistic provable formulas are given with a Hilbert-style proof. For that, we make use of a family of intuitionistic deduction theorems, which are also presented in this paper by means of Mizar system [2], [1]. Our axiom system of intuitionistic propositional logic IPC is based on the propositional subsystem of H<sub>1</sub>-<bold>IQC</bold> in Troelstra and van Dalen [6, p. 68]. We also owe Heyting [4] and van Dalen [7]. Our treatment of a set-theoretic intuitionistic deduction theorem is due to Agata Darmochwał’s Mizar article “Calculus of Quantifiers. Deduction Theorem” [3].</p>
</abstract>

This paper is a continuation of Inoué [5]. As already mentioned in the paper, a number of intuitionistic provable formulas are given with a Hilbert-style proof. For that, we make use of a family of intuitionistic deduction theorems, which are also presented in this paper by means of Mizar system [2], [1]. Our axiom system of intuitionistic propositional logic IPC is based on the propositional subsystem of H1-IQC in Troelstra and van Dalen [6, p. 68]. We also owe Heyting [4] and van Dalen [7]. Our treatment of a set-theoretic intuitionistic deduction theorem is due to Agata Darmochwał’s Mizar article “Calculus of Quantifiers. Deduction Theorem” [3].

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

Department of Medical Molecular Informatics

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

This paper is a continuation of Inoué [5]. As already mentioned in the paper, a number of intuitionistic provable formulas are given with a Hilbert-style...

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

Publicado en línea: 21 dic 2022

Páginas: 1 - 12

Aceptado: 30 abr 2022

DOI: https://doi.org/10.2478/forma-2022-0001

Palabras clave
intuitionistic logic, deduction theorem, consequence operator

© 2022 Takao Inoué et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

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

Publicado en línea: 21 dic 2022

Páginas: 1 - 12

Aceptado: 30 abr 2022

DOI: https://doi.org/10.2478/forma-2022-0001

Palabras claveintuitionistic logic, deduction theorem, consequence operator

© 2022 Takao Inoué et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Palabras clave
intuitionistic logic, deduction theorem, consequence operator