Univalentiškumas, aibių teorija ir mechanizuoto įrodymo ribos
Tyrimų kontekstas
theory comparison · conditional · Patikros data 2026-10-10
Univalentiškumo principas teigia, kad kanoninis atvaizdis iš visatos tipų tapatumo į jų ekvivalentiškumą pats yra ekvivalentiškumas.
Esminės žinios
Univalentiškumo principas teigia, kad kanoninis atvaizdis iš visatos tipų tapatumo į jų ekvivalentiškumą pats yra ekvivalentiškumas. Aukštesnysis induktyvusis apskritimas įveda tašką ir kilpą bei priklausomojo eliminavimo taisykles. Tai suteikia struktūrinį pagrindą, kitokį nei ZFC aibės ir priklausymas aibei; nė viena iš šių sistemų nėra empirinė teorija, konkuruojanti dėl atitikties duomenims. Santykiniai semantiniai modeliai pagrindžia konkrečius teiginius apie neprieštaringumą, o įrodymų asistentas tikrina formalų teiginį pagal konkrečias savo aksiomas ir patikimą tikrinimo programą.
Vertės ir lygtys
idtoeqv:(A=_U B)→Equiv(A,B) is an equivalence
- U
- Konkreti univalentiška visata
- A,B
- Visatos U tipai
- Equiv(A,B)
- Ekvivalentiškumų tarp A ir B tipas
Sąlygos ir taikymo ribos
- Univalentiškumas yra papildomas principas, taikomas konkrečiai visatai, o ne bet kurios intensionaliosios tipų teorijos teorema.
- HoTT taisyklės, ZFC aksiomos ir tikroji Lean branduolio teorija yra skirtingos sistemos; Lean savaime nėra HoTT realizacija.
- Mašininė patikra nepatvirtina, kad formalizuota teorema tiksliai išreiškia numatytą neformalų teiginį.
Šaltiniai · 2
Šaltiniai
Šaltiniai išlaiko savo taikymo ribas. Vien nuoroda nepatvirtina kiekvieno teiginio patikrinimo.
Pagrindimas ir peržiūra
Autorius patikrino šį anglišką teiginį, pateiktą lygtį, jei ji yra, ir nurodytas prielaidas pagal šias šaltinių vietas: 1–3 skyrių tipų ir tapatybės taisykles, §2.10 aksiomą 2.10.3, §6.4 apskritimą ir aukštesniuosius induktyviuosius tipus; semantikos priedus; teoremos formuluotės prasmę, branduolio patikras, aksiomų auditus ir pasitikėjimą savuoju vykdymu; dabartinis puslapis patikrintas 2026 m. spalio 10 d. Patikra apsiriboja užfiksuotais teiginiais; neteigiama, kad atlikta išsami įrodymo rekonstrukcija, pakartotinis programinis įrodymo vykdymas ar užtikrinta visos literatūros aprėptis.
2026-10-10 · Autoriaus atlikta šaltinio pagrindinio teksto, teiginio, lygties ir apibrėžimo srities patikra; kiekvienos grafo sąsajos aprėptis nustatyta atskirai. Prieš užbaigiant šaką būtina atskira nepriklausoma turinio, šaltinių ir inventoriaus peržiūra.
Įrašo informacija
Nuolatinė nuoroda į šį įrašą ↗- Įrašo identifikatorius
- research-math-univalence-foundation-comparison
- Versija
- research.1
- Struktūruotas žinyno įrašas
- Podiplominis ir tyrimų žinynas