Gibt es Proof-Size-Aware-Logiken?

Ich kenne Beweisbarkeitslogiken, die eine Notation haben ◻ P für " P ist beweisbar", aber mir ist keine bekannt, die "feinkörniger" ist und eine Vorstellung von der Größe des Beweisbegriffs hat (z. B. mit Prädikaten P R Ö Ö F ( X , P ) für " X ist ein Beweis dafür P " Und S ich z e ( X , N ) für " X ist ein Größenbegriff N ").

Ein solches System könnte die Aussage ausdrücken „es gibt keinen Beweisterm für ⊥ Größe kleiner als 3 ^ ^ ^ 3 ". Vielleicht hat es einen Beweis für diese Aussage, und der Beweisterm ist (viel) kleiner als 3 ^ ^ ^ 3 . Dies führt mich zu einigen Folgefragen:

  • Wäre dieses Ergebnis nützlich? Ich nehme an, die meisten Mathematiker möchten, dass ihre logischen Systeme vollständig konsistent sind , aber ich könnte mich mit "konsistent innerhalb der Grenzen von Beweisbegriffen, die ich jemals beobachten kann" zufrieden geben.
  • Gibt es ein offensichtliches Diagonalisierungs-/Gödelsches Argument, das diese Art von Ergebnis verhindert?
  • Hängt das irgendwie mit parakonsistenter Arithmetik zusammen, in dem Sinne, dass wir uns nicht um ausreichend „weit entfernte“ Widersprüche kümmern?
Vielleicht interessieren Sie sich für einige Arbeiten zum Thema Ultrafinitismus, wie z. B. Vladimir Yu. Sasonovs „Über realisierbare Zahlen“. Hier ist die Prämisse zu zeigen, dass ein System der Arithmetik plus dem Axiom, dass " 2 1000 existiert nicht" hat einen kürzesten Widerspruchsbeweis von besonders großer Größe (insbesondere zu groß, um ihn tatsächlich im bekannten physikalischen Universum aufzuschreiben).

Antworten (1)

Es ist einfach, Konzepte wie die Beweislänge in jeder ausreichend komplexen logischen Sprache durch Godelisierung auszudrücken. Sobald Sie einen Beweis als Zahl oder Zeichenfolge ausdrücken können, können Sie eine Funktion als ihre Länge definieren, sodass es nicht notwendig ist, ein neues Symbol dafür über syntaktischen Zucker hinaus hinzuzufügen.

Komplexität ist ein ziemlich verbreitetes Konzept in Logik und Informatik. Es gibt zahlreiche damit zusammenhängende Theoreme https://en.m.wikipedia.org/wiki/Proof_complexity

Im Allgemeinen ist das Begrenzen durch eine feste Konstante nicht so nützlich, da es unendlich viele wahre Dinge gibt, sodass Sie innerhalb einer festen Länge nicht alles beweisen können, was wahr ist. Ein nützlicheres Konzept ist, ob jede wahre Aussage einen polynomiell beschränkten Beweis zulässt. Die Existenz eines solchen Beweissystems ist ein offenes Problem.

Zu zeigen, ob ein bestimmter Satz eine Untergrenze für die Beweisgröße hat, ist ebenfalls ein allgemein schwieriges Problem, obwohl wir in bestimmten Fällen einige Beweise haben.

Gibt es Proof-Size-Aware-Logiken?
AntwortenHierDatenschutz-Bestimmungen1y, 0v