La logica del primo ordine Arity definisce la decidibilità?

Question

Ho letto la logica del primo ordine è in generale indecidibile e questo potrebbe essere decidabile solo quando si lavora con operatori unari. (Penso che sia una logica proposizionale, correggimi se sbaglio)

La domanda è Perché Arity porta a problemi indecidibili?

Vorrei vedere un po 'di materiale di riferimento, o almeno un po' semplice esempio Di esso, come un modo per pensare in questo passaggio da unario a n-ary e perché porta a problemi indecidibili.

Answer 1

Logica con unaria predicati (non operatori), si chiama monadico. La cosa che si chiama proposizionale solo la logica ha noullary predicati, cioè costanti true e false, e nessun quantificatori.

Il indecidibilità della logica predicata segue perché la logica predicata (con almeno un predicato binario) è abbastanza potente da Descrivi come funziona una macchina Turing, e quindi possiamo esprimere nella logica dichiarazioni sufficientemente complicate sulle macchine Turing per ottenere indecidibilità. Al contrario, nella logica monadica, dove abbiamo solo predicati unari, non possiamo descrivere il funzionamento di una macchina Turing. Sono deliberatamente vago qui per dare un'idea senza impantanarsi nei tecnicismi.

Answer 2

Mentre Raphael indicava un commento, probabilmente stai chiedendo la decidibilità del problema di decisione classica per i frammenti della logica del primo ordine con predicati unari.

La ricerca di frammenti sintatticamente limitati della logica del primo ordine in cui la validità delle formule è decidibile è stata un campo di ricerca attivo per oltre 100 anni. È stato inteso molto presto che sono le dipendenze tra variabili che rendono difficile il problema delle decisioni. E le dipendenze sono meglio espresse quando si verificano due variabili all'interno degli argomenti di un predicato. Pertanto i predicati binari o i simboli funzionali (se si consentono di simboli funzionali) sono essenziali per l'indecidabilità.

Fu Löwenheim che nel 1915 diede una procedura decisionale per la logica del primo ordine con predicati unari. Se sei interessato, potresti trovare intrigante un documento di esposizione intitolato "Sul problema di decisione classica"Scritto da Yuri Gurevich sotto forma di un dialogo di due personaggi fittizi. Il documento è stato pubblicato per la prima volta nel Bollettino di EATCS.

L'articolo non solo introduce il problema, ma spiega come la ricerca si è sviluppata per trovare una classificazione completa di frammenti decidabili e indecidibili in termini di prefissi del quantificatore.