Lógica de Predicados

Uma fórmula de primeira ordem, na lógica de predicados, afirma propriedades e relações de objetos num domínio. Termos nomeiam, predicados classificam, e ∀ e ∃ percorrem o domínio inteiro.

Tradução para ∀ e ∃, satisfação em estruturas e resolução deste tópico — e Hilbert, dedução natural, sequentes e completude nos seguintes — partem dessa fórmula.

As páginas se agrupam em quatro blocos. O primeiro contrapõe o átomo proposicional à fórmula que percorre um domínio com ∀ e ∃.

O segundo monta a gramática da cadeia e traduz o português para ∀ e ∃, inclusive a negação aninhada.

O terceiro decide quando a sentença é verdadeira numa estrutura, e quando Γ acarreta φ.

O quarto prova Γ⊨φ por refutação: converte premissas e ¬φ a cláusulas e deriva a cláusula vazia □.

Proposicional versus Predicados decide se átomos e conectivos bastam para o fato com todo ou existe. Sintaxe da Lógica de Primeira Ordem escreve ∀x(P(x)→Q(x)) ou ∃x(P(x)∧Q(x)).

Decidir se a cadeia é fórmula bem formada, e se a variável está ligada ou livre, está em Sintaxe da Lógica de Primeira Ordem. Decidir se a sentença vale na estrutura está em Semântica da Lógica de Primeira Ordem.

Γ⊨φ por modelos — todo modelo de Γ satisfaz φ — está em Semântica da Lógica de Primeira Ordem. Derivar □ de Γ∪{¬φ} por Skolem, unificação e resolução está em Prova Automática de Teoremas.

Sintaxe da Lógica de Primeira Ordem escreve o prefixo ∀∃ ou o prefixo ∃∀. Prova Automática de Teoremas troca o ∃ interno por uma função de Skolem e o ∃ externo por uma constante de Skolem.