Forma prenessa

In logica matematica, una formula si dice in forma prenessa se essa è composta da una parte sinistra contenente solo quantificatori e variabili e una parte destra non contenente alcun quantificatore.

Nell'ambito della logica classica, ogni formula è equivalente ad una formula in forma prenessa. Per esempio, se $\phi$, $\psi$ e $\rho$ sono formule in cui non compare alcun quantificatore, allora alla formula:

$\forall x((\exists y\phi )\lor ((\forall z\psi )\rightarrow \rho ))$

si può associare la seguente formula in forma prenessa:

$\forall x\exists y\exists z(\phi \lor (\psi \rightarrow \rho ))$

Conversione in forma prenessa

Ogni formula del primo ordine è logicamente equivalente (all'interno della logica classica) ad una qualche formula in forma prenessa. Ci sono alcune regole di conversione che possono essere applicate ricorsivamente per convertire una formula. La regola da applicare ad un dato passo della conversione dipende dal connettivo logico che appare più esterno nella formula.

Congiunzione e disgiunzione

Le regole per congiunzione e disgiunzione stabiliscono che

$(\forall x\phi )\land \psi$ è equivalente a $\forall x(\phi \land \psi )$,

$(\forall x\phi )\lor \psi$ è equivalente a $\forall x(\phi \lor \psi )$;

e

$(\exists x\phi )\land \psi$ è equivalente a $\exists x(\phi \land \psi )$,

$(\exists x\phi )\lor \psi$ è equivalente a $\exists x(\phi \lor \psi )$.

Le equivalenze sono valide quando $x$ non appare come variabile libera in $\psi$; se vi compare, deve essere sostituita con un'altra variabile libera (che non compaia quantificata né in $\psi$ né in $\phi$).

Per esempio, nel linguaggio degli anelli,

$(\exists x(x^{2}=1))\land (0=y)$ è equivalente a $\exists x(x^{2}=1\land 0=y)$,

ma

$(\exists x(x^{2}=1))\land (0=x)$ non è equivalente a $\exists x(x^{2}=1\land 0=x)$

perché la formula a sinistra è vera in ogni anello quando la variabile libera $x$ è uguale a 0, mentre la formula a destra non ha variabili libere ed è falsa in qualsiasi anello.

Negazione

Le regole per la negazione stabiliscono che:

$\lnot \exists x\phi$ è equivalente a $\forall x\lnot \phi$

$\lnot \forall x\phi$ è equivalente a $\exists x\lnot \phi$.

Implicazione

Ci sono quattro regole per l'implicazione: due che rimuovono i quantificatori dall'ipotesi e due che li rimuovono dalla conclusione. Queste regole possono essere derivate dalle precedenti semplicemente riscrivendo l'implicazione $\phi \rightarrow \psi$ come $\lnot \phi \lor \psi$. Come nel caso delle disgiunzioni, per l'applicazione di queste regole si presuppone che una variabile quantificata in una subformula non sia presente come formula libera nell'altra subformula; in caso contrario, bisogna sostituirne tutte le occorrenze con un'altra variabile opportunamente scelta.

Le regole per rimuovere il quantificatore dall'ipotesi sono

$(\forall x\phi )\rightarrow \psi$ è equivalente a $\exists x(\phi \rightarrow \psi )$,

$(\exists x\phi )\rightarrow \psi$ è equivalente a $\forall x(\phi \rightarrow \psi )$.

Le regole per rimuovere il quantificatore dalla tesi sono

$\phi \rightarrow (\exists x\psi )$ è equivalente a $\exists x(\phi \rightarrow \psi )$,

$\phi \rightarrow (\forall x\psi )$ è equivalente a $\forall x(\phi \rightarrow \psi )$.

Esempio

Siano $\phi$, $\psi$ e $\rho$ formule senza alcun quantificatore al loro interno e supponiamo che prese a due a due non condividano nessuna variabile libera. Consideriamo la formula

$(\phi \lor \exists x\psi )\rightarrow \forall z\rho$.

Applicando ricorsivamente le regole, partendo dalle formule più interne, otteniamo la seguente sequenza di formule logicamente equivalenti:

$(\exists x(\phi \lor \psi ))\rightarrow \forall z\rho$,

$\forall x((\phi \lor \psi )\rightarrow \forall z\rho )$,

$\forall z\forall x((\phi \lor \psi )\rightarrow \rho )$.

Questa non è però la sola forma prenessa equivalente alla formula originale. Per esempio, trattando la tesi prima dell'ipotesi nell'esempio precedente, avremmo ottenuto la forma prenessa:

$\forall x\forall z((\phi \lor \psi )\rightarrow \rho )$

Logica intuizionista

Le regole per convertire una formula in forma prenessa fanno un utilizzo intenso della logica classica. In logica intuizionista, non è vero che ogni formula è equivalente ad una formula in forma prenessa. Un ostacolo è dato dal simbolo di negazione. Ma anche l'operatore "implicazione" viene trattato diversamente in logica intuizionista rispetto alla logica classica; in logica intuizionista non è infatti ridefinibile utilizzando semplicemente gli operatori di disgiunzione e negazione.

L'interpretazione BHK illustra il motivo per cui alcune formule non hanno nessuna forma prenessa equivalente in senso intuizionistico. In questa interpretazione, una dimostrazione di

$(\exists x\phi )\rightarrow \exists y\psi \qquad (1)$

è una funzione che, dati un $x$ specifico ed una dimostrazione di φ(x), produce uno specifico y ed una dimostrazione di ψ(y). In questo caso il valore di y può essere ricavato dal valore dato per x. Una dimostrazione di

$\exists y(\exists x\phi \rightarrow \psi ),\qquad (2)$

produce un singolo valore specifico di y e una funzione che converte qualsiasi dimostrazione di $\exists x\phi$ in una dimostrazione di ψ(y). Se ogni x che soddisfa φ può essere utilizzato per ricavare una y che soddisfa ψ ma nessuna tale y potrà essere ricavata senza prima conoscere una tale x, allora la formula (1) non è equivalente alla formula (2).

Le regole per convertire una formula in forma prenessa che non sono valide in logica intuizionistica sono le seguenti:

(1) $\forall x(\phi \lor \psi )$ implica $(\forall x\phi )\lor \psi$,

(2) $\forall x(\phi \lor \psi )$ implica $\phi \lor (\forall x\psi )$,

(3) $(\forall x\phi )\rightarrow \psi$ implica $\exists x(\phi \rightarrow \psi )$,

(4) $\phi \rightarrow (\exists x\psi )$ implica $\exists x(\phi \rightarrow \psi )$,

(5) $\lnot \forall x\phi$ implica $\exists x\lnot \phi$,

(x non appare come variabile libera di $\,\psi$ in (1) e (3); x non appare come variabile libera di $\,\phi$ in (2) e (4)).

Utilità della forma prenessa

Alcuni metodi di calcolo dei predicati presuppongono che tutte le formule della teoria siano in forma prenessa. Il concetto è essenziale per lo sviluppo della gerarchia aritmetica e della gerarchia analitica.

La dimostrazione che Gödel ha dato del suo teorema di completezza per le logiche del primo ordine presuppone che tutte le formule vengano riconvertite in forma prenessa.

La definizione classica di forma normale di Skolem è "una formula la cui forma prenessa contenga solo quantificatori universali".

Forma normale prenessa

Come si è visto nella regola di conversione per l'operatore di implicazione, in generale una formula può essere equivalente a diverse formule in forma prenessa. Per questo motivo, parlare di forma normale prenessa sarebbe improprio. Ciononostante, questa dicitura è piuttosto diffusa ed è in parte giustificata dal fatto che, ai fini pratici, le formule in forma prenessa equivalenti tra di loro possono essere considerate uguali, dato che differiscono solo per l'ordine in cui sono disposti alcuni quantificatori universali (o esistenziali) consecutivi. In altre parole, le seguenti formule:

• $\forall x\forall y\phi$
• $\forall y\forall x\phi$

vengono considerate uguali, così come le seguenti:

• $\exists x\exists y\phi$
• $\exists y\exists x\phi$

Non a caso, in matematica sono comuni le grafie $\exists x,y(\phi )$ e $\forall x,y(\phi )$, in cui vengono quantificate "contemporaneamente" più variabili.

Bibliografia

• Hinman, P., Fundamentals of Mathematical Logic, A K Peters, 2005, ISBN 1-56881-262-0.

Collegamenti esterni

• (EN) prenex normal form, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
• (EN) Eric W. Weisstein, Forma prenessa, su MathWorld, Wolfram Research.