20.500.12556/RUL-138470 Primerjava teorije množic in teorije tipov kot temeljev matematike delo diplomskega seminarja Comparison between set theory and type theory as foundations of mathematics 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. 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. teorija množic teorija tipov tip izomorfizem identični tip izjave aksiom univalentnosti grupe množice konstruktivna logika relevantnost dokazov princip strukturne identitete set theory type theory type isomorphism identity type propositions univalence axiom groups sets constructive logic proof relevance structure identity principle true false false Slovenski jezik Angleški jezik Delo diplomskega seminarja/zaključno seminarsko delo/naloga 2022-07-22 08:15:02 2022-07-22 08:15:10 2024-05-29 12:21:18 0000-00-00 00:00:00 2022 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.3 123162 118531843 4455.pdf 4455.pdf 1 3126602AE142462719E19772587AF465 f61446150edeefad350a582f4ec26bd0474c0aa948ce651b15e5f5909ec51172 63734315-0985-11ed-8aca-00155dcfd717 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=158822 Fakulteta za matematiko in fiziko 0 0 0