Logica di ordine superiore

In matematica e logica, una logica di ordine superiore è una forma di logica dei predicati che si distingue dalla logica del primo ordine da quantificatori aggiuntivi. Una logica di ordine superiore si differenzia dai predicati più comunemente noti e dalle logiche del primo ordine consentendo la quantificazione su variabili di funzione. Questa estensione aumenta sostanzialmente l'espressività della logica e quindi la logica di ordine superiore può essere utilizzata per la specificazione formale della maggior parte dei concetti e delle teorie matematiche.

Nella logica dei predicati di primo ordine ci sono simboli per individui fissi, relazioni e funzioni su un dato universo di individui e ci sono variabili che vanno oltre gli individui, con quantificatori associati. La "logica del secondo ordine" aggiunge variabili che vanno oltre le relazioni e le funzioni sull'universo degli individui e quantificatori associati, che sono chiamati variabili e quantificatori del secondo ordine. A volte si aggiungono anche simboli per relazioni e funzioni fisse di ordine superiore tra e sulle relazioni, funzioni e individui dell'universo originario. Si possono aggiungere variabili di "terzo ordine" che spaziano su relazioni e funzioni tra e sulle relazioni, funzioni e individui dell'universo, con quantificatori associati, e così via, per produrre logiche di ordine ancora superiore. È normale utilizzare sistemi di dimostrazione per logiche di ordine superiore che includono analoghi delle regole di quantificazione di primo ordine per tutti i quantificatori.

Bibliografia

• J. Lambek, P. J. Scott "Introduction to Higher-Order Categorical Logic" 1988 Cambridge University Press ISBN 9780521356534
• Chad Brown "Automated Reasoning in Higher-order Logic" College Publications 2007 ISBN 9781904987574

Voci correlate

• Funzione di ordine superiore