Eine Interpretation des intuitionistischen Aussagenkalküls. (Q2624162)

Verf. sagt, daß man den \textit{Heyting}schen Aussagenkalkül interpretieren kann mit Hilfe der Begriffe des gewöhnlichen Aussagenkalküls und des Begriffes \(Bp\), d. h. \(p\) ist beweisbar, wenn man das folgende Axiomensystem \(\mathfrak S\) hinzufügt: \[ (1)\;Bp\rightarrow p,\qquad (2)\;Bp\rightarrow \cdot \,B(p\rightarrow q)\rightarrow Bq,\qquad (3)\;Bp\rightarrow BBp, \] und dazu noch die Schlußregel: Aus \(A\) darf man \(BA\) schließen. Dabei sind die \textit{Heyting}schen Grundbegriffe \(\neg p\), \(p\supset q\), \(p\vee q\), \(p\wedge q\) bzw. so zu übersetzen: \(\sim Bp\), \(Bp\rightarrow Bq\), \(Bp\vee Bq\), \(p\cdot q\). Man kann auch \(\neg p\) durch \(B\sim Bp\) und \(p \wedge q\) durch \(Bp \cdot Bq\) übersetzen. Dann folgt die Übersetzung jeder im \textit{Beyting}schen System gültigen Formel aus \(\mathfrak S\); dagegen folgt aus \(\mathfrak S\) nicht die Übersetzung von \(p\vee \neg p\) und überhaupt keine Formel der Gestalt \(BP \vee BQ\), für die nicht schon entweder \(BP\) oder \(BQ\) aus \(\mathfrak S\) beweisbar ist. Verf. vermutet, daß eine Formel im \textit{Heyting}schen Kalkül dann und nur dann gilt, wenn ihre Übersetzung aus \(\mathfrak S\) beweisbar ist. Er bemerkt weiter, daß \(\mathfrak S\) mit dem \textit{Lewis}schen ``System of strict implication'' äquivalent ist, wenn \(Bp\) durch \(Np\) (Notwendigkeit von \(p\)) übersetzt wird, und das \textit{Becker}sche Axiom \(Np < NNp\) hinzugefügt wird.