Okay, so heute werden wir über die Komplizität des Intuitionisten reden,

wie ich es erwähnt habe.

Wir haben bereits über diese verschiedenen Notionen des Modells gesprochen.

Eine der Notionen war, was wir nennen, eine totale, vorgeorderte Ressource-Monoid.

Also, erinnern Sie sich, was das ist?

Das ist eine Monoid.

Total bedeutet einfach, dass es eine Monoid ist, wie wir es kennen und lieben.

Also, es hat eine totale Verschleimungsoperation.

Deshalb heißt es total, obwohl wir, wenn wir monoid sagen und nichts mit ihr, natürlich immer total monoid.

Und das Ding ist mehr oder weniger bestätigt oder vorbestätigt, um genau zu sein.

Es ist mit einer transitive und reflexiven Transition-Resonanzierung ausgestattet, wenn wir will.

Also, das Ding ist eine Form des Kripke-Modells. Und eigentlich, da es eine reflexive und transitive Transition-Resonanzierung ist,

ist es ein S4-Modell oder, wie wir es kennen, ein Intuitionistisches Modell.

Was uns überrascht, ist, dass wir hier eine Kombination der Semantik des Linielloge mit einer Multiplikation-Operation für eine Multiplikative Konjunktion sehen.

Und eine Vorordnung, die die additive Parten verwendet, die nur mit einer Intuitionistischen Logik aussehen.

In dem Buch, also in Tims Buch, die Semantik und die Proof-Theorie, glaube ich, von Bunch-Dimplikationen,

ist es gesagt, dass es eine komplette Semantik für Bunch-Dimplikationen gibt, solange man den Bottom auslöst.

Wir haben hier ein Übungswerk, das euch vorstellt, dass man den Bottom auslöst. Mit Bottom in der Sprache ist es nicht komplett.

Aber ohne Bottom, sagen sie, ist es komplett. Ich habe schon vor einerinhalb Wochen gesagt,

ich habe meine Wochen verpoilt, um diese Proof zu schaffen. Ich habe eine E-Mail zu Tim geschrieben und erhielt eine sehr schwere Antwort,

dass es hier etwas falsch ist und er nicht mehr sicher ist, dass das wahr ist.

Der Status des Stags hier ist sehr offen. Ich habe hier die Frage markiert. Nicht nur ist die Proof in dem Buch nicht richtig,

ich kann das nicht sehen, aber es ist auch nicht klar, ob das Ergebnis so ist.

Ich meine das nicht derisiv oder derogativ. Das passiert.

Es gibt realistische Erkenntnisse zum Eindruck, dass 40% aller kompletten mathematischen Texte falsch sind.

Während ich mir denken möchte, dass die Verteilung nicht so viel ist, wissen viele von euch, dass meine eigenen Werke Fehler haben.

Also, eine gewisse Verteilung, wenn ihr nicht so gut seid. Ja, das passiert.

Und eigentlich weiß niemand, der Ergebnis könnte trotzdem wahr sein, wir wissen es nicht.

Was tun wir? Es gibt zwei Dinge, die man machen kann, um das zu verhindern.

Einer würde das noch weiter verhindern und gehen für BI ohne den ganzen Teil des Stags,

ohne den unteren Teil, also den rechten Teil, und ohne den Binary-Join.

Das ist eher einfach, und ich glaube, dass total pre-orderte Ressorts Monoids eine komplette Semantik sind für diese weiter reduzierte Logik.

Und für eine Zeit wollte ich nur den reduzierten Klaim machen, der eigentlich ziemlich schnell zu beweisen ist und auch die ganze Session werden.

Oder ihr nehmt die Semantik.

Es ist klar, dass ihr die Semantik trotzdem ändern müsst, um einen wirklich satisfizierten Ergebnis zu bekommen.

Denn, ja, ohne den unteren Teil ist es gut und gut, aber ihr wollt nicht wirklich eine Sprache ohne den unteren Teil.

Und das wurde schon gemacht, also gibt es diese Probe in der Literatur, um das zu ändern. Tadeusz hat das schon erwähnt,

dass man das in einer P-Siege ändern muss, um die Komplizität mit dem Unteren zu bekommen.

Wir haben das nicht geproft, ich habe die Papiere nicht gelesen, die das prüfen.

Ich werde nicht explizite Gefahr darüber sprechen.

Ich werde in einem Moment illustrieren, warum ich glaube, dass es eigentlich notwendig ist, non-deterministisch zu bewegen.

Aber natürlich ist die Probe, dass das mit dem Teilen funktioniert,

ich glaube, ist viel mehr detailliert als die, dass es die totalen Pre-O-Lit-Resource-Monoids in der Buchung gibt.

Ist das richtig? Garmisch und Mehdi und Püm, sie prüfen das, oder?

Es soll die Komplizität mit dem PPRM entgegensteigen.

Okay, also es gibt noch diese Frage, die wir nicht in detail gelesen haben.

Partial bedeutet, dass wir die universalen Definiten des Monoids bewegen.

Wir können einen Schritt weiter gehen und

und non-deterministisch bewegen, die Pre-Order-Resource-Monoids.

Die Monoid-Operation ist nicht nur partial, in dem Sinne, dass sie nicht bezeichnet werden,