Decidibilità (logica) - Decidability (logic)

In logica , un problema di decisione vero/falso è decidibile se esiste un metodo efficace per derivare la risposta corretta. I sistemi logici come la logica proposizionale sono decidibili se l'appartenenza al loro insieme di formule (o teoremi) logicamente validi può essere determinata efficacemente. Una teoria (insieme di frasi chiuse sotto conseguenza logica ) in un sistema logico fisso è decidibile se esiste un metodo efficace per determinare se formule arbitrarie sono incluse nella teoria. Molti problemi importanti sono indecidibili , cioè è stato dimostrato che per essi non può esistere un metodo efficace per determinare l'appartenenza (restituire una risposta corretta dopo un tempo finito, anche se forse molto lungo in tutti i casi).

Decidibilità di un sistema logico

Ciascun sistema logico è dotato sia di una componente sintattica , che tra l'altro determina la nozione di dimostrabilità , sia di una componente semantica , che determina la nozione di validità logica . Le formule logicamente valide di un sistema sono talvolta chiamate teoremi del sistema, specialmente nel contesto della logica del primo ordine dove il teorema di completezza di Gödel stabilisce l'equivalenza della conseguenza semantica e sintattica. In altri contesti, come la logica lineare , la relazione di conseguenza sintattica (dimostrabilità) può essere utilizzata per definire i teoremi di un sistema.

Un sistema logico è decidibile se esiste un metodo efficace per determinare se le formule arbitrarie sono teoremi del sistema logico. Ad esempio, la logica proposizionale è decidibile, perché il metodo della tavola di verità può essere utilizzato per determinare se una formula proposizionale arbitraria è logicamente valida.

La logica del primo ordine non è decidibile in generale; in particolare, l'insieme delle validità logiche in ogni firma che include l'uguaglianza e almeno un altro predicato con due o più argomenti non è decidibile. Anche i sistemi logici che estendono la logica del primo ordine, come la logica del secondo ordine e la teoria dei tipi , sono indecidibili.

Le validità del calcolo dei predicati monadici con identità sono tuttavia decidibili. Questo sistema è una logica del primo ordine limitata a quelle firme che non hanno simboli di funzione e i cui simboli di relazione diversi dall'uguaglianza non accettano mai più di un argomento.

Alcuni sistemi logici non sono adeguatamente rappresentati dal solo insieme di teoremi. (Ad esempio, la logica di Kleene non ha affatto teoremi.) In tali casi vengono spesso utilizzate definizioni alternative di decidibilità di un sistema logico, che richiedono un metodo efficace per determinare qualcosa di più generale della semplice validità delle formule; per esempio, la validità delle successioni , o la relazione di conseguenza {(Г, A ) | Г ⊧ A } della logica.

Decidibilità di una teoria

Una teoria è un insieme di formule, spesso ritenute chiuse in conseguenza di conseguenze logiche . La decidibilità per una teoria riguarda se esiste una procedura efficace che decide se la formula è un membro della teoria o meno, data una formula arbitraria nella firma della teoria. Il problema della decidibilità sorge naturalmente quando una teoria è definita come l'insieme delle conseguenze logiche di un insieme fisso di assiomi.

Ci sono diversi risultati di base sulla decidibilità delle teorie. Ogni teoria inconsistente (non paraconsistente ) è decidibile, poiché ogni formula nella firma della teoria sarà una conseguenza logica della teoria e quindi un membro della teoria. Ogni teoria del primo ordine enumerabile ricorsivamente completa è decidibile. Un'estensione di una teoria decidibile potrebbe non essere decidibile. Ad esempio, ci sono teorie indecidibili nella logica proposizionale, sebbene l'insieme delle validità (la teoria più piccola) sia decidibile.

Una teoria coerente che ha la proprietà che ogni estensione coerente è indecidibile è detta essenzialmente indecidibile . In effetti, ogni estensione coerente sarà essenzialmente indecidibile. La teoria dei campi è indecidibile ma non essenzialmente indecidibile. L'aritmetica di Robinson è nota per essere essenzialmente indecidibile, e quindi ogni teoria coerente che include o interpreta l'aritmetica di Robinson è anche (essenzialmente) indecidibile.

Esempi di teorie del primo ordine decidibili includono la teoria dei campi chiusi reali e l'aritmetica di Presburger , mentre la teoria dei gruppi e l' aritmetica di Robinson sono esempi di teorie indecidibili.

Alcune teorie decidibili

Alcune teorie decidibili includono (Monk 1976, p. 234):

I metodi utilizzati per stabilire la decidibilità includono l' eliminazione del quantificatore , la completezza del modello e il test Łoś-Vaught .

Alcune teorie indecidibili

Alcune teorie indecidibili includono (Monk 1976, p. 279):

  • L'insieme delle validità logiche in qualsiasi firma del primo ordine con uguaglianza e: un simbolo di relazione di arietà non inferiore a 2, o due simboli di funzione unari, o un simbolo di funzione di arietà non inferiore a 2, stabilito da Trakhtenbrot nel 1953.
  • La teoria del primo ordine dei numeri naturali con addizione, moltiplicazione ed uguaglianza, stabilita da Tarski e Andrzej Mostowski nel 1949.
  • La teoria del primo ordine dei numeri razionali con addizione, moltiplicazione ed uguaglianza, stabilita da Julia Robinson nel 1949.
  • La teoria dei gruppi del primo ordine, stabilita da Alfred Tarski nel 1953. Sorprendentemente, non solo la teoria generale dei gruppi è indecidibile, ma anche diverse teorie più specifiche, ad esempio (come stabilito da Mal'cev 1961) la teoria dei gruppi finiti . Mal'cev ha anche stabilito che la teoria dei semigruppi e la teoria degli anelli sono indecidibili. Robinson stabilì nel 1949 che la teoria dei campi è indecidibile.
  • L'aritmetica di Robinson (e quindi qualsiasi estensione coerente, come l'aritmetica di Peano ) è essenzialmente indecidibile, come stabilito da Raphael Robinson nel 1950.
  • La teoria del primo ordine con uguaglianza e due simboli di funzione

