Se 
é uma fórmula, 
um termo, e 
uma variável, então
é a fórmula que se obtém de substituindo todas as ocorrências livres de
por . A substituição é
válida se nenhuma variável de ocorrer
muda em .
Regra da Eliminação Universal, E.U., 
: Se é uma fórmula, um termo, e uma variável, então
deduz-se de 
se a
substituição de por em
for válida. De forma equivalente: 
se a substituição de por em for válida. Ou ainda: se
é um conjunto de fórmulas e 
então 
, se a substituição de
por em for válida.
Se é uma fórmula numa prova, uma
variável diz-se marcada em
se é uma premissa e
é livre em , ou existe uma
premissa 
na qual
ocorre livre e que é utilizada na dedução de .
Regra da Generalização Universal, G.U., 
: Se é uma fórmula e é uma variável, então deduz-se
de se não é uma
variável marcada em . De forma equivalente: se
é um conjunto de fórmulas e 
então se não
ocorrer livre em .