Die Mathe-Redaktion - 25.11.2017 06:22 - Registrieren/Login
Auswahl
Schwarzes Brett
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 oder den Newsletter bestellen.

Der Newsletter Okt. 2017

Für Mitglieder
Mathematisch für Anfänger
Wer ist Online
Aktuell sind 311 Gäste und 1 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: 913
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: in der letzten Woche
Dabei seit: 09.11.2016
Mitteilungen: 7
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: 913
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: in der letzten Woche
Dabei seit: 09.11.2016
Mitteilungen: 7
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
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 218
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, eingetragen 2017-11-09 17:12


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: 3070
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.5, eingetragen 2017-11-09 17:21


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
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 218
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.6, eingetragen 2017-11-11 12:56


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: in der letzten Woche
Dabei seit: 09.11.2016
Mitteilungen: 7
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.7, eingetragen 2017-11-12 21:09


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: in der letzten Woche
Dabei seit: 09.11.2016
Mitteilungen: 7
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.8, eingetragen 2017-11-12 21:23


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: 3070
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.9, eingetragen 2017-11-12 21:56


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: in der letzten Woche
Dabei seit: 09.11.2016
Mitteilungen: 7
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.10, eingetragen 2017-11-12 22: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
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 218
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.11, eingetragen 2017-11-12 22:18


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
asdfusername
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 18.03.2017
Mitteilungen: 218
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.12, eingetragen 2017-11-12 22:23


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
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-2017 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]