The constructive negation and postintuitionism

Prelegent(ci)

Michał Gajda

Język referatu

angielski

Termin

9 maja 2025 12:15

Pokój

p. 5450

Tytuł w języku polskim

Konstruktywna negacja i postintuicjonizm

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Spróbuję w skondensowany sposób przedstawić logikę ultrafinistyczną z kwantyfikatorami
(uniwersalnym i egzystencjalnym) jako rozwinięcie wcześniejszych wników opublikowanych
w pracy
https://drops.dagstuhl.de/enti<wbr></wbr>ties/document/10.4230/LIPIcs.<wbr></wbr>TYPES.2023.5.
Oprócz kwantyfikatorów dodana zostanie również równość. Pokażę też, jak
zakodować abstrakcyjne typy danych. Na koniec przedstawię złożoność
poszukiwania dowodów oraz udowadniania uniwalencji.

---

I will attempt at a minimalist exposure of ultrafinitist logic with
quantifiers (both forall and exists), which is expansion of previous
work published in
https://drops.dagstuhl.de/enti<wbr></wbr>ties/document/10.4230/LIPIcs.<wbr></wbr>TYPES.2023.5.
Beside quantifiers, I also add equality and show how to encode abstract data types.
We will finish considering complexity of proof search and proving univalence.

---