En lógica matemática , un juicio (o sentencia ) o aserción es una afirmación o enunciado en un metalenguaje . Por ejemplo, los juicios típicos en lógica de primer orden serían que una cadena es una fórmula bien formada , o que una proposición es verdadera . De manera similar, un juicio puede aseverar la ocurrencia de una variable libre en una expresión del lenguaje objeto, o la demostrabilidad de una proposición . En general, un juicio puede ser cualquier aserción definible inductivamente en la metateoría .
Los juicios se utilizan para formalizar sistemas de deducción : un axioma lógico expresa un juicio, las premisas de una regla de inferencia se forman como una secuencia de juicios y su conclusión también es un juicio (por lo tanto, las hipótesis y las conclusiones de las pruebas son juicios). Un rasgo característico de las variantes de los sistemas de deducción de estilo Hilbert es que el contexto no cambia en ninguna de sus reglas de inferencia, mientras que tanto la deducción natural como el cálculo consecuente contienen algunas reglas que cambian el contexto. Por lo tanto, si solo nos interesa la derivabilidad de tautologías , no los juicios hipotéticos, entonces podemos formalizar el sistema de deducción de estilo Hilbert de tal manera que sus reglas de inferencia contengan solo juicios de una forma bastante simple. Lo mismo no se puede hacer con los otros dos sistemas de deducción: como el contexto cambia en algunas de sus reglas de inferencia, no se pueden formalizar de modo que se puedan evitar los juicios hipotéticos, ni siquiera si queremos usarlos solo para probar la derivabilidad de tautologías.
Esta diversidad básica entre los diversos cálculos permite tal diferencia que el mismo pensamiento básico (por ejemplo, el teorema de deducción ) debe probarse como un metateorema en un sistema de deducción de estilo Hilbert, mientras que puede declararse explícitamente como una regla de inferencia en la deducción natural .
En la teoría de tipos se utilizan algunas nociones análogas a las de la lógica matemática (lo que da lugar a conexiones entre los dos campos, por ejemplo, la correspondencia Curry-Howard ). La abstracción de la noción de juicio en la lógica matemática también se puede aprovechar en la base de la teoría de tipos.