You are not logged in | Log in

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.