Die Mathe-Redaktion - 28.05.2018 12:04 - Registrieren/Login
Auswahl
ListenpunktHome
ListenpunktAktuell und Interessant ai
ListenpunktArtikelübersicht/-suche
ListenpunktAlle Links / Mathe-Links
ListenpunktFach- & Sachbücher
ListenpunktMitglieder / Karte
ListenpunktRegistrieren/Login
ListenpunktArbeitsgruppen
ListenpunktSchwätz / Top 15
ListenpunktWerde Mathe-Millionär!
ListenpunktAnmeldung MPCT Juli
ListenpunktFormeleditor fedgeo
Aktion im Forum
Suche
Stichwortsuche in Artikeln und Links von Matheplanet
Suchen im Forum
Suchtipps

Bücher
Englische Bücher
Software
Suchbegriffe:
Mathematik bei amazon
Naturwissenschaft & Technik
In Partnerschaft mit Amazon.de
Kontakt
Mail an Matroid
[Keine Übungsaufgaben!]
Impressum

Bitte beachten Sie unsere Nutzungsbedingungen, die Distanzierung, unsere Datenschutzerklärung und
die Forumregeln.

Sie können Mitglied werden. Mitglieder können den Matheplanet-Newsletter bestellen, der etwa alle 2 Monate erscheint.

Der Newsletter Okt. 2017

Für Mitglieder
Mathematisch für Anfänger
Wer ist Online
Aktuell sind 364 Gäste und 9 Mitglieder online.

Sie können Mitglied werden:
Klick hier.

Über Matheplanet
 
Zum letzten Themenfilter: Themenfilter:
Matroids Matheplanet Forum Index
Moderiert von matroid
Matroids Matheplanet Forum Index » Aktuelles und Interessantes » Garben und Logik: In Entstehung befindlich,
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule Garben und Logik: In Entstehung befindlich,
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 1215
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2017-10-25


... und keinen schlechten Eindruck machend: Lernen!



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, eingetragen 2017-10-26


Ich freue mich, wenn ich an dieser Stelle Fragen beantworten kann oder interessante Kommentare erfahre!

Die Vorlesung wird aufgezeichnet: www.youtube.com/playlist?list=PLR-3Jx6BfhkgjagoGM3Z15G0j5hv5i66v



  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 1215
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, vom Themenstarter, eingetragen 2017-10-26


Ein Kommentar (der vielleicht nicht sonderlich interessant ist, aber zur Verbesserung beitragen kann):
1. Das Kreide-Blau ist in den Aufzeichnungen eigentlich nicht vom Kreide-Weiß zu unterscheiden.
2. Man hört das Publikum nicht. Würden Fragen und dergleichen von dir kurz wiederholt, müsste man weniger raten.

Ansonsten: Weiter so!  smile



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, eingetragen 2017-10-27


Vielen Dank für die Anregung, tactac! Die Aufzeichnung der heutigen Vorlesung wird unter dem Fragenverständlichkeitsgesichtspunkt dann leider nicht optimal sein, weil es dieses Mal recht viele Fragen gab, die ich nicht wiederholt habe. Ich werde versuchen, ab dem nächsten Mal daran zu denken!



  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, eingetragen 2017-11-09


Wieso wird eine Sequenz als <math>\phi\vdash_{\dots}\psi</math> aufgefasst und nicht als <math>\Gamma\vdash_{\dots}\psi</math>, wobei <math>\Gamma</math> eine ganze Ansammlung von Voraussetzungen ist? Es kommen ja in der Mathematik durchaus manchmal mehrere Voraussetzungen vor.

EDIT: Danke, dass du deine Vorlesungen online stellst! Ist wirklich gut und hilfreich.



  Profil  Quote  Link auf diesen Beitrag Link
Triceratops
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 28.04.2016
Mitteilungen: 3606
Aus: Berlin
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.5, eingetragen 2017-11-09


Eine größere Schrift auf der Tafel würde die Qualität und das Nachvollziehen der Videos erheblich verbessern. Dies betrifft nicht so sehr die Formeln wie geschriebenen Text.

Ich hatte mir vor einigen Tagen bereits einige Videos angesehen.



  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.6, eingetragen 2017-11-11


Ingo, noch eine zweite Frage:

Kann man in einer intuitionistischen Metatheorie ein Modell von PA konstruieren?



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.7, eingetragen 2017-11-12


asdfusername: Zu deiner Frage, wieso wir links vom Turnstile nicht eine ganze (endliche) Liste von Annahmen zulassen: Das ist keine besonders tiefsinnige Entscheidung. Wo andere Leute Kommata setzen, um die einzelnen Annahmen links vom Turnstile voneinander zu trennen, schreiben wir halt das Zeichen fürs logische Und. Die beiden Kalküle sind zueinander äquivalent.

