Speaker: Konrad Zdanoski
Institute of Mathematics
Polish Academy of Science

Title: On the second order intuitionistic propositional logic without
universal quantifier

We examine the second order intuitionistic propositional logic,
${\rm IPC}^2$.
Let $\cF_\exists$ be the set of formulas  with only existential
quantification.
We prove Glivenko's theorem for the formulas in $\cF_\exists$
that is, for $\vp\in\cF_\exists$, $\vp$ is a classical tautology
if and only if $\neg\neg\vp$ is a tautology of ${\rm IPC}^2$.
We show that for each sentence $\vp\in\cF_\exists$ (without
free variables), $\vp$ is a classical tautology
if and only if $\vp$ is an intuitionistic tautology.
As a corollary we obtain a semantical argument that
the quantifier $\forall$ is not definable in ${\rm IPC}^2$
from $\bot, \disj, \conj, \rightarrow, \exists$.