Welche Rolle spielt in der topostheoretischen Interpretation der Physik von Isham & Doering die intuitionistische Logik?

Isham & Doering haben eine Reihe von Artikeln geschrieben, die untersuchen, wie man die Physik in Topoi begründet. Nun ist die interne Logik von Topoi eine intuitionistische Logik höherer Ordnung. Welche Rolle spielt in ihrer Theorie die intuitionistische Logik? Was sind die Typen in ihrer Theorie?

Ich habe diese Frage auch auf Math.Overflow gestellt

Die Schnittmenge der Gruppe von Physikern und der Gruppe von Menschen, die die Topos-Theorie verstehen, ist klein. Ich vermute, dass Sie viel wahrscheinlicher eine gute Antwort erhalten, wenn Sie dies auf mathoverflow.net posten. Wenn Sie dies tun, verlinken Sie es bitte, da ich ihm gerne folgen möchte (soweit mein Fachwissen dies zulässt).
Es ist im Allgemeinen ein schlechter Stil, gleichzeitig auf zwei Seiten zu posten. Am besten probieren Sie zuerst eine Seite aus, und wenn sie nach ein paar Tagen nicht funktioniert, versuchen Sie es mit der anderen.
@ tpg2114: Sicher, aber wie Crowell betont, gibt es nur wenige Leute, die sowohl mit Physik als auch mit Topoi vertraut sind. In diesem Fall denke ich, dass es gerechtfertigt ist.
Welche Rolle interessiert Sie bei der ersten Frage?
Bei der zweiten Frage werden höhere Typen, wenn sie in einem Topos interpretiert werden, als Objekte im Topos interpretiert.
Auch wenn diese Frage hier im Moment nicht beantwortet werden kann, wird sie einige inspirieren, vielleicht mehr über dieses faszinierende Thema zu erfahren.
@Dorais: Es ist weniger, welche Rolle ich sehe, sondern wie sie es sehen. Ich habe versucht, die Frage selbst zu beantworten, in der Hoffnung, dass andere sie verbessern könnten.
@MoziburUllah: Das ist eine noch seltsamere Frage, da das nur die Autoren wissen. Objekte in Topoi werden verwendet, um Typen zu interpretieren, nicht umgekehrt.
@ Dorais: Aber vermutlich haben sie das Papier geschrieben, um ihre Sichtweise zu erklären. Schließlich ist die intuitionistische Logik in der Physik nicht üblich, man erwartet von ihr einen gewissen Begründungsaufwand. Ok, interpretieren ist das falsche Wort. Ich habe verstanden, dass man aus einem Topos eine Binnensprache extrahieren kann. Ein Topos enthält ein Wahrheitsobjekt, ist sprachlich etwas mit dem Wahrheitsobjekt verbunden? Oder irre ich mich hier immer noch? Isham sagt in ihrer Zeitung: „Das sollte es geben Ω was ist der sprachliche Vorläufer des Unterobjekt-Klassifikators?
@MoziburUllah: Typentheorie nicht Ω und Modelle werden von jeder kartesischen geschlossenen Kategorie und nicht nur von Topoi bereitgestellt. Einen Typ für Aussagen zu haben, ist etwas imprädikativ und daher nicht immer wünschenswert. Mehr über die Zusammenhänge zwischen Typentheorie und Kategorien erfahren Sie hier: ncatlab.org/nlab/show/type+theory
@Francois: guter Punkt, aber nur der Vollständigkeit halber beachten Sie Folgendes: Während die einfache abhängige Typtheorie nicht das syntaktische Analogon eines Unterobjektklassifizierers hat, wie Sie sagen, in der Version der intensionalen Typtheorie, die jetzt als Homotopietyptheorie bezeichnet wird ( ncatlab.org/ nlab/show/homotopy+type+theory ) eine solche "Art von Propositionen" ( ncatlab.org/nlab/show/type+of+propositions ) existiert, sogar eine "Art von Typen" existiert ( ncatlab.org/nlab/ show/type+of+types ), was die intensionsabhängige Typentheorie mit dem "Univalenz-Axiom" tatsächlich zu einer Sprache für (höhere) Topos macht.
@Urs: Ja, aber beachten Sie, dass es für jedes Universum ein anderes ist (es sei denn, Sie gehen von einer propositionalen Größenänderung aus). In der Praxis spielt dies keine große Rolle, da die typische Mehrdeutigkeit die Illusion eines Typs für Aussagen erweckt.
Ja, ich würde sogar sagen, dass es in der Praxis nicht nur egal ist, sondern dass genau das in der Praxis sowieso heimlich passiert. Alles ist so, wie es sein sollte. (Außer, dass es sehr verwirrend werden kann, in einem Physikforum in diesem Sinne über Universen zu sprechen! ;-)

