Heyting axiomatization

رده‌ها Intuitionistic logic

1.𝐴⊐(𝐴∧𝐴) A⊐(A∧A) A→(A∧A)IL.H.01axiom✹

2.(𝐴∧𝐵)⊐(𝐵∧𝐴) (A∧B)⊐(B∧A) (A∧B)→(B∧A)IL.H.02axiom✹

3.(𝐴⊐𝐵)⊐[(𝐴∧𝐶)⊐(𝐵∧𝐶)] (A⊐B)⊐[(A∧C)⊐(B∧C)] (A→B)→[(A∧C)→(B∧C)]IL.H.03axiom✹

4.[(𝐴⊐𝐵)∧(𝐵⊐𝐶)]⊐ (𝐴⊐𝐶) [(A⊐B)∧(B⊐C)]⊐ (A⊐C) [(A→B)∧(B→C)]→ (A→C)IL.H.04axiom✹

5.𝐴⊐(𝐵⊐𝐴) A⊐(B⊐A) A→(B→A)Introduction of an assumption IL.H.05axiom✹

6.[𝐴∧(𝐴⊐𝐵)]⊐𝐵 [A∧(A⊐B)]⊐B [A∧(A→B)]→BIL.H.06axiom✹

7.𝐴⊐(𝐴∨𝐵) A⊐(A∨B) A→(A∨B)IL.H.07axiom✹

8.(𝐴∨𝐵)⊐(𝐵∨𝐴) (A∨B)⊐(B∨A) (A∨B)→(B∨A)IL.H.08axiom✹

9.[(𝐴⊐𝐶)∧(𝐵⊐𝐶)]⊐[(𝐴∨𝐵)⊐𝐶] [(A⊐C)∧(B⊐C)]⊐[(A∨B)⊐C] [(A→C)∧(B→C)]→[(A∨B)→C]IL.H.09axiom✹

10.⇁𝐴⊐(𝐴⊐𝐵) ⇁A⊐(A⊐B) ⇁A→(A→B)IL.H.10axiom✹

11.[(𝐴⊐𝐵)∧(𝐴⊐⇁𝐵)]⊐⇁𝐴 [(A⊐B)∧(A⊐⇁B)]⊐⇁A [(A→B)∧(A→⇁B)]→⇁AIL.H.11axiom✹