Provability of existential quantification in intuitionistic logics

Speaker(s)

Aleksy Schubert

Affiliation

MIM

Date

Jan. 20, 2023, 12:15 p.m.

Room

room 5820

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

 

---