Kalkyyli on yksinkertaisimmillaan aksioomista ja syntaktisista päättelysäännöistä muodostuva merkkijonoihin liittyvä formaali systeemi.lähde? Aksioomat ja päättelysäännöt (tai laskusäännöt) esittävät, mitä kalkyylissä voidaan päätellä, eli ne esittävät sen, kuinka mielivaltaista lausetta on lupa käsitellä.lähde?
Yleensä vaaditaan, etteivät päättelysäännöt saa olla liian monimutkaisia ollakseen periaatteessa ihmisen käytettävissä.lähde? Tämän ajatellaan usein tarkoittavan sitä, että päättelysääntöjä voi olla vain äärellinen määrä, ja että on oltava mekaanisesti ratkaistavissa, milloin sääntöä on sovellettu oikein, milloin väärin. lähde?