Ich bin mir nicht sicher, ob ich Ihre Fragen vollständig verstehe, aber ich werde versuchen, eine Antwort zu geben, die durch die jüngsten formalen Ergebnisse der Beweistheorie und meinen Standpunkt eines Informatikers voreingenommen ist. Es wird also keine sehr "philosophische" Antwort in dem Sinne sein, dass ich mich nicht vollständig auf philosophische Referenzen verlasse.

Beachten Sie, dass die Art des Beweises überhaupt nicht klar ist und wir immer noch danach suchen. Darauf haben wir tatsächlich mehrere Antworten.

Glauben Sie, dass wir als Menschen im Allgemeinen bestimmte Beweisstrategien anwenden, um Dinge zu beweisen?

Zu einer Formalisierung des Beweises . Mathematiker führten schon lange Beweise, bevor die formale Logik auftauchte. Um das 19. und 20. Jahrhundert herum wurden viele Beweissysteme nach unserer Vorstellung von Beweisen eingeführt.

• Frege ging mit seiner Begriffsschrift von der von Aristoteles und den Stoikern gelieferten Konzeption der Logik aus.

• Hilbert hat ein System entwickelt, in dem der Modus Ponens die einzige Regel ist, und wir versuchen, Beweise aus bereits etablierten Axiomen abzuleiten

• Noch interessanter: Gentzen hat zuerst ein System entwickelt, das auf der Verwendung von Logik in mathematischen Methoden basiert und als Natürliche Deduktion bezeichnet wird (weil es die empirische Verwendung von Logik durch Menschen reproduziert). Beim Beweisen führen wir Konnektoren ein und eliminieren sie später :

  • von A und B können wir A /\ B reduzieren (Definition von "und")
  • aus A /\ B können wir entweder A oder B ableiten (Verwendung von "und")

Mit einem solchen System können wir den Beweisraum innerhalb der Einführung und Eliminierung einer endlichen Menge von Konnektoren einschränken.

Also ja, wir verwenden bestimmte Strategien, um Dinge zu beweisen . Andere Fragen:

• Woher kommen diese Regeln?
• Ist Logik mehr als das?
• Warum verwenden wir diese Regeln und keine anderen?

Die ersten beiden Fragen können beantwortet werden, die letzte kann eine Frage der Psychologie oder Biologie sein (es gibt tatsächlich einige Literatur darüber).

Wenn das oben Gesagte zutrifft, bedeutet dies, dass es bestimmte Strategien sind, denen wir folgen müssen, wo kommt Ihrer Meinung nach die Kreativität ins Spiel?

Eine feine Analyse der Logik . Als er auf Gentzen zurückkam, stellte er fest, dass Abzüge aus dem System der natürlichen Deduktion reduziert/vereinfacht werden könnten: Wenn wir einen Konnektor einführen und ihn gleich danach eliminieren, machen wir eine "Abweichung", die nicht notwendig ist.

Er konnte das nicht beweisen, also entwickelte er ein anderes System namens Sequent Calculus . Dieses System basierte nicht auf der Untersuchung der Verwendung von Beweisen, sondern auf einer Analyse der natürlichen Deduktion und Logik. Der Sequent Calculus analysiert die Tiefenstruktur der Logik und ihre Symmetrien gemäß einer Dualitätshypothese / Schlussfolgerung und nicht einer Einführung / Eliminierung oder Definition / Verwendung.

Das letzte System war angemessen genug, um das Konzept der "Abweichung" explizit zu machen: Es heißt Schnittregel und hier kommt Kreativität ins Spiel (aber das wusste er nicht).

Kreativität und die Verwendung von Lemmata . Die Schnittregel wird wie folgt ausgedrückt: Aus Γ ⊢ Δ,A (links = Konjunktion der Hypothese, rechts = Disjunktion der Schlussfolgerungen, die griechischen Buchstaben sind mehrere Formelsätze) und Σ,A ⊢ Π können wir Γ,Σ ⊢ Π ableiten, Δ. Wenn wir die Regel in umgekehrter Richtung lesen, bedeutet dies, dass Sie, wenn wir Γ,Σ ⊢ Π,Δ beweisen wollen (was Sie wollen), ein beliebiges A einführen können, vorausgesetzt, dass A mit einer Hypothese Γ bewiesen werden kann, die Sie haben, und das Wenn Sie A und einige andere Hypothesen Σ geben, können Sie beweisen, was Sie wollten.

Die Schnittregel ist eigentlich die Verwendung von Lemma in der Mathematik. Wenn Sie etwas beweisen wollen, beweisen Sie ein Lemma A und verwenden Sie es.

