Heyting axiomatization, اصل‌بندی هیتینگ, پی افکنی هیتینگ, پی‌افکنی هیتینگ

پی‌افکنی هیتینگ

پی‌افکنی هیتینگ

IL.H.01
𝐴⊐(𝐴∧𝐴) A⊐(A∧A) A→(A∧A)
IL.H.02
(𝐴∧𝐵)⊐(𝐵∧𝐴) (A∧B)⊐(B∧A) (A∧B)→(B∧A)
IL.H.03
(𝐴⊐𝐵)⊐[(𝐴∧𝐶)⊐(𝐵∧𝐶)] (A⊐B)⊐[(A∧C)⊐(B∧C)] (A→B)→[(A∧C)→(B∧C)]
IL.H.04
[(𝐴⊐𝐵)∧(𝐵⊐𝐶)]⊐ (𝐴⊐𝐶) [(A⊐B)∧(B⊐C)]⊐ (A⊐C) [(A→B)∧(B→C)]→ (A→C)
IL.H.05
𝐴⊐(𝐵⊐𝐴) A⊐(B⊐A) A→(B→A)
IL.H.06
[𝐴∧(𝐴⊐𝐵)]⊐𝐵 [A∧(A⊐B)]⊐B [A∧(A→B)]→B
IL.H.07
𝐴⊐(𝐴∨𝐵) A⊐(A∨B) A→(A∨B)
IL.H.08
(𝐴∨𝐵)⊐(𝐵∨𝐴) (A∨B)⊐(B∨A) (A∨B)→(B∨A)
IL.H.09
[(𝐴⊐𝐶)∧(𝐵⊐𝐶)]⊐[(𝐴∨𝐵)⊐𝐶] [(A⊐C)∧(B⊐C)]⊐[(A∨B)⊐C] [(A→C)∧(B→C)]→[(A∨B)→C]
IL.H.10
⇁𝐴⊐(𝐴⊐𝐵) ⇁A⊐(A⊐B) ⇁A→(A→B)
IL.H.11
[(𝐴⊐𝐵)∧(𝐴⊐⇁𝐵)]⊐⇁𝐴 [(A⊐B)∧(A⊐⇁B)]⊐⇁A [(A→B)∧(A→⇁B)]→⇁A