You are not logged in | log in

Wydział Matematyki, Informatyki i Mechaniki Uniwersytetu Warszawskiego

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

Aktualności — Wydarzenia



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.