Consequência Sintática de Primeira Ordem

$$H⊢p$$

A consequência sintática de primeira ordem é uma simples extensão da consequência sintática proposicional, com as regras de introdução e eliminação dos quantificadores e da igualdade.

De resto,

• Uma prova é uma sequência de fórmulas em que cada fórmula ou é uma hipótese ou resulta das anteriores por aplicação de uma regra.
• A expressão $H⊢p$ significa que existe uma prova da conclusão $p$ com hipóteses em $H$.

Porém, o facto da linguagem da lógica de primeira ordem ser substancialmente mais rica do que da lógica proposicional obriga a cuidados especiais com as variáveis: se foram descartadas ou se estão livres para substituições.