Eine Umformung des Heytingschen Axiomensystems für den intuitionistischen Aussagenkalkül. Dem Andenken an Heinrich Scholz gewidmet

✍ Scribed by Karl Schröter

• Publisher: John Wiley and Sons
• Year: 1957
• Tongue: English
• Weight: 606 KB
• Volume: 3
• Category: Article
• ISSN: 0044-3050
• DOI: 10.1002/malq.19570030103

✦ Synopsis

Von KARL SCHROTER in Berlin A. HEYTIN&) hat bekanntlich fur den intuitionistischen Aussagenkalkul (AH) das folgende Axiomensystem in der intuitionistischen Implikation (Funktor : +), der intuitionistischen Konjunktion (Funktor : A), der intuitionistischen Alternative (Funktor : v ) und der intuitionistischen Negation (Funktor : Ein Strich uber dem betreffenden Ausdruck) angegebenz ) :

(I) und (XI) 3. p -t q . -+ . p ~r + q r \ r 4. (I, 3 a) A (a -+ r ) 3 (P 3 r ) 5. p + ( ( I + p ) 6. p A @+(I)-+q 7. P --t P V P 8. p v q -t q v p 9. ( p + r ) A (q -+ r ) -+ ( p v (I .+ T )

10. ( P -? a) A ( P -+ n, -+ I, 11. .p+ (P-+4) Aul3er der Einsetzungs-und der Abtrennungsregel 1aBt A. HEYTING bei Ableitungen noch eine sogenannte Konjunktionsregel zu. Diese ist jedoch nach einer Bemerkung von P. BERNAys3) unter Benutzung der Axiome 1, 3, 5 schon mit Hilfe der Einsetzungs-und der Abtrennungsregel beweisbar. Denn es gilt: D i e K o n j u n k t i o n s r e g e l . Sind aus dem HEYTINaschen Axiomensystem mit Hilfe won Einsetzungsund Abtrennungsregel H, and H, ableitbar, so auch HI A H , . 1) A. HEYTINQ, Die formalen Regeln der intuitionistischen Logik, S.-B. preuB. Akad. Wiss.

physik.-math. Klasse, Jg. 1930, 42-56 (1930).

2 ) p , q , r, s sind in dieser Arbeit Aussagenvariablen; + trennt stilrker d s V, V stiirker als A ; ein mit k (k > 0) Punkten versehener Funktor trennt starker als jeder Funktor mit weniger Punkten; fiir Funktoren mit gleichviel Punkten gilt dieselbe Verrcbredung wie fur Funktoren ohne Punkte. ,,H", evtl. mit Indizes, ist stets eine Variable fur Ausdriicke. Genaue Ausfiihrungen siehe in K. SCHROTER, Theorie des logischen SchlieBens; diese Zeitschr. 1, 37-86 (1955), S. 45. 8 ) Brief von P. BERNAYS an H. SCHOLZ Ende 1937.

4*. p

lo*. p --f q .+. q -> 11*. ?-+ ( p -t q ) I) I. JOHANSSON, Der Minimalkalkiil, ein reduzierter intuitionistisoher Formalismus, Compositio mathematica 4, 119-136 (1936).