www.wikidata.de-de.nina.az
Die Pradikatenlogik erster Stufe ist ein Teilgebiet der mathematischen Logik Sie befasst sich mit der Struktur gewisser mathematischer Ausdrucke und dem logischen Schliessen mit dem man von derartigen Ausdrucken zu anderen gelangt Dabei gelingt es sowohl die Sprache als auch das Schliessen rein syntaktisch das heisst ohne Bezug zu mathematischen Bedeutungen zu definieren Das dadurch ermoglichte Zusammenspiel von rein syntaktischen Uberlegungen einerseits und semantischen Betrachtungen andererseits fuhrt zu wichtigen Erkenntnissen die Bedeutung fur die gesamte Mathematik haben denn diese lasst sich mittels der Zermelo Fraenkel Mengenlehre in der Pradikatenlogik erster Stufe formulieren Im Unterschied zur Aussagenlogik macht die Pradikatenlogik von Quantoren Gebrauch Inhaltsverzeichnis 1 Ein motivierendes Beispiel 2 Die Sprache der Pradikatenlogik erster Stufe 2 1 Symbole 2 2 Terme 2 3 Ausdrucke 2 4 1 Stufe 2 5 Freie Variablen 2 6 Metasprachliche Ausdrucke 2 7 Substitutionen 2 8 Schlussbemerkung zur Syntax 3 Semantik 3 1 Strukturen 3 2 Interpretationen 3 3 Modelle 3 4 Gleichheit 4 Mathematisches Schliessen 4 1 Folgerungen 4 2 Sequenzenkalkul 4 3 Vollstandigkeit und Korrektheit 5 Eigenschaften 5 1 Erfullbarkeitssatz 5 2 Kompaktheitssatz 5 3 Isomorphien 5 4 Satz von Lowenheim Skolem 5 5 Satz von Lindstrom 6 Siehe auch 7 Literatur 8 Einzelnachweise und AnmerkungenEin motivierendes Beispiel BearbeitenDie unten aufzustellenden Definitionen sollen am Beispiel der Theorie der geordneten abelschen Gruppen motiviert werden Eine geordnete abelsche Gruppe besteht zunachst aus einer abelschen Gruppe G displaystyle G nbsp das heisst man hat folgende Eigenschaften Assoziativgesetz Fur alle x y z G displaystyle x y z in G nbsp gilt x y z x y z displaystyle x y z x y z nbsp Kommutativgesetz Fur alle x y G displaystyle x y in G nbsp gilt x y y x displaystyle x y y x nbsp Neutrales Element 0 Fur alle x G displaystyle x in G nbsp gilt x 0 x displaystyle x 0 x nbsp Inverses Element Fur alle x G displaystyle x in G nbsp gibt es ein x G displaystyle x in G nbsp sodass gilt x x 0 displaystyle x x 0 nbsp In mathematischer Kurzschreibweise kann man das auch als x y z x y z x y z x y x y y x x x 0 x x x x 0 displaystyle forall xyz colon x y z x y z quad forall xy colon x y y x quad forall x colon x 0 x quad forall x colon x x 0 nbsp wiedergeben Dabei schreiben wir x displaystyle forall x nbsp an Stelle des oft verwendeten x G displaystyle forall x in G nbsp da wir hier ohnehin uber nichts anderes als die Elemente der Gruppe etwas aussagen wollen Ferner haben wir eine displaystyle leq nbsp Relation fur die Ordnung auf der Gruppe die den folgenden Axiomen genugen muss die hier gleich in Kurzschreibweise angegeben werden Reflexivitat x x x displaystyle forall x colon x leq x nbsp Transitivitat x y z x y y z x z displaystyle forall xyz colon x leq y land y leq z rightarrow x leq z nbsp Gruppenvertraglichkeit x y z x y x z y z displaystyle forall xyz colon x leq y rightarrow x z leq y z nbsp Beispiele fur geordnete abelsche Gruppen sind etwa R displaystyle mathbb R leq nbsp oder Z displaystyle mathbb Z leq nbsp Insgesamt haben wir einige der sogenannten logischen Symbole displaystyle forall exists land lor rightarrow leftrightarrow neg nbsp verwendet Klammern als Hilfssymbole ferner das Gleichheitszeichen und Variablen fur die Elemente Die fur die Theorie der geordneten abelschen Gruppen charakteristischen Symbole sind die Konstante 0 die Funktionen und sowie die Relation displaystyle leq nbsp wobei die in der Mathematik ublichen Schreibweisen benutzt wurden das heisst x y displaystyle x y nbsp statt x y displaystyle x y nbsp bzw x y displaystyle x leq y nbsp statt x y displaystyle x y in leq nbsp Die beiden Funktionen haben unterschiedliche Stelligkeit ist zweistellig die Inversenbildung ist einstellig die betrachtete Ordnungsrelation ist zweistellig Damit sind die Symbole einer ganz bestimmten Sprache beschrieben in der man die Theorie der geordneten abelschen Gruppen formulieren kann Manche der aus den Symbolen gebildeten Zeichenketten sind vernunftig d h nach gewissen Gesetzmassigkeiten gebildet und manche von diesen drucken daruber hinaus wahre Aussagen aus Dies wird im Folgenden verallgemeinert insbesondere werden der Unterschied zwischen den nach Regeln gebildeten vernunftigen Zeichenketten und einem moglichen Wahrheitsgehalt solcher Zeichenketten herausgearbeitet sowie sich daraus ergebende Konsequenzen Diese haben fur die gesamte Mathematik Bedeutung Die Sprache der Pradikatenlogik erster Stufe BearbeitenWir beschreiben hier die verwendete Sprache auf rein syntaktische Weise das heisst wir legen die betrachteten Zeichenketten die wir Ausdrucke der Sprache nennen wollen ohne Bezug auf ihre Bedeutung fest Symbole Bearbeiten Eine Sprache erster Stufe wird aus folgenden Symbolen aufgebaut 1 2 3 S 45 logische Symbole Quantoren displaystyle forall exists nbsp Junktoren displaystyle land lor rightarrow leftrightarrow neg nbsp technische Zeichen displaystyle equiv nbsp Variablensymbole v 0 v 1 v 2 displaystyle v 0 v 1 v 2 ldots nbsp eine moglicherweise leere Menge C displaystyle mathcal C nbsp von Konstantensymbolen eine moglicherweise leere Menge F displaystyle mathcal F nbsp von Funktionssymbolen eine moglicherweise leere Menge R displaystyle mathcal R nbsp von Relationssymbolen Terme Bearbeiten Die nach folgenden Regeln aufgebauten Zeichenketten heissen Terme 4 5 3 S 45 6 S 3 7 S 4 Ist v displaystyle v nbsp ein Variablensymbol so ist v displaystyle v nbsp ein Term Ist c displaystyle c nbsp ein Konstantensymbol so ist c displaystyle c nbsp ein Term Ist f displaystyle f nbsp ein einstelliges Funktionssymbol und ist t 1 displaystyle t 1 nbsp ein Term so ist f t 1 displaystyle ft 1 nbsp ein Term Ist f displaystyle f nbsp ein zweistelliges Funktionssymbol und sind t 1 t 2 displaystyle t 1 t 2 nbsp Terme so ist f t 1 t 2 displaystyle ft 1 t 2 nbsp ein Term und so weiter fur 3 4 5 stellige Funktionssymbole AnmerkungenIst zum Beispiel c displaystyle c nbsp eine Konstante und sind f displaystyle f nbsp und g displaystyle g nbsp ein bzw zweistellige Funktionssymbole so ist f g v 2 f c displaystyle fgv 2 fc nbsp ein Term da er sich durch Anwendung obiger Regeln erstellen lasst c displaystyle c nbsp ist ein Term daher auch f c displaystyle fc nbsp f c displaystyle fc nbsp und v 2 displaystyle v 2 nbsp sind Terme daher auch g v 2 f c displaystyle gv 2 fc nbsp und damit schliesslich auch f g v 2 f c displaystyle fgv 2 fc nbsp Wir verzichten hier auf Klammern und Kommata als Trennzeichen das heisst wir schreiben f g v 2 f c displaystyle fgv 2 fc nbsp und nicht f g v 2 f c displaystyle f g v 2 f c nbsp Wir setzen damit implizit voraus dass unsere Symbole derart beschaffen sind dass eine eindeutige Lesbarkeit gewahrleistet ist Siehe Polnische Notation Konstanten werden manchmal als nullstellige Funktionen aufgefasst was in dieser Notation besonders naheliegend ist Die Regeln fur die Funktionssymbole fasst man oft so zusammen o Ist f displaystyle f nbsp ein n stelliges Funktionssymbol und sind t 1 t n displaystyle t 1 ldots t n nbsp Terme so ist f t 1 t n displaystyle ft 1 ldots t n nbsp ein Term Damit ist nichts anderes als die oben angedeutete unendliche Folge von Regeln gemeint denn die drei Punkte displaystyle ldots nbsp gehoren nicht zu den vereinbarten Symbolen Dennoch wird manchmal von dieser Schreibweise Gebrauch gemacht Uber den Aufbau der Terme lassen sich weitere Eigenschaften definieren So ist zunachst die Menge v a r t displaystyle mathrm var t nbsp der in einem Term t displaystyle t nbsp vorkommenden Variablen durch die folgenden drei Regeln rekursiv definiert Ist v displaystyle v nbsp ein Variablensymbol so sei v a r v v displaystyle mathrm var v v nbsp Ist c displaystyle c nbsp ein Konstantensymbol so sei v a r c displaystyle mathrm var c emptyset nbsp Ist f displaystyle f nbsp ein n stelliges Funktionssymbol und sind t 1 t n displaystyle t 1 ldots t n nbsp Terme so sei v a r f t 1 t n v a r t 1 v a r t n displaystyle mathrm var ft 1 ldots t n mathrm var t 1 cup ldots cup mathrm var t n nbsp Ausdrucke Bearbeiten Wir erklaren nun durch Bildungsgesetze welche Zeichenketten wir als Ausdrucke der Sprache ansehen wollen 8 9 3 S 46 f 7 S 4Atomare Ausdrucke 6 S 5 Sind t 1 displaystyle t 1 nbsp und t 2 displaystyle t 2 nbsp Terme so ist t 1 t 2 displaystyle t 1 equiv t 2 nbsp ein Ausdruck Ist R displaystyle R nbsp ein einstelliges Relationssymbol und ist t 1 displaystyle t 1 nbsp ein Term so ist R t 1 displaystyle Rt 1 nbsp ein Ausdruck Ist R displaystyle R nbsp ein zweistelliges Relationssymbol und sind t 1 t 2 displaystyle t 1 t 2 nbsp Terme so ist R t 1 t 2 displaystyle Rt 1 t 2 nbsp ein Ausdruck und so weiter fur 3 4 5 stellige Relationssymbole 10 Dabei gelten die oben zur Schreibweise bei Termen gemachten Bemerkungen Zusammengesetzte Ausdrucke 6 S 6Wir beschreiben hier wie sich aus Ausdrucken weitere gewinnen lassen 11 Ist f displaystyle varphi nbsp ein Ausdruck so ist auch f displaystyle neg varphi nbsp ein Ausdruck Sind f displaystyle varphi nbsp und ps displaystyle psi nbsp Ausdrucke so sind auch f ps displaystyle varphi land psi nbsp f ps displaystyle varphi lor psi nbsp f ps displaystyle varphi rightarrow psi nbsp und f ps displaystyle varphi leftrightarrow psi nbsp Ausdrucke Ist f displaystyle varphi nbsp ein Ausdruck und ist x displaystyle x nbsp eine Variable so sind auch x f displaystyle forall x varphi nbsp und x f displaystyle exists x varphi nbsp Ausdrucke Damit sind alle Ausdrucke unserer Sprache festgelegt Ist zum Beispiel f displaystyle f nbsp ein einstelliges Funktionssymbol und R displaystyle R nbsp ein 2 stelliges Relationssymbol so ist v 0 R v 0 v 1 v 0 f v 1 v 2 R v 0 v 2 displaystyle forall v 0 Rv 0 v 1 lor v 0 equiv fv 1 rightarrow exists v 2 neg Rv 0 v 2 nbsp ein Ausdruck da er sich durch Anwendung obiger Regeln aufbauen lasst Es sei noch einmal darauf hingewiesen dass wir die Ausdrucke mittels der genannten Regeln rein mechanisch erstellen ohne dass die Ausdrucke zwangslaufig irgendetwas bezeichnen mussten 1 Stufe Bearbeiten Unterschiedliche Sprachen erster Stufe unterscheiden sich lediglich in den Mengen C displaystyle mathcal C nbsp F displaystyle mathcal F nbsp und R displaystyle mathcal R nbsp die man ublicherweise zur Symbolmenge S displaystyle S nbsp zusammenfasst und auch die Signatur der Sprache nennt Man spricht dann auch genauer von S displaystyle S nbsp Termen bzw S displaystyle S nbsp Ausdrucken Die Sprache das heisst die Gesamtheit aller nach obigen Regeln gebildeten Ausdrucke wird mit L S displaystyle L S nbsp L S displaystyle L S nbsp oder L I S displaystyle L I S nbsp bezeichnet Bei letzterem steht die romische I displaystyle I nbsp fur die erste Stufe Dies bezieht sich auf den Umstand dass gemass letzter Erzeugungsregel fur zusammengesetzte Ausdrucke nur uber Variablen quantifiziert werden kann L I S displaystyle L I S nbsp sieht nicht vor uber alle Teilmengen einer Menge uber Relationen 12 oder uber Funktionen zu quantifizieren So lassen sich die ublichen Peano Axiome nicht in L I S displaystyle L I S nbsp ausdrucken da das Induktionsaxiom eine Aussage uber alle Teilmengen der naturlichen Zahlen macht Das kann als Schwache dieser Sprache angesehen werden allerdings sind die Axiome der Zermelo Fraenkel Mengenlehre samtlich in der ersten Stufe mit dem einzigen Symbol displaystyle in nbsp formulierbar so dass die erste Stufe prinzipiell fur die Mathematik ausreicht 13 Freie Variablen Bearbeiten Weitere Eigenschaften von Ausdrucken der Sprache L I S displaystyle L I S nbsp lassen sich ebenfalls rein syntaktisch definieren Gemass dem oben beschriebenen Aufbau durch Bildungsregeln wird die Menge f r e i f displaystyle mathrm frei varphi nbsp der im Ausdruck f displaystyle varphi nbsp frei vorkommenden Variablen wie folgt rekursiv definiert 14 3 S 48 f 7 S 6 f r e i t 1 t 2 v a r t 1 v a r t 2 displaystyle mathrm frei t 1 equiv t 2 mathrm var t 1 cup mathrm var t 2 nbsp f r e i R t 1 t n v a r t 1 v a r t n displaystyle mathrm frei Rt 1 ldots t n mathrm var t 1 cup ldots cup mathrm var t n nbsp f r e i f f r e i f displaystyle mathrm frei neg varphi mathrm frei varphi nbsp f r e i f ps f r e i f f r e i ps displaystyle mathrm frei varphi land psi mathrm frei varphi cup mathrm frei psi nbsp und genauso fur displaystyle lor rightarrow leftrightarrow nbsp f r e i x f f r e i f x displaystyle mathrm frei forall x varphi mathrm frei varphi setminus x nbsp f r e i x f f r e i f x displaystyle mathrm frei exists x varphi mathrm frei varphi setminus x nbsp Nicht freie Variable heissen gebundene Variable Ausdrucke f displaystyle varphi nbsp ohne freie Variable das heisst solche mit f r e i f displaystyle mathrm frei varphi emptyset nbsp nennt man Satze Samtliche in obigem motivierenden Beispiel angegebenen Axiome der geordneten abelschen Gruppen sind bei entsprechender Ubersetzung in die Sprache L I 0 displaystyle L I 0 leq nbsp Satze so zum Beispiel v 0 v 1 v 0 v 1 v 1 v 0 displaystyle forall v 0 forall v 1 v 0 v 1 equiv v 1 v 0 nbsp fur das Kommutativgesetz Metasprachliche Ausdrucke Bearbeiten Das gerade gegebene Beispiel v 0 v 1 v 0 v 1 v 1 v 0 displaystyle forall v 0 forall v 1 v 0 v 1 equiv v 1 v 0 nbsp als Symbolisierung des Kommutativgesetzes in der Sprache L I 0 displaystyle L I 0 leq nbsp zeigt dass die entstehenden Ausdrucke oft schwer lesbar sind Daher kehrt der Mathematiker und oft auch der Logiker gern zur klassischen Schreibweise x y x y y x displaystyle forall x y x y y x nbsp zuruck Letzteres ist aber kein Ausdruck der Sprache L I 0 displaystyle L I 0 leq nbsp sondern nur eine Mitteilung eines solchen Ausdrucks unter Verwendung anderer Symbole einer anderen Sprache hier der sogenannten Metasprache das heisst derjenigen Sprache in der man uber L I 0 displaystyle L I 0 leq nbsp spricht Aus Grunden der besseren Lesbarkeit lasst man auch gern uberflussige Klammern weg Das fuhrt nicht zu Problemen solange klar bleibt dass man die leichter lesbaren Zeichenketten jederzeit zuruckubersetzen konnte Substitutionen Bearbeiten Haufig werden in der Mathematik Variablen durch Terme ersetzt Auch das lasst sich hier rein syntaktisch auf Basis unserer Symbole erklaren Durch folgende Regeln legen wir fest was es bedeuten soll den Term t displaystyle t nbsp fur eine Variable x displaystyle x nbsp einzusetzen Die Substitution wird fur Terme s displaystyle s nbsp als s t x displaystyle s frac t x nbsp und fur Ausdrucke f displaystyle varphi nbsp als f t x displaystyle varphi frac t x nbsp gleichermassen durch eckige Klammern notiert Die eckigen Klammern durfen auch weggelassen werden Fur Terme s displaystyle s nbsp wird die Substitution s t x displaystyle s frac t x nbsp wie folgt definiert Ist v displaystyle v nbsp ein Variablensymbol so ist v t x displaystyle v frac t x nbsp gleich t displaystyle t nbsp falls v x displaystyle v x nbsp und v displaystyle v nbsp sonst Ist c displaystyle c nbsp ein Konstantensymbol so ist c t x c displaystyle c frac t x c nbsp Sind f displaystyle f nbsp ein n stelliges Funktionssymbol und t 1 t n displaystyle t 1 ldots t n nbsp Terme so ist f t 1 t n t x f t 1 t x t n t x displaystyle ft 1 ldots t n frac t x ft 1 frac t x ldots t n frac t x nbsp Fur Ausdrucke f displaystyle varphi nbsp legen wir fest t 1 t 2 t x t 1 t x t 2 t x displaystyle t 1 equiv t 2 frac t x t 1 frac t x equiv t 2 frac t x nbsp R t 1 t n t x R t 1 t x t n t x displaystyle Rt 1 ldots t n frac t x Rt 1 frac t x ldots t n frac t x nbsp f t x f t x displaystyle neg varphi frac t x neg varphi frac t x nbsp f ps t x f t x ps t x displaystyle varphi lor psi frac t x varphi frac t x lor psi frac t x nbsp analog fur die Junktoren displaystyle land rightarrow leftrightarrow nbsp y f t x y f fur x y y f t x fur x y und y var t u f u y t x fur x y und y var t displaystyle exists y varphi frac t x begin cases exists y varphi amp text fur x y exists y varphi frac t x amp text fur x neq y text und y notin operatorname var t exists u varphi frac u y frac t x amp text fur x neq y text und y in operatorname var t end cases nbsp dabei sei u displaystyle u nbsp eine Variable die nicht in f displaystyle varphi nbsp oder t displaystyle t nbsp vorkommt zum Beispiel die erste der Variablen v 0 v 1 v 2 displaystyle v 0 v 1 v 2 ldots nbsp die diese Bedingung erfullt Bei dieser Definition wurde darauf geachtet dass Variablen nicht unbeabsichtigt in den Einflussbereich eines Quantors geraten Falls die gebundene Variable x displaystyle x nbsp im Term auftritt so wird diese zuvor durch eine andere ersetzt um so die Variablenkollision zu vermeiden analog fur den Quantor displaystyle forall nbsp Schlussbemerkung zur Syntax Bearbeiten Es sei noch einmal betont dass alles bisher Gesagte nur den Aufbau beziehungsweise die Manipulation gewisser Zeichenketten beschreibt es handelt sich um rein syntaktische Begriffe Weder den Zeichenketten noch ihren Manipulationen sind irgendwelche Bedeutungsinhalte zugeordnet Selbstverstandlich liest man unwillkurlich die Bedeutungen mit die durch obiges Beispiel suggeriert sind das heisst man liest ein displaystyle forall nbsp als fur alle und ein displaystyle land nbsp als und und kann sich nur schwer von ihren umgangssprachlichen Bedeutungen frei machen Man sollte sich aber daruber im Klaren sein dass eine solche Bedeutung fur die vorgestellten Begriffsbildungen nicht erforderlich ist und an keiner Stelle verwendet wird Es ist ein wesentlicher Punkt dass die intendierte Bedeutung dieser Zeichenketten ihre Semantik erst in einem im Folgenden vorgestellten Schritt hinzugefugt wird Semantik BearbeitenWir gehen von einer Sprache L I S displaystyle L I S nbsp aus Die nach obigen Regeln in dieser Sprache gebildeten Ausdrucke sollen nun mit mathematischen Strukturen in Verbindung gebracht werden In diesen Strukturen kann man die Ausdrucke dann auf ihren Wahrheitsgehalt hin untersuchen was im Folgenden prazisiert wird Strukturen Bearbeiten Eine Struktur A displaystyle mathcal A nbsp uber einer Signatur S displaystyle S nbsp ist eine nicht leere Menge A displaystyle A nbsp zusammen mit einem Element c A A displaystyle c mathcal A in A nbsp fur jedes Konstantensymbol c S displaystyle c in S nbsp einer Funktion f A A n A displaystyle f mathcal A A n rightarrow A nbsp fur jedes n displaystyle n nbsp stellige Funktionssymbol f S displaystyle f in S nbsp einer Relation R A A n displaystyle R mathcal A subset A n nbsp fur jedes n displaystyle n nbsp stellige Relationssymbol R S displaystyle R in S nbsp Im eingangs gegebenen Beispiel geordneter abelscher Gruppen ist R 0 displaystyle mathbb R 0 leq nbsp eine 0 displaystyle 0 leq nbsp Struktur Durch S displaystyle S nbsp Strukturen werden also die Symbole aus S displaystyle S nbsp mit echten Konstanten Funktionen und Relationen in Zusammenhang gebracht Interpretationen Bearbeiten Eine Interpretation von L I S displaystyle L I S nbsp ist ein Paar I A b displaystyle mathcal I mathcal A beta nbsp bestehend aus einer S displaystyle S nbsp Struktur A displaystyle mathcal A nbsp und einer Abbildung b v i i N 0 A displaystyle beta v i i in mathbb N 0 rightarrow A nbsp Man verbindet damit die Vorstellung dass die Struktur das mathematische Objekt ist das mit der Sprache beschrieben werden soll wahrend b displaystyle beta nbsp die Variablen mit Werten aus der Grundmenge A displaystyle A nbsp belegt weshalb man diese Abbildung auch Belegung nennt Die Belegung einer Interpretation kann leicht auf Terme ausgedehnt werden diese Ausdehnung hangt von der Interpretation der Konstantensymbole und Funktionssymbole ab und wird daher ebenfalls mit I displaystyle mathcal I nbsp bezeichnet man legt fest Ist v displaystyle v nbsp eine Variable so sei I v b v displaystyle mathcal I v beta v nbsp Ist c displaystyle c nbsp ein Konstantensymbol so sei I c c A displaystyle mathcal I c c mathcal A nbsp Ist f displaystyle f nbsp ein n stelliges Funktionssymbol und sind t 1 t n displaystyle t 1 ldots t n nbsp Terme so sei I f t 1 t n f A I t 1 I t n displaystyle mathcal I ft 1 ldots t n f mathcal A mathcal I t 1 ldots mathcal I t n nbsp Setzt man etwa b v i i R displaystyle beta v i i in mathbb R nbsp so ist I R 0 b displaystyle mathcal I mathbb R 0 leq beta nbsp eine solche Interpretation Dann gilt I v 1 v 7 A I v 1 A I v 7 1 7 6 displaystyle mathcal I v 1 v 7 mathcal A mathcal I v 1 mathcal A mathcal I v 7 1 7 6 nbsp Andern wir eine Belegung nur an der Stelle x displaystyle x nbsp ab und bilden dieses x displaystyle x nbsp auf a A displaystyle a in A nbsp ab so schreiben wir b a x displaystyle beta frac a x nbsp fur die so abgeanderte Belegung und I a x A b a x displaystyle mathcal I frac a x mathcal A beta frac a x nbsp Oft ist die Belegung der Variablen klar oder unwichtig dann nennen wir etwas unsauber aber praktisch auch die Struktur A displaystyle mathcal A nbsp eine Interpretation Modelle Bearbeiten Wir wollen sagen dass eine Interpretation I A b displaystyle mathcal I mathcal A beta nbsp ein Modell fur einen S displaystyle S nbsp Ausdruck f displaystyle varphi nbsp ist und dafur I f displaystyle mathcal I vDash varphi nbsp schreiben wenn sich dies auf Grund folgender Regeln ergibt 15 I t 1 t 2 I t 1 I t 2 I R t 1 t n R A I t 1 I t n I f nicht I f I f ps I f und I ps I f ps I f oder I ps I f ps wenn I f dann auch I ps I f ps I f genau dann wenn I ps I x f I a x f fur alle a A I x f es gibt ein a A mit I a x f displaystyle begin matrix mathcal I vDash t 1 equiv t 2 amp Leftrightarrow amp mathcal I t 1 mathcal I t 2 mathcal I vDash Rt 1 ldots t n amp Leftrightarrow amp R mathcal A mathcal I t 1 ldots mathcal I t n mathcal I vDash neg varphi amp Leftrightarrow amp text nicht mathcal I vDash varphi mathcal I vDash varphi land psi amp Leftrightarrow amp mathcal I vDash varphi text und mathcal I vDash psi mathcal I vDash varphi lor psi amp Leftrightarrow amp mathcal I vDash varphi text oder mathcal I vDash psi mathcal I vDash varphi rightarrow psi amp Leftrightarrow amp text wenn mathcal I vDash varphi text dann auch mathcal I vDash psi mathcal I vDash varphi leftrightarrow psi amp Leftrightarrow amp mathcal I vDash varphi text genau dann wenn mathcal I vDash psi mathcal I vDash forall x varphi amp Leftrightarrow amp mathcal I frac a x vDash varphi mbox fur alle a in A mathcal I vDash exists x varphi amp Leftrightarrow amp text es gibt ein a in A text mit mathcal I frac a x vDash varphi end matrix nbsp Diese Definition orientiert sich wieder am regelhaften Aufbau der Ausdrucke der Sprache L I S displaystyle L I S nbsp Die Punktchenschreibweise in der zweiten Regel steht hier wieder fur eine Liste von Regeln fur jede Stelligkeit eine Durch den Begriff der Interpretation wurden die Variablen und die Symbole aus S displaystyle S nbsp mit einer Bedeutung versehen Durch die gerade definierte Modellbeziehung werden erstmals auch die logischen Symbole interpretiert Fur eine Menge F displaystyle Phi nbsp von Ausdrucken schreiben wir I F displaystyle mathcal I vDash Phi nbsp wenn I f displaystyle mathcal I vDash varphi nbsp fur alle f F displaystyle varphi in Phi nbsp gilt und sagen I displaystyle mathcal I nbsp sei ein Modell von F displaystyle Phi nbsp Bezeichnet F displaystyle Phi nbsp etwa die oben genannten Axiome der geordneten abelschen Gruppen so gilt I A b F displaystyle mathcal I mathcal A beta vDash Phi nbsp genau dann wenn A displaystyle mathcal A nbsp eine geordnete abelsche Gruppe ist Dabei scheint die Belegung b displaystyle beta nbsp keine Rolle zu spielen da F displaystyle Phi nbsp nur aus Satzen besteht also keine freien Variablen enthalt Das ist tatsachlich der Fall wie das sogenannte Koinzidenzlemma aussagt In einem solchen Fall kann man b displaystyle beta nbsp weglassen und einfach A F displaystyle mathcal A vDash Phi nbsp schreiben Damit ist dann ausgesagt dass I A b displaystyle mathcal I mathcal A beta nbsp fur jede Belegung b displaystyle beta nbsp ein Modell aller Ausdrucke aus F displaystyle Phi nbsp ist Gleichheit Bearbeiten Zur Verwendung der Gleichheit ist anzumerken dass wir in der Sprache erster Stufe das Symbol displaystyle equiv nbsp eingefuhrt haben Ein Ausdruck der Form f ps displaystyle varphi psi nbsp ist kein Ausdruck der Sprache erster Stufe sondern die metasprachliche Behauptung der Gleichheit der beiden Ausdrucke f displaystyle varphi nbsp und ps displaystyle psi nbsp Letzteres lasst sich in der Sprache erster Stufe gar nicht symbolisieren dort konnen nur Terme gleich sein Parallel zum hier betrachteten Aufbau gibt es auch die Pradikatenlogik erster Stufe ohne Gleichheit dazu entfernt man das Symbol displaystyle equiv nbsp und die es betreffende Bildungsregel Zwar kann man die Gleichheit dann uber eine Relation wieder ins Spiel bringen setzt diese dann aber Interpretationen aus so dass man nicht dasselbe erhalt wie eine Logik mit Gleichheit Die logische Gleichheit displaystyle equiv nbsp hingegen bedeutet in jeder Interpretation Gleichheit von Individuen und das ist der Grund warum man Logiken mit Gleichheit betrachtet 16 Mathematisches Schliessen BearbeitenFolgerungen Bearbeiten Es sei F displaystyle Phi nbsp eine gegebene Menge von Ausdrucken zum Beispiel obige Axiome der geordneten abelschen Gruppen Der Mathematiker interessiert sich dafur welche Folgerungen aus ihnen gezogen werden konnen Wir sagen der Ausdruck f displaystyle varphi nbsp folge aus F displaystyle Phi nbsp und schreiben dafur F f displaystyle Phi vDash varphi nbsp wenn jedes Modell von F displaystyle Phi nbsp auch Modell von f displaystyle varphi nbsp ist Das ist die sogenannte semantische Schlussweise da sie Bezug auf alle moglichen Interpretationen der Symbole nimmt Sequenzenkalkul Bearbeiten Hauptartikel Sequenzenkalkul In der Regel schliesst der Mathematiker nicht semantisch sondern er wendet gewisse Schlussregeln an mit denen er sich von einer Aussage zur nachsten bis zur Behauptung vorarbeitet Ausgehend von einer gegebenen Folge F displaystyle Phi nbsp von Ausdrucken geht er zu neuen Folgen F f ps displaystyle Phi varphi psi ldots nbsp uber um am Ende mit einer Folge F f displaystyle Phi varphi nbsp bewiesen zu haben dass f displaystyle varphi nbsp aus F displaystyle Phi nbsp folgt Der Beweis ist dabei eine endliche Liste solcher Folgen Hier werden einige solcher Schlussregeln vorgestellt ihr inhaltlicher Hintergrund beleuchtet und anschliessend mit der semantischen Schlussweise verglichen In F f ps displaystyle Phi varphi psi ldots nbsp nennt man F displaystyle Phi nbsp das Antezedens und die nachfolgenden Ausdrucke das Sukzedens Voraussetzungsregel F f displaystyle Phi varphi nbsp ist eine erlaubte Folge wenn f F displaystyle varphi in Phi nbsp Dahinter steckt der einfache Tatbestand dass man jederzeit eine der Voraussetzungen aus F displaystyle Phi nbsp verwenden darf Antezedensregel Falls man F f displaystyle Phi varphi nbsp bereits hat so kann man zu F f displaystyle Phi varphi nbsp ubergehen falls F F displaystyle Phi subset Phi nbsp Wenn man namlich von F displaystyle Phi nbsp auf f displaystyle varphi nbsp schliessen kann so kann man das erst recht unter noch starkeren Voraussetzungen tun Fallunterscheidung Falls man F ps f displaystyle Phi psi varphi nbsp und F ps f displaystyle Phi neg psi varphi nbsp bereits hat so kann man zu F f displaystyle Phi varphi nbsp ubergehen Man kann im Falle ps displaystyle psi nbsp von F displaystyle Phi nbsp auf f displaystyle varphi nbsp schliessen und auch im Falle von ps displaystyle neg psi nbsp Daher kann man in jedem Fall von F displaystyle Phi nbsp auf f displaystyle varphi nbsp schliessen Widerspruch Falls man F f ps displaystyle Phi neg varphi psi nbsp und F f ps displaystyle Phi neg varphi neg psi nbsp bereits hat so kann man zu F f displaystyle Phi varphi nbsp ubergehen Nimmt man namlich im Sinne eines Widerspruchsbeweises an dass f displaystyle neg varphi nbsp gilt so ergibt sich aus den Voraussetzungen sowohl ps displaystyle psi nbsp als auch ps displaystyle neg psi nbsp insgesamt also ein Widerspruch Daher war die Annahme f displaystyle neg varphi nbsp falsch und man kann auf f displaystyle varphi nbsp schliessen Odereinfuhrung im Antezedens Falls man F f x displaystyle Phi varphi chi nbsp und F ps x displaystyle Phi psi chi nbsp bereits hat so kann man zu F f ps x displaystyle Phi varphi lor psi chi nbsp ubergehen Unter den Voraussetzungen F displaystyle Phi nbsp ergibt sich x displaystyle chi nbsp sowohl aus f displaystyle varphi nbsp als auch aus ps displaystyle psi nbsp Daher ergibt sich x displaystyle chi nbsp bereits wenn f displaystyle varphi nbsp oder ps displaystyle psi nbsp gilt Odereinfuhrung im Sukzedens Falls man F f displaystyle Phi varphi nbsp bereits hat so kann man zu F f ps displaystyle Phi varphi lor psi nbsp ubergehen Das ist klar da mit f displaystyle varphi nbsp erst recht f ps displaystyle varphi lor psi nbsp gilt Entsprechend kann man auch zu F ps f displaystyle Phi psi lor varphi nbsp ubergehen Gleichheit Man kann jederzeit den Ausdruck t t displaystyle t equiv t nbsp hinschreiben wobei t displaystyle t nbsp ein beliebiger Term ist Diese Regel bedarf keiner Erlauterung Die noch folgenden drei Schlussregeln verwenden die oben definierte Substitution von Variablen durch Terme Substitution Falls man F f t x displaystyle Phi varphi frac t x nbsp bereits hat so kann man zu F t s f s x displaystyle Phi t equiv s varphi frac s x nbsp ubergehen Wenn man aus F displaystyle Phi nbsp auf f t x displaystyle varphi frac t x nbsp das heisst auf f displaystyle varphi nbsp mit der Ersetzung t displaystyle t nbsp an Stelle von x displaystyle x nbsp schliessen kann so auch auf f displaystyle varphi nbsp mit der Ersetzung s displaystyle s nbsp an Stelle von x displaystyle x nbsp falls t displaystyle t nbsp gleich s displaystyle s nbsp ist Existenzeinfuhrung im Antezedens Falls man F f y x ps displaystyle Phi varphi frac y x psi nbsp bereits hat so kann man zu F x f ps displaystyle Phi exists x varphi psi nbsp ubergehen Um mit der Existenzvoraussetzung x f displaystyle exists x varphi nbsp arbeiten zu konnen darf man ein y displaystyle y nbsp verwenden fur das f y x displaystyle varphi frac y x nbsp gilt In Beweisen die diese Regel verwenden heisst dann nach der Existenzvoraussetzung Sei y displaystyle y nbsp so ein Existenzeinfuhrung im Sukzendens Falls man F f t x displaystyle Phi varphi frac t x nbsp bereits hat so kann man zu F x f displaystyle Phi exists x varphi nbsp ubergehen Auch diese Regel ist einsichtig denn wenn man mit t displaystyle t nbsp ein Beispiel fur f displaystyle varphi nbsp gefunden hat so kann man auf die Existenzaussage schliessen und braucht das Beispiel dabei nicht mehr zu erwahnen Die hier vorgestellten Regeln die den sogenannten Sequenzenkalkul bilden sind logisch schlussig wie als Zusatz zu jeder Regelnennung ausgefuhrt wurde Mathematiker verwenden noch einige andere Schlussregeln von denen aber gezeigt werden kann dass sie alle aus den oben genannten hergeleitet werden konnen das heisst ihre Anwendung kann durch eine endliche Kette obiger Regeln ersetzt werden Wenn man ausgehend von F displaystyle Phi nbsp nach endlich vielen Anwendungen dieser Regeln zu F f displaystyle Phi varphi nbsp gelangt ist so ist damit f displaystyle varphi nbsp aus F displaystyle Phi nbsp logisch schlussig abgeleitet wir schreiben dafur F f displaystyle Phi vdash varphi nbsp Im Gegensatz zur oben erklarten semantischen Schlussweise sind die Beweise F f displaystyle Phi vdash varphi nbsp rein syntaktischer Natur man kann sie als Manipulation von Zeichenketten der betrachteten Sprache ansehen Um die Schlussregeln anwenden zu konnen muss man nicht wissen was die Symbole bedeuten Vollstandigkeit und Korrektheit Bearbeiten Hauptartikel Vollstandigkeit Logik und Godelscher Vollstandigkeitssatz Ist die Interpretation I displaystyle mathcal I nbsp ein Modell fur eine Menge F displaystyle Phi nbsp von Ausdrucken der Sprache L I S displaystyle L I S nbsp und ist F f displaystyle Phi vdash varphi nbsp so ist I displaystyle mathcal I nbsp auch ein Modell fur f displaystyle varphi nbsp denn der mit F f displaystyle Phi vdash varphi nbsp einhergehende Beweis lasst sich ja ohne Weiteres direkt im Modell ausfuhren Es gilt also der sogenannte Korrektheitssatz dass aus F f displaystyle Phi vdash varphi nbsp stets F f displaystyle Phi vDash varphi nbsp folgt Umgekehrt ware es durchaus denkbar dass es zu einer Ausdrucksmenge F displaystyle Phi nbsp nur einige wenige Modelle gibt die zufallig eine in der Sprache erster Stufe ausdruckbare Eigenschaft f displaystyle varphi nbsp gemeinsam haben ohne dass es dazu eine Moglichkeit gabe sie durch obige syntaktische Zeichenkettenoperationen aus F displaystyle Phi nbsp ableiten zu konnen Dass dies nicht der Fall ist sondern dass semantische und syntaktische Schlussweisen gleichwertig sind ist als Godelscher Vollstandigkeitssatz bekannt und ein zentrales Ergebnis der Pradikatenlogik erster Stufe Man kann zeigen dass sich zu einer Pradikatenlogik zweiter Stufe in der man Quantifizierungen uber Relationen zulasst kein zur semantischen Schlussweise gleichwertiger Sequenzenkalkul finden lasst Eigenschaften BearbeitenErfullbarkeitssatz Bearbeiten Eine Menge F displaystyle Phi nbsp von Ausdrucken der Sprache L I S displaystyle L I S nbsp heisst widerspruchsfrei wenn sich kein Ausdruck der Form f f displaystyle varphi land neg varphi nbsp aus F displaystyle Phi nbsp ableiten lasst Damit ist Widerspruchsfreiheit ein rein syntaktischer Begriff Es gilt folgender Erfullbarkeitssatz der sich aus dem Satz von Henkin herleiten lasst und eng mit dem Godelschen Vollstandigkeitssatz verbunden ist Zu jeder widerspruchsfreien Menge F displaystyle Phi nbsp gibt es ein Modell Kompaktheitssatz Bearbeiten Kompaktheitssatz Ist F displaystyle Phi nbsp eine Menge von Ausdrucken der Sprache L I S displaystyle L I S nbsp und gibt es zu jeder endlichen Teilmenge von F displaystyle Phi nbsp ein Modell so gibt es auch ein Modell fur F displaystyle Phi nbsp 17 Gabe es namlich kein Modell fur F displaystyle Phi nbsp so ware F displaystyle Phi nbsp nach dem Erfullbarkeitssatz nicht widerspruchsfrei und es gabe dann eine Ableitung F f f displaystyle Phi vdash varphi land neg varphi nbsp Da ein Beweis aber nur eine endliche Lange hat und daher auch nur endlich viele der Ausdrucke aus F displaystyle Phi nbsp involvieren kann muss es bereits eine endliche Teilmenge F 0 displaystyle Phi 0 nbsp geben mit F 0 f f displaystyle Phi 0 vdash varphi land neg varphi nbsp Nach dem Vollstandigkeitssatz folgt F 0 f f displaystyle Phi 0 vDash varphi land neg varphi nbsp das heisst es kann fur F 0 displaystyle Phi 0 nbsp kein Modell geben im Widerspruch zur Voraussetzung Der Endlichkeitssatz wird auch Kompaktheitssatz genannt Man wahle zu jeder widerspruchsfreien Menge F displaystyle Phi nbsp von Satzen ein Modell A F displaystyle mathcal A Phi nbsp und fasse die so gefundenen Modelle zu einer Menge X displaystyle mathcal X nbsp zusammen Fur einen Satz f displaystyle varphi nbsp sei X f A X A f displaystyle X varphi mathcal A in mathcal X mathcal A vDash varphi nbsp Dann bilden die Mengen X f displaystyle X varphi nbsp die Basis einer Topologie auf X displaystyle mathcal X nbsp und der Endlichkeitssatz ist zur Kompaktheit dieses Raums aquivalent Isomorphien Bearbeiten Aus dem Kompaktheitssatz folgt Gibt es zu einer Menge F displaystyle Phi nbsp von Ausdrucken der Sprache L I S displaystyle L I S nbsp ein unendliches Modell so gibt es Modelle beliebig hoher Machtigkeit Ist namlich F displaystyle Phi nbsp gegeben und ist k displaystyle kappa nbsp eine Kardinalzahl so sei c a a lt k displaystyle c alpha alpha lt kappa nbsp eine Menge von nicht in S displaystyle S nbsp enthaltenen Konstantensymbolen Jede endliche Teilmenge von F c a c b a lt b lt k displaystyle Phi cup neg c alpha equiv c beta alpha lt beta lt kappa nbsp hat dann ein Modell in der Sprache L I S displaystyle L I tilde S nbsp wobei S displaystyle tilde S nbsp die um die neuen Konstantensymbole erweiterte Symbolmenge sei Wegen des Endlichkeitssatzes gibt es dann ein Modell fur F c a c b a lt b lt k displaystyle Phi cup neg c alpha equiv c beta alpha lt beta lt kappa nbsp und das hat mindestens die Machtigkeit k displaystyle kappa nbsp Mit etwas genauerer Argumentation kann man sogar ein Modell der Machtigkeit k displaystyle kappa nbsp finden falls die Machtigkeit von F displaystyle Phi nbsp kleiner gleich k displaystyle kappa nbsp ist Hier zeigt sich eine Schwache der Pradikatenlogik erster Stufe Mittels der Sprache der ersten Stufe kann fur Ausdrucksmengen mit unendlichen Modellen niemals eine Charakterisierung bis auf Isomorphie gelingen denn die Klasse aller Modelle zu einer solchen widerspruchsfreien Menge von Ausdrucken enthalt stets Modelle beliebig hoher Machtigkeit also auch nicht isomorphe Modelle Man nennt zwei Modelle elementar aquivalent wenn die Mengen der Ausdrucke fur die sie Modelle sind ubereinstimmen Die Sprachen erster Stufe konnen daher unendliche Strukturen bzw Modelle nur bis auf elementare Aquivalenz charakterisieren Satz von Lowenheim Skolem Bearbeiten Hauptartikel Satz von Lowenheim Skolem Ebenfalls aus dem Satz von Henkin lasst sich der Satz von Lowenheim Skolem ableiten Gibt es zu einer hochstens abzahlbaren Menge F displaystyle Phi nbsp von Ausdrucken der Sprache L I S displaystyle L I S nbsp ein unendliches Modell so gibt es auch ein abzahlbares Modell Im einleitenden Beispiel ist Z displaystyle mathbb Z leq nbsp ein abzahlbares Modell In vielen mathematischen Theorien lassen sich diese sehr leicht finden in der Modelltheorie hat das Lowenheim Skolem Theorem aber tiefgehende Anwendungen Satz von Lindstrom Bearbeiten Wegen oben genannter Schwachen der Sprache erster Stufe kann man nach geeigneten Erweiterungen suchen Wenn man auf diese Weise echt ausdrucksstarkere Sprachen findet was naturlich noch zu prazisieren ware so zeigen die Satze von Lindstrom dass man dann auf den Endlichkeitssatz oder auf den Satz von Lowenheim Skolem verzichten muss Will man beide Satze beibehalten so ist die Pradikatenlogik erster Stufe also das Beste was man erreichen kann Siehe auch BearbeitenLogik hoherer Stufe fur weitere Erweiterungen der Logik Lokalitat Logik zu Grenzen der Ausdrucksstarke der Pradikatenlogik erster Stufe Godelscher Unvollstandigkeitssatz ein grundlegender Satz der Pradikatenlogik erster Stufe und der mathematischen Logik uberhauptLiteratur BearbeitenH D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik Spektrum Akademischer Verlag 1996 ISBN 3 8274 0130 5 Wolfgang Rautenberg Einfuhrung in die Mathematische Logik 3 Auflage Vieweg Teubner Wiesbaden 2008 ISBN 978 3 8348 0578 2 doi 10 1007 978 3 8348 9530 1 Einzelnachweise und Anmerkungen Bearbeiten Das Kommazeichen wird hier nur als Trennzeichen fur die Aufzahlung der Symbole benutzt es ist nicht Symbol der Sprache Zur aussagenlogischen Entsprechung siehe Aussagenlogik Bausteine der aussagenlogischen Sprache a b c d Erich Gradel Mathematische Logik Mathematische Grundlagen der Informatik SS 2009 RWTH Aachen S 129 uni dortmund de PDF H D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik Spektrum Akademischer Verlag ISBN 3 8274 0130 5 II Definition 3 1 Zur aussagenlogischen Entsprechung siehe Aussagenlogik Formationsregeln a b c W Vogler Logik fur Informatiker WS 2007 2008 Univ Augsburg Institut fur Informatik Augsburg S 49 uni augsburg de PDF a b c R Kruse C Borgelt Grundbegriffe der Pradikatenlogik Computational Intelligence Otto von Guericke Universitat Magdeburg 2008 S 14 fuzzy cs ovgu de PDF H D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik Spektrum Akademischer Verlag ISBN 3 8274 0130 5 II Definition 3 2 Es findet sich auch die Bezeichnung Formel siehe Elementare Sprache Formeln und Logische Formel Entsprechend steht dann Atomformel fur Atomaren Ausdruck Gelegentlich werden nullstellige Relationen zugelassen dies treten dann als logische Konstanten im Prinzip Bezeichner fur wahr oder falsch auf Als alternativer Ausdruck fur die Relationssymbole findet man auch Pradikate Siehe Stefan Brass Mathematische Logik mit Datenbank Anwendungen Martin Luther Universitat Halle Wittenberg Institut fur Informatik Halle 2005 S 176 hier S 19 uni halle de PDF Auch als Aussagenlogische Verknupfungen bezeichnet mit dem Spezialfall einstelliger Relationen Teilmengen H D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik Spektrum Akademischer Verlag ISBN 3 8274 0130 5 VII Zur Tragweite der ersten Stufe H D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik Spektrum Akademischer Verlag ISBN 3 8274 0130 5 II Definition 5 1 H D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik Spektrum Akademischer Verlag ISBN 3 8274 0130 5 III Definition 3 2 Philipp Rothmaler Einfuhrung in die Modelltheorie Spektrum Akademischer Verlag 1995 ISBN 978 3 86025 461 5 Ende des Absatzes 3 1 H D Ebbinghaus J Flum W Thomas Einfuhrung in die mathematische Logik Spektrum Akademischer Verlag ISBN 3 8274 0130 5 VI 2 1 Abgerufen von https de wikipedia org w index php title Pradikatenlogik erster Stufe amp oldid 236675905