Logikk og metallogikk
På en måte skal logikk identifiseres med predikatberegningen for den første ordren, kalkulaturen der variablene er begrenset til individer med et fast domene - selv om det også kan omfatte identitetens logikk, symbolisert "=," som tar de ordinære egenskapene til identitet som en del av logikken. I denne forstand oppnådde Gottlob Frege en formell beregning av logikk allerede i 1879. Noen ganger blir logikk imidlertid tolket som å inkludere også høyere ordens predikatberegninger, som innrømmer variabler av høyere typer, for eksempel de som strekker seg over predikater (eller klasser og relasjoner) og så videre. Men så er det et lite skritt til inkludering av settteori, og faktisk blir aksiomatisk settteori ofte sett på som en del av logikken. For formålene med denne artikkelen er det imidlertid mer hensiktsmessig å begrense diskusjonen til logikk i første forstand.
Det er vanskelig å skille ut betydelige funn i logikken fra de i metalogic, fordi alle teorier av interesse for logikere handler om logikk og derfor tilhører metalogic. Hvis p er et matematisk teorem - spesielt en om logikk - og P er forbindelsen til de matematiske aksiomene som er brukt for å bevise p, kan hver p omgjøres til et teorem, "enten ikke-P eller p," i logikk. Matematikk gjøres imidlertid ikke ved å utføre eksplisitt alle trinnene som formalisert i logikk; valg og intuitiv forståelse av aksiomene er viktig både for matematikk og for metamatematikk. Faktiske derivasjoner i logikk, slik som de som ble utført rett før første verdenskrig av Alfred North Whitehead og Bertrand Russell, er av liten egeninteresse for logikere. Det kan derfor virke overflødig å introdusere begrepet metalogic. I den nåværende klassifiseringen er imidlertid metalogic tenkt som ikke bare å gjøre med funn om logiske beregninger, men også studier av formelle systemer og formelle språk generelt.
Et vanlig formelt system skiller seg fra en logisk kalkyle ved at systemet vanligvis har en tiltenkt tolkning, mens den logiske kalkulus bevisst lar de mulige tolkningene være åpne. Dermed snakker man for eksempel om sannhet eller falskhet av setninger i et formelt system, men med hensyn til en logisk kalkulus snakker man om gyldighet (dvs. å være sann i alle tolkninger eller i alle mulige verdener) og om tilfredshet (eller å ha en modell - dvs. være sant i en bestemt tolkning). Følgelig har fullstendigheten av en logisk kalkulus en helt annen betydning enn den for et formelt system: en logisk kalkulus tillater mange setninger slik at verken setningen eller dens negasjon er et teorem fordi det er sant i noen tolkninger og usant i andre, og det krever bare at hver gyldig setning er et teorem.
