**Description: **Intuitionistic logic is
now developed separately, so we need not first
focus on intuitionally valid axioms ax-1 6 and
ax-2 7
any longer.
Alternatively, I start from Jan Lukasiewicz's axiom system here, i.e.,
ax-mp 5, ax-luk1 35101, ax-luk2 35102 and ax-luk3 35103. I rather copy this
system than use luk-1 1658 to luk-3 1660, since the latter are theorems,
while we need axioms here.
(Contributed by Wolf Lammen, 23-Feb-2018.) (New usage is discouraged.)
(Proof modification is discouraged.) |