Resumen: Este artículo tiene como objetivo examinar la correspondencia entre teoría de la prueba y teoría de modelos en la lógica clásica de primer orden en relación con sus metateoremas. Aunque algunos metateoremas reciben una formulación exclusivamente sintáctica o semántica, pretendemos mostrar que debido al teorema de completud estos metateoremas pueden formularse de ambas maneras. No solamente pretendemos mostrar que esta hipótesis es cierta, sino también presentaremos una discusión detallada de las formulaciones sintácticas y semánticas para los casos de los teoremas de compacidad e interpolación. Concluiremos que esos teoremas están íntimamente conectados con el teorema de completud y el teorema de Henkin, y ese hecho se puede confirmar a través de un análisis de las pruebas de completud, tanto de la basada en el teorema de Henkin como las que parten de compacidad e interpolación.

Abstract: This paper1 aims to examine the correspondence between proof theory and model theory in classical first-order logic in relation to its metatheorems. Although some metatheorems usually receive an exclusively syntactic or semantic formulation, we aim to show that due to the completeness theorem, metatheorems can be formulated in both ways. Not only do we intend to show that this hypothesis holds, but we will also present a detailed discussion of syntactic and semantic formulations for the cases of the compactness and interpolation theorems. We will conclude that these theorems are closely connected to the completeness theorem and Henkin’s theorem, and this fact can be confirmed by an analysis of proofs of completeness, be it the one based on Henkin’s theorem or the ones based on compactness and interpolation.