Reje: Keltirip shıǵarıw qaǵıydaları

Aytimlar algebrasining tolıqlıǵı
Oy-pikirler esabınıń tiykarǵı túsinikleri
Bul bapta alınǵan nátiyjelerdi bayanlawda zárúr bolǵan tiykarǵı túsinikler: oy-pikirler esabı formulası túsinigi, tastıyıqlanıwshı formula tariypi, oy-pikirler esabınıń hákisiomalar sisteması, keltirip shıǵarıw qaǵıydaları jáne onıń nátiyjeleri, formulalar
kompleksinen formulanı keltirip shıǵarıw qaǵıydası oy-pikirler algebrasi hám oy-pikirler esabı ortasındaǵı munasábetler bayanlaingan.
Oy-pikirler esabı hákisiomatik logikalıq sistema bolıp, oy-pikirler algebrasi bolsa onıń interpretasiyasi bolıp tabıladı (talqini bolıp tabıladı).
Berilgen hákisiomalar sisteması negizinde (bazasında ) qurılǵan hákisiomatik teoriya dep sol hákisiomalar sistemasına súyene otirip tastıyıqlanıwshı hámme teoremalar kompleksine aytıladı.
Hákisiomatik teoriya formal hám formalmas teoriyalerge bólinedi.
Formalmas hákisiomatik teoriya teoriyalıq -kompleksiy mazmun menen toldırılǵan bolıp, keltirip shıǵarıw túsinigi anıq berilmegen jáne bul teoriya tiykarlanıp pikir mazmunına tayanadi.
Qaralayotgan hákisiomatik teoriya ushın tómendegi shártler orınlanǵan bolsa, yaǵnıy :
1) teoriyanıń tili berilgen;
2) formula túsinigi anıqlanǵan;
3) hákisiomalar dep atalatuǵın formulalar kompleksi berilgen;
4) bul teoriyada keltirip shıǵarıw qaǵıydası anıqlanǵan bolsa, formal hákisiomatik teoriya anıqlanǵan dep esaplanadı.
Tómende oy-pikirler esabınıń simvollari, formulası, hákisiomalar sisteması, keltirip shıǵarıw qaǵıydaları, formulalar kompleksinen formulanı keltirip shıǵarıw qaǵıydası, deduksiya hám ulıwmalasqan deduksiya teoremalari, ayırım logika nızamlarınıń tastıyıqı, oy-pikirler algebrasi hám oy-pikirler esabı ortasındaǵı munasábetler, oy-pikirler esabında sheshilish, zidsizlik, tolıqlılıq hám erkinlik máseleleri sıyaqlı máseleler aytıladı.
1. Ornına qoyıw qaǵıydasi
MH dıń quramında A ózgeriwshi oy-pikir qatnasqan
ℑ ( A ), hám de iùtiyoriy ℬ formulaları berilgen bolsın. Eger ℑ ( A ) oy-pikirler esabınıń keltirip shıǵarılıwshı (k. ch.) formulası bolsa, ol halda ℑ ( ℬ ) formula da oy-pikirler esabınıń keltirip shıǵarılıwshı formulası boladı
Bul qaǵıyda qısqasha sxematik túrde
ℑ ( A )
ℑ ( ℬ )
kóriniste belgilenad
2. Juwmaq shıǵarıw ( Modus ponens -MR ) qaǵıydas
Eger ℑ Þ ℬ hám ℑ formulalar MH dıń keltirip shıǵarılıwshı formulaları bolsa, ol halda ℬ formula da MH dıń keltirip shıǵarılıwshı formulası bolıp tabıladı. Bul qaǵıyda qısqasha tómendegi kóriniste belgilenedi : ℑ, ℑ Þ ℬ
ℬ.
2. 3 - tariyp. 1º. Hár bir hákisioma oy-pikirler esabınıń keltirip shıǵarılıwshı formulası bolıp tabıladı.
2º. Oy-pikirler esabınıń keltirip shıǵarılıwshı formulasına ornına qoyıw qaǵıydasın qóllaw nátiyjesinde payda etińan formula oy-pikirler esabınıń keltirip shıǵarılıwshı formulası bolıp tabıladı.

3º. Oy-pikirler esabınıń keltirip shıǵarılıwshı formulalarına ùulosa shıǵarıw qaǵıydasın qo'lllash nátiyjesinde payda etińan formula oy-pikirler esabınıń keltirip shıǵarılıwshı formulası bolıp tabıladı.