Nach seinem Tor bewies Gentzen, dass die Verwendung der Cut-Regel (die Abweichungen darstellt, die jetzt als "Cuts" bezeichnet werden) entfernt werden konnte. Das bedeutet, dass wir Dinge ohne Lemmata und nur mit reiner Anwendung logischer Regeln beweisen können. Nur ein Problem: Das Reduzieren eines Beweises durch Kürzungen kann zu einer Explosion der Komplexität mit Beweisen von enormer Größe (manchmal von absurder Größe) führen.

Ein konkretes Beispiel für Kürzungen . Angenommen, Sie wollen beweisen, dass 5+3 dasselbe ist wie 3+5. Sie können entweder "reine Regelanwendung" verwenden, die auf beiden Seiten zum Ergebnis 8 führt, ODER Kreativität / ein Lemma / die Schnittregel verwenden: Wir beweisen, dass die Addition kommutativ ist (für alle n und m, n + m = m + n ) und dass die Kommutativität der Addition beweist, was wir wollen.

Wir machen eine Abweichung, die nicht notwendig, aber kreativer, nützlicher, interessanter ist ...

Wie unterscheidet sich das Beweisen von Dingen in der Mathematik von der realen Welt? [...] Mit anderen Worten, um q im wirklichen Leben zu beweisen, können wir leicht ap finden, was zu q führt, und es ist nicht sehr schwierig. Was macht dies jedoch in der Mathematik zu einer Herausforderung?

Hm ... Ich bin mir nicht sicher, ob ich das verstehe. In Ihrem Beispiel kann der Grund sein, dass der Suchraum endlich ist , während er in der Mathematik unendlich sein kann . Aber es ist keine allgemeine Sache, wenn Sie in der "realen Welt" zum Beispiel Ergebnisse über Physik einbeziehen.

Epilog: Zur Tiefenstruktur der Logik

Der Ursprung der Regeln . Im 20. Jahrhundert entdeckten Logiker und Informatiker etwas Erstaunliches, den Curry-Howard-Isomorphismus . Es sagt, dass :

• Der Beweis einiger logischer Systeme entspricht tatsächlich genau den Computerprogrammen einiger Systeme (Die Intuitionistische Natürliche Deduktion entspricht dem Lambda-Kalkül).

• Für die entsprechenden Systeme kann die durch einen Beweis bewiesene Formel als Typ des entsprechenden Programms angesehen werden.

• Die Eliminierung von Kürzungen kann als Ausführung von Programmen angesehen werden

Es gibt nicht viel Literatur darüber, aber ich denke, dass Korrespondenz den logischen Regeln einen "natürlichen" Status verleiht, da sie aus dem natürlichen Konzept der "Berechnung" stammen.

Dieses Paradigma interpretiert logische Regeln als Programmkonstruktionen: logische Implikation wird als Funktion in einer Programmiersprache gesehen, Konjunktion als Paar, Disjunktion als Summentyp /algebraischer Typ ...

Eine noch feinere Analyse der Logik . Kürzlich versuchten Logiker wie Jean-Yves Girard, noch tiefer in die Analyse der Logik einzudringen: In den meisten Beweissystemen haben wir eine Regel zum „Duplizieren“ und „Löschen von Formeln“. Wenn wir zum Beispiel A ⊢ A geben, gilt immer noch: A,A ⊢ A. Und wenn wir A,A ⊢ A geben, haben wir A ⊢ A, was immer noch gilt. Was wäre, wenn wir diese Regeln aufheben und Beweise wie chemische Reaktionen sehen, bei denen wir Formeln konsumieren? Es führte zur linearen Logik , die schließlich die Unendlichkeit/Statizität der Wahrheit mit den neuen Operatoren !A und ?A wieder einführte.

Die lineare Logik führte schließlich zu einem neuen dynamischen und interaktiven Status für Beweise, der bis heute erforscht wird. Dieser neue Ansatz stützt sich vollständig auf das Konzept der Schnitteliminierung, das jetzt als Interaktion angesehen wird , eine zentrale Idee der aktuellen Forschung in der Beweistheorie.

Auf dem Weg zu einer vollständig internen Logik . Wie Sie sagten, kann das Problem der Axiome und des Theorems problematisch sein. In der Logik verlassen wir uns zu sehr auf eine Außenwelt. Logiker versuchten, eine interne Logik namens Ludics zu entwickeln, die ebenfalls derzeit untersucht wird. Ludics haben ein Konzept von "partiellen" Beweisen, bei denen zwei partielle Beweise zusammenwirken, wobei einer versucht, eine Formel A zu beweisen, und der andere die Dual/Negation und nur einer gewinnt.

