Re: Intuitionistic second order propositional logic: Any sources?

Jan Burse says...

Daryl McCullough schrieb:
Jan Burse says...
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..

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

Why do you say it becomes classical? What you don't
have is ~~A -> A from this interpretation.
In terms of f, you don't have
((A -> f) -> f) -> A

You have to fill in the "Etc..".

Someone already did.

A or B == forall C, (A -> C) -> ((B -> C) -> C)
A and B == forall C, (A -> (B->C)) -> C
false == forall C, C
not A == A -> false
(alternatively, not A can be defined as forall C, A -> C)

This logic is not classical, because you cannot prove
not (not A) -> A

--
Daryl McCullough
Ithaca, NY

.

Relevant Pages