Por que avaliações ao definir FOL?

Por que precisamos de avaliações para definir a semântica da lógica de primeira ordem? Por que não apenas defini-lo para sentenças e também definir substituições de fórmulas (da maneira esperada). Isso deve ser o suficiente:

ao invés de

É perfeitamente possível definir satisfação usando apenas frases como você sugere e, de fato, costumava ser a abordagem padrão por algum tempo.

A desvantagem deste método é que ele requer para misturar objetos semânticos em sintaxe: a fim de fazer uma definição indutiva de satisfação de sentenças em um modelo , não é suficiente para defini-lo para sentenças da língua original do M . Você precisa primeiro expandir o idioma com constantes individuais para todos os elementos do domínio M e, em seguida, definir a satisfação das sentenças no idioma expandido. Esta é, acredito, a principal razão pela qual essa abordagem entrou em desuso; se você usar avaliações, poderá manter uma distinção conceitual clara entre fórmulas sintáticas do idioma original e entidades semânticas usadas para modelá-las.$M$$M$$M$

O significado de uma fórmula fechada é um valor de verdade ou ⊤ . O significado de uma fórmula que contém uma variável livre x variando sobre um conjunto A é uma função de A para valores verdadeiros. As funções A → { ⊥ , ⊤ } formam uma álgebra booleana completa, para que possamos interpor nela a lógica de primeira ordem.$\bot$$\top$$x$$A$$A$$A \to \lbrace \bot, \top \rbrace$

Da mesma forma, um termo fechado indica um elemento de algum domínio D , enquanto um termo com uma variável livre indica uma função D → D porque o elemento depende do valor da variável.$t$$D$$D \to D$

$\phi(x_1, \ldots, x_n)$$x_1, \ldots, x_n$$D^n \to \lbrace{\bot, \top\rbrace}$$D$

$\phi(x)$$\forall x . \phi(x)$$\phi(x)$$\forall x . \phi(x)$

Para resumir:

• fórmulas com variáveis ​​livres são inevitáveis, pelo menos na lógica de primeira ordem usual,
• o significado de uma fórmula com uma variável livre é uma função de verdade ,
• $D^n \to \lbrace\bot, \top\rbrace$
• o fechamento universal de uma fórmula não é equivalente à fórmula original,
• é um erro equiparar o significado de uma fórmula ao significado de seu fechamento universal, assim como é um erro equiparar uma função ao seu codomain.

$x > 2$$x$$\pi$$x$$\pi$$x > 2$$\pi$$x$

Quero reforçar a resposta de Alexey e afirmar que a razão é que a primeira definição sofre de dificuldades técnicas , e não apenas que a segunda maneira (padrão) é mais natural.

O ponto de Alexy é que a primeira abordagem, ou seja:

$M \models \forall x . \phi \iff$$d \in M$$M \models \phi[x\mapsto d]$

combina sintaxe e semântica.

Por exemplo, vamos pegar o exemplo de Alexey:

${(0,\infty)} \models x > 2$

$(0,\infty) \models \pi > 2$

$\pi > 2$$\pi$$M$$\pi \approx 3.141\ldots$

$M\models\sqrt[15]{15,000,000} > 2$$\sqrt{}$$15$$15,000,000$

Para entender melhor, considere o que acontece quando o modelo que apresentamos tem uma estrutura mais complicada. Por exemplo, em vez de pegar números reais, use os cortes de Dedekind (uma implementação específica dos números reais).

$(A,B)$

$({q \in \mathbb Q | q < 0 \vee q^2 < 5}, {q \in \mathbb Q | 0 \leq q \wedge q^2 > 5}) > 2$$\sqrt{5}$$x > 2$

$[ x \mapsto t]: Terms \to Terms$

É possível que você consiga superar esses detalhes técnicos, mas acho que precisará trabalhar muito.

A abordagem padrão mantém a distinção entre sintaxe e semântica. O que mudamos é a avaliação, uma entidade semântica, e mantemos as fórmulas sintáticas.