Die Verweigerung . Neuere Forschungen in der Beweistheorie interagieren stark mit der Informatik und neigen dazu, der Logik eine bevorzugte Behandlung zu geben, wie sie durch Berechnungen erklärt wird.

Eine ziemlich umstrittene Frage ist: Was ist mit den logischen Systemen, bei denen das Theorem der Schnittelimination (Schnitte können eliminiert werden) nicht gilt und für die es kein entsprechendes System in der Informatik gibt? Sind sie wirklich „gültig“?

Einige Systeme in der "philosophischen Logik" mögen den Satz der Schnittelimination nicht, aber es ist eine andere Debatte.

Zusammenfassung

• Ein Beweis kann als Programm eines Programmiersystems in der Informatik angesehen werden

• Informatik und die Schnittregel geben wirklich interessante Richtungen

• Die Schnittregel und das Schnittausschlussverfahren können der Kern von Logic sein

• Ohne die Verwendung der Logik durch den Menschen zu berücksichtigen, können wir die formale Struktur der Logik noch tiefer und feiner studieren

• Formale Ergebnisse in Informatik, Beweistheorie und Mathematik sollten mehr mit Philosophen interagieren: philosophische Ideen sind den meisten ersteren unbekannt, Berechnungen und technische Details letzteren.

Dies ist eine sehr weit gefasste Frage; aber vielleicht können wir es etwas eingrenzen, indem wir uns auf den Kontrast konzentrieren, den Sie zwischen rechtlichen und mathematischen Beweisen vorschlagen. Zumindest kann Ihnen dies einige Ideen geben, wo Sie mit Ihrer Suche beginnen könnten. Also sagst du:

„Wenn wir im wirklichen Leben beweisen wollen, dass jemand unschuldig ist, finden wir einfach eine Gruppe vertrauenswürdiger Zeugen, um zu bezeugen, dass jemand unschuldig ist. Mit anderen Worten, um q im wirklichen Leben zu beweisen, können wir leicht p finden, was zu q führt, und es ist nicht sehr schwierig. Was macht dies jedoch zu einer Herausforderung in der Mathematik?“

Drei kurze Vorbehalte. (i) Ich werde weiterhin „Beweis“ sowohl für die mathematische als auch für die juristische Sache verwenden, obwohl es wahrscheinlich am besten wäre, zwei verschiedene Wörter zu verwenden. (ii) Achten Sie darauf, nicht ins Psychologische abzudriften, wenn Sie fragen, warum wir juristische Beweise leichter finden und ob wir kognitive Strategien haben, um an Beweise heranzugehen. (iii) Ich bin mir nicht sicher, warum Sie sagen, dass rechtliche Beweise einfacher sind als mathematische: Es gibt einfache Beweise in der Mathematik und harte Beweise im Gesetz.

Wenn Sie nun auf die Tatsache hinweisen, dass rechtliche Beweise, aber keine mathematischen Beweise, auf empirischen Beweisen beruhen, könnten Sie sich mit der Unterscheidung zwischen A priori und A posteriori befassen . Freges „Grundlagen der Arithmetik“ kann ein guter Ausgangspunkt sein. (Beachten Sie, dass einige argumentieren, dass mathematisches Wissen aus empirischen Beweisen abgeleitet werden kann: Beispielsweise wird die Goldbach-Vermutung wohl von den Computern gestützt, die sie überprüfen. Alexander Paseau hat darüber geschrieben.)

Wenn Sie sich insbesondere über den epistemischen Status von Zeugenaussagen wundern, können Sie in der Literatur zu Knowledge by Testimony nachsehen . (Beachten Sie, dass das mathematische Wissen vieler Menschen wahrscheinlich aus Zeugnissen stammt: Ich weiß, dass 2 + 2 = 4, weil meine Mutter / meine Lehrer es mir gesagt haben, nicht weil ich es bewiesen habe.)

