Lógica proposicional de segundo orden

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 .

• Fórmula booleana cuantificada verdadera
• Aritmética de segundo orden
• Lógica de segundo orden
• Teoría de tipos

• Parigot, Michel (diciembre de 1997). "Pruebas de normalización fuerte para la deducción natural clásica de segundo orden". Journal of Symbolic Logic . 62 (4) (publicado el 12 de marzo de 2014): 1461–1479. doi :10.2307/2275652. ISSN  0022-4812. JSTOR  2275652.