Nie jesteś zalogowany | zaloguj się

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

  • Skala szarości
  • Wysoki kontrast
  • Negatyw
  • Podkreślenie linków
  • Reset

Aktualności — Wydarzenia

SLIWOWICA

 

Provability of existential quantification in intuitionistic logics


Prelegent: Aleksy Schubert

2023-01-20 12:15

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.