1§. Мулоҳазалар алгебраси

Ечилиши: Исбот кетма-кетлигини қурамиз:

(1) (A ((B A)A))((A(BA))(AA)). (A2 аксиома).

(2) (A ((B A)A). (A1 аксиома).
(3) (A(BA))(AA). ((1), (2) дан MP бўйича).
(4) (A(BA)). (A1 аксиома).
(5) AA. ((3), (4) дан MP бўйича).

Шундай қилиб биз AA формула учун таърифда айтилган исбот кетма-кетлигини қура олдик. Бу кетма-кетлик (1), (2), (3), (4), (5) формулалар кетма-кетлигидан иборат. Бу ерда исбот узунлиги n5 га тенг.

L назариянинг формулаларидан ташкил топган бирор тўплам берилган бўлсин. Бу формулалар тўпламидан келтириб чиқарилувчанлик тушунчаси қуйидагича аниқланади.
Таъриф; L назариянинг A формуласи AA_n бўладиган A₁,...,A_n формулалар кетма-кетлиги мавжуд бўлиб, бунда i{1,...,n}да ҳар бир A_i ёки L нинг аксиомаси, ёки нинг формуласи, ёки ўзидан олдинги формулалардан келтириб чиқариш қоидалари ёрдамида келтириб чиқарилган бўлганда ва фақат шу ҳолда нинг формулаларининг натижаси ёки дан келтириб чиқарилган дейилади.


n сонига исбот узунлиги дейилади.

Бу A₁,...,A_n кетма-кетлик A нинг даги исботи дейилади. Бу ҳолда нинг формулалари гипотезалар дейилади.

A формула дан келиб чиқади, дейиш ўрнига ├A ёзувдан фойдаланамиз.
Агар чекли бўлса {B₁,...,B_n}├A ёзув ўрнига B_1,B₂,...,B_n ├A ёзувдан фойдаланамиз.
Масалан; A, B, A(BC)├ C ёзув C формуланинг L назарияда {A,B,A(BC)} формулалар тўпламидан келтириб чиқарилишини, шу формулаларнинг натижаси ёки шу тўпламда исботга эга эканини билдиради. Бу исботни A, B, A(BC) гипотезалардаги исбот деб айтишимиз мумкин.