Um sistema dedutivo formal para a lógica de primeira-ordem. Teorema da correção. Teorema da dedução. O teorema de Lindenbaum.

O teorema da indefinibilidade da verdade de Tarski

O primeiro teorema da completude de Gödel (versão semântica).

Notas sobre a função beta de Gödel e sobre as definições de predicados \Sigma_1 por fórmulas E-rudimentares.

Relações e funções aritmeticamente definíveis. Toda a função recursiva primitiva é aritmeticamente definível (uso do lema da função beta de Gödel).

Teorias recursivamente axiomatizáveis.

O teorema da completude de Gödel na seguinte versão abstrata: se T é uma teoria recursivamente axiomatizável da lógica de primeira ordem com igualdade, então o conjunto (dos números de Gödel) de todas as consequências de T é recursivamente enumerável.