Sistem formal

Sistem formal ialah set barang-barang data niskala, yang mendefinisikan hukum-hukum sintaks dengan mana satu set simbol-simbol niskala boleh dimanipulasi.

Ia mengandungi:

suatu abjad terhad simbol-simbol (“perbendaharaan kata”)
suatu tatacara utk membentuk perkataan (“nahu”/ “tatabahasa”)
suatu set aksiom (semuanya perkataan)
suatu set terhad hukum deduksi (dengan mana suatu set perkataan tambahan boleh dideduksi daripada suatu set yang diberi):

u₁ & u₂ & … & u_p → w₁ & w₂ & … & w_n

Bukti

Ini merupakan jujukan terhad perkataan-perkataan M₁ , M₂ , … , M_r di mana M_i adalah samada aksiom, atau M_j → M_i, dengan j < i.

Teorem

Teorem ialah perkataan t yang mana wujud bukti dengan M_r ≡ t. (Ini bermakna semua aksiom adalah teorem.)

Teorem di sini ialah suatu binaan sintaks semata-mata, yang membabitkan manipulasi simbol, dan tidak ada kena-mengena dengan 'kebenaran'nya.

Kebolehputusan

Diberi suatu perkataan, bolehkah ia dibuktikan sebagai teorem atau dibuktikan sebagai bukan teorem (dalam bilangan langkah terhad)? Jika ini boleh dibuat oleh sesuatu sistem formal itu, maka ia dikatakan bolehputus, dan takbolehputus jika sebaliknya.

Tafsiran (semantik)

Semantik merujuk kepada hubungan antara sistem formal dan dunia luar (yakni tafsiran makna yang diberikan kepada simbol-simbol).

Tafsiran boleh diadakan yang membabitkan nilai benar/palsu kepada perkataan-perkataan. Di sini, biasanya ingin dicari tafsiran di mana setiap teorem merupakan perkataan benar (atau dalam cakap logik, ayat benar).

Lengkap & sahih

Konsep-konsep ini membabitkan hubungan di antara sintaks dan semantik sesuatu sistem formal.

Sesuatu sistem itu dikatakan lengkap jika semua perkataan sah (ayat benar) adalah teorem. Dalam lain perkataan, setiap perkataan yang mempunyai tafsiran 'benar', boleh dibuktikan sebagai teorem secara manipulasi simbolan.

Sesuatu sistem itu dikatakan sahih jika semua teorem adalah sah. Dalam kata lain, setiap teorem yang boleh dibuktikan secara sintaks, mempunyai tafsiran semantik yang sepada dengan 'benar'.

Bagi sistem logik, yang dikehendaki ialah sistem yang lengkap dan sahih, supaya sintaksnya mencerminkan semantiknya, dan begitulah sebaliknya.