Antworten (2)

Angenommen C -Algebra A , sein „ Bohr-Topos “ (siehe dort für eine Übersicht) ist der Prägarben-Topos auf seinen kommutativen Unteralgebren. Die Idee hier ist, dass, wenn wir daran denken A als Algebra der Quantenoperatoren eines quantenmechanischen Systems (zum Beispiel alle beschränkten Operatoren auf dem Hilbert-Zustandsraum eines Systems), dann entsprechen die kommutativen Unteralgebren klassisch simultanen Observablen, und eine Prägarbe auf diese ist alles, was " durch all solche "klassischen Kontexte" sondiert". Da Niels Bohr in seinen informellen Schriften die Idee propagierte, dass die Quantenmechanik, was auch immer sie ist, durch klassische Beobachtungen kommunizierbar sein sollte, wurde argumentiert, dass dies Bohrs Sicht auf die Quantenphysik formalisieren würde.

Auf jeden Fall sind die Typen in der inneren Logik des Bohr-Topos, also die Objekte des Bohr-Topos, alle "an klassischen Kontexten prüfbare Beobachtungen".

Das Hauptergebnis dieser Konstruktion kann wie folgt zusammengefasst werden: Eine klassische Observable innerhalb des Bohr-Topos ist äquivalent eine Quantenobservable on A , im Sinne einer Operatoralgebra formulierten QM. Einzelheiten finden Sie unter Kinematik eines Bohr-Topos . Dies mag sich wie ein zufriedenstellender Zustand anfühlen. Wozu das noch führen soll, ist allerdings noch nicht ganz klar.

Man sollte sich davor hüten, zu übertreiben, was Bohrs Ziele erreichen. Ob sie als „Grundlage der Physik“ dienen, müsste sich noch zeigen. Bisher dienen sie lediglich der Formalisierung von Zustandsräumen quantenmechanischer Systeme. Tatsächlich sind sie eine Möglichkeit, Hilbert-Räume so zu betrachten, dass der Begriff der Quantenobservablen natürlicher zu dem der klassischen Observablen passt.

Schon die Dynamik (z. B. Hamiltonianer) wird von Bohrs Toposen als solche nicht erfasst. Mein Student Joost Nuiten zeigte, wie man die lokalen Netze von Observablen der algebraischen QFT in Form von Garben von Bohr-Toposen auf der Raumzeit formulieren kann. Siehe Bachelorarbeit von Nuiten . Sein Hauptergebnis ist, dass die kausale Lokalität der Quantenfeldtheorie einer natürlichen Abstammungseigenschaft der Sammlung von Bohr-Toposen entspricht, die jeder offenen Teilmenge der Raumzeit zugeordnet sind.

Dies bezieht die quantenfeldtheoretische Dynamik in die Theorie der Bohr-Toposen ein. Aber auch hier ist derzeit nicht ganz klar, wohin das führen wird. Obwohl ich das interessant finde, ist es weit davon entfernt, eine Grundlage für die gesamte Physik zu sein. Es kann jedoch als topos-theoretische Formulierung von AQFT angesehen werden. So schön es ist, ob AQFT überhaupt eine Grundlage der gesamten Lorentzschen Quantenfeldtheorie ist, ist umstritten.

Wenn man wirklich Grundlagen der Physik sehen will, muss man etwas tiefer graben, würde ich sagen. Einen ziemlich detaillierten Vorschlag, wie man dabei vorgehen könnte, habe ich bei Synthetic Quantum Field Theory und in den von dort verlinkten Artikeln beschrieben.

Joost Nuiten verteidigt übrigens gerade heute seine Masterarbeit zu diesem umfassenderen Thema. Siehe bei der Masterarbeit Nuiten seine Arbeit "Cohomological quantization of local prequantum Boundary Field Theory". Darüber habe ich vor zwei Tagen beim "Geometry and Physics XI"-Workshop in Pittsburgh einen Vortrag gehalten, siehe Motivic quantization of local prequantum field theory .

Dies beschreibt eine Geschichte, in der man in der Unendlichkeits-Topos-Theorie beginnt und darin die gesamte lokale Präquantenfeldtheorie und schließlich ihre motivische Quantisierung zur lokalen Quantenfeldtheorie entdeckt. Der Beispielteil von Nuitens Dissertation zeigt, wie die gewöhnliche Quantenmechanik auf diese Weise reproduziert wird, die Quantisierung von Poisson-Mannigfaltigkeiten, von Poisson-Modell-Topologie-Strings, von Typ-II-Strings und von heterotischen Strings, wobei insbesondere die Wittener Gattungs-Partitionsfunktion der Heterotik reproduziert wird 2D-Sigma-Modell-Feldtheorie. Nicht zuletzt zeigt dies zumindest, dass es eine nicht-triviale echte Physik gibt, die von dieser Formalisierung erfasst wird.