Zum Studium klassischer Systeme ist es ganz nett, links vom Turnstile Listen von Annahmen zuzulassen, weil man darauf gestoßen wird, auch rechts vom Turnstile endliche Listen von Formeln zuzulassen (vorgestellt als Disjunktion). Ein solches Vorgehen bedingt aber automatisch das Prinzip vom ausgeschlossenen Dritten.

Wenn man links vom Turnstile Listen zulässt, muss man auch einige strukturelle Regeln für deren Umgang ergänzen: etwa, dass man die einzelnen Annahmen in ihrer Reihenfolge vertauschen darf oder dass man Annahmen duplizieren darf. Dadurch, dass wir nicht Listen zulassen, entfällt dieser Zusatzbedarf an Regeln.

Diese Zusatzregeln könnte man auch dadurch vermeiden, indem man links vom Turnstile endliche Mengen statt Listen zulässt. Dann muss aber die Metatheorie mächtig genug sein, um über endliche Mengen von Formeln sprechen zu können. Das ist keine wirkliche Einschränkung, weil sogar PRA das kann – allerdings nur mittels nicht ganz trivialen Kodierungen.

Hier noch der wahre Grund, wieso ich mich gegen Listen entschieden habe: Der Elephant, die Standardreferenz zur Topostheorie, macht's genauso. Und zwar weil man in der kategoriellen Logik Formeln durch Objekte von Kategorien interpretieren kann; eine Sequenz in unserem Sinn wird dann zur Aussage, dass die Interpretation der Formel links vom Turnstile ein Unterobjekt der Interpretation der Formel rechts vom Turnstile ist. Wenn man links vom Turnstile Listen zulassen würde, müsste man diesen Zusammenhang etwas komplexere formulieren.

Beantwortet das deine Frage? Fällt dir ein Anwendungsfall ein, der für Listen spricht und den ich übersehen habe?



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.8, eingetragen 2017-11-12


Zu deiner zweiten Frage, asdfusername: Ja, kann man in einer (hinreichend infinitistischen) intuitionistischen Metatheorie ein Modell von PA konstruieren. Ein Modell von HA ist ja schnell hingeschrieben, dafür kann man einfach die Menge der natürlichen Zahlen nehmen. Diese wird aber natürlich kein Modell von PA sein.

Nun ist es aber so, dass man Modelle von formalen Systemen nicht nur im Standardtopos, dem Topos der Mengen, suchen kann, sondern auch in jedem anderen Topos. Konkret bedeutet das, dass man nicht von einem Modell fordert, eine Menge zusammen mit geeigneten Operationen zu sein, sondern erlaubt, dass ein Modell ein Objekt eines gewissen Topos zusammen mit gewissen Morphismen ist.

Wenn man diese Verallgemeinerung erlaubt, dann kann man ein Modell von PA hinschreiben. Es lebt im "kleinsten dichten Untertopos von Set", demjenigen Untertopos, der von dem Doppelnegationsoperator ausgeschnitten wird. Was all diese Begriffe bedeuten, werden wir im letzten Teil der Vorlesung kennenlernen! (Kleiner Spoiler: Eine Aussage gilt genau dann in diesem Modell von PA, wenn ihre doppelnegationsübersetzte Aussage in den natürlichen Zahlen gilt.)

Übrigens: Es gibt eine Spielart von konstruktiver Mathematik, in der man zeigen kann: Es gibt genau ein Modell von HA (bis auf Isomorphie). In einer klassischen Metatheorie ist das völlig falsch, da gibt es viele exotische Modelle von HA (und damit auch von PA). Das ist recht spannend, weil eine der großen Nachteile von Logik erster Ordnung ist, dass es stets kuriose Nichtstandardmodelle mit Geisterelementen gibt. (Andere sehen das nicht als Nachteil, sondern als wunderbares Phänomen an!) In dieser Spielart von konstruktiver Mathematik existiert dieser Sachverhalt jedenfalls nicht.



  Profil  Quote  Link auf diesen Beitrag Link
Triceratops
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 28.04.2016
Mitteilungen: 3606
Aus: Berlin
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.9, eingetragen 2017-11-12


2017-11-12 21:23 - IngoBlechschmidt in Beitrag No. 8 schreibt:
Es gibt eine Spielart von konstruktiver Mathematik, in der man zeigen kann: Es gibt genau ein Modell von HA (bis auf Isomorphie). [...]
 
Kannst du vielleicht genauer sagen, was hier mit "Spielart" gemeint ist? Stichpunkte reichen, dann google ich danach.



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.10, eingetragen 2017-11-12


Triceratops, ich bezog mich auf "rekursive Mathematik" (die "russische Schule" konstruktiver Mathematik). Dort gilt folgendes Axiom: Jede Funktion <math>\mathbb{N} \to \mathbb{N}</math> ist berechenbar (durch eine Turingmaschine).

