logik.txt

=== Cantor

* Sei phi : A --> P(A) eine Abbildung. Dann kann man explizit
  ein Element der Wertemenge angeben, das nicht getroffen wird, nämlich

      { x \in A | x \not\in phi(x) }.

  Also gibt es keine surjektive Abbildung A --> P(A).

* Auch kann man zeigen, dass es keine injektive Abbildung phi : P(A) --> A
  geben kann: Definiere

      U := { x \in A | \forall V \subseteq A: x \in V ==> x != phi(V) }
      x0 := phi(U).

  Dann folgt x0 \not\in U:

      Sei x0 in U. Speziell für V := U folgt dann, da x0 in U, dass x0 !=
      phi(U) ist. Das ist falsch.

  Andererseits kann man (unter Benutzung der Injektivität) zeigen, dass für
  alle V \subseteq A die Implikation

      x0 \in V ==> x0 != phi(V)

  gilt:

      Sei x0 in V. Angenommen x0 = phi(V). Dann folgt, da phi injektiv ist,
      dass U = V. Also liegt x0 in U. Das ist ein Widerspruch. Also x0 !=
      phi(V).

  Also gilt doch x0 \in U. Widerspruch.

  In Coq: https://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/

* Eine Injektion N^N --> N kann es schon geben: etwa in Eff(STM).
  Damit gibt es in Eff(STM) auch eine Injektion 2^N --> N. Das ist kein
  Widerspruch zum Vorherigen, weil 2 != Omega.

* Thierry, Paradox of trees:
  https://www.cs.bham.ac.uk/~mhe/TypeTopology/Various.LawvereFPT.html#16570


=== Chaitin

* http://math.ucr.edu/home/baez/surprises.html

  There exists a constant L such that no string of bits has Kolmogorov
  complexity that provably exceeds L.

* http://www.ams.org/notices/201011/rtx101101454p.pdf
  Beweis von Gödel II mit Chaitin und dem unexpected hanging paradox


=== Unlösbare Probleme

Poonen.
Undecidable problems: a sampler.
http://www-math.mit.edu/~poonen/papers/sampler.pdf


=== Vollständigkeit

Benjamin Frot.
Gödel's Completeness Theorem and Deligne's Theorem.
http://arxiv.org/abs/1309.0389

Empfohlen von John Baez!


=== Naive Mengenkomprehension

* Russels Antinomie ist ja bekannt.

* Aber auch ohne Negation gibt es Paradoxa:
  http://www.logicmatters.net/resources/pdfs/gwt/GWT2f.pdf
  Seite 99


=== Gödel

* http://quantropy.org/14/1/godel.pdf

* http://rgheck.frege.org/pdf/notes/TheFixedPointTheorem.pdf

* http://goodmath.scientopia.org/2013/03/12/finally-gdels-proof-of-incompleteness/

* http://www.logicmatters.net/resources/pdfs/gwt/GWT2f.pdf

* http://jdh.hamkins.org/are-all-godel-sentences-equivalent/
  In einem gewissen Sinn sind alle Gödelsätze zueinander beweisbar äquivalent,
  da sie alle äquivalent sind zu Con(PA).

