Deduktives Argument, bei dem jeder Schritt und jede Prämisse explizit angegeben wird?

Gibt es in der Philosophie ein Wort/einen Begriff, der ein Argument beschreibt, in dem alle Prämissen und Regeln für die Ableitung von diesen Prämissen explizit angegeben sind, so dass sogar ein Computer dies überprüfen kann? Ich weiß, dass es zum Beispiel in der Aussagenlogik möglich ist, logische Konsequenz leicht zu beweisen, indem man prüft, ob die Formel in allen Fällen wahr ist, in denen die Formeln einer Theorie Twahr sind (zB durch eine Wahrheitstabelle). Es gibt sogar eine zweite Möglichkeit, dies zu beweisen, die formal das Axiomatiksystem von Hilbert verwendet. Der erste Beweis ist informell, der zweite Beweis ist formal, aber beide sind gleichermaßen "rigoros". Gibt es ein Wort/einen Begriff, mit dem Philosophen oder Mathematiker ein Argument oder einen Beweis bezeichnen, der "maximal streng" ist (was bedeutet, dass alles explizit angegeben ist und von einem Computer überprüft werden könnte, wenn er in eine Programmiersprache umgeschrieben wird)? Gibt es auch ein Wort / einen Begriff für eine "schwächere" Form eines Arguments oder Beweises (was bedeutet, dass nicht alle Schritte der Argumentation explizit sind - selbst in Hilberts Kalkül, wenn wir nicht alle von uns verwendeten Regeln explizit angeben, würde ich Nennen wir es in diesem Sinne "schwächeren" Beweis)?

Ich habe festgestellt, dass diese Arten von Argumenten Argumentum a priori oder deduktive Argumente genannt werden. Diese Begriffe beschreiben jedoch kein Argument, bei dem jeder Schritt explizit angegeben oder auf einem Papier niedergeschrieben werden muss - daher könnte Raum für Mehrdeutigkeiten bestehen, wenn eine Person nichts über die Aussagenlogik oder ein anderes System weiß.

Die folgenden Fachgebiete haben einen Abschnitt, den sie unter dem, was als Logik gilt, unterrichten: Philosophie, Psychologie, Rhetorik (wie sie im modernen Recht oder in der Politik zu sehen ist), Mathematik und Informatik. Ich erwähne dies, weil der Begriff Logik oft ein missverstandener Begriff ist und in diesen Zusammenhängen verschiedene Dinge bedeuten könnte. Einige Terminologien werden NICHT universell verwendet. Dieselben Wörter können etwas anderes bedeuten, je nachdem, welches der aufgeführten Themen die sogenannte Logik lehrt. Deduktives Denken ist ein größerer Satz dessen, was Logik umfasst. Beim deduktiven Denken geht es um Gewissheit, nicht um die anderen Arten des Denkens.
@Logikal, die Verwendung der Terminologie durch den Fragesteller ist völlig angemessen. Bitte beenden Sie es mit dem obsessiven Beharren darauf, dass sich jeder auf dem Gebiet irrt.
Formaler Beweis oder Herleitung .
@ Paul Ross, ich habe nicht darauf bestanden, dass sich jeder in einem Feld irrt. Ich weise deutlich und oft darauf hin, dass alle Logik nicht mathematisch ist. Manche Leute haben den Eindruck, dass Logik Logik ist und alles Mathematik ist, die ich ständig korrigieren muss. Viele Bereiche der Logik sind nicht identisch, was die Mathematiker zu forcieren scheinen. Ich bin kein Mathematiker und wurde auch nicht so unterrichtet, wie ich es hier oft sehe. Philosophie & Mathematik sind nicht identisch. Logik ist ein zu vager Begriff, um ihn allein zu verwenden. Wenn sich jemand auf mathematische Logik bezieht, sollte er ausdrücken, dass es sich um mathematische Logik handelt, insbesondere nicht um Logik.
@Logikal Es ist ziemlich ironisch, dass Sie beim Versuch, andere in Fragen der Logik zu korrigieren, "alle Logik ist nicht mathematisch" schreiben, wenn Sie sagen wollen, dass Logik nicht nur Mathematik ist.
@Eliran, ich sehe, was du da gemacht hast. Leider habe ich in einer bestimmten Reihenfolge geschrieben, WEIL so viele Leute bereits DENKEN "Alle Logik ist Mathematik". Ich erwähne oft die aristotelische Logik, um zu zeigen, dass der Kontext von Begriffen unterschiedlich sein kann, und gebe Gegenbeispiele. Ich erinnere mich jedoch nicht, dass ich gesagt habe, dass jeder in einem Bereich falsch liegt, und ich habe die Leute auch nicht in Fragen der Logik korrigiert. Ich habe die Idee des deduktiven Denkens im Allgemeinen dem OP kommentiert, das anscheinend nur mathematisch denkt. Alles Denken ist nicht Mathematik, das ist mein Punkt. Nichts über Korrektur hier. Informationen, die abweichen können, werden Op zur Sensibilisierung angezeigt.

