Kleene axiomatization, اصل‌بندی کلینی, پی افکنی کلینی, پی‌افکنی کلینی

گویایی درگس‌باوری

پی‌افکنی کلینی

پی‌افکنی کلینی

IL.K.01
𝐴⊐(𝐵⊐𝐴) A⊐(B⊐A) A→(B→A)
IL.K.02
(𝐴⊐𝐵)⊐ ((𝐴⊐(𝐵⊐𝐶))⊐(𝐴⊐𝐶)) (A⊐B)⊐ ((A⊐(B⊐C))⊐(A⊐C)) (A→B)→ ((A→(B→C))→(A→C))
IL.K.03
𝐴⊐(𝐵⊐𝐴∧𝐵) A⊐(B⊐A∧B) A→(B→A∧B)
IL.K.04
𝐴∧𝐵⊐𝐴 A∧B⊐A A∧B→A
IL.K.05
𝐴∧𝐵⊐𝐵 A∧B⊐B A∧B→B
IL.K.06
𝐴⊐𝐴∨𝐵 A⊐A∨B A→A∨B
IL.K.07
𝐵⊐𝐴∨𝐵 B⊐A∨B B→A∨B
IL.K.08
(𝐴⊐𝐶)⊐((𝐵⊐𝐶)⊐(𝐴∨𝐵⊐𝐶)) (A⊐C)⊐((B⊐C)⊐(A∨B⊐C)) (A→C)→((B→C)→(A∨B→C))
IL.K.09
(𝐴⊐𝐵)⊐ ((𝐴⊐ ⇁𝐵)⊐⇁𝐴) (A⊐B)⊐ ((A⊐ ⇁B)⊐⇁A) (A→B)→ ((A→ ⇁B)→⇁A)
IL.K.10
⇁𝐴⊐(𝐴⊐𝐵) ⇁A⊐(A⊐B) ⇁A→(A→B)
IL.K.11
∀𝑥𝑃𝑥⊐𝑃𝑡 ∀xPx⊐Pt forall xPx→Pt
IL.K.12
𝑃𝑡⊐∃𝑥𝑃𝑥 Pt⊐∃xPx Pt→existsxPx