Una lógica proposicional de segundo orden es una lógica proposicional extendida con cuantificación sobre proposiciones. Un caso especial son las lógicas que permiten proposiciones booleanas de segundo orden , donde los cuantificadores pueden variar ya sea justo por encima de los valores de verdad booleanos o bien por encima de las funciones de verdad con valores booleanos .
El formalismo más conocido es la lógica intuicionista con cuantificación impredicativa, Sistema F. Parigot (1997) mostró cómo este cálculo puede extenderse para admitir la lógica clásica .