4º. Oy-pikirler esabınıń basqa keltirip shıǵarılıwshı formulaları joq.
2. 4 - tariyp. Eger formulalardıń chekli izbe-izligi ℑ1, ℑ2,.. ., ℑn de hár bir ℑi ( i q1, n ) formula yamasa oy-pikirler esabınıń keltirip shıǵarılıwshı formulası, yamasa ûzidan aldınǵı formulalardan ornına qoyıw yamasa ùulosa shıǵarıw qaǵıydaları járdeminde payda etińan formulalar bolsa, ol halda bul izbe-izlik aqırǵı ℑn formulanıń formal tastıyıqı, n bolsa tastıyıqtıń uzınlıǵı dep ataladı
Oy-pikirler esabınıń hákisiomalari tastıyıqınıń uzınlıǵı 1 ge teń tastıyıqlanıwshı formulalar retinde qaralıwı múmkin. Oy-pikirler esabınıń tastıyıq uzınlıǵı birdan úlken bolǵan tastıyıqlanıwshı formulaların teoremalar dep ataymız.
«ℑ formula oy-pikirler esabınıń keltirip shıǵarılıwshı formulası» degen gápti qısqasha ⊢ ℑ belgi arqalı ańlatpalaymız.
2. 5 - teorema. ⊢ A Þ A. Tastıyıq. tómendegi izbe-izlikti qaraylıq :
A Þ ( v Þ A ).
( A Þ ( v Þ A )) Þ (( A Þ v ) Þ ( A Þ A )).
( A Þ v ) Þ ( A Þ A ).
( A Þ ( v Þ A )) Þ ( A Þ A ).
A Þ A.
A Þ A.
Bul izbe-izlik A Þ A formulanıń formal tastıyıqı ekenligin kóriw qıyın emes. Haqıyqatlıqtan da,
A Þ (v Þ A)- formula I1 hákisioma;
( A Þ (v Þ A )) Þ (( A Þ v ) Þ (A Þ A ))- formula 2 hákisiomadagi S ni A menen almastırıw nátiyjesinde payda etińan;
( A Þ v ) Þ ( A Þ A ) formula 2 - formulaǵa MR qaǵıydasın qo'lllash nátiyjesinde payda etińan;
( A Þ ( v Þ A )) Þ ( A Þ A ) formula ûzidan aldınǵı formulada v ni v Þ A formula menen almastırıw nátiyjesinde payda etińan;
A Þ A formula 4 - formulaǵa MR qaǵıydasın qo'lllash nátiyjesinde payda etińan;
A Þ A formula A ni A menen almastırıw nátiyjesinde payda etińan.
Endigiden oy-pikirler esabınıń keltirip shıǵarılıwshı formulasın ℛ xarfi, ù ℛ ni ℱ xarfi menen belgilep alamız.
2. 6 - teorema. ℑ oy-pikirler esabınıń iùtiyoriy formulası bolsın. Ol halda ℑ Þ ℛ oy-pikirler esabınıń keltirip shıǵarılıwshı formulası bo'lad, yaǵnıy ⊢ ℑ Þ ℛ.
Tastıyıq. 1. A Þ ( v Þ A ).
2. ℛ Þ ( v Þ ℛ ).
3. v Þ ℛ.
4. ℑ Þ ℛ.

Bul ketma - ketlik teoremaning formal tastıyıqı bolıp tabıladı. Haqıyqatlıqtan da, 1 - formula I1 hákisioma. 2 - formula 1 -formuladan A ni ℛ menen almastırıw nátiyjesinde payda etińan. 3 - formula 2 - formuladan MR qaǵıyda járdeminde payda etińan. 4 - formula bolsa 3 - formulada v ni ℑ formula menen almshtirish nátiyjesinde payda etińan.

2. 7 - teorema. ⊢ ℱ Þ ù ù ℑ.
Tastıyıq. 1. ( A Þ v ) Þ ( ù v Þ ù A ).
2. ( ù A Þ v ) Þ ( ù v Þ ù ù A ).
3. ( ù A Þ ℛ ) Þ ( ù ℛ Þ ù ù A ).
4. ù ℛ Þ ù ù A.
ℱ Þ ù ù A.
ℱ Þ ù ù ℑ.