Ich war mir daher nicht sicher, was die Verbindung zwischen Ishams & Doerings Herangehensweise an Spitters Bohrifizierung ist. Aber im Intro zu Nuitens BA-Thesis schreibt er: „Vor einem Jahrzehnt wurde von Buttereld und Isham vorgeschlagen, dass die Topos-Theorie einen besseren Rahmen für die Formulierung von so etwas wie Quantenlogik bieten könnte. Insbesondere bemerkten sie, dass es sich dabei um einen Quantenphasenraum handelt existiert nicht als gewöhnlicher topologischer Raum, sondern als Topos mit einem internen „Raum“ oder Gebietsschema.
Diese Perspektive ermöglichte es ihnen, eine geometrische Formulierung des Kochen-Specker-Theorems zu geben, die dann genau besagte, dass dieser interne Phasenraum keine globalen Punkte hatte. Davon inspiriert, haben Spitters et al. beschrieben einen Quantenphasenraum als einen Topos mit einem internen Gebietsschema unter Verwendung eines Verfahrens, das sie Bohrikation nannten.
@Mozibur, der Unterschied besteht darin, dass Isham-Doering kontravariante Funktoren auf kommutativen Subalgebren mit Einschlüssen zwischen ihnen betrachtet, während Heunen-Landsman-Spitters kovariante Funktoren betrachtet. Die grundlegenden Aussagen über Observables funktionieren in beiden Formulierungen. Sander Wolters hat die Beziehung zwischen den beiden in "A Comparison of Two Topos-Theoretic Approaches to Quantum Theory" ein wenig diskutiert arxiv.org/abs/1010.2031 . Aus Sicht von Heunen-Landsman-Spitters sind die Bohr-Topos natürlich beringte Topos ( ncatlab.org/nlab/show/ringed+topos ), was sie ...
... wodurch sie gut in den breiteren Kontext der algebraischen und höheren/abgeleiteten Geometrie passen, bei der es um die Modellierung von Räumen durch ringförmige Topos geht ( ncatlab.org/nlab/show/structured+(infinity,1)-topos ). In Nuitens Diskussion der Quantenfeldtheorie durch Bohr Topos ist es entscheidend, dass das Axiom der kausalen Lokalität als Abstiegsbedingung solcher ringförmiger Topos kodiert wird. Für diese Anwendung auf QFT tendiere ich dazu, sie zu bevorzugen, aber für grundlegende Aussagen kann man genauso gut das andere Modell verwenden.

Mit Blick auf das erste Papier in ihrer Reihe, A Topos Foundation for Physics: I. Formal Languages ​​for Physics

Bei einem geschlossenen physikalischen System ist eine Theorie dafür eine typisierte intuitionistische Logik höherer Ordnung L , was hat Σ , der Zustandsraumtyp; Und R , der Menge-Wert-Typ; und die höheren Typen sind Observables A : Σ R . Aussagen über das System sind Untertypen von Σ die eine Heyting-Algebra bilden und denen Wahrheitswerte über den Wahrheitstyp zugewiesen werden Ω , das ist die Unterobjektkennung.

Dann eine Darstellung von L in einem Topos T ist eine konkrete physikalische Theorie. Wenn der Topos T Ist S e T , reduziert sich dies auf die klassische realistische Beschreibung, in der sie Aussagen über das System erklären, die von der Booleschen Logik und nicht von der intuitionistischen Logik des Topos behandelt werden.

Sie rechtfertigen die Einführung eines Mengentyps, indem sie die Annahme kritisieren, dass Mengen realwertig sein sollten. Zur intuitionistischen Logik sagen sie in einer Fußnote:

Der Hauptunterschied zwischen Sätzen, die mit Heyting-Logik bewiesen werden, und solchen, die mit Boolescher Logik bewiesen werden, besteht darin, dass bei ersteren keine Beweise durch Widerspruch verwendet werden können. Das bedeutet insbesondere, dass man nicht beweisen kann, dass etwas existiert, indem man argumentiert, dass die Annahme, dass es nicht zu einem Widerspruch führt; stattdessen muss ein konstruktiver Beweis für die Existenz der betreffenden Einheit erbracht werden. Dies schränkt die Theoriebildung der Physik wohl nicht wesentlich ein.

Man könnte argumentieren, dass dies aus physikalischer Sicht intuitionistische Logik ist, genauso wie Physiker schnell und locker mit Kalkül und einschränkenden Argumenten spielen.