Formallogikkorrektheit
Formallogik–Korrektheit 'Korrektheit in der formalen Logik (Formallogik)'
Um eine noch genauere und allgemeinere Charakterisierung der Korrektheit einer Schlussfolgerung bemüht sich die formale Logik. Wegen der größeren Komplexität und der Mehrdeutigkeit natürlicher Sprachen werden natürlichsprachliche Aussagen in Aussagen einer exakt definierten formalen Sprache übersetzt. Auf diesen formalen Objekten wird dann ein Ableitbarkeitsbegriff definiert, der meist durch das Zeichen ⊢ symbolisiert ist. Die Motivation dabei ist oft die, dass genau dann zwischen den formalen Objekten eine Ableitbarkeitsbeziehung besteht, wenn die natürlichsprachlichen Gebilde, deren Übersetzungen sie darstellen, auseinander folgen.
Spätestens im Stadium der Formalisierung lassen sich die philosophischen und intuitiven Unterschiede im Verständnis von „Folgerung“ – und damit hinsichtlich dessen, welche Argumente gültig sind – nicht mehr überdecken. Entsprechend gibt es unterschiedliche, zueinander nicht äquivalente Ableitbarkeitsbegriffe, die die unterschiedlichen Spielarten des intuitiven und wissenschaftlichen Schlussbegriffs wiedergeben. Am häufigsten verwendet werden der klassische und der intuitionistische Ableitbarkeitsbegriff, deren Unterscheidung sowohl auf ein sehr unterschiedliches Verständnis der logischen Ausdrücke (z. B. der Junktoren „und“, „oder“ und „nicht“) als auch auf einen unterschiedlichen Wahrheitsbegriff zurückgeht.
Die Definition des Ableitbarkeitsbegriffs geschieht durch Schlussregeln und gegebenenfalls durch Axiome. Ein formales System, das Schlussregeln und Axiome festlegt, heißt Kalkül. Siehe hierzu auch den allgemeinen Artikel Beweis (Logik). Eine einführende Darstellung eines konkreten logischen Systems mit einer detaillierten Ausformulierung des Ableitbarkeitsbegriffs findet sich im Artikel Aussagenlogik. Zur automatischen Inferenz steht in der Informatik die Inferenzmaschine zur Verfügung.