Quote:
|
Originariamente inviato da ]DaLcA[
In effetti non mi sono spiegato molto bene 
Se prima di effettuare la skolemizzazione di una formula posta in forma normale prenessa (FNP) si effettua la chiusura universale sulla FNP, la forma di Skolem uscirebbe nettamente differente dal trasformare in forma di Skolem la FNP senza i quantificatori universali davanti perché, ad esempio, si introdurrebbero lettere funzionali che senza la chiusura universale non avrebbero bisogno di esserci.
Spero che così sia più chiaro  |
Un po' più chiaro è stato
Sul Web ho trovato
questo testo, che ha il pregio di essere ASCII.
Da quanto ho capito, una formula F e la sua skolemizzata S(F) non sono equidimostrabili, ossia non è vero che i modelli di F sono tutti e soli i modelli di S(F): però sono equisoddisfacibili, ossia F ha un modello se e solo se S(F) ha un modello.
In compenso, come dicevamo prima, una formula F e la sua chiusura universale U(F) sono equidimostrabili,quindi anche equisoddisfacibili.
Per cui: dato che applicando la skolemizzazione rinunci all'equidimostrabilità ma non all'equisoddisfacibilità, direi che considerare o no la chiusura universale prima di skolemizzare non è importante, perché S(F) e S(U(F)) sono in ogni caso equisoddisfacibili. (Scrivendo "A e B sono equisoddisfacibili" come "A eqs B", hai S(F) eqs F eqs U(F) eqs S(U(F)): l'equisoddisfacibilità è ovviamente una relazione di equivalenza.)