Teoria typów homotopii i twierdzenia o niekompletności Gödla

Twierdzenia Kurta Gödela o niekompletności ustanawiają „nieodłączne ograniczenia wszystkich oprócz najbardziej trywialnych systemów aksomatycznych zdolnych do wykonywania arytmetyki”.

Teoria typów homotopii stanowi alternatywną podstawę dla matematyki, podstawę jednoznaczną opartą na wyższych typach indukcyjnych i aksjomat jedności . Książka HoTT wyjaśnia, że typy są wyższe groupoids funkcje są funktory, rodziny typu są brations fi itp

Niedawny artykuł „Formalnie zweryfikowana matematyka” w CACM autorstwa Jeremy'ego Avigada i Johna Harrisona omawia HoTT w odniesieniu do formalnie zweryfikowanej matematyki i automatycznego dowodzenia twierdzeń.

Czy twierdzenia Gödela o niekompletności dotyczą HoTT?

A jeśli tak,

czy teoria typu homotopii jest naruszona przez twierdzenie Gödela o niekompletności (w kontekście formalnie zweryfikowanej matematyki)?

lo.logic type-systems homotopy-type-theory

— Sokole Oko
źródło

Interesujące pytanie. Czy czytałeś coś, co sugerowało, że HTT nie cierpi z powodu niekompletności Godela? (Zwróć uwagę, że poprzednie próby fundamentów - takie jak teoria mnogości - również cierpią z powodu niekompletności Godela ...)

— Joshua Grochow

HoTT „cierpi” oczywiście na niekompletność Gödla, ponieważ ma obliczalny język i reguły wnioskowania, i możemy sformalizować w nim arytmetykę. Autorzy książki HoTT doskonale zdawali sobie sprawę z jej niekompletności. (W rzeczywistości jest to dość oczywiste, zwłaszcza gdy połowa autorów jest pewnego rodzaju logikami).

Ale czy niekompletność „zaburza” HoTT? Nie bardziej niż jakikolwiek inny system formalny i myślę, że cała sprawa jest nieco myląca. Pozwól mi spróbować analogii. Załóżmy, że masz samochód, który nie zabierze Cię wszędzie na świecie. Na przykład nie może wspiąć się pionowo po ścianie. Czy samochód jest „uszkodzony”? Oczywiście nie może cię dostać na szczyt budynku Empire State. Czy samochód jest bezużyteczny? Daleko od tego, może zabrać Cię zbyt wiele innych interesujących miejsc. Nie wspominając o tym, że budynek Empire State ma windy.

— Andrej Bauer
źródło

Nie sądzę, że analogia samochodu całkiem działa, ponieważ pytanie nie brzmi tak: „Czy samochód jest bezużyteczny?” ale „Czy samochód może służyć jako transport fundamentowy?” Ale w każdym razie podstawową kwestią jest to, że każdy system, który będzie podstawą matematyki, jest koniecznie niekompletny.

— David Richerby

Chodzi mi o to, że ludzie nie oczekują istnienia idealnej maszyny transportowej i nie martwią się, że jej nie ma, ale jakoś martwią się tym, że żadna (rozsądna) podstawa matematyki nie jest kompletna.

— Andrej Bauer,