ℸq)→(r V s)), (ℸℸpq)) қавсҳоро ин тавр партофтан мумкин аст:
pℸq→rVs, ℸℸp q)

§6. Ҳисоби предикатҳо

Яке аз воситаҳои таҳқиқи муҳокимаронӣ дар мантиқи муосир – мантиқи предикатҳост. Тарзи оддитарини мантиқи предикатҳо системаи натиҷагирии натуралӣ аст.
Забони мантиқи предикатҳо, инчунин соҳаи таъсири (амалӣ) квантор ва озод ё ин ки вобаста аз ворид шудани тағйирёбанда дар формулаҳо дар § 4-и боби 3 муайян карда шуда буд.
Мафҳуми гузориши терм ба ҷои тағйирёбандаи фардиро ворид мекунем. Амали гузориш ба ҷои тағирёбандаи фардӣ гуфта онро меноманд, ки тағйирёбандаҳои озодро дар формула бо ягон терм иваз намоянд.
Дар формулаи ба ҷои тағирёбандаи х доимии фардии а-ро гузоштан мумкин мебошад: мумкин аст, ки тағирёбандаи гузошта шавад: ∀уR(,у)→Р()- аммо тағирёбандаи у-ро гузоштан мумкин нест, чунки пас аз гузориш формулаи ∀уR(у,у) →Р(у) ҳосил мешавад, ки дар он воридшавии якуми тағирёбандаи у ба зерформулаи R(y,y) вобаста аст.
Ҳолати хусусии гузориш чунин гузоришест, ки дар он ба ҷои тағйирёбанда худи ҳамин тағйирёбанда гузошта шудааст.
Дар системаи натиҷагирии натуралӣ (СНН) ду гурўҳ қоидаи истинтоҷ мавҷуданд. Қоидаҳои гурўҳи якумро мустақим ва қоидаҳои гурўҳи дуюмро ғайримустақим меноманд.
Қоидаҳои натиҷагирии навъи якум инҳоанд:

ДК: А,В ХК1: АВ ХК2 : АВ ИК: ℸ(АВ)
А А В ℸАvℸВ

ДД1: А ДД2: В ХД1: АvВ, А ХД2: АvВ,
АvВ АvВ В А

ИД: (АvВ) ХИ: ХИ2 : ИИ:
АВ

ДЭ: А→ ХЭ1: ХЭ2: ДИ: А