Logica e metalogica
In un certo senso, la logica deve essere identificata con il calcolo predicato del primo ordine, il calcolo in cui le variabili sono confinate agli individui di un dominio fisso, sebbene possa includere anche la logica dell'identità, simboleggiata "=", che prende le proprietà ordinarie dell'identità come parte della logica. In questo senso Gottlob Frege ha raggiunto un calcolo formale della logica già nel 1879. A volte la logica è interpretata, tuttavia, includendo anche calcoli di predicati di ordine superiore, che ammettono variabili di tipo superiore, come quelli che vanno oltre i predicati (o classi e relazioni) e così via. Ma poi è un piccolo passo verso l'inclusione della teoria degli insiemi e, di fatto, la teoria degli insiemi assiomatici è spesso considerata parte della logica. Ai fini di questo articolo, tuttavia, è più appropriato limitare la discussione alla logica nel primo senso.
È difficile separare i risultati significativi della logica da quelli del metalogico, perché tutti i teoremi di interesse per i logici riguardano la logica e quindi appartengono al metalogico. Se p è un teorema matematico, in particolare uno sulla logica, e P è la congiunzione degli assiomi matematici impiegati per dimostrare p, allora ogni p può essere trasformato in un teorema, "non-P o p", in logica. La matematica non si realizza, tuttavia, eseguendo esplicitamente tutti i passaggi formalizzati nella logica; la selezione e la comprensione intuitiva degli assiomi è importante sia per la matematica che per la metamatematica. Le effettive derivazioni logiche, come quelle effettuate appena prima della prima guerra mondiale da Alfred North Whitehead e Bertrand Russell, sono di scarso interesse intrinseco per i logici. Potrebbe quindi sembrare ridondante introdurre il termine metalogico. Nella presente classificazione, tuttavia, metalogic è concepito non solo per quanto riguarda i risultati sui calcoli logici, ma anche per gli studi sui sistemi formali e sui linguaggi formali in generale.
Un ordinario sistema formale differisce da un calcolo logico in quanto il sistema di solito ha un'interpretazione voluta, mentre il calcolo logico lascia deliberatamente aperte le possibili interpretazioni. Pertanto, si parla, ad esempio, della verità o della falsità delle frasi in un sistema formale, ma rispetto ad un calcolo logico si parla di validità (vale a dire, essendo vero in tutte le interpretazioni o in tutti i mondi possibili) e della soddisfacibilità (o avere un modello - vale a dire, essere vero in qualche particolare interpretazione). Quindi, la completezza di un calcolo logico ha un significato abbastanza diverso da quello di un sistema formale: un calcolo logico consente molte frasi in modo tale che né la frase né la sua negazione sono un teorema perché è vero in alcune interpretazioni e falso in altri, e richiede solo che ogni frase valida sia un teorema.
