%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % Die Sprache der Mengenlehre als % (PROLOG-)berechenbares System % % Ein PROLOG-Programm zur Identifikation % von Formeln der Mengenlehre und zur % Durchführung syntaktischer % Operationen % % Eine Sitzung mit dem Programm % termlanguage.pro % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1. Fragen und Antworten. Dem Programm können Fragen folgender Art gestellt werden: ?- variable(1). Es antwortet mit: Saving. Compiling the file: D:\Prolog\Programme\termlanguage.pro 0 errors, 0 warnings. Yes. Wir verwenden die naürlichen Zahlen 0,1,2,... als Variablensymbole. Auf die Frage ?- variable(-22). antwortet es: Saving. Compiling the file: D:\Prolog\Programme\termlanguage.pro 0 errors, 0 warnings. No. 2. Epsilon-Formeln ?- formel([ex,0,[all,1,[not,[1,in,0]]]]). Yes. Das Mengenexistenzaxiom ist eine Formel. ?- formel([ex,0,1,2,3]). No. Diese Liste ist keine Formel. 3. Das Axiomensystem EML ?- eml(X),write(X),nl. [ex,0,[all,1,[not,[1,in,0]]]] Yes. Das Programm liefert eine erste Lösung X und stoppt dann mit Erfolg: "Yes". Um das gesamte System EML zu erhalten, muß jede Einzellösung als Mißerfolg "fail" behandelt werden, das Programm sucht dann weiter: ?- eml(X),write(X),nl,nl,fail. [ex,0,[all,1,[not,[1,in,0]]]] [all,0,[all,1,[[all,2,[[2,in,0],iff,[2,in,1]]],then,[0,eq,1]]]] [all,0,[all,1,[ex,2,[all,3,[[3,in,2],iff,[[3,eq,0],or,[3,eq,1]]]]]]] [all,0,[ex,1,[all,2,[[2,in,1],iff,[ex,3,[[3,in,0],and,[2,in,3]]]]]]] No. 4. Klassenterme ?- term(3). Yes. ?- term([0,0]). No. ?- term([0,[not,[0,eq,0]]]). Yes. Dies ist die Klasse aller v_0, die die Formel v_0 ungleich v_0 erfüllen. 5. Formeln mit Klassentermen ?- tformel([[0,[not,[0,eq,0]]],in,[0,[0,eq,0]]]). Yes. Dies ist die Formel: Die leere Klasse ist ein Element des Universums. 6. Substitution ?- sub(Y,[0,eq,1],0,1), write([0,eq,1]),nl, write(Y),nl. [0,eq,1] [1,eq,1] Yes. ?- sub(Y,[all,0,[0,eq,1]],0,1), write([all,0,[0,eq,1]]),nl, write(Y),nl. [all,0,[0,eq,1]] [all,0,[0,eq,1]] Yes. Eine gebundene Variable wird nicht substituiert. ?- sub(Y,[all,0,[0,eq,4]],4,0), write([all,0,[0,eq,4]]),nl, write(Y),nl. [all,0,[0,eq,4]] [all,10,[10,eq,0]] Yes. Vor dem Substituieren von v_4 durch v_0 muß zunächst die gebundene Variable umbenannt werden. 7. Elimination von Klassentermen ?- kelim([[0,[not,[0,eq,0]]],in,[0,[0,eq,0]]],X), write([[0,[not,[0,eq,0]]],in,[0,[0,eq,0]]]),nl, write(X),nl. [[0,[not,[0,eq,0]]],in,[0,[0,eq,0]]] [ex,9,[[9,eq,9],and,[all,11,[[11,in,9],iff,[not,[11,eq,11]]]]]] Yes. Die leere Klasse ist Element des Universums, man beachte die Einführung der neuen Variablen. ?- kelim([all,0,[[1,[ex,4,[[4,in,0],and, [1,in,4]]]],in,[0,[0,eq,0]]]],X), write([all,0,[[1,[ex,4,[[4,in,0],and, [1,in,4]]]],in,[0,[0,eq,0]]]]),nl, write(X),nl. [all,0,[[1,[ex,4,[[4,in,0],and,[1,in,4]]]], in,[0,[0,eq,0]]]] [all,0,[ex,17,[[17,eq,17],and,[all,19,[[19,in,17], iff,[ex,4,[[4,in,0],and,[19,in,4]]]]]]]] Yes. Dies ist das Vereinigungsaxiom. 8. Abkürzungen für Klassenterme und Formeln ?- def([aus,universe],X), write(X),nl. [all,0,[[0,cap,universe],in,universe]] Yes. Eine (triviale) Instanz des Aussonderungsschemas. Elimination der Abkürzungen: ?- def([aus,universe],X), elim(X,Y), write(Y),nl. [all,0,[[9,[[9,in,0],and,[9,in,[0,[0,eq,0]]]]], in,[0,[0,eq,0]]]] Yes. Dieses ist eine Formel mit Klassentermen: ?- tformel([all,0,[[9,[[9,in,0],and,[9,in,[0,[0,eq,0]]]]], in,[0,[0,eq,0]]]]). Yes. Und schließlich die Elimination der Klassenterme: ?- def([aus,universe],X), elim(X,Y), kelim(Y,Z),write(Z),nl. [all,0,[ex,17,[[17,eq,17],and,[all,19,[[19,in,17],iff, [[19,in,0],and,[19,eq,19]]]]]]] Yes. Dieses ist eine Epsilonformel: ?- def([aus,universe],X), elim(X,Y), kelim(Y,Z),formel(Z),nl. Yes. 9. Das System ZFC