Re: Intuitionistic second order propositional logic: Any sources?

Jan Burse <janburse@xxxxxxxxxxx> writes:

Dear All

It seems that intuitionistic logic, when equipped
with quantifiers that range over propositional
variables, becomes classical.

Because we can define:

f= forall p p
Etc..

why would that make the logic become classical?

Anybody knows approaches to second order propositional
logic which does not collapse this way?

Dana Scott, I think, showed hoe to define the propositional connectives
in this context from a small number of primitives (the propositional
connectives are mostly not interdefinable in the usual case).

Best Regards

--
Alan Smaill
.