Мулоҳазалар ҳисоби аксиомалари

II гуруҳ аксиомалари .

II₁. A  B  A .
II₂. A  B  B .
II₃. ( A  B )  (( A  C )  ( A  B  C )).
III гуруҳ аксиомалари .
III₁. A  A  B .
III₂. B  A  B .
III₃. ( A  C )  (( B  C )  ( A  B  C )) .
IY гуруҳ аксиомалари .
IY₁. ( A  B )  (  B   A ) .
IY₂. A    A .
IY_3.   A  A .


Келтириб чиқариш қоидалари.

1. Ûрнига қûйиш қоидаси.

МҲ нинг таркибида А ûзгарувчи мулоҳаза қатнашган ℑ(А) , ҳамда иҳтиёрий ℬ формулалари берилган бûлсин. Агар ℑ ( А )

МҲ нинг келтириб чиқарилувчи (к.ч.) формуласи бûлса, у ҳолда ℑ ( ℬ ) формула ҳам МҲ нинг к.ч. формуласи бûлади.
Бу қоида қисқача сҳематик равишда ℑ( А ) кûринишда ℑ ( ℬ )
белгиланади.
2. Ҳулоса чиқариш ( Modus ponens –МР ) қоидаси.
Агар ℑ  ℬ ва ℑ формулалар МҲ нинг к.ч. формулалари бûлса, у ҳолда ℬ формула ҳам МҲ нинг к.ч. формуласидир. Бу қоида қисқача қуйидаги кûринишда белгиланади : ℑ , ℑ  ℬ
ℬ
Таъриф. 1º. Ҳар бир аксиома МҲ нинг к.ч. формуласидир.
2º. МҲ нинг к.ч. формуласига ûрнига қûйиш қоидасини қûллаш натижасида ҳосил қилинган формула МҲ нинг к.ч. формуласидир.
3º. МҲ нинг к.ч. формулаларига ҳулоса чиқариш қосдасини қûллаш натижасида ҳосил қилинган формула МҲ нинг к.ч. формуласидир.
4º. МҲ нинг бошқа к.ч. формулалари йûқ.
Таъриф. Агар формулаларнинг чекли кетма-кетлиги ℑ₁, ℑ₂, . . . , ℑ_n да ҳар бир ℑ_i ( i қ1, n ) формула ё МҲ нинг к.ч. формуласи, ё ûзидан олдинги формулалардан ûрнига қûйиш ёки ҳулоса чиқариш қоидалари ёрдамида ҳосил қилинган формулалар бûлса, у ҳолда бу кетма-кетлик оҳирги ℑ_n формуланинг формал исботи , n эса исботнинг узунлиги дейилади.
МҲ нинг аксиомалари исботининг узунлиги 1 га тенг исботланувчи формулалар сифатида қаралиши мумкин. МҲ нинг исбот узунлиги бирдан катта бûлган исботланувчи формулаларини теоремалар деб атаймиз.
« ℑ формула МҲ нинг к.ч. формуласи » деган жумлани қисқача ⊢ ℑ орқали ифодалаймиз.
Теорема. ⊢ А  А .
Исбот. +уйидаги кетма-кетликни қарайлик :

1. 
   А  ( В  А ) .
   
2. 
   ( А  ( В  А ))  (( А  В )  ( А  А )) .
   
3. 
   ( А  В )  ( А  А ) .
   
4. 
   ( А  ( В  А ))  ( А  А ) .
   
5. 
   А  А .
   
6. 
   А  А .
   

Бу кетма-кетлик А  А формуланинг формал исботи эканлигини кûриш қийин эмас. Ҳақиқатдан ҳам, А (В  А )- формула I₁ аксиома; ( А  (В  А ))  (( А  В )  (А  А ))- формула I₂ аксиомадаги С ни А билан алмаштириш натижасида ҳосил қилинган; ( А  В )  ( А  А ) формула 2-формулага МР қоидасини қûллаш натижасида ҳосил қилинган; ( А  ( В  А ))  ( А  А ) формула ûзидан олдинги формулада В ни В  А формула билан алмаштириш натижасида ҳосил қилинган; А  А формула 4 – формулага МР қоидасини қûллаш натижасида ҳосил қилинган; А  А формула А ни А билан алмаштириш натижасида ҳосил қилинган.
Бундан кейин МҲ нинг к.ч. формуласини ℛ ҳарфи, ℛ ни ℱ ҳарфи билан белгилаб оламиз.
Теорема. ℑ МҲ нинг иҳтиёрий формуласи бûлсин. У ҳолда ℑ  ℛ МҲ нинг к.ч. формуласи бûлади, яъни ⊢ ℑ  ℛ.
Теорема. ⊢ ℱ    А .
Исбот. 1. ( А  В )  (  В   А ).
2. (  А  В )  (  В    А ).
3. (  А  ℛ )  (  ℛ    А ).
4. ℛ    А.
5. ℱ    А .

7. ℱ   ℑ .

Адабиётлар :


1. Ёқубов Т.,Каллибеков С. Математик мантиқ элементлари.Т.,1996.
2. Новиков П.С. Элементы математической логики.М.1973.
3. Чёрч А. Введение в математическую логику.М.,1960.
4. Мальцев А.И. Алгоритмы и рекурсивные функции.М.,1965.
5. ЛавровИ.А., Максимова Л.Л. Задачи по теории множеств,математической логике и теории алгоритмов.М.,1975.