Provability of existential quantification in intuitionistic logics

Prelegent(ci)

Aleksy Schubert

Afiliacja

MIM

Termin

20 stycznia 2023 12:15

Pokój

p. 5820

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

The type inhabitation problem, in other terminology formula provability problem, in the second-order lambda calculus with existential quantifier and arrow will be proved during the talk to be undecidable, which contrasts with the result that the second-order lambda calculus with existential quantifier, conjunction and negation is decidable. The proof of the undecidability will be done with help of the tiling puzzle technique. In addition the picture of the complexity of provability for constructive logics will be shown.

 

---