Antworten (2)

Ich bin mir nicht sicher, wie genau die Konzepte, mit denen ich vertraut bin, mit dem übereinstimmen, was Sie anstreben, aber ich bin mit der Entwicklung der Beweistheorie vertraut, und Ihre Suche nach Begriffen scheint mit einigen Ideen übereinzustimmen, die wir habe auf diesem Gebiet geforscht.

In der Beweistheorie, insbesondere in Diskussionen über Natürliche Deduktion , sprechen wir manchmal davon, dass ein Beweis oder Argument in Normalform vorliegt. Ein Normalform-Argument ist eines, das auf „die grundlegendste Weise“ geschrieben wurde, d "), dann wieder zusammengesetzt, um die gewünschten Schlussfolgerungen zu strukturieren (über "Einführungsregeln").

Nicht alle formalen Argumente oder sogar alle gültig konstruierten formalen natürlichen Deduktionsbeweise sind in Normalform. Viele formale Systeme zielen jedoch darauf ab, so etwas wie ein Normalisierungstheorem zu zeigen, mit dem Effekt, dass wir, wenn eine nicht minimale Verwendung unserer logischen Regeln aufgerufen wird, das Argument ohne Verlust der Allgemeingültigkeit umschreiben könnten, um es zu eliminieren. Einer der Hauptbefürworter dieser Art von Arbeit war Dag Prawitz, dessen Dissertation über die beweistheoretische Analyse natürlicher Deduktion dazu beitrug, einen Großteil der folgenden philosophischen Schriften über Beweise, Schlussfolgerungen und Berechnungen zu informieren.

Ein wertvolles Konzept, das Prawitz in seine Arbeit einführt, ist der Begriff eines "Argument Skeleton". (Siehe On the Idea of ​​a General Proof Theory für einen besser zugänglichen Überblick). Dies ist eine Verallgemeinerung der Baumstrukturen, die an formalen natürlichen Deduktionsargumenten oder Beweisen beteiligt sind, da wir nicht nur zulassen, dass wir von logischen Axiomen als Prämissen zu Schlussfolgerungen arbeiten (was wir als geschlossenes Argument bezeichnen), sondern auch, dass wir unbewiesene Argumente zulassen können Antezedenzien, die über die gleiche Art von logischen Schlußregeln zu Konsequenzen führen - diese "offenen Argument"-Strukturen sind auch Argumentskelette.

(Natürliche Deduktion versucht in ihren Strukturen oft ganz auf Axiome zu verzichten, sondern alles „rein Logische“ auf die Anwendung struktureller Schlussregeln zu verschieben.)

Vielleicht könnten also einige nützliche Wendungen folgende sein: Ihre "schwächeren" formalen Argumente sind offene Argumente und ihre "Beweise" sind Argumentskelette, da sie auf eine Beweisstruktur hinweisen, die möglicherweise weiterentwickelt werden könnte. Ihre "stärkeren" Argumente sind geschlossene Argumente, da ihre Skelette keine außerlogischen Annahmen baumeln lassen, und die syntaktisch minimalste Version eines solchen Arguments (idealerweise für die maschinelle Verarbeitung geeignet) wäre seine Normalform.

Es gibt alternative Interpretationen dieser Art von Arbeit in anderen Formen der Beweistheorie. Wo Prawitz Argument Skeletons verwendet, um sein natürliches Deduktionssystem zu unterstützen, erlaubt uns die häufigere Sequent Calculus- Technologie, die von Gerhard Gentzen aus Hilberts System entwickelt wurde, Transformationsregeln für Schlussfolgerungen zu erfassen, wodurch die Unterscheidung zwischen offenen und geschlossenen Argumenten zusammenbricht. Das Verständnis dieser Unterscheidung kann jedoch dabei helfen, ein Verständnis dafür zu bekommen, was der Folgenkalkül anders macht und wie wir die Prinzipien der Konsistenz und der stichhaltigen Argumenttransformationen bei der mechanischen Manipulation von Beweisketten anwenden können.