Ein Modell für rekursive Mathematik bietet die interne Welt des effektiven Topos. Mehr dazu: Foliensatz 1, Foliensatz 2, Video

Die Erkenntnis zur angesprochenen Modelleindeutigkeit stammt von Benno van den Berg und Jaap von Oosten: Arithmetic is Categorical.



  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.11, eingetragen 2017-11-12


Vielen Dank für die ausführlichen Antworten!

2017-11-12 21:09 - IngoBlechschmidt in Beitrag No. 7 schreibt:
Wenn man links vom Turnstile Listen zulässt, muss man auch einige strukturelle Regeln für deren Umgang ergänzen: etwa, dass man die einzelnen Annahmen in ihrer Reihenfolge vertauschen darf oder dass man Annahmen duplizieren darf. Dadurch, dass wir nicht Listen zulassen, entfällt dieser Zusatzbedarf an Regeln.

Ich vermute, dass diese strukturellen Regeln unnötig sind. Denn angenommen, es gibt eine Herleitung von <math>\phi, \psi\vdash \sigma</math>, dann können wir doch sowieso genauso gut eine Herleitung für <math>\psi, \phi\vdash\sigma</math> hinschreiben.


Hier noch der wahre Grund, wieso ich mich gegen Listen entschieden habe: Der Elephant, die Standardreferenz zur Topostheorie, macht's genauso. Und zwar weil man in der kategoriellen Logik Formeln durch Objekte von Kategorien interpretieren kann; eine Sequenz in unserem Sinn wird dann zur Aussage, dass die Interpretation der Formel links vom Turnstile ein Unterobjekt der Interpretation der Formel rechts vom Turnstile ist. Wenn man links vom Turnstile Listen zulassen würde, müsste man diesen Zusammenhang etwas komplexere formulieren.

Das klingt sehr interessant. Intuitiv kann man sich <math>\phi\vdash\psi</math> ja auch so vorstellen, dass der Wahrheitswert von <math>\psi</math> mindestens so groß ist wie der von <math>\phi</math>.


Beantwortet das deine Frage? Fällt dir ein Anwendungsfall ein, der für Listen spricht und den ich übersehen habe?

Naja, auf mich wirkt es halt zunächst unnötig, dass man sozusagen zwei "Ebenen" von Annahmen hat: die, die links vom <math>\vdash</math> stehen, und die Annahmen von der Theorie <math>T</math> (die selbst wieder die Form <math>\phi\vdash\psi</math> haben). Ich finde es natürlicher, die Variante von Gentzens Kalkül zu benutzen, die mit <math>\Gamma\vdash\psi</math>, wobei <math>\Gamma</math> Menge, als Sequenzen hantiert (statt <math>\phi\vdash\psi</math>) und <math>\text{PA}</math> aufzufassen als Menge von Formeln (anstatt als Menge von Sequenzen mit jeweils Voraussetzung und Behauptung) und dann einfach <math>\text{PA}\vdash\psi</math> zu schreiben (anstatt zu sagen: "in <math>\text{PA}</math> ist <math>\top\vdash\psi</math> herleitbar").
Natürlich hat das den Nachteil, dass dann eine Sequenz ein unendliches Objekt sein kann, da ja beispielsweise <math>\text{PA}</math> unendlich viele Elemente hat.


Übrigens: Es gibt eine Spielart von konstruktiver Mathematik, in der man zeigen kann: Es gibt genau ein Modell von HA (bis auf Isomorphie).

Ist diese Spielart eine Theorie, die ein "Traumaxiom" enthält? Wenn ja, welches?

[Die Antwort wurde nach Beitrag No.8 begonnen.]



  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.12, eingetragen 2017-11-12


Noch eine Frage, die ich mir zum Thema Hydra-Spiel gestellt habe: Könnte man nicht diese Idee mit den Ordinalzahlen auch benutzen, um Collatz zu zeigen? Wurde sowas schon versucht?



  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.13, eingetragen 2017-12-10


In Vorlesung 13 steht:
<math>\Vdash (\forall x \exists y \varphi)\to\exists n (\forall x\varphi[x/x, M_n(x)/y])</math>
Ich glaube, die Formel macht keinen Sinn. Man kann Terme nur durch Terme ersetzen. Du willst hier <math>y</math> durch den Term <math>M_n(x)</math> ersetzen. Das ist aber kein Term. Aber man kann auch nicht sowas schreiben wie <math>\underline {M_n(x)}</math> und damit den Term meinen, der die Meta-Zahl <math>M_n(x)</math> repräsentiert, da <math>M_n(x)</math> nicht einmal eine Meta-Zahl ist, da <math>n</math> nur eine Variable ist, die in der Formel <math>(\forall x \exists y \varphi)\to\exists n (\forall x\varphi[x/x, M_n(x)/y])</math> vorkommt.



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.14, eingetragen 2017-12-10


