[FOM] Compactness of second order propositional logic

Alasdair Urquhart urquhart at cs.toronto.edu
Sun Apr 26 12:13:42 EDT 2015

Classical second order propositional logic is certainly compact,
since you can use quantifier elimination to reduce any
second order formula to an equivalent formula without

If you take second order intuitionistic propositional logic to be defined
by Kripke models, with the quantifiers ranging over
increasing subsets of frames, then it is not recursively axiomatizable
(Skvortsov, APAL Volume 86, pp. 33-46).

Independently of Skvortsov, Philip Kremer proved that this logic
is recursively isomorphic to full second order classical logic
(JSL, Volume 62, pp. 529-544).  It follows that this logic
is not compact.

On Sun, 19 Apr 2015, Guillermo Badia wrote:

> Dear all,
> Are second order propositional languages compact?
> Thanks,
> Guillermo
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom

More information about the FOM mailing list