Mehrere Teile davon sind ausgezeichnet und sehr relevant, wie der Verweis auf Prawitz' Argumentationsskelette; Aber ich denke, der Vorschlag einer „normalen Form“ als Antwort auf die Frage von OP ist wirklich falsch. In normaler Form zu sein, ist eine viel stärkere Eigenschaft als als vollständig formales Argument angegeben zu werden, wie das OP beschreibt - Beweise, die für Computerverifizierungssysteme wie Mizar und Coq geschrieben wurden, sind fast nie in normaler Form (selbst wenn sie vom Typprüfer vollständig ausgearbeitet wurden) und es wäre nicht durchführbar, dies zu verlangen, da die Normalisierung normalerweise zu einer massiven Größenvergrößerung führt.
Danke für deinen Kommentar, Peter – es ist ein sehr starker Grad an Formalisierung, und ich frage mich, ob es sinnvoller ist, was der Fragesteller mit „maximal streng“ meint, wenn etwas weniger Ausgerolltes als die normale Form ausreichen würde um ihre Bedürfnisse zu erfüllen. Vielleicht hilft es, diese Terminologie für die Normalform beizubehalten, um zu erklären, dass das OP auf "etwas weniger als maximal streng" abzielt?

Siehe diesen Beitrag über das Formspektrum einer mathematischen Argumentation . Was Sie als "jeder Schritt und jede Prämisse sind explizit angegeben" beschrieben haben, würde als "absolut formal" eingestuft (und "formaler Beweis" ohne jegliche Qualifikation bedeutet dies häufig). Die meisten mathematischen Argumente werden nicht als absolut formale Beweise ausgedrückt, sondern fallen eher unter "ziemlich formal". Sie haben nach einem Begriff für Beweise in einem deduktiven System gefragt, die die verwendeten Regeln nicht explizit angeben, aber es gibt keinen solchen Begriff, da formale Systeme typischerweise so konzipiert sind, dass mechanisch überprüft werden kann, ob die Regeln befolgt werden oder nicht, und daher dort Es ist nicht erforderlich, festzulegen, welche Regel bei jedem Schritt verwendet wird, außer um die Effizienz des Verifizierungsprozesses zu verbessern.

Sie scheinen jedoch ein Missverständnis über die Art des Beweises einer Aussagentautologie über Wahrheitstabellen zu haben. Während es vernünftig ist, es in dem Sinne als informell zu betrachten, dass Sie eine Tabelle zeichnen und sagen: „Sehen Sie, das sind alle Fälle und die Aussage ist in jedem Fall wahr“, kann es tatsächlich nicht weniger formell ausgedrückt werden als ein Hilbert-Stil oder Fitch -Stil oder sequentiell-Stilnachweisen. Alles, was Sie tun müssen, ist, die Tabelle Zeile für Zeile in einer systematischen Reihenfolge (z. B. lexikografische Reihenfolge) auszuschreiben; für 3 Variablen A,B,C würden Sie die Zeilen 000,001,010,011,100,101,110,111 haben, die die Wahrheitswerte von A,B,C bezeichnen ) und den Wahrheitswert der Aussage für jede Zeile (der mechanisch berechnet werden kann). Dies wird manchmal als semantischer Beweis bezeichnet, da er in jeder Situation (Wahrheitszuweisung von Variablen) auf den Wahrheitswert der Aussage (gemäß der Semantik der Aussagenlogik) überprüft. Im Gegensatz dazu ist ein Beweis in einem deduktiven System ein syntaktischer Beweis, weil es „nur“ eine Frage des Symboldrückens ohne Rücksicht auf die „Bedeutung“ ist. Trotzdem können semantische Beweise genauso formal sein wie syntaktische Beweise, da Sie immer noch einen mechanischen Prozess zur Überprüfung eines syntaktischen Beweises benötigen,

Aber wie immer lohnt es sich zu betonen, dass wir zwar semantische Beweise für die Aussagenlogik haben können, es aber unmöglich ist, semantische Beweise für die vollständige Logik erster Ordnung zu haben (weil die auf PA angewendeten Unvollständigkeitstheoreme zeigen, dass es kein Programm geben kann, das dies kann in endlich vielen Schritten entscheiden, ob ein Eingabesatz der Form "X ⇒ Y" in der Sprache von PA eine Tautologie ist oder nicht, wobei "X" die Konjunktion der Axiome von PA− ist). Syntaktische Beweise bleiben also die einzige vollwertige Beweismethode für die Logik erster Ordnung.

Deduktives Argument, bei dem jeder Schritt und jede Prämisse explizit angegeben wird?
AntwortenHierDatenschutz-Bestimmungen1y, 0v