2017-11-12 22:23 - asdfusername in Beitrag No. 12 schreibt:
Noch eine Frage, die ich mir zum Thema Hydra-Spiel gestellt habe: Könnte man nicht diese Idee mit den Ordinalzahlen auch benutzen, um Collatz zu zeigen? Wurde sowas schon versucht?

Grundsätzlich ist das natürlich eine Möglichkeit! Du müsstest zunächst definieren, wann Ordinalzahlen als gerade oder ungerade zählen sollen. Beachte dabei insbesondere, dass die Ordinalzahlmultiplikation nicht kommutativ ist.

Wenn man etwa definiert: "Eine Ordinalzahl ist genau dann gerade, wenn sie von der Form <math>\alpha \cdot 2</math> ist. Eine Ordinalzahl ist genau dann ungerade, wenn sie der Nachfolger einer geraden Ordinalzahl ist." Dann ist keine unendlich große Ordinalzahl gerade (und auch nicht ungerade).

Wenn man <math>2 \cdot \alpha</math> statt <math>\alpha \cdot 2</math> schreibt, dann wird es interessanter. Dann ist <math>\omega</math> gerade. Und <math>\omega + n</math> ist genau dann gerade, wenn <math>n</math> es ist. Weiter habe ich aber darüber nicht nachgedacht, ich weiß nicht, wie gut sich der Begriff verhält.



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.15, eingetragen 2017-12-10


2017-12-10 12:40 - asdfusername in Beitrag No. 13 schreibt:
In Vorlesung 13 steht:
<math>\Vdash (\forall x \exists y \varphi)\to\exists n (\forall x\varphi[x/x, M_n(x)/y])</math>
Ich glaube, die Formel macht kein Sinn. Man kann Terme nur durch Terme ersetzen. Du willst hier <math>y</math> durch den Term <math>M_n(x)</math> ersetzen. Das ist aber kein Term. Aber man kann auch nicht sowas schreiben wie <math>\underline {M_n(x)}</math> und damit den Term meinen, der die Meta-Zahl <math>M_n(x)</math> repräsentiert, da <math>M_n(x)</math> nicht einmal eine Meta-Zahl ist, da <math>n</math> nur eine Variable ist, die in der Formel <math>(\forall x \exists y \varphi)\to\exists n (\forall x\varphi[x/x, M_n(x)/y])</math> vorkommt.

Oh, gut aufgepasst! Vielen Dank für deine Anmerkung! Stimmt, das ergibt so keinen Sinn. Ist im Skript jetzt korrigiert.

Richtig müssen wir statt <math>M_n(x)</math> schreiben: <math>U(J(n,x))</math>. Dabei ist <math>U</math> die universelle Maschine, die ein (über <math>J</math> als einzelne Zahl kodierte) Paar aus zwei Zahlen <math>n</math> und <math>x</math> als Argument nimmt und die <math>n</math>-te Maschine mit Eingabe <math>x</math> simuliert.

Streng genommen ist das natürlich immer noch Notationsmissbrauch, da Heyting-Arithmetik kein Funktionssymbol für <math>U</math> (oder <math>J</math>) hat. Diesen Missbrauch kann man aber wie im Kapitel über Arithmetisierung von Syntax besprochen formalisieren: Da <math>U</math> eine partielle berechenbare Funktion ist, ist <math>U</math> in Heyting-Arithmetik (und sogar in intuitionistischer Robinson-Arithmetik) darstellbar.



  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.16, eingetragen 2017-12-14


Danke.

Kleiner Typo in den Übungsblättern:

Wie zeigt man, dass alle Funktionen, die Heyting-Arithmetik als total nachweist,
primitiv rekursiv im erweiterten Sinn Sinn



  Profil  Quote  Link auf diesen Beitrag Link
IngoBlechschmidt
Junior Letzter Besuch: vor mehr als 3 Monaten
Dabei seit: 09.11.2016
Mitteilungen: 13
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.17, eingetragen 2017-12-19


2017-12-14 19:42 - asdfusername in Beitrag No. 16 schreibt:
Kleiner Typo in den Übungsblättern:

Danke! Ist korrigiert. :-)



  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.18, eingetragen 2017-12-22


Naja, das letzte "Sinn" soll, so glaube ich, nicht komplett verschwinden, sondern durch "sind" ersetzt werden ;-)



  Profil  Quote  Link auf diesen Beitrag Link
tactac hat die Antworten auf ihre/seine Frage gesehen.
Neues Thema [Neues Thema] Antworten [Antworten]    Druckversion [Druckversion]

 


Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2018 by Matroids Matheplanet
This web site was made with PHP-Nuke, a web portal system written in PHP. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]