[...]
Logiikan tarkoitus on antaa tarpeeksi voimakas (= paljon tuloksia
tuottava) uudelleenkirjoitussäännöstö, jotta kaikki muut teoriat voi
esittää logiikan määrittämän kielen lauseina ja johdella niiden
seuraukset logiikan säännöillä. säännöillä
([todistus]). Tyypillisesti logiikan ainoa varsinainen
uudelleenkirjoitussääntö on ''modus ponens'' (MP) niin sanottujen
sievennyssääntöjen lisäksi: MP kertoo, että ilmauksesta (and ''q''
(suff ''p'' ''q'')) voidaan johtaa ilmaus ''p''. Kaikki muut
uudelleenkirjoitukset määritetään suff-ilmauksina ("implikaatioina").
Esimerkiksi luonnollisten lukujen epäaito pienemmyysjärjestys voidaan
määrittää seuraavana ensimmäisen asteen predikaattilogiikan (FOL)
ilmauksena: (forall (''x'' ''y'') (and (<= 0 ''y'') (suff (<= (succ
''x'') (succ ''y'')) (<= ''x'' ''y'')))). Aito voidaan taas määrittää
tämän perusteella seuraavasti: (forall (''x'' ''y'') (suff (< ''x''
''y'') (<= ''x'' ''y'') (not (<= ''y'' ''x'')))).
[...]