Computertypentheorie für Topos-Logik
Meine Frage ist im Grunde, welche Ansätze wurden gemacht, um computerfeste Assistenten herzustellen, die mit der internen Logik eines Topos umgehen können.
Um es zu erklären: Als ich die Topos-Theorie lernte, war ich beeindruckt von der Eleganz der Mitchell-Bénabou-Sprache (der inneren Sprache eines Topos). Ich war mehr erfreut, als ich Toposes und lokale Mengen-Theorien von Bell las und herausfand, dass es möglich ist, die Topos-Logik axiomatisch aufzubauen und zur Beschreibung der Topos-Theorie zu verwenden. Obwohl ich es noch nicht gelesen habe, haben Lambek und Scott einen ähnlichen Ansatz zur Beschreibung von Topos (diesmal solche mit natürlichen Zahlenobjekten) unter Verwendung von sogenannten intuitionistischen Typentheorien (aber ich bin mir nicht sicher). Ich habe auch gehört, dass es eine abhängige Typentheorie und eine Homotopietypentheorie gibt, aber ich weiß nicht wirklich über sie Bescheid.
Bevor ich versuchte, unabhängig einen Beweisassistenten für die lokale Mengenlehre zu erstellen, wollte ich verstehen, was zuvor getan wurde. Ich habe also folgende Fragen:
(1) Sind die Theorie des abhängigen Typs und / oder die Theorie des Homotopietyps beschreibend genug, um die interne Logik eines Topos zu handhaben? Sind sie mindestens so allgemein wie die intuitionistische Typentheorie / lokale Mengenlehre, in dem Sinne, dass sie mit nicht-binären Wahrheitswerten usw. umgehen können?
(2) Wie sieht der typentheoretische Ansatz für den Umgang mit Topos-Logik aus?
(3) Welche praktische Software gibt es, um Beweise in solchen Typentheorien zu erstellen? Sollte ich nach Agda, Coq, Idris suchen? Muss ich meine eigenen schreiben?
Ich hoffe, mein Mangel an typentheoretischen Kenntnissen lässt meine Fragen nicht zu albern klingen. Ich versuche nur herauszufinden, welche Theorie ich lernen sollte, um Beweise in der Topos-Theorie auf eine Weise zu automatisieren, die von den Gemeinschaften der Leute, die computergestützte Beweise machen, und in der Typentheorie akzeptiert wird.
Antworten
(1) Ja. Die spezielle Theorie des abhängigen Typs, die man verwenden möchte, hat UIP (Uniqueness of Identity Proofs), ein Universum aller Sätze (im Sinne der Homotopie-Typ-Theorie, dh Subsingletons), das die Aussagenerweiterung erfüllt, Pushouts (eine Art höherer induktiver Typ) und Satzkürzungen. Dies ist eine Art abgeschnittene Version der Homotopietypentheorie.
(2) Die oben beschriebene Typentheorie ist ein Stand der Technik. Alternativ kann man eine Logik höherer Ordnung verwenden, wie sie beispielsweise in Skizzen eines Elefanten beschrieben ist . Ich bevorzuge die Theorie abhängiger Typen, da abhängige Typen in der Mathematik natürlich vorkommen. Die Semantik und Metatheorie sind in diesem Fall jedoch schwieriger (und das Ausfüllen einiger Details ist ein Problem der aktuellen Forschung).
(3) Agda, Coq, Idris können diese Typentheorie leicht verwalten, wenn sie durch Axiome (für UIP, Propositional Extensionality usw.) angemessen erweitert werden. Die Hauptfalte ist, dass sie alle einen Turm von Universen haben, den ein beliebiger elementarer Topos möglicherweise nicht hat; Aber Sie können die größeren Universen einfach ignorieren. Sie können in einem solchen Proof-Assistenten auch in Logik höherer Ordnung argumentieren, indem Sie die abhängigen Typen einfach nicht verwenden.