The basic idea is that for purposes of testing whether a sentence is a tautology, we must treat any quantified constituent of the sentence as if it is atomic. We don't look "inside" quantified parts of the sentence. But we do pay attention to all of the truthfunctional connectives that are not in the scope of a quantifier. We'll describe a procedure for replacing the quantified and atomic constituents of a sentence with letters, A, B, C, . . . , so that the result displays all and only the truthfunctional connectives that aren't inside quantified pieces of the sentence. The result of applying this procedure is called the truth-functional form of the original sentence. The procedure has two main steps. The first annotates the sentence by labeling the constituents that we must treat as atomic, either because they are quantified or because they really are atomic. The second step replaces the underlined constituents with the sentence letters used to label them.
In LOGI la sintassi dei simboli proposizionali
prevede simboli proposizionali fra apici. Dunque è facile costruire la forma vero-funzionale;
basta racchiudere fra apici le sottoformule quantificate e atomiche non comprese nello scopo di un
quantificatore più esterno. Ad esempio la formula
∃y (P(y) ∨ R(y))
→ ∀x (P(x) ∧ Q(x))) →
(∀x (P(x) ∧ Q(x)) → ∃y (P(y) ∨ R(y))
ha forma vero-funzionale
con due simboli proposizionali: '∃y (P(y) ∨ R(y))' e '∀x (P(x) ∧ Q(x)))'.
L'uso degli apici semplifica la costruzione della forma vero-funzionale ma richiede attenzione. Due sequenze di caratteri sono eguali sse coincidono anche nella posizione e numero degli spazi bianchi, per cui bisogna usare la stessa spaziatura in tutte le occorrenze della medesima sottoformula; ad esempio, anche se '∃y (P(y) ∨ R(y))' e '∃ y (P(y) ∨ R(y))' rappresentano la stessa formula, sono simboli atomici diversi perché hanno spaziature diverse (nella seconda c'è uno spazio fra ∃ e y, mentre nella prima non ci sono spazi fra i due caratteri).