Il metodo dell'interpretabilità viene spesso utilizzato per stabilire l'indecidibilità delle teorie. Se una teoria essenzialmente indecidibile T è interpretabile in una teoria coerente S , allora anche S è essenzialmente indecidibile. Questo è strettamente correlato al concetto di riduzione multipla nella teoria della computabilità.

semidecidibilità

Una proprietà di una teoria o di un sistema logico più debole della decidibilità è la semidecidibilità . Una teoria è semidecidibile se esiste un metodo efficace che, data una formula arbitraria, dirà sempre correttamente quando la formula è nella teoria, ma può dare una risposta negativa o nessuna risposta quando la formula non è nella teoria. Un sistema logico è semidecidibile se esiste un metodo efficace per generare teoremi (e solo teoremi) tale che ogni teorema alla fine verrà generato. Questo è diverso dalla decidibilità perché in un sistema semidecidibile potrebbe non esserci una procedura efficace per verificare che una formula non sia un teorema.

Ogni teoria o sistema logico decidibile è semidecidibile, ma in generale non è vero il contrario; una teoria è decidibile se e solo se sia essa e il suo complemento sono semidecidibili. Ad esempio, l'insieme delle validità logiche V della logica del primo ordine è semidecidibile, ma non decidibile. In questo caso, è perché non esiste un metodo efficace per determinare per una formula arbitraria A se A non è in V . Allo stesso modo, l'insieme delle conseguenze logiche di qualsiasi insieme ricorsivamente enumerabile di assiomi del primo ordine è semidecidibile. Molti degli esempi di teorie indecidibili del primo ordine dati sopra sono di questa forma.

Rapporto con la completezza

La decidibilità non deve essere confusa con la completezza . Ad esempio, la teoria dei campi algebricamente chiusi è decidibile ma incompleta, mentre l'insieme di tutte le affermazioni vere del primo ordine sugli interi non negativi nel linguaggio con + e × è completo ma indecidibile. Sfortunatamente, come ambiguità terminologica, il termine "affermazione indecidibile" è talvolta usato come sinonimo di dichiarazione indipendente .

Relazione con la calcolabilità

Come per il concetto di insieme decidibile , la definizione di una teoria o sistema logico decidibile può essere data sia in termini di metodi efficaci sia in termini di funzioni calcolabili . Questi sono generalmente considerati equivalenti per la tesi di Church . In effetti, la prova che un sistema logico o una teoria è indecidibile utilizzerà la definizione formale di computabilità per dimostrare che un insieme appropriato non è un insieme decidibile, e quindi invocherà la tesi di Church per dimostrare che la teoria o un sistema logico non è decidibile da alcun metodo (Enderton 2001, pp. 206 ss. ).

Nel contesto dei giochi

Alcuni giochi sono stati classificati in base alla loro decidibilità:

  • Gli scacchi sono decidibili. Lo stesso vale per tutti gli altri giochi a due giocatori finiti con informazioni perfette.
  • Il matto in n negli scacchi infiniti (con limitazioni su regole e pedine) è decidibile. Tuttavia, ci sono posizioni (con un numero finito di pezzi) che sono vincenti forzate, ma non si accoppiano in n per qualsiasi n finito .
  • Alcuni giochi di squadra con informazioni imperfette su un tabellone finito (ma con tempo illimitato) sono indecidibili.
  • Il gioco della vita di Conway è indecidibile.

Guarda anche

Riferimenti

Appunti

Bibliografia

  • Barwise, Jon (1982), "Introduzione alla logica del primo ordine", in Barwise, Jon (ed.), Handbook of Mathematical Logic , Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
  • Cantone, D., EG Omodeo e A. Policriti, "Teoria degli insiemi per l'informatica. Dalle procedure decisionali alla programmazione logica con gli insiemi", Monografie in Informatica, Springer, 2001.
  • Chagrov, Alessandro; Zakharyaschev, Michael (1997), Logica modale , Oxford Logic Guides, 35 , The Clarendon Press Oxford University Press, ISBN 978-0-19-853779-3, MR  1464942
  • Davis, Martin (1958), Computabilità e irrisolvibilità , McGraw-Hill Book Company, Inc, New York
  • Enderton, Herbert (2001), Un'introduzione matematica alla logica (2a ed.), Boston, MA: Academic Press , ISBN 978-0-12-238452-3
  • Keisler, HJ (1982), "Fondamenti della teoria dei modelli", in Barwise, Jon (a cura di), Manuale di logica matematica , Studi in logica e fondamenti della matematica, Amsterdam: North-Holland, ISBN 978-0-444-86388-1
  • Monk, J. Donald (1976), Logica matematica , Berlino, New York: Springer-Verlag