Da Sie von p sprechen , das zu q führt, sollten Sie sich auch die Literatur zu deduktiven, induktiven und abduktiven Beweisen/Reasoning ansehen . Mathematische Beweise sind natürlich deduktiv; aber es ist nicht offensichtlich, dass rechtliche Beweise sind. (Wenn Sie dies noch nicht getan haben, kann es auch hilfreich sein, sich einige mathematische Beweise „in Aktion“ anzusehen. Beispielsweise ist Endertons „A Mathematical Introduction to Logic“ formal streng und sehr gut lesbar. Oder schauen Sie sich Robbins und Courants „ Was ist Mathematik". Für eine eher philosophische Perspektive siehe zB Giaquintos "Die Suche nach Gewissheit".)

Da Sie zwischen der mathematischen Welt und der realen Welt unterscheiden, werfen Sie einen Blick auf die Debatte zwischen Realismus und Nominalismus . Eine Herausforderung, der sich der Realist gegenübersieht, ist die Frage, wie wir etwas über Mathematik wissen können, wenn Zahlen abstrakte Objekte sind.

Schließlich kann eine andere Möglichkeit, sich der Natur der „mathematischen Welt“ zu nähern, darin bestehen, nach dem Status der Axiome zu fragen – zB: Wie kennen wir „grundlegende Wahrheiten“? Siehe z. B. Maddys „Defending the Axioms“ und Mary Lengs Rezension darüber.

Dies sind nur einige Hinweise, die Ihre Frage nicht direkt beantworten. Wie ich bereits sagte, ist es viel wahrscheinlicher, dass Sie eine zufriedenstellende Antwort finden, wenn Sie die Frage ein wenig eingrenzen können.

(Ich hoffe, eine einigermaßen kurze Antwort zu geben, indem ich eine bestimmte Perspektive wähle, anstatt zu versuchen, einen Überblick zu geben.)

Der Intuitionismus wurde vorgeschlagen, um die Probleme anzugehen, die Menschen mit dem mathematischen Platonismus hatten , als sie versuchten, die verbale Logik zu formalisieren. Sie stellten fest, dass Dinge wie Russels Paradoxon schwerer zu umgehen waren, als man annehmen würde. Und das versetzte der gewöhnlichen, platonischen Sichtweise auf den Prozess der Mathematik einen tiefen Schlag.

Intuitionisten wiesen darauf hin, dass der Platonismus eher ein Ergebnis als die wahre Ursache dessen sein könnte, was im mathematischen Prozess vor sich geht. Dass es in der Mathematik nicht um absolut stabile Ideen geht, sondern dass sie diese Ideen zum Nutzen der anderen Wissenschaften sucht.

Eine Interpretation des Neo-Intuitionismus ist, dass Mathematik eine echte experimentelle Wissenschaft ist. Es ist die reinste Form der Psychologie. Es bestimmt experimentell, welche intuitiven Konzepte Menschen nicht einfach loslassen können, sobald sie sie haben, und wie diese Konzepte gut oder schlecht kombiniert werden können. Die Mathematik untersucht also nicht einen festen Bereich der Natur außerhalb von uns selbst, sie untersucht menschliches Denken und kreative Prozesse.

1. Dies setzt "Ja" zu Ihrer Frage 1 voraus. Aber es sagt nicht, was sie sind. Sie scheinen zu existieren, weil wir sie finden. Und wir gehen davon aus, dass es noch mehr davon gibt, weil wir sie immer wieder finden.

Sie tut dies auf die gleiche Weise wie die Chemie, indem sie Produkte nimmt, von denen sie bereits ihre Fähigkeit zur zuverlässigen Herstellung nachgewiesen hat, und sie zusammen in einer künstlichen Umgebung verwendet.

Der Beweis ist also nichts Bestimmtes, das festgestellt und festgestellt werden kann. Es basiert darauf, welche stabilen Intuitionen herangezogen werden können, die nicht leicht zu unterminieren sind, und wie sie nach Mustern kombiniert werden können, die wir nur schwer zurückweisen können.

(Der Nebeneffekt dieser Ansicht, für die der Intuitionismus am bekanntesten ist, ist, dass wir vorsichtig sein sollten, was die Reichweite der „Bewiesenheit“ angeht, und nicht davon ausgehen sollten, dass alle Dinge, die wir beweisen, vollständig miteinander übereinstimmen. Wir finden Widersprüche schwierig psychologisch, also sollten wir sie vermeiden. Aber wir haben keinen Grund zu glauben, dass die menschliche Intuition in sich konsistent ist.)

2. Das gibt uns durch direkte Beobachtung eine klare Antwort auf Ihre zweite Frage: Kreativität gehört offensichtlich zu diesen Prozessen, und sie könnten ohne sie nicht funktionieren. Sogar die Konstruktion von Algorithmen und formalen Systemen selbst ist eine kreative Aktivität, die vom Gefühl der Klarheit und unserem gemeinsamen menschlichen Geschmack für Eleganz in der Logik angetrieben wird.

Aus dieser Sicht sind mathematische Ergebnisse relevant, aber was wirklich untersucht und weiterentwickelt wird, sind die Prozesse der Kombination und Ableitung.

Formale Systeme und frühere Ergebnisse bieten Möglichkeiten, um zu überprüfen, ob wir übereinstimmen, aber sie lösen keine Probleme für uns. Soweit die Probleme bereits mechanisch gelöst werden, sind dies Werkzeuge der Ingenieurskunst und nicht mehr Gegenstand der eigentlichen Mathematik.

3. Das ist der Unterschied zwischen Mathematik und anderen Beweisformen. Es konzentriert sich darauf, reine Intuitionen und Modelle, die von Situationen abstrahiert wurden, zu rein mechanischen Formen zusammenzusetzen, unvermischt mit anderen Daten. Es zielt nicht darauf ab, die vorliegenden Probleme zu lösen, sondern Methoden zur Lösung von Problemen im Allgemeinen bereitzustellen, die sich für eine Vielzahl menschlicher Benutzer automatisch als vertrauenswürdig anfühlen.

Ich werde nur versuchen, einen kleinen Teil Ihrer Frage zu beantworten. Sie fragen grob: "Gibt es in der Mathematik bestimmte Strategien, mit denen wir Dinge beweisen?" Nun, um Theoreme zu beweisen, gibt es sicherlich einige Strategien, die Mathematiker immer wieder anwenden. Ich habe unten ein paar aufgelistet.

• Reductio ad Absurdum: Um zu beweisen, dass eine bestimmte Aussage wahr ist, nehmen wir an, dass die Umkehrung wahr ist und versuchen, einen Widerspruch zu finden. Wenn dies eintritt, können wir sagen, dass die ursprüngliche Aussage wahr ist. Diese Technik wird oft als Beweis durch Widerspruch bezeichnet.

• Induktion: Wenn wir eine Aussage P(n) für jedes Element n der natürlichen Zahlen beweisen wollen, verwenden wir oft Induktion. Dies geschieht, indem bewiesen wird, dass die Aussage für eine bestimmte natürliche Zahl n_0 gilt, und dann gezeigt wird, dass, wenn die Aussage für n gilt, sie auch für n+1 gelten muss. Das Lehrbuchbeispiel dafür zeigt, dass n^2 <= 2^n für n >= 5.

Es gibt viele andere Werkzeuge, um Beweise zu finden, aber sie neigen dazu, spezialisierter zu sein, abhängig von dem Zweig der Mathematik, in dem wir versuchen, einen Beweis zu finden. Beispielsweise können wir in der reellen Analysis versuchen zu zeigen, dass eine Eigenschaft P(x) für jedes x auf dem reellen Zahlenstrahl gilt. Um dies zu tun, können wir stattdessen zeigen, dass die Menge von Werten x, für die P(x) gilt, {x : P(x)}, sowohl offen als auch abgeschlossen ist . Dann können wir aus einem anderen Satz der Topologie schließen, dass P(x) für jede reelle Zahl gilt.

Ihre nächste Frage lautet: Wenn es all diese Techniken zum Erstellen von Proofs gibt, wo kommt dann die Kreativität ins Spiel? Nun, Kreativität wird eingesetzt, um alle Teile sinnvoll zusammenzufügen. Darüber hinaus wird es verwendet, wenn alle Techniken einfach nicht ausreichen, um einen Beweis zu vervollständigen, was bemerkenswert oft vorkommt. Zu diesem Zeitpunkt werden neue Techniken erfunden, die sehr verbreitet oder nur auf wenige Sonderfälle beschränkt sein können.

Unterscheidet sich diese Art der Vorstellung schließlich von der Verwendung eines Computers, um einfach alle möglichen Wege in einem Beweis auszuprobieren, um zu sehen, ob wir finden können, was wir wollen? Nun, man könnte vielleicht sagen, dass wir immer wieder dieselben Techniken anwenden und dass dies in einen Computer einprogrammiert werden könnte. Dies würde jedoch wahrscheinlich enorme Mengen an Rechenzeit in Anspruch nehmen, länger als die Lebensdauer des Universums. Der Unterschied besteht darin, dass wir bei der Erstellung unserer rigorosen Beweise oft eine vage Vorstellung davon haben, wie wir vorgehen wollen, und die Strenge kommt erst danach. Die Kreativität besteht darin, eine Idee zu entwickeln, wie wir in einem Beweis vorankommen wollen: die Intuition dahinter, warum etwas wahr ist. Dies erfordert Vorstellungskraft und Einsicht.