Primerjava teorije množic in teorije tipov kot temeljev matematike

delo diplomskega seminarja

Matej Jazbec (Author), Alex Simpson (Mentor)

Abstract

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.

Keywords

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

Data

Language:	Slovenian
Year of publishing:	2022
Typology:	2.11 - Undergraduate Thesis
Organization:	UL FMF - Faculty of Mathematics and Physics
Publisher:	[M. Jazbec]
UDC:	510.3
COBISS:	118531843
Views:	508
Downloads:	58
Average score:	0 (0 votes)
Metadata:

Other data

Secondary language:	English
Secondary title:	Comparison between set theory and type theory as foundations of mathematics
Secondary abstract:	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.
Secondary keywords:	mathematics;set theory;type theory;types;isomorphisms;identity type;propositions;univalence axiom;groups;sets;constructive logic;proof relevance;structure identity principle;
Type (COBISS):	Final seminar paper
Study programme:	0
Embargo end date (OpenAIRE):	1970-01-01
Thesis comment:	Univ. v Ljubljani, Fak. za matematiko in fiziko, Oddelek za matematiko, Matematika - 1. stopnja
Pages:	37 str.
ID:	15972729