Loogika ja metaloogika
Ühes mõttes tuleb loogikat samastada esimese järgu predikaatkalkulaadiga, milleks on muutujad piiratud fikseeritud domeeni üksikisikutega, ehkki see võib sisaldada ka identiteediloogikat, mida sümboliseerib „=”, mis võtab identiteedi tavalised omadused loogika osana. Selles mõttes saavutas Gottlob Frege formaalse loogikaarvutuse juba 1879. aastal. Mõnikord tõlgendatakse loogikat siiski nii, et see hõlmab ka kõrgema järgu predikaatkalkule, mis võimaldavad kõrgemat tüüpi muutujaid, näiteks selliseid, mis ulatuvad predikaatidest (või klassidest ja suhetest)) ja nii edasi. Kuid siis on see väike samm setteooria kaasamiseni ja tegelikult peetakse aksioomaatilist setteooriat sageli loogika osaks. Selle artikli jaoks on siiski asjakohasem piirduda aruteluga loogikaga esimeses tähenduses.
Loogika olulisi leide on raske eristada metaloogika leidudest, sest kõik logistidele huvipakkuvad teoreemid käsitlevad loogikat ja kuuluvad seetõttu metaloogika alla. Kui p on matemaatiline teoreem - eriti üks loogika kohta - ja P on p tõestamiseks kasutatud matemaatiliste aksioomide konjunktsioon, siis saab iga p muuta loogikas teoreemiks, “kas mitte-P või p”. Matemaatikat ei tehta siiski kõigi loogika vormis vormistatud sammude selgesõnalise sooritamisega; aksioomide valik ja intuitiivne mõistmine on olulised nii matemaatika kui ka metamaatika jaoks. Loogika tegelikud tuletised, näiteks need, mille Alfred North Whitehead ja Bertrand Russell tegid vahetult enne Esimest maailmasõda, pakuvad logistidele vähe sisemist huvi. Seetõttu võib termini metaloogika kasutuselevõtt osutuda ülearuseks. Käesolevas klassifikatsioonis on metaloogika aga mõeldud käsitlema mitte ainult loogiliste arvutuste tulemusi, vaid ka formaalsete süsteemide ja formaalsete keelte uurimist üldiselt.
Tavaline formaalne süsteem erineb loogilisest arvutusest selle poolest, et süsteemil on tavaliselt ette nähtud tõlgendus, samas kui loogiline arvutus jätab teadlikult võimalikud tõlgendused lahtiseks. Nii räägitakse näiteks lausete tõesusest või valedest formaalses süsteemis, loogilise arvutuse osas aga räägitakse kehtivusest (st tõesuse esinemisest kõigis tõlgendustes või kõigis võimalikes maailmades) ja rahuldatavusest (või mudeli omamine - st mingis konkreetses tõlgenduses tõele vastamine). Seega on loogilise arvutuse täielikkusel üsna erinev tähendus kui formaalsel süsteemil: loogiline arvutus lubab paljusid lauseid, nii et lause ega selle eitus pole teoreem, kuna see on mõnes tõlgenduses tõene ja teistes vale, ja see nõuab ainult seda, et iga kehtiv lause oleks teoreem.
