delo diplomskega seminarja
Matej Jazbec (Avtor), Alex Simpson (Mentor)

Povzetek

Besedilo obravnava razlike v zasnovi teorije množic in teorije tipov kot temeljev matematike. Za vodilo nam služi primer bolj ali manj upravičenega enačenja izomorfnih matematičnih struktur, specifično grup. Osvežimo potrebno znanje teorije množic in se dlje časa posvečamo predstavitvi Martin-Löfove teorije tipov: spoznamo elementarne koncepte, kot so tipi in pravila, po katerih se vedejo, konstruktivno logiko, ki jo implicira interpretacija tipov kot izjav, ter podrobno razdelamo identične tipe, s katerimi implementiramo pojem izjavne enakosti (ki se razlikuje od trivialne sodbene). Konstruiramo tip, katerega elementi so grupe. Predstavimo tehnično konstrukcijo univalentnega tipa in vpeljemo aksiom univalentnosti, ki nam omogoča, da izomorfne matematične strukture formalno smatramo za enake. Kjer so prisotne, navajamo razlike med obravnavanima temeljnima teorijama. Navedemo klasifikacijo tipov glede na kompleksnost njihovih identičnih tipov ter izpostavimo obnašanje dveh skupin tipov analogno množicam oz. izjavam.

Ključne besede

matematika;teorija množic;teorija tipov;tipi;izomorfizmi;identični tipi;izjave;aksiom univalentnosti;grupe;množice;konstruktivna logika;relevantnost dokazov;princip strukturne identitete;

Podatki

Jezik: Slovenski jezik
Leto izida:
Tipologija: 2.11 - Diplomsko delo
Organizacija: UL FMF - Fakulteta za matematiko in fiziko
Založnik: [M. Jazbec]
UDK: 510.3
COBISS: 118531843 Povezava se bo odprla v novem oknu
Št. ogledov: 508
Št. prenosov: 58
Ocena: 0 (0 glasov)
Metapodatki: JSON JSON-RDF JSON-LD TURTLE N-TRIPLES XML RDFA MICRODATA DC-XML DC-RDF RDF

Ostali podatki

Sekundarni jezik: Angleški jezik
Sekundarni naslov: Comparison between set theory and type theory as foundations of mathematics
Sekundarni povzetek: The text treats fundamental design differences between set theoretic and type theoretic foundations, led by the more or less justified deployment of sameness in the case of isomorphic mathematical structures, specifically groups. We refresh the necessary knowledge of set theory and progress via an in-depth presentation of Martin-Löf's type theory, acknowledging elementary concepts regarding types and the rules they obey, the constructive logic implemented by the propositions as types correspondence and present the peculiar identity types, resulting in the general notion of equality. We construct the type of groups. The univalence axiom is introduced following a rather technical construction of the univalence type, enabling us to sketch a proof of the structure identity principle for the special case of groups. Remarks are given when different approaches in both foundational theories emerge. The h-level classification of types is subsequently provided together with two special subclasses from it, behaving as sets and propositions.
Sekundarne ključne besede: mathematics;set theory;type theory;types;isomorphisms;identity type;propositions;univalence axiom;groups;sets;constructive logic;proof relevance;structure identity principle;
Vrsta dela (COBISS): Delo diplomskega seminarja/zaključno seminarsko delo/naloga
Študijski program: 0
Konec prepovedi (OpenAIRE): 1970-01-01
Komentar na gradivo: Univ. v Ljubljani, Fak. za matematiko in fiziko, Oddelek za matematiko, Matematika - 1. stopnja
Strani: 37 str.
ID: 15972729