💾 Archived View for groupoid.ch › math.gmi captured on 2020-11-07 at 00:49:13. Gemini links have been rewritten to link to archived content

-=-=-=-=-=-=-

Groupoid – Mathematics

Last edited on 24th of August 2020.

Research questions

Linear Logic

Why can’t I find (papers about) something like (full) linear predicate logic with actual predicates and not just variables? All variants of linear logic which are called “predicate linear logic” that I find, only have variables and quantifiers but no predicates as classical first-order-logic has them.

I think the following cases are possible:

I didn’t search well enough.
It is not actually a useful thing to study, I just didn’t get that fact.
The topic is too young, so nobody has written about it.

How would one formulate analysis in linear logic? Is that even possible? Mike Shulman wrote a paper “Linear logic for constructive mathematics” which goes in that direction, but the “linear logic” he develops differs greatly from the linear logic of Girard. For example in Shulman’s paper “P times P times P” is equivalent to “P times P”, where “times” is the multiplicative conjunction. This is not compatible with Girard’s linear logic where these two formulae are not equivalent.

Is it possible to develop something like HoTT in a linear logic i.e. linear type system?

Linear logic, a reference to Shulman’s paper and more on the nlab:

https://ncatlab.org/nlab/show/linear%20logic

Miscellaneous questions

Does something like “amorphous sets” exist in HoTT or the default type theory of Coq? Is a statement like “the calculus of inductive constructions (CIC) with ‘amorphous sets’ is consistent iff the CIC is consistent” true/provable?

Opinions

In Remmerts „Funktionentheorie 1“ finde ich Satz 0.6.1 bemerkenswert (Paraphrase): „Ein metrischer Raum ist genau dann zusammenhängend (d.h. nur die leere Menge und der ganze Raum sind gleichzeitig offen und geschlossen), wenn jede lokal-konstante Funktion konstant ist.“ Dieser Satz gilt auch für topologische Räume und kommt (wenn ich mich recht erinnere) in Munkres nicht vor. Dieser Satz zeigt Zusammenhang von einem anderen (für mich neuen) Blickwinkel als die „clopen“ Definition von Zusammenhang.

Offenen Mengen

Ich schrieb am 19. August 2020:

Ich finde, dass der Begriff „(nicht-zwingend-offene) Umgebung“ führt zu intuitiveren Definitionen und Aussagen in Topologie, als der Begriff der offenen Menge. Offenen Mengen sind für mich eher technisch und abstrakt. Ich denke (im Moment) „eine Menge ohne Rand“ oder „eine offene Menge ist Umgebung all ihrer Punkte“, um mir offene Mengen vorzustellen. Dafür ist es mühsamer mit Umgebungen zu arbeiten, als mit offenen Mengen, da Umgebungen nur durch ihre Eigenschaften „in der Nähe“ des ausgesuchten Punkts charakterisiert sind, während offene Mengen durch ihre Eigenschaften in all ihren Punkten charakterisiert sind.

Ich schrieb am 24. August 2020:

Ich habe noch darüber nachgedacht. Wahrscheinlich sind nicht alle Formulierungen mit „Umgebungen“ intuitiver als mit „offenen Mengen“. Z.B. Kompaktheit lässt sich vermutlich nur schwierig über Umgebungen definieren. Der Begriff der Umgebung gibt aber mindestens eine neue Sichtweise auf die Definitionen. Ich habe festgestellt, dass die oben erwähnten Vorstellungen von „offener Menge“ (Menge ohne Rand, Umgebung all ihrer Punkte) ziemlich ausreichend sind.

Z.B. für’s die Definition einer Differenzierbaren Funktion „f : U → V“ ist es wichtig, dass der Definitionsbereich offen ist. Aber für die Definition der Differenzierbarkeit in einem Punkt „x_0“ würde es genügen, dass „U“ eine Umgebung von „x_0“ ist.

Dieser Abschnitt ist wohl viel heisse Luft um ein kleines Problem.