Bir joyli predikatni ta’rifi

O’zgaruvchilarni standartlashtirish yoki o’zgaruvchilarni ajratish amalga oshiriladi:

16.

17.

18.

19.

Bu erda y o’zgaruvchi B formulaga taalluqli emas deb qaraladi.

20.  X

bu yerda y o’zgaruvchi A (x) va B (x) formulalarga taalluqli emas,

bu yerda y o’zgaruvchi A (x) va B (x) formulalarga taalluqli emas.

Bu bosqichda har bir formulada bog’liq o’zgaruvchilar shunday qayta nomlanadiki, kvantorlar bilan bog’langan oz’garuvchilar har bir kvantor uchun yagona o’zgaruvchilarga aylanadi. Bu shunday fakt asosida amalga oshiriladiki, bunda bog’liq o’zgaruvchilar kvantor doirasida formulaning chinligini o’zgartimaydigan va formulada qatnashmagan boshqa o’zgaruvchiga almashtiriladi.

Masalan, ifoda

ifodaga almashtiriladi.

18. 
    Predikatlar mantiqi formulalarida skolemli o’zgarmaslarni va funksiyalarni kiritish nima uchun kerak?
    

Mavjudlik kvantorlarini yo’qotish. Bu bosqichda mavjudlik kvantorlari g(x) deb ataladigan Skolema funksiyasi yoki argumentli predkatlarni o'tkazish (hisoblash), ya’ni o’zgaruvchi-argumentning aniqlanish sohasidagi o’zgarmaslar bilan almashtiriladi.

16-20 tengkuchliliklar predikatlar mantiqining ixtiyoriy formulasini quyidagi ko’rinishga almashtiradi:

bu yerda ixtiyoriy Q_i- bu umumiylik kvantori yoki mavjudlik kvantori, – kvantorlarni saqlamovchi formula. Bunday ko’rinishdagi formulaga skolemli o’zgarmaslarni va funksiyalarni kiritish bilan barcha mavjudlik kvantorlarini yo’qotish mumkin. Buning uchun predikatlar mantiqining quyidagi qonunlaridan foydalanish mumkin:

21.

bu erda Q₁, …, Q_m- ixtiyoriy kvantorlar, a - o’zgarmas simvol formulaning boshida turgan ( ) ifodasiga mos keluvchi shunday o’zgarmaslar sifatida alfavitga kiritiladi va a - o’zgarmas simvol skolemli o’zgarmas deb ataladi.

22.

qayer , …, - ixtiyoriy kvantorlar, k-joyli funksionalli simvol f formulaning boshida turgan ifodasiga mos keluvchi shunday funksiya sifatida alfavitga kiritiladi va - funksiya skolemli fuksiya deb ataladi.

23. ∃xA(x)≡A(a), bu erda a - skolemli o’zgarmas.

Almashtirishlarga misollar:

Boshlang’ich formula Natijaviy formula

bu yerda a va b – o’zgarmaslar. Skolema funksiyasi mavjudlik kvantori bilan bog’langan o’zgaruvchilarning aniqlanish sohasini boshqa o’zgaruvchilarning aniqlanish sohasiga akslantirishni amalga oshiradi.

19. 
    Deduktiv xulosalash masalalari qanday formallashtiriladi?