The constructive negation and postintuitionism

Speaker(s)

Michał Gajda

Language of the talk

English

Date

May 9, 2025, 12:15 p.m.

Room

room 5450

Title in Polish

Konstruktywna negacja i postintuicjonizm

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---

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.

---