* Gödels Erster sagt: Ist PA konsistent, so ist G nicht beweisbar.

  Der Beweis von Gödels Erstem lässt sich formalisieren. So folgt:
  PA beweist Con(PA) --> neg Prov(G). Die Umkehrung ist sowieso beweisbar.
  Zudem ist G beweisbar äquivalent zu neg(Prov(G)). Also beweist PA,
  dass Con(PA) zu G äquivalent ist.

  Damit kann man Gödels Zweiten zeigen: Falls PA |- Con(PA), so PA |- G,
  aber dem ist nicht so.

  Das ganze gilt auch analog für HA.

  Fazit: PA |- (Con(PA) <-> neg Prov(#(Con(PA)))).

  In PA folgt automatisch, dass Prov(#(1=0)) und Prov(#(Con(PA))) äquivalent sind.
  Die analoge Aussage für HA folgt nicht automatisch. Stimmt sie trotzdem?

* Ein Beweis von Gödels Zweitem übers unexpected hanging paradox:
  http://www.ams.org/notices/201011/rtx101101454p.pdf

* Falls PA konsistent ist, so gibt es Theorien, die ihre Inkonsistenz beweisen,
  obwohl sie konsistent sind. (Sie sind dann nicht omega-konsistent.)

  Etwa ist PA + neg(Con(PA)) eine solche:
  https://golem.ph.utexas.edu/category/2011/09/the_inconsistency_of_arithmeti.html#c039574

* Auch in schwachen Metatheorien gibt es insofern sowas wie NN, als dass es
  sinnvoll ist, von NN |== A zu sprechen. Aber NN |== PA gilt eventuell nicht,
  wegen des in PA enthaltenen Induktionsaxioms oder wegen der in PA enthaltenen
  klassischen Logik. (Achtung, bedenke Tarski!)

* Das Diagonallemma besagt: Sei F(n) eine Aussageform. Dann gibt es
  eine Aussage A mit PA |- (A <-> F(#A)).

  Ein Beweis geht so. Definiere zunächst diag : NN --> NN durch
  diag(m) = #(B(m)), falls m die Kodierung einer Aussageform B(n) ist,
  und beliebig sonst. Es diag darstellbar durch eine Formel Diag(n,m)
  in PA, d.h. für alle natürlichen Zahlen n gilt

        PA |- forall y. Diag(n,y) <-> y = diag(n).

  Definiere die Aussageform B(n) := (exists y. Diag(n,y) wedge F(y)).
  Sei m = #(B(n)).

  Dann setze A := B(m). Es gilt diag(m) = #(B(m)) = #A.
  Dann: A -||- (exists y. Diag(m,y) wedge F(y)) -||- F(diag(m)) -||- F(#A).

  Geht alles konstruktiv und für HA statt PA. Einziger Punkt, bei dem ich mir
  nicht sicher bin, ist die Darstellung von diag durch eine Formel.

  Etwas einfacher schreibt sich das ganze so.

  Setze B(n) := F(diag(n)). Dabei ist nun "diag" das Funktionssymbol für die
  Funktion diag von oben.

  Dann m := #(B(n)) und A := B(m). Dann A -||- F(diag(m)) -||- F(#(B(m))) -||- F(#A).

  Auf deutsch lässt sich A so definieren: A = F(Gödelnummer derjenigen
  Zeichenkette, die man erhält, wenn man in der Zeichenkette "F(Gödelnummer, die
  man erhält, wenn man in derjenigen Zeichenkette, die durch n kodiert ist, die
  vorkommende Variable durch n ersetzt)" die vorkommende Variable durch die
  Gödelnummer dieser Zeichenkette ersetzt). https://mathoverflow.net/a/66405/31233

  Die Gödel-Aussage lautet: "Die Aussage, die man erhält, wenn man in der
  Aussage 'Die Aussage, die man erhält, wenn man in der Aussage x die
  vorkommende Variable durch die Gödelnummer dieser Aussage ersetzt, ist nicht
  beweisbar.' die vorkommende Variable durch die Gödelnummer dieser Aussage
  ersetzt, ist nicht beweisbar."

  Der Beweis zeigt noch etwas mehr: Nämlich, dass nicht zu PA zeigt,
  dass A zu Prov(#A) äquivalent ist, sondern auch, dass A tatsächlich zu
  Prov(#A) äquivalent ist. Das ist gut zu wissen, falls man nicht unterstellen
  möchte, dass PA sound ist. Denn damit unterstellt man ja gleich die
  Konsistenz von PA.

* Definiere Gödelnummerierung. Erhalte Aussageform Prov(n) mit

      NN |== Prov(#A)  genau dann, wenn  PA |- A

  für alle Aussagen A. Finde mit Diagonallemma Aussage A mit

      PA |- (A <-> neg Prov(#A)).

  Dann ist es nicht der Fall, dass PA A zeigt, sofern PA konsistent ist. Denn
  angenommen schon. Sei p ein Beweis. Dann auch PA |- Proof(p, #A).
  Insbesondere PA |- Prov(#A). Da auch PA |- Prov(A), folgt PA |- bot.

  Sofern PA sogar omega-konsistent ist, folgt auch, dass PA nicht neg(A) zeigt.

  In jedem Fall gilt NN |== A.

* Was gibt's konstruktiv zu sagen? Es sollte auch eine Aussageform Prov(n)
  mit

      NN |== ProvI(#A)  genau dann, wenn  HA |- A

  für alle Aussagen A geben. Diagonallemma sollte auch Bestand haben, es gibt
  also eine Aussage A wie oben. Auch der Rest lässt sich so wiederholen.

* Definiere Aussageform Prov^R(n) durch

      Prov^R(n) := (exists p. Proof(p,n) wedge (forall q. q <= p --> neg Proof(q, neg(n)))).

  Es gilt: Lässt sich A in PA beweisen, so zeigt PA auch Prov^R(#A), sofern PA
  konsistent ist. Denn sei p ein Beweis von A. Dann auch PA |- Proof(p, #A).
  Sei ferner q <= p. Dann ist q kein Beweis von neg(A), denn neg(A) ist unter
  der Konsistenzannahme nicht beweisbar. Es gilt dann auch PA |- neg Proof(q, #(neg(A))).
  Ganz sauber geht das wohl so:

      Es gibt eine primitiv-rekursive Funktion Beh, die die Gödelnummer der
      gezeigten Behauptung zurückliefert, falls sie mit der Gödelnummer eines
      korrekten Beweises aufgerufen wird, und die andernfalls eine designierte
      andere Zahl zurückliefert.

      Proof(r,n) ist definiert als Beh(r) = n.

      In unserem Kontext gilt Beh(q) != neg(#A).

      neg(Proof(q,neg(#A))) ist beweisbar äquivalent zu neg(Beh(q) = neg(#A)).
      Es sind Beh(q) und neg(#A) zwei konkrete verschiedene Zahlen. PA kann
      daher zeigen, dass sie nicht gleich sind.

  Insgesamt folgt PA |- forall q. q <= p --> neg Proof(q, neg(#A)), denn es
  das gilt das Lemma PA |- forall q. q <= p --> bigvee_{i=0}^p (q = i).

  Es gilt sogar ohne die Konsistenzannahme, dass aus PA |- A schon
  PA |- Prov^R(#A) folgt. Denn sei p ein Beweis von A. Dann auch PA |- Proof(p,#A).
  Sei nun q <= p. Es ist q ein Beweis von neg(A) oder nicht. Im ersten Fall
  zeigt PA also A und neg(A), somit bot, somit auch Prov^R(#A). Im zweiten Fall
  kann wie oben argumentiert werden.

  Das war alles konstruktiv. Außerdem gilt das alles konstruktiv auch für HA
  statt PA.

  Für die weitere Anwendung in HA muss man auch Folgendes nachweisen (*):
  Gelte HA |- neg(A). Dann nicht nur HA |- ProvI^R(#(neg(A))), sondern auch

      HA |- exists p. ProofI(p,neg(#A)) wedge (forall q. q <= p --> neg ProofI(q,#A)).
                                (schon klar wäre es mit neg(neg(#A)) hinten)

  Denn sei p die Nummer eines Beweises von neg(A). Dann HA |- ProofI(p,neg(#A)).
  Sei nun q <= p. Dann BehI(q) = A oder nicht. Im ersten Fall folgt also HA |- A,
  also HA |- bot, also HA |- neg(ProofI(q,#A)). Im zweiten Fall folgt das
  ebenfalls.

* Sei nun A eine Aussage mit PA |- (A <-> neg Prov^R(#A)).

  Dann lässt sich A nicht beweisen, sofern PA konsistent ist. Denn angenommen
  schon. Dann folgt PA |- Prov^R(#A). Andererseits PA |- neg(Prov^R(#A)). Also
  PA |- bot.

  Auch dies gilt alles auch für HA. Man muss dann natürlich ProvI^R verwenden.

  Im Übrigen gilt NN |== A. Denn das bedeutet einfach, dass Prov^R(#A) nicht
  stimmt. Angenommen Prov^R(#A). Dann insbesondere Proof(#A). Also PA |- A.
  Aber das stimmt ja nicht.

* Nun wollen wir zeigen, dass PA auch nicht neg(A) zeigt. Wenn NN ein Modell
  von PA ist, ist das klar: Denn angenommen PA |- neg(A). Dann auch NN |== neg(A).
  Das ist ein Widerspruch zu NN |== A.

  Rein syntaktisch geht es auch, nur unter der Annahme der Konsistenz, der
  Beweis auf https://en.wikipedia.org/wiki/Rosser%27s_trick ist gut. Habe auch
  geprüft, dass es wieder für HA durchgeht. Dazu benötigt man oben
  angesprochene Verfeinerung (*).

* Was passiert, wenn man in einer intuitionistischen Metatheorie mit
  antiklassischen Axiomen arbeitet? McCarty weiß Antwort:
  https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093635833

* Löbs Theorem: Genau dann ist Prov(#A) --> A ableitbar, wenn A es ist.

  Die Rückrichtung ist klar.

  Die Hinrichtung geht so: Finde mit dem Diagonallemma eine Aussage B
  mit PA |- (B <-> (Prov(#B) --> A)). Dann kann man einsehen, dass
  PA |- (Prov(#B) --> Prov(#A)). Insgesamt also PA |- B. Somit auch
  PA |- Prov(#B). Und damit PA |- A.

  Siehe
  http://www.michaelbeeson.com/teaching/StanfordLogic/Lecture15Slides.pdf,
  Folie 16. Geht alles auch konstruktiv für HA durch.

  Mit Kontraposition kann man das auch aus Gödels zweitem
  Unvollständigkeitssatz ableiten, aber das geht dann wohl nicht konstruktiv.
  http://web.mit.edu/24.242/www/2ndIncompleteness.pdf, Seite 11.

  Gödel 1 und 2 verallgemeinert "auf A statt bottom":

  Sei B eine Aussage mit PA |- (B <-> (Prov(#B) --> A)).

  Dann sehen wir: (PA |- A  ==>  A)  ===>  B.
  Denn B ist ja äquivalent zu (PA |- B) ==> A. (Hier geht ein, dass die
  Diagonalität nicht nur beweisbar ist, sondern auch stimmt!)
  Gelte also PA |- B. Wir wollen A zeigen. Da PA |- B, auch
  PA |- Prov(#B). Also PA |- A. Nach Voraussetzung somit A.

  Wenn wir das Argument formalisieren, sehen wir:

      PA |- (Prov(#A) --> A) --> B.

  Falls nun PA |- Prov(#A) --> A, so folgt PA |- B, also PA |- Prov(#B),
  also PA |- A.

* Ein Henkin-Satz behauptet seine eigene Beweisbarkeit:

      PA |- (H <-> Prov(#H)).

  Ein solcher ist nach Löbs Theorem beweisbar.

* Löbs Theorem ist dasselbe wie der Y-Kombinator:
  https://semantic-domain.blogspot.com/2016/05/lobs-theorem-is-almost-y-combinator.html

* http://gdz.sub.uni-goettingen.de/pdfcache/PPN379931524_0022/PPN379931524_0022___LOG_0008.pdf

* Man kann ja eigentliche alle Argumentationen in PA oder meinetwegen ZFC
  formalisieren. Aber es gibt eine große Klasse an wichtigen Ausnahmen:
  Argumente, die das Prinzip "Prov(#A) --> A" verwenden. Solche kann man nicht
  formalisieren, denn (vorausgesetzt PA ist konsistent), so ist das Prinzip
  nicht beweisbar (der Fall A = bottom ist Gödels zweiter
  Unvollständigkeitssatz).

  Sind Spezialfälle beweisbar? Für gewisse Arten von Aussagen? Aber eher nicht,
  oder?

  Die Umkehrung, A --> Prov(#A), ist (denke ich) für manche Aussagen beweisbar:
  Für Sigma-Aussagen (geometrische).

* Sei L vom Diagonallemma geliefert mit

      PA |- (L <-> (forall p. len(p) < f(n) --> neg Proof(p, #L))),

  wobei f eine rasch steigende Funktion ist.

  Dann gilt L, unter Annahme der Konsistenz von PA:

      L ist ja (auch, wenn PA nicht sound ist) äquivalent zu der genannten
      allquantifizierten Aussage. Sei also p eine Zahl mit len(p) < f(n).
      Angenommen, p ist ein Beweis von L. Dann weiß PA das auch, also folgt
      PA |- Proof(p, #L). Da PA |- L, folgt damit PA |- neg Proof(p, #L).
      Das ist ein Widerspruch zur Konsistenz.

  Internalisiert folgt: PA |- (Con(PA) --> L). Der das bezeugende Beweis ist
  kurz! (Er enthält n, und vielleicht die Beschreibung von f, aber er ist auf
  jeden Fall kürzer als f(n).)

* Warnung vor "die Axiome sind offensichtlich wahr": Hat man beim naiven
  Mengenkomprehensionsaxiom auch gedacht.

* Logical Dreams: https://arxiv.org/pdf/math/0211398.pdf

* Es gibt ein Polynom mit ganzzahligen (nicht nur natürlichzahligen)
  Koeffizienten, das genau dann eine Nullstelle in N^r (äquivalent: Z^r)
  besitzt, wenn PA inkonsistent ist.

  Denn die Menge X = { n >= 0 | n kodiert einen Beweis von bottom } ist
  rekursiv aufzählbar. Daher gibt es ein Polynom f(n,x_1,...,x_k) mit
  ganzzahligen Koeffizienten, sodass für alle n >= 0 gilt:

      n in X  <==>  exists x_1,...,x_k >= 0: f(n,x_1,...,x_k) = 0.

  Somit:

      PA inkonsistent  <==>  exists n: n in X  <==>  f besitzt Lösung in N^{k+1}.

  Ich weiß nicht, wie konstruktiv der Beweis des MRDP-Problems ist. Vermutlich
  kann man f schon hinschreiben. Damit man aus einer Lösung einen
  Inkonsistenzbeweis gewinnen könnte, würde schon

      neg neg (n in X)  <==  neg neg (exists x...)

  genügen. Ich weiß aber leider auch nicht, wie viel Konsistenzannahmen im
  Beweis des MRDP-Problems drinstecken.

* http://www.maths.ed.ac.uk/~mbooth/mrdp.pdf. Putnams Trick:

  Sei eine rekursiv aufzählbare Menge X mit 0 nicht in X gegeben. Nach MRDP
  gibt es ein Polynom f(n,x_1,...,x_k) mit (n in X <==> exists x: f(n,x) = 0).
  Indem wir f durch f^2 ersetzen, können wir davon ausgehen, dass alle
  Funktionswerte von f (an Tupeln natürlicher Zahlen) nichtnegativ sind. Das
  Polynom Q(n,x) = x * (1 - f(n,x)) hat nun folgende Eigenschaft:

      Die nichtnegativen Funktionswerte von Q(n,x), wobei n und x alle
      natürliche Zahlen ablaufen, sind genau die Elemente aus X.

* Sei P folgendes Programm ("das universelle Programm"):

      Suche systematisch alle HA-Beweise nach einem Beweis der Form "Programm P
      gibt nicht die Liste x_1,...,x_k aus" ab. Sobald ein solcher Beweis
      gefunden wurde, gib die Liste x_1,...,x_k aus.

  Ist HA konsistent, so gilt für jede Liste xs: HA beweist nicht, dass P nicht
  die Liste xs ausgibt. Denn angenommen schon. Dann gibt es auch irgendeine
  erste Liste ys, für die HA beweist, dass P nicht die Liste ys ausgibt. Also
  gibt P ys aus. Das kann HA auch beweisen. Also zeigt HA bottom.

  (Alternativer Beweis: Denn angenommen schon. Dann hält P. Somit gibt es eine
  Liste ys, sodass HA beweist, dass P nicht ys ausgibt, und sodass P trotzdem ys
  ausgibt. HA beweist dann auch, dass P ys ausgibt. Also zeigt HA bottom.)

  Somit ist HA + (P gibt Liste xs aus) konsistent, falls HA es ist.

  "Somit" gibt es ein Modell von HA + (P gibt Liste xs aus). In diesem gibt P
  natürlich die Liste xs aus (nach Axiom). Innerhalb dieses Modells gibt es
  also einen HA-Beweis (mit Nichtstandardlänge), dass P nicht xs ausgibt.

* Jetzt gibt es auch die "universelle Menge"!
  http://jdh.hamkins.org/wp-content/uploads/2018/04/Set-theoretic-potentialism-and-universal-finite-set-SLS-2018-1.pdf

* Jede Menge Beweise im Gödel-Umfeld:
  https://mathoverflow.net/questions/72062/what-are-some-proofs-of-godels-theorem-which-are-essentially-different-from-t

* Toller Beweis von Dominik Kirst


=== Nichtzeigbarkeit von Äquikonsistenz

Sei S ein formales System (das die Voraussetzungen von Gödel II erfüllt), zum
Beispiel ZFC. Sei U ein Axiom mit S+U ⊢ Con(S), zum Beispiel ein großes
Kardinalzahlaxiom.

Sei B ein Basissystem, das höchstens so stark wie S ist, etwa PA.

Sei ☻ die Aussage: "Incon(S) ↔ Incon(S+U)". Dann gilt:

    Falls B ⊢ ☻, so B ⊢ Incon(S).

Etwa werden PA oder ZFC nicht beweisen, dass ZFC äquikonsistent zu ZFC+U ist
(während sie schon beweisen, dass ZFC und ZFC+CH oder ZF und ZFC etc.
äquikonsistent sind).

Das geht so. Gelte B ⊢ ☻. Dann auch S ⊢ ☻ und B ⊢ (S ⊢ ☻). Den Rest erledigen
wir durch Arbeit in B:

    Wir haben also ☻ und S ⊢ ☻. Da S+U ⊢ Con(S) und S+U ⊢ ☻, haben wir
    S+U ⊢ Con(S+U). Mit Gödel II folgt Incon(S+U). Mit ☻ folgt Incon(S).


=== Selbstreferentielle Reflektion

Sei S ein (rekursiv axiomatisierbares, Heyting-Arithmetik umfassendes und die
HBL-Bedingungen erfüllendes) formales System, das als eine seiner erlaubten
Schlussregeln folgende enthält:

    Um (im leeren Kontext, ohne Annahmen) eine Aussage φ zu folgern, genügt es,
    die arithmetische Aussage S ⊢ φ gefolgert zu haben.

Ich fühle mich wohler, wenn wir diese Schlussregel formal in einem Kalkül
natürlichen Schließens aufschreiben:

    ⊤ ⊢ (S ⊢ φ)
    -----------   (♡)
       ⊤ ⊢ φ
      
Dann wird der Unterschied zu folgender anderen Schlussregel, die viel stärker
als (♡) ist, mit Gödel I sofort Inkonsistenz impliziert und nicht gemeint ist,
klarer:

    -----------------
    ⊤ ⊢ ((S ⊢ φ) ⇒ φ)

[ Es ist nicht ganz klar, dass man ein System S mit (♡) konstruieren kann. Aber
es geht dank der Existenz von Quines [*]. ]

Dank dieser Schlussregel gilt jedenfalls für jede Formel φ:

    Falls S ⊢ (S ⊢ φ), so auch S ⊢ φ.  (☺)

Diese Beobachtung fängt aber die Besonderheit von S noch überhaupt nicht ein!
Für HA gilt (☺) zum Beispiel auch (eine infinitäre Metatheorie vorausgesetzt):
Da HA ja nur wahre Aussagen beweist, können wir aus HA ⊢ (HA ⊢ φ) folgern, dass
HA ⊢ φ.

Das Besondere an S ist, dass Beobachtung (☺) nicht nur gilt, sondern dass sie
auch formal beweisbar ist. Und zwar schon in schwachen Systemen, denke schon in
PRA, aber auf jeden Fall in HA und damit in S. Es gilt also:

    S ⊢ ((S ⊢ (S ⊢ φ)) ⇒ (S ⊢ φ)).

Mit Löbs Theorem folgt S ⊢ (S ⊢ φ). Mit (☺) folgt S ⊢ φ.

Das System S beweist also jede Formel φ.

Offene Punkte:

* Wie kann man möglichst einfach ein Programm angeben, was einen Beweis von
  jeder beliebigen Formel φ berechnet?

* Die Regel (♡) kann man auf mehrere Arten und Weisen abschwächen, zum Beispiel
  könnte man statt "∃p. p ist ein Beweis von φ" schreiben: "∃p. p ist ein
  Beweis von φ und p ist ein Numeral". (Dann haben wir abzählbar viele Regeln,
  je eine (für jede Formel φ und) jede externe natürliche Zahl.) Statt "ist ein
  Numeral" könnte man auch sagen: "ist ein Term, in dem nur Numerale, Addition
  und Subtraktion vorkommen". (Das sollte äquivalent sein.) Oder "ist ein Term,
  in dem nur primitiv-rekursive Funktionen vorkommen".

* Im intuitionistischen Fall wäre es interessant, Beweisbarkeit durch doppelt
  negierte Beweisbarkeit zu ersetzen.


[*] Wir beginnen mit einem Beweischecker für, sagen wir, HA. Dieser nimmt (eine
Gödel-Kodierung eines) angeblichen Beweisbaums und prüft, ob es sich dabei um
einen korrekten HA-Beweis handelt. Dieser Beweischecker soll als Turingmaschine
vorliegen. Wir können aber dank des Quine-Theorems ohne Einschränkung davon
ausgehen, dass wir ihn in einer Programmiersprache schreiben können, die ein
Primitiv bereitstellt, das den Quelltext des laufenden Programms zurückgibt.

Nun modifizieren wir diesen Beweischecker leicht, indem wir folgende Klausel in
seiner langen if-Abfrage zur Validitätsprüfung hinzufügen:

    Falls der aktuell zu begutachtende Beweisschritt von der Form

        ⊤ ⊢ ∃p. (P hält bei Eingabe von p mit Ausgabe "ja, ist ein korrekter Beweis von #φ")
        ------------------------------------------------------------------------------------
                                            ⊤ ⊢ φ

    ist, wobei P (das Numeral zur) (Gödel-Kodierung des) eigenen Quelltexts und
    #φ (das Numeral zur) (Gödel-Kodierung der) Formel φ ist, so wird dieser
    Schritt akzeptiert.

In der oberen Zeile der abgesetzten Schlussregel kommt noch deutscher Text vor.
Logiker*innen wissen, wie der zu einer arithmetischen Aussage übersetzt werden
kann.

[ Bemerkung am Rande: Der so erhaltene Beweischecker ist keinesfalls eindeutig
bestimmt. Das Quine-Theorem (übliche Bezeichnung: "recursion theorem")
garantiert Existenz, aber nicht Eindeutigkeit, auch nicht modulo beobachtbarem
Verhalten. ]

Jedenfalls kann man sich leicht überlegen, dass das entstehende Programm immer
noch bei jeder Eingabe terminiert und HA-Beweise als korrekt beurteilt.

Wir konstruieren das gesuchte System S dann so: Für jede Sequenz σ, die der
neue Beweischecker als validen Beweisschritt akzeptiert, nehmen wir σ als
Schlussregel. Andere Schlussregeln soll es nicht geben.

Dann kann man sich überlegen, dass S rekursiv axiomatisierbar ist; alle
Schlussregeln von HA enthält; die HBL-Bedingungen erfüllt; und außerdem Regel (♡)
enthält.


=== Quantitatives Löb-Theorem

* Hier noch mal zur Erinnerung, wie man Löb beweist.

  Gelte S ⊢ (Prov(#φ) → φ).

  Mit dem Diagonallemma finden wir eine Formel α mit

      S ⊢ (α ↔ (Prov(#α) → φ)).

  Dann S ⊢ (Prov(#α) → Prov(#φ)). Also durch Nachschalten der Annahme
  S ⊢ (Prov(#a) → φ). Also S ⊢ α. Also S ⊢ φ.

* Geht das auch quantitativ? Gibt es zu jeder Formel φ eine Zahl n
  sodass aus r : S ⊢ (Prov_{<n}(#φ) → φ) schon S ⊢ φ folgt?
  Weiß nicht; es folgt aber ein Argument, wieso für jede Zahl R
  und jede Formel φ eine Zahl n existiert, sodass aus der Existenz eines
  <R-Beweises von (Prov_{<n}(#φ) → φ) schon S ⊢ φ folgt.

  Naja: Lass zunächst dieselbe Formel α versuchen.

  Habe also p : S ⊢ (α ↔ (Prov(#α) → φ)).
  Dann folgt aus q : S ⊢ α schon S ⊢ φ, und zwar so:

      Gelte S ⊢ α.
      Dann auch S ⊢ Prov(#α).
      Habe auch S ⊢ (Prov(#a) → φ).
      Mit Schnittregel folgt S ⊢ φ.

  Wie lang ist dieser Beweis insgesamt? Etwa len(p) +
  len(Verifizierungsprotokoll von p) + len(q) + Konstanten.
  Schreibe f_p(|q|) dafür. Ist eine ganz einfache Funktion, auf jeden Fall
  primitiv-rekursiv.

  Wir haben also: Aus Prov_{<Q}(#α) folgt Prov_{<f_p(Q)}(#φ).

  Das System S kann das auch alles einsehen. Also haben wir:

      S ⊢ (Prov_{<Q}(#α) → Prov_{<f_p(Q)}(#φ)).

  Dieser Beweis hat in etwa Länge len(Verifizierungsprotokoll von p) + Konstanten.

  Wenn wir n := f_p(Q) setzen, wobei wir Q noch zu bestimmen haben, folgt also
  S ⊢ (Prov_{<Q}(#α) → φ). Dieser Beweis hat in etwa Länge len(Protokoll von p) + len(r).

  Nun sollte diese Implikation äquivalent zu α sein, die Arbeitshypothese, α
  aus dem unquantitativen Beweis zu übernehmen, müssen wir also leicht
  anpassen. Wenn wir das unterstellen, haben wir S ⊢ α, und zwar durch einen
  Beweis, der in etwa die Länge len(Proto p) + len(r) + len(p) =: Q' hat.

  Es folgt S ⊢ (Prov_{<Q'}(#α)). Wir brauchen Q' <= Q. Dann folgt S ⊢ φ.

  Wenn wir mal unterstellen, dass Zahlliterale wegen der Möglichkeit der
  Binärkodierung nicht ins Gewicht fallen, sind wir fertig:
  Verifizierungsprotokolle sollten in etwa so lang sein wie die Beweise selbst.
  Gut, für jeden Beweisschritt kommen noch die Ablaufprotokolle des S-Checkers
  hinzu. Jedenfalls ist das wohl im Vorfeld berechenbar.

  Dann bekommen wir(?) doch diagonal-/quinemäßig eine Zahl Q und eine Formel α,
  für die ein Beweis

      p : S ⊢ α ↔ (Prov_{<Q}(#α) → Prov_{<f_p(Q)}(#φ))

  der Länge len(p) mit len(p) + len(Proto p) + R <= Q existiert. Und damit
  gehen alle obigen Schritte durch.

  Die R-Abhängigkeit kann man eventuell verbessern durch eine trickreichere
  Argumentation.

* Die KI-Leute sagen in https://arxiv.org/pdf/1602.04184.pdf:

  Für jede Formel φ(n) mit freier Variable n und jede berechenbare Funktion f,
  die gewisse asymptotische untere Schranken erfüllt, gibt es ein K, sodass:

      Falls S ⊢ ∀k. Proof_{<f(k)}(φ(k)) → φ(k),
      so    S ⊢ ∀k > K. φ(k).


=== Gödel und Turing

* Sei PA korrekt für Aussagen über das Halteverhalten von Turingmaschinen.
  Sei PA vollständig. Dann ist das Halteproblem lösbar.

  Nämlich durch folgende Turingmaschine: Gegeben eine Maschine M, suche alle
  Beweise von PA ab nach einem Beweis, dass M hält, oder einem Beweis, dass M
  nicht hält. Wegen Vollständigkeit terminiert die Suche. Wegen Korrektheit
  stimmt das vermeldete Ergebnis.

* Dieses Argument kann man angeblich verbessern, sodass man die Korrektheitannahme
  nicht benötigt, behauptet Joel David Hamkins:
  https://mathoverflow.net/a/227316/31233 Mir ist aber nicht klar, wie das
  geht.

* Von Andreas Kaseorg (https://news.ycombinator.com/reply?id=18117460):

  Sei M diejenige Maschine, die nach einem S-Beweis, dass M nicht halten wird,
  sucht, und bei Auffinden eines solchen Beweises anhält.

  Falls S zeigt, dass M nicht hält, dann hält M; S kann das auch einsehen; also
  ist S inkonsistent.

  Falls M hält, so zeigt S auch, dass M hält; zudem gibt es dann einen
  S-Beweis, dass M nicht hält; also ist S inkonsistent.

  Wenn wir annehmen, dass S konsistent ist, ist die Aussage "M hält nicht" also
  wahr, aber nicht in S beweisbar.

  Wir können das sogar ein wenig verbessern: Falls S zeigt, dass M hält, dann
  zeigt S auch, dass S inkonsistent ist. (Hierzu muss S ein bisschen was
  können; HA zu umfassen genügt völlig. Vielleicht genügt sogar IQ.) Okay, das
  ist leider nicht ganz dasselbe wie "S zeigt bottom".

* Können wir den Rosser-Trick einbauen?

  Sei M diejenige Maschine, die systematisch alle S-Beweise durchgeht.
  Trifft sie auf einen Beweis, dass M nicht hält, dann hält sie.
  Trifft sie auf einen Beweis, dass M hält, dann geht sie in eine
  Endlosschleife.

  Zeige S, dass M nicht hält. Dann können wir alle vorherigen Beweise
  durchgehen. Ist dabei einer dabei, der zeigt, dass M hält, so ist S
  inkonsistent. Andernfalls sehen wir, dass M hält. S kann das auch einsehen.
  Somit ist S inkonsistent.

  Zeige S, dass M hält. Dann können wir alle vorherigen Beweise
  durchgehen. Ist dabei einer dabei, der zeigt, dass M nicht hält, so ist S
  inkonsistent. Andernfalls sehen wir, dass M nicht hält. Zudem zeigt S,
  dass S zeigt, dass M hält. (Hier benötigt man noch nicht sowas wie die
  HBL-Bedingungen!) Zusammen mit der Internalisierung der Erkenntnisse über
  frühere Beweise folgt, dass S zeigt, dass M nicht hält. Also ist S
  inkonsistent.


=== Verschachtelte formale Systeme

* In /Axiomatization of induced theories/ gibt Azriel Lévy die Antwort auf
  folgende Frage: Wie kann das formale System "A |- B |- phi" axiomatisch
  charakterisiert werden?
  https://www.ams.org/journals/proc/1961-012-02/S0002-9939-1961-0122702-2/S0002-9939-1961-0122702-2.pdf


=== Hereditär endliche Listen

* Es gibt zwei kanonische Ordnungen auf der Menge der hereditär endlichen
  Listen: die Partialordnung "ist ein Element von" und die bekannte
  Totalordnung mit Ordnungstyp ε_0.


=== Parikh

* Es gibt Aussagen, die nur einen langen Beweis haben, aber einen kurzen Beweis,
  dass sie einen Beweis haben.

  Nämlich "Diese Aussage besitzt keinen Beweis von weniger als n Zeichen",
  wobei n eine natürliche Zahl ist, die wir so hochschrauben können, wie wir
  möchten.

  Unter der Annahme, dass PA konsistent ist, kann es nicht sein, dass diese
  Aussage einen Beweis von weniger als n Zeichen besitzt. Denn wenn schon, dann
  beweist PA einen Widerspruch.

  Wir können alle Beweise von weniger als n Zeichen durchgehen. Dabei werden
  wir unter der Konsistenzannahme keinen Beweis der Aussage finden. Diese
  Überlegung kann PA auch beweisen. Damit hat sie die Beweisbarkeit der Aussage
  bewiesen.

  Siehe etwa http://www.math.ucla.edu/~asl/bsl/0903/0903-004.ps,
  Yanofsky: A Universal Approach to Self-Referential Paradoxes,
  Incompleteness and Fixed Points.

  Originalartikel: https://www.jstor.org/stable/pdf/2269958.pdf.


=== Inkonsistenz von PA

* https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2010_09_25_slides.pdf

  Problem mit üblichem "Beweis", dass PA konsistent ist: Nicht alle Teilmengen,
  die über Formeln in PA definiert werden, haben eine "Bedeutung": Für manche
  gilt für keine Zahl, dass beweisbar ist, dass sie in der Menge liegt, oder
  dass beweisbar ist, dass sie nicht in der Menge liegt.

* McLarty in
  https://artscimedia.case.edu/wp-content/uploads/2013/07/14182256/General-talk.pdf:

  "I point I owe to John Mayberry: we have only ever applied
  induction for conditions φ that make sense.

  If the formalism conceals an inconsistency we should expect it to
  lie in conditions φ with no apparent sense."


=== Finitistisch akzeptables Schließen

... wird laut manchen Leuten formalisiert durch PRA (primitiv-rekursive
Arithmetik). Manchmal genügt sogar ERA, das ist wie Peano-Arithmetik, aber mit
dem Induktionsprinzip eingeschränkt auf elementar berechenbare Prädikate.

http://www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf


=== Definierbarkeit

* Klar, es gibt Tarskis Resultat.

* Man kann aber in Mengenlehre, für jede Menge U, definieren, wann
  eine Formel (der Mengenlehre), kodiert als natürliche Zahl, U-relativiert
  gilt. Dazu muss man halt einen Interpreter schreiben. Dessen Typ ist sowas
  wie

      N --> Omega^Env,

  wobei Env die Menge der endlichen Listen von Elementen aus U ist. In ZF kann
  man ja bekanntlich rekursive Definitionen treffen.

* Wenn man dieses Verfahren auch für das Universum U, die Klasse aller Mengen,
  durchführen möchte, so gibt es natürlich ein Problem (wie von Tarski
  vorhergesehen). Zunächst gibt es keine passende Menge Env. Das ist aber noch
  nicht an sich ein Problem, denn man muss ja in ZF nicht Zielmengen von
  Abbildungen angeben. Allerdings muss ja f(#top) sowas sein wie

      const {*}, d.h.
          { <e, {*}> | e aus Env },

  und das existiert auch nicht.

* Eine Menge M heißt genau dann definierbar rel X, wenn es eine Formel phi
  von Mengenlehre gibt, sodass M = { z in X | phi gilt rel X für z }.
  (Man kann die Definition nicht derart ausweiten, dass auch nicht-Teilmengen
  von X eine Chance hätten, definierbar rel X zu sein.)

* Def(X) ist die Menge aller rel X definierbaren Teilmengen von X.

  Damit dieses Konzept nicht sehr pervers ist, muss X zumindest sowas wie
  transitiv sein. Zum Beispiel sollte ja die Teilmenge der positiven
  natürlichen Zahlen rel N definierbar sein. Das stimmt schon auch, ist aber
  nicht völlig trivial. Denn die rel-U-Extension von "n ist positiv",
  ausgeschrieben "0 in n" bzw. "exists z. z in n wedge forall y. neg (y in z)"
  lautet:

      exists z in N.
          z in n  wedge
              forall y in N. neg (y in z).

  Das besagt also nicht, dass 0 (die leere Menge) ein Element von n ist. Nur,
  dass eine Menge z ein Element von n ist, welche keine natürlichen Zahlen
  enthält. Wegen der Transitivität von N folgt dann aber, dass z die leere
  Menge ist. Denn sei y in z. Dann y in z in N. Also y in N. Also Widerspruch.


=== Wahrheit vs. Beweisbarkeit

* "Because it’s the case that if a number-theoretic statement is true, then its
  witnessing functions exist, we might hope that it would be the case that if a
  number-theoretic statement is provable, then its witnessing functions are
  computable, that is, that we could extract a computer program for the
  witnessing functions from the proof."
  https://xorshammer.com/2008/08/13/kreisels-no-counterexample-interpretation/

  Aber so naiv stimmt es natürlich nicht: Die Aussage "für alle n gibt es ein m
  sodass die n-te Turingmaschine nach m Schritten hält oder niemals hält" ist
  beweisbar in Peano-Arithmetik, aber besitzt keinen berechenbaren Zeugen.


=== Quantorenelimination

* Quantorenelimination ist bei der Theorie algebraisch abgeschlossener Körper
  möglich. Idee: Ersetze zwei Gleichungen

      f(x) = 0  und  g(x) = 0

  mit f(x) = a x^n + ..., g(x) = b x^m + ..., n >= m, durch

      (b  = 0 und (f(x) = 0 und g(x)-bx^m = 0)) oder
      (b != 0 und (b*f(x) - a*x^{n-m}*g(x) = 0 und g(x) = 0)).

  Die neu auftretenden Gleichungen haben geringeren Grad. Schlussendlich
  bleiben nur Gleichungen zwischen Konstanten übrig (die Variable x wurde also
  eliminiert) und Gleichungssysteme bestehend aus einer einzelnen Gleichung
  übrig (welche wegen der Voraussetzung der algebraischen Abgeschlossenheit
  stets lösbar sind). Dann kann man rekursiv mit den in den Konstanten
  versteckten weiteren Variablen weitermachen.

* Quantorenelimination zieht nach sich: Bilder quantorfrei definierter Mengen
  unter definierbaren Abbildungen sind wieder quantorfrei definierbar.

* Auch die Theorie reell abgeschlossener Körper besitzt Quantorenelimination.
  Daher sind Bilder semialgebraischer Mengen unter polynomiellen Abbildungen
  wieder semialgebraisch.

* Inwieweit ist Chevalleys Theorem eine Verallgemeinerung?

* Ting Zhang. A survey of quantifier elimination: syntactic and semantic
  approaches. http://theory.stanford.edu/~tingz/talks/qe.ps

* http://homepages.math.uic.edu/~marker/orsay/orsay2.pdf

* Quantifier elimination in C*-algebras. http://arxiv.org/abs/1502.00573

* Zahlentheoretische Aussagen, die nur die Quantoren "für fast alle n"
  und "es gibt unendlich viele n" verwenden, sind entscheidbar.
  Weil man auch R statt N verwenden kann.
  https://xorshammer.com/2008/08/25/almost-a-number-theoretic-miracle/


=== Analytische Hierarchie

Achtung, hier klassische Logik benutzt!

* Jede Pi_1^1-Aussage ist äquivalent zu einer Aussage der Form

      forall f : N --> N. exists m : N. R(n, f^(m)),

  wobei R ein rekursives Prädikat ist.
  Dabei ist f^ die "course of values"-Funktion, also f^(n) = (f(0),...,f(n-1)).

  Siehe: Cor. IV.2.10 in /Classical Recursion Theory/ von Odifreddi.

  (Wenn man Mengenquantoren statt Funktionsquantoren verwendet, muss man zwei
  Zahlquantoren verwenden. Stimmt das?)

* Eine Menge X natürlicher Zahlen ist genau dann eine Pi_1^1-Menge,
  wenn es eine rekursive Folge (T_n)_n rekursiver Bäume mit

      n in X  <==>  T_n ist fundiert

  gibt.

  Die Richtung "<==" ist klar, denn die Bedingung, dass T_n fundiert ist, ist
  eine Pi_1^1-Bedingung.

  Zur Richtung "==>" nutzen wir aus, dass die Menge X von der Form
  X = { n | forall f. exists m. R(n, f^(m)) } ist und definieren den Baum T_n
  so: Eine Folge xs von natürlichen Zahlen soll genau dann zum Baum gehören,
  wenn für jedes echte Suffix ys von xs die Aussage R(n, ys) falsch ist.

  Die Blätter des Baums geben also Plätze an, bei denen R(n, __) das erste Mal
  gilt.

* Eine analoge Aussage gibt es mit fundierten Ordnungen statt fundierten
  Bäumen.

* Mehr steht zur arithmetischen und analytischen Hierarchie in:

  * Beklemishev: Provability, Computability and Reflection
  * Grzegorczyk: An Outline of Mathematical Logic: Fundamental Results and
    Notions Explained

* https://xorshammer.com/2016/05/14/the-arithmetic-hierarchy-meets-the-real-world/


=== Temporale Logik

* Diodoreanische Modalität in Minkowski-Raumzeit (in Goldblatts Buch)


=== Induktive Logik

https://books.google.it/books?id=oxxaRUjhD_QC&printsec=frontcover#v=onepage&q&f=false
Handbook of the History of Logic: Inductive logic
herausgegeben von Dov M. Gabbay, John Hayden


=== Russel konstruktiv statt imprädikativ

http://staff.math.su.se/palmgren/CERRTT.pdf


=== Funktionssymbole

Folgende drei Theorien zeigen dieselben Formeln, die in der Sprache von HA
formuliert werden können:

1. HA

2. HA ergänzt um je ein Funktionssymbol für jeden Aufbau einer
primitiv-rekursiven Funktion, ergänzt um Axiome für das Funktionssymbol, welche
sich aus dem Aufbau der primitiv-rekursiven Funktion ergeben.

3. HA ergänzt um je ein Funktionssymbol für jede primitiv-rekursive Funktion,
ergänzt um Axiome für das Funktionssymbol, welche sich aus allen möglichen
Aufbauten der primitiv-rekursiven Funktion ergeben. Hier geht ein Lemma ein,
nämlich dass HA die Äquivalenz von Funktionen darstellenden Formeln zeigen
kann, sofern die Funktionen gleich sind.

Hier ein paar Details zu primitiv-rekursiven Funktionen und Co.

* Die Klasse der rekursiven Funktionen ist die kleinste Klasse von Funktionen
  N^k --> N, die die konstante Nullfunktion, die Nachfolgerfunktion und die
  Projektionsfunktionen enthält und abgeschlossen unter Komposition, primitiver
  Rekursion und regulärer Minimierung ist (unbeschränkte Minimierung über eine
  Relation, von der in der Metatheorie bekannt ist, dass sie erfüllt ist).

  Man kann aber auf die Zutat der primitiven Rekursion verzichten, sofern man
  im Gegenzug Addition, Multiplikation und (x,y) |-> delta_{x,y} aufnimmt.
  Das zeigt man mit der unten beschriebenen beta-Funktion:

  Sei h durch primitive Rekursion definiert:

      h(0,    zvec) = f(zvec)
      h(s(n), zvec) = g(n, h(n,zvec), zvec),

  wobei wir von f und g schon wissen, dass sie nur aus den genannten Zutaten
  aufgebaut sind.

  Dann definieren wir:

      H(n, zvec) = mu d.
          beta(d,0) = f(zvec) wedge
              forall i < n: beta(d,i+1) = g(i, beta(d,i), zvec).

  Dann h(n, zvec) = beta(H(n,zvec), n).

* Jede rekursive Funktion f ist in Q (und wohl auch sowas wie IQ,
  intuitionistische Q-Arithmetik) darstellbar. Das bedeutet, dass es eine
  Formel A(x,y) gibt, sodass für jedes x

      Q |- forall y. A(x,y) <--> y = f(x)

  gilt. (Dabei kann x auch Abkürzung für "x_1, ..., x_n" sein. Je zwei solche
  Formeln sind zueinander beweisbar äquivalent. Oder nicht? Zumindest hat man
  für jedes x, dass Q |- forall y. A(x,y) <--> A'(x,y). Das genügt aber nicht.
  Betrachte etwa die Formeln (beide im Kontext n:N) "n ist kein Beweis von
  bottom und "top". Für jedes Numeral n sind die beiden Formeln beweisbar
  äquivalent (infinitistische Metalogik vorausgesetzt). Aber sie sind nicht
  selbst beweisbar äquivalent. Das würde nämlich heißen, dass Q (oder was auch
  immer) seine Konsistenz zeigt.)

  Das folgt, da die Zutaten auf der zweiten Zutatenliste oben alle darstellbar
  sind.

  Ich glaube, dass HA noch etwas mehr kann: Zeigen, dass die so definierten
  Formeln zu primitiv-rekursiven Funktionen wirklich funktional sind, d.h.
  zeigen:

      HA |- forall x. exists! y. A(x,y).

  Für beliebige Funktionen gilt das sicher nicht. Zum Beispiel nicht für
  diejenige Funktion, die einer Zahl n die Länge von Goodstein(n) zuordnet.
  Das ist eine berechenbare Funktion!

  Das sollte so gehen: Ist für die Grundfunktionen klar. Bleibt nur primitive
  Rekursion. Sei also h über primitive Rekursion gegeben:

      h(0,    zvec) = f(zvec)
      h(s(n), zvec) = g(n, h(n,zvec), zvec),

  Dann zeigen wir jetzt die Funktionalität mittels Induktion über n.

  Der Induktionsanfang ist klar. Wir wissen ja schon, dass h dargestellt werden
  kann, und für das Numeral 0 haben wir Funktionalität.

  Nun der Induktionsschritt. Wir wissen

      exists! y. n h y

  und wollen zeigen:

      exists! v. (n+1) h v.

  Dabei jeweils die Parameter zvec unterdrückt.

  Zur Existenz: Finde y mit n h y. Finde v mit (n,y) g v. Dann (n+1) h v.
  Hier muss man sich etwas in die beta-Funktion einwühlen!

  Zur Eindeutigkeit: ...

* Es gilt auch die Umkehrung: Ist f in Q (oder IQ) durch eine Formel A
  darstellbar, so ist f berechenbar. Denn f(n) kann man wie folgt berechnen:
  Gehe alle Beweise von Q durch, bis ein Beweis einer Aussage der Form A(n,y)
  auftritt. Gib dann y zurück. Dieses Verfahren terminiert nach Voraussetzung.
  Sofern man unterstellt, dass Q konsistent ist, ist der Rückgabewert auch
  gerade f(n).

* Es gibt eine Funktion beta : N^2 --> N, sodass für jede Folge (a_0,...,a_n)
  eine Zahl d existiert, sodass beta(d,i) = a_i für i <= n, und sodass beta
  aus den Grundfunktionen und regulärer Minimierung (aber nicht primitiver
  Rekursion) hervorgeht.

  Nutze chinesischen Restsatz für hinreichend große Moduli und eine
  Paarungsfunktion, um neben der so erhaltenen Zahl auch eine weitere Zahl zu
  kodieren, aus der die Moduli extrahiert werden können.

  Genauer geht das so.

  Zunächst können wir die Paarungsfunktion J(x,y) = (x+y) (x+y+1) / 2 + x
  definieren. Dazu braucht's nur reguläre Minimierung: J(x,y) ist das kleinste z,
  sodass (x+y)*(x+y+1) + 2*x = 2z ist.

  Die Projektionen gehen auch:

      K(z) = mu x. exists y <= z. z = J(x,y),
      L(z) = mu y. exists x <= z. z = J(x,y).

  Es gilt dann K(J(x,y)) = x, L(J(x,y)) = y für alle x, y.

      Prelude> mapM_ print [ [ j x y | x <- [0..5] ] | y <- [0..5] ]
      [0,2,5,9,14,20]
      [1,4,8,13,19,26]
      [3,7,12,18,25,33]
      [6,11,17,24,32,41]
      [10,16,23,31,40,50]
      [15,22,30,39,49,60]

  Dann definieren wir:

      beta*(d0, d1, i) = rem(1 + (i+1) d1, d0)  und
      beta(d, i) = beta*(K(d), L(d), i).

  Sind nun Zahlen a_0, ..., a_n gegeben, so setzen wir

      j  := max { n, a_0, ..., a_n } + 1,
      d1 := j!,
      d0 so, dass d0 = a_i mod (1 + (i+1) d1) (existiert eindeutig).

Siehe: Um Seite 85 von
http://people.ucalgary.ca/~rzach/static/open-logic/courses/phil479/phil479-screen.pdf.

* Eine Funktion ist genau dann primitiv rekursiv, wenn ihr Graph es ist und
  wenn sie nach oben durch eine primitiv rekursive Funktion beschränkt wird:
  https://mathoverflow.net/questions/76037/inverse-ackermann-primitive-recursive-or-not


=== Lineare Logik

* Ein Grund "wieso": Weil automatisches Beweisen praktikabel wird.
  https://blog.plover.com/math/logic/cut-rule.html


=== Beweisprädikate, die die HBL-Bedingungen nicht erfüllen

* "x besitzt einen schnittregelfreien Beweis"

* https://mathoverflow.net/a/231011/31233


=== Wie viele Beweise besitzt eine Aussage?

* Jost: Wenn die Behauptung hinreichend weit von den Voraussetzungen
  entfernt ist, dann kann sie verschiedene Beweise zulassen.

* FTA ist wohl ein Beispiel.

* Einfachheit und Länge von Beweisen:
  http://www.phil.uu.nl/~iemhoff/Mijn/Papers/simplicity.pdf


=== Robinson-Arithmetik Q

* Beweist konkrete Aussagen (etwa jede Instanz der binomischen Formel),
  aber kaum allgemeine Aussagen.

* Ein Modell von Q ist die Menge all derjenigen Polynome aus Z[X],
  deren Leitkoeffizient (sofern vorhanden) positiv ist, mit der üblichen
  Polynomaddition und -multiplikation und +1 als Nachfolgeroperation.


=== Anwendungen von Logik in Mainstreammathematik

* Klar: Proof Mining, interne Sprache von Topoi, ...

* Whitehead

* In der Theorie der assoziativen Algebren oder so gab es Aussagen,
  die zunächst unter Verwendung großer Kardinalzahlen gezeigt wurden.
  https://mathoverflow.net/a/71258/31233


=== Proof mining

* https://www2.mathematik.tu-darmstadt.de/~kohlenbach/novikov.pdf

* https://www.sciencedirect.com/science/article/pii/S0001870818304900
  Die Einleitung enthält eine tolle Einführung in die Denkansätze von proof
  mining

* Möchte Spectors Ansatz für AC-Extraktion via bar recursion verstehen:
  https://doc.rero.ch/record/293640/files/S0022481200015127.pdf

* Mehr zu L in negneg:
  https://doc.rero.ch/record/293640/files/S0022481200015127.pdf#page=6


=== Big Five

* Beispiele für Theoreme, die die Big-Five-Kategorisierung sprengen:

  Ramsey Theorem (https://www.sciencedirect.com/science/article/pii/S0168007216300860)

  Infinite Pidgeonhole Principle (Hirst, Combinatorics in subsystems of second
  order arithmetic)

  WWKL (Measure theory and weak König's lemma)

  Szemerédi regularity lemma


=== Überblick über die vielen Varianten von HA^ω

https://staff.fnwi.uva.nl/b.vandenberg3/papers/note_on_haomega.pdf


=== Catalan-Zahlen

* https://mathoverflow.net/questions/272394/reference-request-heyting-algebra-structure-on-catalan-numbers


=== Ein Beweis für alle Gödel-style Resultate

* https://arxiv.org/pdf/1812.00990.pdf

* https://arxiv.org/abs/math/9204207 Interessanter Beweis von Jech für
  Mengenlehren


=== Higher-order reverse mathematics

* Sam Sanders.

* https://arxiv.org/abs/1711.08939

* https://arxiv.org/pdf/1805.11342.pdf: Zerfällungen (A <-> B wedge C)
  und Disjunktionen (A <-> B vee C) gibt es in HRM zuhauf (in klassischer RM
  nur sehr selten).


=== Hilberts Programm

* Aus Konsistenz von HA folgt Π_0^1-Soundness von HA, und das ist vielleicht
  wichtiger als Konsistenz:

  Gelte HA ⊢ ∀x. φ(x). Wir möchten zeigen, dass für alle x φ(x) gilt.
  Sei also x beliebig. Da φ quantorfrei ist, gilt φ(x) oder ¬φ(x).
  Im zweiten Fall folgt HA ⊢ ¬φ(x), also HA ⊢ ⊥.


=== Theorien ohne Vergangenheit ("The Speech", John Steel)

Jede Π_0^1-Konsequenz eines Systems S ist schon eine Konsequenz von PRA +
Con(S). (Umgekehrt gilt das nicht, denn Con(S) ist eine solche Konsequenz von
PRA + Con(S).)

Das zeigt, dass man -- wenn man nur an Π_0^1-Konsequenzen interessiert ist --
auch gerne in PRA + Con(S) arbeiten kann. Also zum Beispiel in PRA + Con(ZFC).
Dann kann man also die Position vertreten, dass unendliche Mengen, große
Kardinalzahlen usw. alle nicht existieren, aber trotzdem die Früchte dieser
Annahmen ernten.

Steel vergleicht diese Position aber mit der Vorstellung, die Welt sei heute
früh entstanden, aber auf eine Art und Weise, die vermuten lässt, dass es eine
Vergangenheit gab (Fossilien, Hintergrundstrahlung, ...).

Steel begegnet damit dem Argument, man könne V = L mit großen Kardinalzahlen
vereinen: indem man in ZFC + V=L + Con(große Kardinalzahl) arbeite. Darin gibt
es dann Modelle von ZFC mit großen Kardinalzahlen, aber der Zauberspruch V = L
erstreckt sich nicht auf diese.

https://cs.nyu.edu/pipermail/fom/2000-January/003643.html


=== Löb in KI-Forschung

* https://agentfoundations.org/item?id=320: Procrastination Paradox,
  Consistency Waterfall


=== Existenzeigenschaft

* HA zeigt nicht die Existenzeigenschaft von HA:
  https://mathoverflow.net/questions/413659/is-heyting-arithmetic-sufficient-to-prove-its-own-formalized-existence-propert

  Wenn dem so wäre, würde HA + Con(HA) seine Konsistenz zeigen, denn es könnte
  wie folgt argumentieren:

  Gelte HA + Con(HA) ⊢ ⊥. Dann HA ⊢ ¬¬Incon(HA). Somit PA ⊢ Incon(HA).
  Somit HA ⊢ Incon(HA). Nach Voraussetzung gibt es n mit HA ⊢ Proof_HA(n, "⊥").
  Habe auch ¬Proof_HA(n, "⊥"). Also HA ⊢ ¬Proof_HA(n, "⊥"). Also HA ⊢ ⊥.
  Also ⊥.


=== Art der Zeugen in Dialectica

* Die Dialectica-Übersetzung von "∀P. ∃x. (Px → ∀y. Py)" ist "∀P,y. P(fP) → P(y)".

* Die Dialectica-Übersetzung von "∀a,b. a = b → f(a) = f(b)" ist sie selbst.

* Die Dialectica-Übersetzung von "∀α,β. (∀n. α(n) = β(n)) → f(a) = f(b)" ist
  "α(Λ(α,β)) = β(Λ(α,β)) → f(α) = f(β)", kann noch definiert werden als
  Λ(α,β) = min { n | α(n) ≠ β(n) } (sonst 0).

* Zeugen werden immer komplizierter (gelernt von Kohlenbach auf Dagstuhl 2021):
  erst nicht berechenbar, dann sogar nicht ZF-definierbar.

* Dialectica hat was mit Ableitung und automatic differentiation zu tun:
  https://hal.science/hal-03123968/document


=== Conway's Game of Life

https://arxiv.org/pdf/1711.02456.pdf

Gödel = Halteproblem = Conway


=== Iterierte Konsistenz

* Iterierte Konsistenz, nichttrivial formal zu fassen, gibt in einem gewissen
  Sinn Vollständigkeit: https://mathoverflow.net/questions/67214/pi1-sentence-independent-of-zf-zfconzf-zfconzfconzfconzf-etc


=== Knowability

* Shapiro,
  https://sci-hub.se/https://www.sciencedirect.com/science/article/abs/pii/S0049237X08701381


=== Beispiele für unabhängige Aussagen

* Endliche Automaten deren Eigenschaften unabhängig von ZFC+X sind:
  https://hal.science/hal-01588572v1/document

* https://math.mit.edu/~poonen/papers/sampler.pdf


=== Graph minor theorem

* Der endliche Satz von forbidden minors ist definitiv nicht im Allgemeinen
  berechenbar: "On Search, Decision, and the Efficiency of Polynomial-Time
  Algorithms", Michael Fellow.

* Primzahl-Check in Polynomialzeit gegeben ERH:
  Riemann's Hypothesis and Tests for Primality, Gary Miller.


=== Beweistheoretische Härte (proof-theoretic ordinal)

* http://www1.maths.leeds.ac.uk/~rathjen/realm.pdf

* Es gibt keine Ordinalzahl α, sodass PA + Con(PA) beweistheoretisch äquivalent
  zu PA + bigcup_{β < α} TI(β) ist: Seite 9 in Rathjen.

* Anwendungen von ordinal analysis nach Rathjen:

  (1) Consistency of subsystems of classical second order
      arithmetic and set theory relative to constructive theories

  (2) reductions of theories formulated as conservation theorems

  (3) combinatorial independence results

  (4) classifications of provable functions and ordinals

* Es gibt Konservativitätsbeweise, die NICHT Interpretierung oder Übersetzung
  verwenden, sondern ordinal analysis (und nur Beweise transformieren können,
  wobei die Aussagen potenziell völlig verfremdet werden).

  Ein einfaches Beispiel ist vielleicht die Reduktion von PA auf PRA + QF-TI(ε₀).

  Gibt (laut Ulrik) auch Beispiele, wo imprädikative auf prädikative Systeme
  zurückgeführt werden.

  Mit mehr Arbeit ist dann potenziell doch wieder eine Übersetzung möglich,
  etwa von BG nach ZF oder von ACA₀ nach PA: https://www.jstor.org/stable/2267646

* PA + Incon(S) lässt sich in PA interpretieren: Habe ich gelernt vom Anhang
  von https://math.stanford.edu/~feferman/papers/reductive.pdf (hatte Ulrik
  empfohlen), dort wird auf http://matwbn.icm.edu.pl/ksiazki/fm/fm49/fm4915.pdf
  verwiesen, scheint mir Thm. 6.6 zu sein. Den Beweis dort verstehe ich nicht.
  Aber es scheint mir grob zu gehen:

  Es gilt Incon(PA) oder Con(PA). Im ersteren Fall ist N ein (class-sized)
  model von PA + Incon(PA). Im zweiteren Fall folgt Con(PA + Incon(PA)) und
  Gödels Vollständigkeitssatz (in PA ausgeführt) liefert dann ein Modell von PA + Incon(PA).

* Hamkins sagt, dass ein Axiom X gibt, sodass PA + Incon(S) + X äquikonsistent
  zu ZFC ist. (Vorletzte Folie von
  https://jdh.hamkins.org/pluralism-in-the-foundations-of-mathematics-asl-apa-nyc-january-2024/)

* wtf, PA + TI(|S|) und S zeigen dieselben arithmetischen Formeln.

  Ulrik: https://mathoverflow.net/questions/115809/arithmetic-strength-of-peano-the-howard-ordinal/115826#115826
  Pohlers, A short course in ordinal analysis, Seite 53.

* Martín hat ein schönes Skript, in dem man gut erkennt, wie es immer
  schwieriger wird, Ordinalzahlen zu definieren, und inwiefern Universen
  helfen: https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Codes.html

* Es kann sein, dass sowohl A als auch B für sich genommen predicatively
  reducible sind, aber nicht A ∧ B. Sam Sanders, Mail an fom vom3. Juli 2023,
  "Re: [FOM] The difficulty I had with Weaver's argument". Er gibt das
  Lindelöf-Lemma für Baire-Räume und die Aussage "es gibt Riemann-integrierbare
  Funktionen f, g mit f . g nicht Riemann-integrierbar" an.

* https://arxiv.org/pdf/2405.09275 Feferman-Resultat, dass man durch geeignete
  Reflektionsaxiome jede beliebige wahre Aussage beweisbar machen kann.


=== ACA_0

* ACA_0 kann formulieren, dass eine Menge X ein Wahrheitsprädikat darstellt, oder?

  Eine Zahl n soll genau dann in X liegen, wenn
  - n top kodiert und top gilt
  - n bot kodiert und bot gilt
  - n "x = y" kodiert und tatsächlich x = y ist
  - n "∀x. φ(x)" kodiert und für alle x₀ die Zahl "φ(x₀)" in X liegt
  - etc.

* Sei ψ(n) die Aussage, dass es ein Wahrheitsprädikat für Σ⁰ₙ-Formeln gibt.

  Dann kann ACA₀ zeigen, dass ψ(0) und ∀n. ψ(n) ⇒ ψ(n+1).
  (https://www.andrew.cmu.edu/user/avigad/Talks/survey1.pdf#page=10)

  ACA kann damit ∀n. ψ(n) und so die Existenz eines allgemeinen
  Wahrheitsprädikats und so die Konsistenz von PA zeigen.

  ACA₀ kann damit, für jedes Numeral n, polynomiell lange Beweise von Con(IΣ⁰ₙ)
  führen. Aber PA braucht dafür exponentiell lange Beweise.

* https://www.sas.upenn.edu/~htowsner/prooftheory/ReverseMath.pdf

* https://www.uni-goettingen.de/de/document/download/07769c2a15f0bfbc24991e7dac4ada66.pdf/Gentzen.pdf
  Seite 39, dort wird Simpson zitiert: "The proof-theoretic ordinal of Π¹₁-CA₀
  is too complicated to describe here, but we briefly explain why"


=== Fan-Theorem

* Rein kombinatorische/induktive Formulierung von Fridlender:
  https://www.brics.dk/RS/98/39/BRICS-RS-98-39.pdf

  Siehe auch https://fpfm.github.io/Slides_Larchey-Wendling.pdf.

  Wenn ich das richtig verstehe, ist es ∇ T Q xs ⇒ ∇ T° ∀Q (xs ∷ []).


=== Ultrafinitismus

* Die Relation "x^y = z" ist Δ₀-definierbar:
  https://dml.cz/bitstream/handle/10338.dmlcz/106264/CommentatMathUnivCarol_024-1983-4_8.pdf

* φ(2 ⇑ 2 ⇑ 4) ist mit einem übersichtlichen Beweis etablierbar;
  φ(2 ⇑ 2 ⇑ 5) nicht. (Nelson, Seite 85. Dabei φ ein neues Prädikat ohne
  Induktionsprinzip, das aber die Voraussetzungen von Induktion erfüllt.)

* Zeigt prädikative Arithmetik σ(n), so zeigt sie auch σ(Sn). Dabei besagt σ(n)
  etwas zur Existenz von Potenztürmen mit n als Basis. Aber prädikative
  Arithmetik zeigt nicht die Implikation σ(n) ⇒ σ(Sn). Nur unter der
  Zusatzforderung ∀n. ε(n). (Seite 186.)

  Nelson schlägt σ als das "ist eine Zahl"-Prädikat vor. (Aber auch φ hat er
  schon diesen Namen gegeben und dann hat er auch noch ein Konzept von
  "Endlichkeit", unter das schon 80^5000 nicht fällt.)

* Nelson präzisiert: (in
  https://mathoverflow.net/questions/142669/illustrating-edward-nelsons-worldview-with-nonstandard-models-of-arithmetic)

  Eine angemessene Formalisierung von "ist eine Zahl" ist ψ ohne
  Induktionsschritt, nur als Regel.

* Kann wenn ich mag ein Funktionssymbol (^) mit den üblichen Rekursionsregel
  für Potenzierung zu Q hinzufügen und so "Exponentiation total machen". Aber
  das hilft nicht viel. Denn um Induktion simulieren zu können, muss ich ja
  Cuts bilden. Aber die sind dann nicht mehr abgeschlossen unter
  Exponentiation. Die Exponentiationsfähigkeit geht also schnell verloren.

  Umgekehrt sagt https://mathweb.ucsd.edu/~sbuss/ResearchWeb/nelson/talk.pdf#page=16:
  Kann auch (+) und (*) als untotale Relationen nehmen.

  Vermutlich dann C¹(x) definieren als: für alle y mit Cy gibt es x + y und es
  gilt C(x+y).

  Idee: Ruhig für jedes Funktionsrezept ein partielles Funktionssymbol
  einführen. Das schadet nicht. Existenz ist dann halt eine offene Frage.
  "predicative mathematics"!

* Ist es problematisch, dass wir in der Definition von C¹ & Co. unbeschränkte
  Quantifikation verwenden?

  Cuts lieber pointfree definieren? Unterraum derjenigen n wo eine geometrische
  Sequenz gilt?

* https://en.wikipedia.org/wiki/Alexander_Esenin-Volpin
  "He sketched a program for proving the consistency of Zermelo–Fraenkel set
  theory using ultrafinitistic techniques"


=== Prädikative Mengenlehre

* Können wir analog zu Nelsons Cuts für Zahlentheorie Cuts in Mengenlehre bauen?

* Powersets alleine sind noch nicht so schlimm (damit auch nicht "Prop" in Coq).
  Erst in Kombination mit comprehension (oder evtl. schon induction) wird es
  imprädikativ.


=== Type in Type

* Thierry: https://inria.hal.science/inria-00076023/document


=== Predictive mathematics

* (Idee von Josif? Oder Ulrik? Jedenfalls Dagstuhl 2024.) Lass weniger um
  Terminierung von Funktionen stressen und eher Aussagen der Form beweisen:
  Falls sie terminiert, dann gilt ...


=== Konservativität von HA^ω + AC + DC über HA

Goodman's Theorem; lässt sich schick über Realisierbarkeit + Forcing beweisen:
https://msp.org/pjm/1979/84-1/pjm-v84-n1-p01-s.pdf,
https://proofassistants.stackexchange.com/a/1729/607


=== Forcing in Typentheorie

https://www.fing.edu.uy/%7Eamiquel/publis/lics11.pdf


=== Umgang mit Inkonsistenz

Freek Wiedijk erzählte mir auf PC2024, dass sein Lieblingssystem Type in Type sei
(genauer lambda star).

Ja, darin kann man im leeren Kontext ⊥ beweisen, das System ist inkonsistent.
Aber: Kein Term vom Typ ⊥ terminiert. Gewissermaßen ist die Inkonsistenz nicht
schlimm, da sie auffällt.

Das erinnert mich an Voevodskys letzten Vortrag, in dem er eine Unterscheidung
zwischen Beweisen (in möglicherweise inkonsistenten Systemen) und tatsächlich
belastbaren Zertifikaten vorschlug.


=== Friedman's Grand Conjecture

* Widerlegt durch Karims Resultat?
  https://www.cse.chalmers.se/~coquand/centrem1.pdf#page=9 Schranken sind nicht
  primitiv rekursiv.


=== Nächste Schritte

* Kann man explizit x, y mit phi(x) != phi(y) angeben?

* http://golem.ph.utexas.edu/category/2012/12/universe_polymorphism_and_typi.html

* https://arxiv.org/pdf/1504.03380.pdf

* Inwieweit ist der Rekursionssatz eine Anwendung von Lawveres Fixpunktsatz?
  https://mathoverflow.net/a/130901/31233


=== Quellen

* https://www.logicmatters.net/resources/pdfs/godelbook/GodelBookLM.pdf
* https://www.logicmatters.net/resources/pdfs/GWT3_LM.pdf