Tengo problemas para entender la prueba del primer lema de la sección del teorema de Herbrand del libro. La prueba del lema comienza con una fórmula existencial cerrada A y demuestra que A es un teorema si T [ $\neg$ B ] es incoherente, donde B es la matriz de A . Entonces invoca el teorema de consistencia (que establece que una Teoría abierta T es inconsistente si existe una cuasi-tautología que es una disyunción de negaciones de instancias de axiomas no lógicos de T ) como una cadena para demostrar el lema. Pero para usar eso, ¿no debería $\neg$ B sea un axioma no lógico de T ? y esto no puede ser ni siquiera un caso, ya que el lema establece que T es una teoría sin axiomas no lógicos.
Aquí es donde echo un vistazo para ayudarme a entender el argumento. En esta prueba se adopta la misma técnica.
