Whorf am 22. August 2019 um 15:48 Uhr

2019-08-22T15:48:21Z

← Nächstältere Version		Version vom 22. August 2019, 15:48 Uhr
Zeile 303:		Zeile 303:
	[[Kategorie:WikiPedia Deleted]]		[[Kategorie:WikiPedia Deleted]]
	[[Kategorie:Wikipedia Blamage]]		[[Kategorie:Wikipedia Blamage]]
			[[Kategorie:Logik]]

Whorf am 22. August 2019 um 15:45 Uhr

2019-08-22T15:45:47Z

← Nächstältere Version		Version vom 22. August 2019, 15:45 Uhr
Zeile 302:		Zeile 302:

	[[Kategorie:WikiPedia Deleted]]		[[Kategorie:WikiPedia Deleted]]
			[[Kategorie:Wikipedia Blamage]]

Gerhard kemme: /* Init-Quelle */

2011-11-22T19:14:47Z

Init-Quelle

← Nächstältere Version		Version vom 22. November 2011, 19:14 Uhr
Zeile 295:		Zeile 295:
	== Init-Quelle ==		== Init-Quelle ==
	Entnommen aus der:		Entnommen aus der:
	[http://de.wikipedia.org/wiki/Formales_System_(Logik) Wikipedia]		* [http://de.wikipedia.org/wiki/Formales_System_(Logik) Wikipedia]
			* [http://de.wikipedia.org/wiki/Wikipedia:L%C3%B6schkandidaten/21._Mai_2009#Formales_System_.28Logik.29_.28hier_erledigt.29 Formales System Logik - Löschdiskussion bei Wikipedia] - de.wikipedia.org

	Autoren: Avron, Jkbw, Luha, P. Birken, Birger Fricke, Hubertl, Uwe Lück, Wasserseele, Sebbot, Gereon K., GottschallCh , Allanon, 84.132.211.91 , Ephraim33, Friedemann Lindenthal, Mkleine, Pacogo7, Hubi, Bunt		Autoren: Avron, Jkbw, Luha, P. Birken, Birger Fricke, Hubertl, Uwe Lück, Wasserseele, Sebbot, Gereon K., GottschallCh , Allanon, 84.132.211.91 , Ephraim33, Friedemann Lindenthal, Mkleine, Pacogo7, Hubi, Bunt

	~~{{Link_LD_fehlt}}~~
	[[Kategorie:WikiPedia Deleted]]		[[Kategorie:WikiPedia Deleted]]

Anthoney: LD fehlt

2009-12-06T00:21:14Z

LD fehlt

← Nächstältere Version		Version vom 6. Dezember 2009, 00:21 Uhr
Zeile 298:		Zeile 298:

	Autoren: Avron, Jkbw, Luha, P. Birken, Birger Fricke, Hubertl, Uwe Lück, Wasserseele, Sebbot, Gereon K., GottschallCh , Allanon, 84.132.211.91 , Ephraim33, Friedemann Lindenthal, Mkleine, Pacogo7, Hubi, Bunt		Autoren: Avron, Jkbw, Luha, P. Birken, Birger Fricke, Hubertl, Uwe Lück, Wasserseele, Sebbot, Gereon K., GottschallCh , Allanon, 84.132.211.91 , Ephraim33, Friedemann Lindenthal, Mkleine, Pacogo7, Hubi, Bunt

			{{Link_LD_fehlt}}
			[[Kategorie:WikiPedia Deleted]]

84.166.106.81 am 4. August 2009 um 11:06 Uhr

2009-08-04T11:06:17Z

← Nächstältere Version		Version vom 4. August 2009, 11:06 Uhr
Zeile 1:		Zeile 1:
	~~{{QS-Mathematik}}~~
	{{Redundanztext\|[[Benutzer:Gratisaktie\|Gratisaktie]] 14:02, 17. Sep 2006 (CEST); [[Benutzer:Uwe Lück\|Lückenlos]] 01:38, 9. Jul. 2007 (CEST)\|September 2006\|Formale Sprache\|Formales System\|Formales System (Logik)\|Kalkül}}
	~~----~~
	In der [[Logik]] werden bestimmte Arten '''formaler Systeme''', [[Kalkül]]e, dazu verwendet, exakte Bedingungen für das [[Schlussfolgerung\|Schlussfolgern]] anzugeben, das heißt ohne die Möglichkeit von Mehrdeutigkeiten wiederzugeben oder festzulegen, wie eine [[Logische Aussage\|Aussage]] gefolgert werden kann. Ein [[formales System]], das zu solchen logischen Zwecken verwendet wird, wird auch '''Logikkalkül''' oder '''logischer Kalkül''' genannt.		In der [[Logik]] werden bestimmte Arten '''formaler Systeme''', [[Kalkül]]e, dazu verwendet, exakte Bedingungen für das [[Schlussfolgerung\|Schlussfolgern]] anzugeben, das heißt ohne die Möglichkeit von Mehrdeutigkeiten wiederzugeben oder festzulegen, wie eine [[Logische Aussage\|Aussage]] gefolgert werden kann. Ein [[formales System]], das zu solchen logischen Zwecken verwendet wird, wird auch '''Logikkalkül''' oder '''logischer Kalkül''' genannt.

84.166.106.81: Init

2009-08-04T11:05:27Z

Init

Neue Seite

{{QS-Mathematik}}
{{Redundanztext|[[Benutzer:Gratisaktie|Gratisaktie]] 14:02, 17. Sep 2006 (CEST); [[Benutzer:Uwe Lück|Lückenlos]] 01:38, 9. Jul. 2007 (CEST)|September 2006|Formale Sprache|Formales System|Formales System (Logik)|Kalkül}}
----
In der [[Logik]] werden bestimmte Arten '''formaler Systeme''', [[Kalkül]]e, dazu verwendet, exakte Bedingungen für das [[Schlussfolgerung|Schlussfolgern]] anzugeben, das heißt ohne die Möglichkeit von Mehrdeutigkeiten wiederzugeben oder festzulegen, wie eine [[Logische Aussage|Aussage]] gefolgert werden kann. Ein [[formales System]], das zu solchen logischen Zwecken verwendet wird, wird auch '''Logikkalkül''' oder '''logischer Kalkül''' genannt.

Die strikte Formalisierung logischer [[Schlussregel]]n hatte ihren Ausgangspunkt gegen Ende des [[19. Jahrhundert]]s durch den Logiker, Mathematiker und Philosophen [[Gottlob Frege]]. Die Logik erhielt dadurch eine der mathematischen Formelsprache entsprechende Form, in der exakte, mathematisch strenge Ableitungen und Beweise möglich wurden. Freges Ansatz wurde dann durch Mathematiker wie [[David Hilbert]] und [[Bertrand Russell]] erweitert.

Es gibt unterschiedliche Arten logischer Kalküle, z. B. logische [[Hilbert-Kalkül]]e (axiomatische Kalküle) und [[Gentzentypkalkül]]e (Regelkalküle). Andere Kalkültypen, die in der formalen Logik eingesetzt werden, sind [[Baumkalkül]]e und [[Resolution (Logik)|Resolutionskalküle]] sowie seltener graphische Kalküle wie die [[Existential Graphs]].

Nur in den [[Gentzentypkalkül]]en gilt der [[Gentzenscher Hauptsatz|Gentzensche Hauptsatz]].

==Das MU-Rätsel==

Ein für die Einführung in formale Systeme beliebtes Beispiel ist das '''MU''' Rätsel aus dem Buch ''[[Gödel, Escher, Bach]]'', in dem die [[Beweisbarkeit]] eines formalen "Satzes" und der Bezug formaler Systeme zu den [[Axiomensystem]]en der Mathematik deutlich wird:

===Das formale M,I,U-System===

[[Douglas R. Hofstadter]] erfand dieses System, um die Anwendung von formalen Systemen im Bereich der Logik und Mathematik zu veranschaulichen. Es ist ein sehr einfaches System, das nur drei Symbole und vier Regeln enthält. Schon die Grundrechenarten der Arithmetik, ebenfalls ein formales System, sind wesentlich komplexer. Da das System keine Entsprechungen für reale Dinge hat, im Gegensatz z. B. zu Zahlwörtern, wird der formale Charakter besonders deutlich. Im formalen System spielt ja genau die Bedeutung der Symbole keine Rolle mehr.

Das System besteht aus den drei Symbolen '''M''', '''I''' und '''U'''. Symbolketten können durch die folgenden vier Regeln in andere Ketten verwandelt werden:

:''Regel1:'' Wenn das letzte Symbol '''I''' ist, kann '''U''' angefügt werden (aus '''MI''' wird '''MIU''')
:''Regel2:'' Aus '''M'''''x'' kann '''M'''''xx'' erzeugt werden (aus '''MIU''' wird '''MIUIU''')
:''Regel3:'' '''III''' kann durch '''U''' ersetzt werden (aus '''MUIIII''' wird '''MUIU''')
:''Regel4:'' '''UU''' kann gestrichen werden (aus '''MUUUI''' wird '''MUI''')

''x'' in ''Regel2'' steht für eine beliebige Symbolkette. ''xx'' bedeutet die Verdoppelung der Kette, diese wird also zweimal hinterander gesetzt.

Die Regeln dürfen in beliebiger Reihenfolge auf eine Symbolkette angewendet werden, auch mehrmals hintereinander.

:#'''MI'''
:#'''MII''' ''(Regel2)''
:#'''MIIII''' ''(Regel2)''
:#'''MUI''' ''(Regel3)''
:#'''MUIU''' ''(Regel1)''
:#'''MUIUUIU''' ''(Regel2)''
:#'''MUIIU''' ''(Regel4)''

===Das Rätsel===
#Vorgegeben ist die Symbolkette '''MI'''
#Gibt es eine Folge der Anwendung der Regeln, so dass die Symbolkette '''MU''' aus '''MI''' entsteht?

Die Zahl der Zeichen '''I''' (I-Wert) ist zu Beginn eins also nicht durch drei teilbar. Durch Anwendung einer der vier Regeln ändert sich daran nichts. Damit hat keine beweisbare Zeichenkette einen durch drei teilbaren I-Wert wie die Zeichenkette '''MU''' mit dem I-Wert null.

Die Suche durch Erzeugen aller möglichen Symbolketten ([[Brute-Force-Methode|Brute Force]]-Suche) wird daher nicht zum Erfolg führen.

===Axiomensysteme als formale Systeme===
[[Axiom]]e sind Sätze, die von vornherein als wahr ''vorausgesetzt'' werden. In [[Axiomensystem]]en existieren meist nur einige wenige Axiome. Die [[euklidische Geometrie]] hat z. B. nur fünf Axiome.

Im formalen System lassen sich Axiome durch Symbolfolgen darstellen. Im MU-Rätsel ist '''MI''' das einzige Axiom. Dieses ist also nach Definition ''wahr''. Mit Hilfe der Umwandlungsregeln lassen sich aus den Axiomen andere Symbolfolgen erzeugen. Der Wahrheitswert ändert sich bei Anwendung dieser Regeln nicht, daher gelten die abgeleiteten Symbolketten ebenfalls als ''wahr''.

Eine Symbolkette wird als mathematischer oder logischer ''[[Satz (Mathematik)|Satz]]'' bezeichnet. Die Axiom-Symbolketten sind daher in jedem Fall auch Sätze. Auch die durch Umwandlung erzeugten Symbolketten sind Sätze, genauso wie jede beliebige Symbolfolge.

Kennt man eine Folge der Anwendung der Regeln, die einen Satz aus den Axiom-Symbolketten erzeugt, so ist der Satz ''wahr''. Die Folge ist der ''Beweis'' dieses Satzes. Sätze, für die prinzipiell ein Beweis existiert, nennt man beweisbar. Da sich normalerweise nicht jede Symbolkette erzeugen lässt, gibt es beweisbare und nicht beweisbare Sätze.

Im formalen System ist ein Satz beweisbar, wenn es prinzipiell möglich ist, ihn durch Umwandlung aus den Axiomen zu erzeugen. Das MU-Rätsel fragt nach der [[Beweisbarkeit]] des "Satzes" '''MU'''. Hier darf man nicht Beweis und Beweisbarkeit verwechseln. Kennt man einen Beweis, so ist damit die Beweisbarkeit nachgewiesen. Es ist jedoch nicht immer nötig oder möglich, einen Beweis zu finden. Trotzdem können unter Umständen Aussagen zur Beweisbarkeit oder Nichtbeweisbarkeit gemacht werden, obwohl man den Beweis selbst nicht kennt.

<center>
{| border="1"
!style="background:#ffdead;"|
!style="background:#ffdead;"|Element
|-
| '''Symbole'''
| '''M''', '''I''' und '''U'''
|-
| '''Satz'''
| Jede beliebige Folge der Symbole '''M''' '''I''' '''U'''
|-
| '''Axiom'''
| '''MI'''
|-
| '''Schlussfolgerungs-Regeln'''
| ''Regel1'' bis ''Regel4'' (siehe oben)
|-
| '''Beweis eines Satzes'''
| Reihenfolge der Anwendung von ''Regel1'' bis ''Regel4'' auf das Axiom '''MI''', bis der zu beweisende Satz entsteht.
|-
| '''Beweisbarkeit eines Satzes'''
| Möglichkeit der Existenz eines Beweises
|-
| '''MU-Rätsel'''
| Beweisbarkeit des Satzes '''MU'''
|}
'''Das M,I,U-System als Axiomensystem'''
</center>

=== Widerspruchsfreiheit von Axiomensystemen ===
Verwendet man ein Symbol zum Ausdrücken der Verneinung (z. B. <math>\neg</math>) und definiert, dass nicht wahr gleich falsch ist, so ist ein System widerspruchsfrei, wenn nicht gleichzeitig ein Satz und seine Verneinung bewiesen werden können.

=== Vervollständigung von Axiomensystemen ===
Beweisbare Sätze sind nach Definition stets wahr. In den meisten formalen Systemen können Sätze formuliert werden, die weder beweis- noch widerlegbar sind. Widerlegung ist dabei der Beweis der Verneinung. Man kann ein formales System dann erweitern, indem man für einen solchen Satz einfach definiert, ob er wahr oder falsch ist. Im erweiterten System existiert dann ein Beweis oder eine Widerlegung, nämlich einfach die hinzugefügte Definition.

Erstaunlicherweise kann man jedoch nicht jedes System so erweitern, dass alle Sätze auch beweis- oder widerlegbar sind. In manchen Systemen bleiben stets unentscheidbare Sätze übrig. Dies hat [[Kurt Gödel]] [[1930]] mit seinem [[Gödelscher Unvollständigkeitssatz|Unvollständigkeitssatz]] zweifelsfrei nachgewiesen.

==Symbolische Logik==
Logiksysteme wie die [[Aussagenlogik]] können durch ein formales System definiert werden. Dazu könnte man normale Wörter wie ''und'', ''oder'', ''nicht'' verwenden, was die Verständlichkeit erhöhen würde. Allerdings haben solche Wörter stets Nebenbedeutungen, die den exakten Charakter der Aussagen nicht widerspiegeln. Daher werden neue Symbole eingeführt, deren Interpretation keinen Freiraum mehr bietet:

===Symbole zur Darstellung der Aussagenlogik===
Die folgende Tabelle gibt Symbole wieder, die zu einer Definition der Aussagenlogik dienen können:
{| border="1"
!style="background:#ffdead;" width="10%" align="center" | Symbol
!style="background:#ffdead;"| Beschreibung
|-
| '''A''' '''B''' '''C''' ...
| '''Aussage'''. Eine Aussage wird durch einen Großbuchstaben repräsentiert.
|-
|<math>\neg</math>
| '''nicht'''. Verneinung einer Aussage <math>\neg A</math> ist genau dann wahr, wenn '''A''' falsch ist, und umgekehrt.
|-
|<math>\wedge</math>
| '''und'''. Die Gesamtaussage <math>A \wedge B</math> ist genau dann wahr, wenn sowohl '''A''' als auch '''B''' wahr sind.
|-
|<math>\vee</math>
| '''oder'''. Die Gesamtaussage <math>A \vee B</math> ist genau dann wahr, wenn entweder '''A''' oder '''B''' oder beide wahr sind.
|-
|<math>\leftrightarrow</math>
| '''ist gleichwertig zu'''. Die Gesamtaussage <math>A \leftrightarrow B</math> ist wahr, wenn '''A''' und '''B''' beide wahr oder beide falsch sind.
|-
|<math>\rightarrow</math>
| '''aus''' '''folgt'''. Die Folgerung <math>A \rightarrow B</math> ist falsch, wenn '''A''' wahr, aber '''B''' dennoch falsch ist. In allen anderen Fällen ist <math>A \rightarrow B</math> wahr.
|-
|'''(''' ''')'''
|'''Klammern'''. Klammern dienen dazu, die Ausführung einer Operation '''vor''' einer anderen zu erzwingen, wenn Unklarheiten bestehen.
|}

===Symbolfolgen sind Sätze ===
In formalen Systemen entspricht ein Satz genau einer Folge von Symbolen, also einer Symbolkette, etwa

:'''Satz:'''
:<math>A \wedge B \leftrightarrow \neg ((\neg A) \vee (\neg B))</math>

Übersetzt heißt dies: Die Aussage "A und B" hat denselben Wahrheitswert wie die Verneinung der Aussage "nicht A oder nicht B".

Ein Satz kann wahr oder falsch sein.

===Umwandlungsregeln in einer Logik===
Symbolfolgen kann man in formalen Systemen über Regeln in andere Symbolfolgen umformen. Zur Definition der zugelassenen Regeln kann man auch ein (einfacheres) formales System verwenden:

{| border="1"
!style="background:#ffdead;" width="20%" align="center" | Symbol
!style="background:#ffdead;"| Beschreibung
|-
! '''a''' '''b''' '''c''' ...
| '''Symbolfolge'''. Ein Kleinbuchstabe kann durch eine Symbolfolge ersetzt werden. Gleiche Kleinbuchstaben in einer Folge müssen durch gleiche Symbolfolgen ersetzt werden.
|-
!<math>\Leftrightarrow</math>
| '''kann ersetzt werden durch'''. Die Symbolfolge auf der linken Seite kann durch die Folge auf der rechten Seite ersetzt werden, ohne den Wahrheitsgehalt zu ändern. Ebenso kann die rechte Folge durch die linke ersetzt werden.
|-
|<math>wahr \quad falsch</math>
|Symbole für eindeutig wahre und falsche Aussagen
|}
'''Symbole für Umwandlungsregeln (Beispiel)'''

Eine Umwandlungsregel könnte dann so aussehen:

{| border="0"
|''Schlussregel1:''
|<math>\neg\neg a \Leftrightarrow a</math>.
|}

Dies bedeutet, dass man <math>\neg\neg</math> auf der linken Seite jedes Satzes entfernen oder hinzufügen darf. Umgangssprachlich entspricht dies der doppelten Verneinung:

''Schlussregel1: Die Verneinung der Verneinung einer Aussage ist die Aussage selbst''

Weitere Umwandlungsregeln sind z. B.

{| border="0"
|''Schlussregel2:''
|<math>\neg falsch \Leftrightarrow wahr</math>
|-
|''Schlussregel3:''
|<math>wahr \vee a \Leftrightarrow wahr</math>
|-
|''Schlussregel4:''
|<math>a \vee \neg a \Leftrightarrow wahr</math>
|-
|''Schlussregel5:''
|<math>a \rightarrow b \Leftrightarrow (\neg a) \vee b</math>
|-
|''Schlussregel6:''
|<math>\neg a \vee \neg b \Leftrightarrow \neg (a \wedge b)</math>
|-
|''Schlussregel7:''
|<math>\neg a \wedge \neg b \Leftrightarrow \neg (a \vee b)</math>
|-
|<math>\cdots</math>
|<math>\cdots</math>
|}
Die Punkte deuten an, dass noch viele weitere Umwandlungsregeln definiert werden können. Dies sind die ''Schlussfolgerungs-Regeln'' für die formale Logik. Sie können rein formal ohne Bezug zur Bedeutung der Symbole angewendet werden. Damit verhalten sich die Regeln wie ''Rechenregeln''.

Trotzdem wurden die Regeln "sinnvoll" gewählt. ''Schlussregel3'' bedeutet, dass eine wahre Aussage ''oder'' eine beliebige Aussage als Gesamtaussage immer wahr ist. Dagegen bedeutet die kompliziertere ''Schlussregel5'' (Folgerung) übersetzt etwa:

''Schlussregel5: aus a folgt b kann ersetzt werden durch die Aussage "Verneinung von Aussage a oder Aussage b"''.

Die Folgerung <math>a \rightarrow b</math> ist genau dann falsch, wenn a wahr, aber b dennoch falsch ist. Umgekehrt ist sie also wahr, wenn a falsch oder wenn b wahr ist. Dies entspricht formal <math>(\neg a) \vee b</math> (''lies:'' nicht a oder b).

===Beweise===
Ein zu beweisender Sachverhalt besteht oft aus einer Behauptung und einer Schlussfolgerung. Im formalen System wird eine Behauptung ''b'' als Symbolfolge dargestellt, ebenso die Schlussfolgerung ''s''. Der [[Beweis]] wird geführt, indem der Satz "aus der Behauptung folgt die Schlussfolgerung" in <math>wahr</math> umgewandelt wird:

:'''Formaler Beweis''':
:<math>b \rightarrow s</math> (aus der Behauptung ''b'' folgt die Schlussfolgerung ''s'') kann mit Hilfe der Umwandlungsregeln überführt werden in <math>wahr</math>.

'''Beweis des Satzes: Aus Falschem folgt Beliebiges'''

Der klassische Satz ''ex falso quod libet'' (aus Falschem folgt Beliebiges) kann formal dargestellt und bewiesen werden. In unserem formalen System lautet er:

:<math>\mbox{falsch} \rightarrow b</math>

:''Die Folgerung aus einer falschen Aussage ist immer wahr''

'''Beweis:'''

Zum Beweis wenden wir die Umformungsregel für die Folgerung an:

:<math>\neg \mbox{falsch} \vee b</math> ''(Schlussregel5)''

Nicht falsch ist aber wahr:

:<math>\mbox{wahr} \vee b</math> (''Schlussregel2'')

Schließlich ist eine wahre Aussage ''oder'' Beliebiges immer wahr.

:<math>\mbox{wahr}</math> (''Schlussregel3'')

Der Satz ist damit ''formal'' bewiesen. Der Beweis könnte durch ein Computerprogramm erfolgen, das nur die Symbole kennt und die Schlussregeln anwendet.

==Formale Prädikatenlogik==
Ein klassisches Beispiel für ein Axiomensystem in der Mathematik ist die [[Gruppentheorie]]. Eine Gruppe lässt sich über einer Menge und einer zugehörigen (Rechen-)Operation bilden. Mathematische Sätze lassen sich allein aus den vier Axiomen der Gruppe gewinnen. Die Sätze gelten dann für alle Mengen mit zugehöriger Operation, deren Eigenschaften sich auf die Gruppenaxiome abbilden lassen.

Symbole sind die Elemente der Menge und das Operatorsymbol. Mit Hilfe der [[Prädikatenlogik]] lassen sich Axiome und Sätze formal darstellen und beweisen. Die Prädikatenlogik erweitert die [[Aussagenlogik]] um

:''Prädikatenlogik-Symbol1'': <math>\forall a :</math> ''für alle a gilt:''
:''Prädikatenlogik-Symbol2'': <math>\exists b :</math> ''es existiert (mindestens ein) b, so dass''

Daneben werden die Symbole der Aussagenlogik verwendet:

{| border="1"
|<math>\neg</math>
| '''nicht'''. Verneinung einer Aussage <math>\neg A</math> ist genau dann wahr, wenn '''A''' falsch ist, und umgekehrt.
|-
|<math>\wedge</math>
| '''und'''. Die Gesamtaussage <math>A \wedge B</math> ist genau dann wahr, wenn sowohl '''A''' als auch '''B''' wahr sind.
|-
|<math>\vee</math>
| '''oder'''. Die Gesamtaussage <math>A \vee B</math> ist genau dann wahr, wenn entweder '''A''' oder '''B''' oder beide wahr sind.
|}

''a'', ''b'', ''c'', ... sind Platzhalter für die Elemente der vorgegebenen Menge, <math>\circ</math> das Operatorsymbol. Die Operation wird im Folgenden Multiplikation genannt, obwohl jede beliebige Rechenoperation gemeint sein kann. Dann kann man die Axiome der Gruppentheorie formal so darstellen:

{| border="1"
!style="background:#ffdead;" width="10%" align="center" | Formales Axiom
!style="background:#ffdead;"| Beschreibung
|-
| <math>\forall a : \forall b : \exists c : a \circ b = c \Leftrightarrow wahr</math>
| Für alle ''a'' und ''b'' gibt es ein ''c'', so dass ''a'' mit ''b'' multipliziert ''c'' ergibt.
|-
| <math>\forall a : \forall b : \forall c : (a \circ b) \circ c = a \circ (b \circ c) \Leftrightarrow wahr </math>
| Wird das Ergebnis der Multiplikation von ''a'' und ''b'' anschließend multipliziert mit ''c'', so erhält man dasselbe wie wenn zunächst ''b'' mit ''c'' und danach ''a'' mit dem Ergebnis multipliziert. Dies gilt für alle ''a'', ''b'', ''c''.
|-
| <math>\exists e : \forall b : e \circ b = b \wedge b \circ e = b \Leftrightarrow wahr </math>
| Es existiert ein ''e'', so dass für jedes ''b'' gilt: die Multiplikation von e mit b ergibt stets b, ebenso die Multiplikation von ''b'' mit ''e''. ''e'' heißt ''neutrales Element''.
|-
| <math>\forall a: \exists b : a \circ b = e \wedge b \circ a = e \Leftrightarrow wahr</math>
| Für jedes ''a'' gibt es ein ''b'', das mit diesem zusammen multipliziert das ''neutrale Element'' ergibt.
|}
'''Darstellung der Axiome der Gruppentheorie mit Hilfe der Prädikatenlogik'''

Aus den Umwandlungsregeln der Prädikatenlogik lassen sich aus diesen Axiomen die Sätze der Gruppentheorie rein formal ableiten. Eine solche Regel ist z. B.

:''Prädikatenlogikregel1:'' <math>\neg \exists a : B \Leftrightarrow \forall a : \neg B</math>

Hier die Übersetzung:

:''Prädikatenlogikregel1: Wenn kein Element ''a'' existiert, so dass die Aussage ''B'' erfüllt ist, so ist dies gleichbedeutend damit, dass für alle ''a'' die Aussage ''B'' nicht gilt.

Die dargestellte Prädikatenlogik heißt [[Prädikatenlogik erster Stufe]]. Sie erlaubt Aussagen der Form "Alle Objekte haben die Eigenschaft" bzw. "Mindestens ein Objekt hat die Eigenschaft ...", jedoch keine Aussagen der Form "Für die Eigenschaft gilt: ...". Dies ist Logiken höherer Stufe vorbehalten. Trotzdem erlaubt die Prädikatenlogik erster Stufe die Formalisierung der [[Mengenlehre]] und damit nahezu der gesamten Mathematik.

=== Formale Beweise in der mathematischen Logik===
Mathematische Sätze werden bewiesen, indem man sie mit Hilfe der Schlussregeln der Prädikatenlogik auf die Zeichenkette <math>wahr</math> zurückführt. Stößt man auf ein Axiom, kann man dieses sofort durch <math>wahr</math> ersetzen. Trifft man bei Umformungen auf einen früher bewiesenen Satz, entspricht er dann ebenfalls dem Symbol <math>wahr</math>.

Umgekehrt kann man stets auch <math>wahr</math> durch ein beliebiges Axiom ersetzen. Mathematische Theorien lassen sich daher sukzessive aufbauen, indem man komplizierte Sätze auf einfachere und diese auf die Axiome rückführt (Deduktion) oder durch Umformung aus Axiomen Sätze und aus diesen weitere Sätze bildet (Induktion).

==Literatur==
*[[Douglas R. Hofstadter]]: ''[[Gödel, Escher, Bach]], ein endlos geflochtenes Band''. DTV 1991 ISBN 3423300175
*[[David Hilbert|D. Hilbert]], [[Wilhelm Ackermann|W. Ackermann]]: ''Grundzüge der theoretischen Logik''. 6. Aufl. Springer 1972 ISBN 3540058435

==Weblinks==
* [http://home.arcor.de/rainer.randig/projekte/mathe-kunst-2/mu-loesung.htm Lösung des MU Rätsels]

== Siehe auch ==
*[[Formale Systeme]] (nicht nur in der Logik)
*[[Kalküle]] (mit anderen Schwerpunkten)

[[Kategorie:Logik]]
[[Kategorie:Berechenbarkeitstheorie]]

== Init-Quelle ==
Entnommen aus der:
[http://de.wikipedia.org/wiki/Formales_System_(Logik) Wikipedia]

Autoren: Avron, Jkbw, Luha, P. Birken, Birger Fricke, Hubertl, Uwe Lück, Wasserseele, Sebbot, Gereon K., GottschallCh , Allanon, 84.132.211.91 , Ephraim33, Friedemann Lindenthal, Mkleine, Pacogo7, Hubi, Bunt

Formales System (Logik) - Versionsgeschichte

Whorf am 22. August 2019 um 15:48 Uhr

Whorf am 22. August 2019 um 15:45 Uhr

Gerhard kemme: /* Init-Quelle */

Anthoney: LD fehlt

84.166.106.81 am 4. August 2009 um 11:06 Uhr

84.166.106.81: Init