En particular, las lógicas infinitarias pueden no ser compactas o completas.
Las nociones de compacidad e integridad que son equivalentes en la lógica finitaria a veces no lo son en las lógicas infinitas.
Este artículo abordará las lógicas infinitarias de tipo Hilbert, ya que han sido ampliamente estudiadas y constituyen las extensiones más directas de la lógica finitaria.
Sin embargo, estas no son las únicas lógicas infinitarias que se han formulado o estudiado.
A medida que presentamos un lenguaje con fórmulas infinitamente largas, no es posible escribir explícitamente estas fórmulas.
Para evitar este problema, se utilizan varias utilidades de registro, que estrictamente hablando, no forman parte del lenguaje formal.«
En el caso donde esta notación no es clara, la longitud de la secuencia se anota más adelante.
Cuando esta notación se vuelve ambigua o confusa, sufijos como
La misma notación se puede aplicar a un cuantificador, por ejemplo,
Esto pretende representar una serie infinita de cuantificadores para cada
Es usual en lógica infinitaria asumir como el axioma de elección (como se hace a menudo cuando se habla de lógica infinita), ya que esto es necesario para tener leyes sensibles de distributividad.
Al igual que en la lógica finita, una fórmula a la que se vinculan todas las variables se denomina declaración.
que obedece a las siguientes condiciones: Cada enunciado es un axioma lógico, un elemento de T o se deduce de enunciados anteriores utilizando una regla de inferencia.
Como antes, se pueden usar todas las reglas de inferencia en la lógica finitaria, junto con una más: Los diagramas de axiomas lógicos específicos de la lógica infinitaria se presentan a continuación.
Los últimos dos esquemas de axiomas requieren el axioma de elección porque algunos conjuntos deben estar bien ordenados.
La verdad de los enunciados en los modelos se define por recursión y coincidirá con la definición de lógica finitaria donde ambos se definen.
es completa si para cada sentencia S válida en cada modelo de ella existe una prueba de S. Es fuertemente completa si para cualquier teoría T, para cada sentencia S válida en T existe una prueba de S proveniente de T. Una lógica infinitaria puede ser completa sin ser fuertemente completa.
El concepto de bien fundado solo puede expresarse en una lógica que permita un número infinito de cuantificadores en una declaración individual.
Como consecuencia, muchas teorías, incluyendo la aritmética de Peano, que no puede axiomatizarse adecuadamente en lógica finitaria, puede expresarse en una lógica infinitaria adecuada.
Otros ejemplos incluyen las teorías matemáticas de que incluyen el axioma de Arquímedes o la torsión.
[cita requerida] Las tres teorías mencionadas se pueden definir sin el uso de la cuantificación infinitaria, mediante el uso de uniones infinitas.
La primera es la lógica finitaria estándar de primer orden y la segunda es una lógica infinitaria que solo permite enunciados de tamaño numerable.