Dedução Natural de Primeira Ordem

$$H⊢p$$

As fórmulas da LPO estendem as proposições.

Há quatro tipos de fórmulas: igualdades, conectivos, relações e quantificadores.

• As regras dos conectivos são as da lógica proposicional.
• As regras das relações são específicas de cada domínio.
• As regras da igualdade e dos quantificadores são independentes do domínio.

Dado que as conectivos têm as regras da lógica proposicional e as regras para as relações dependem de cada domínio, restam as regras de dedução da igualdade e dos quantificadores

Continua-se a usar:

• As regras da DNP.
• O símbolo $⊢$.
• As provas em tabela.

Vão-se acrescentar:

• Regras para a igualdade e para os quantificadores.