**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 33608, ax-luk2 33609 and ax-luk3 33610. I rather copy this
system than use luk-1 1750 to luk-3 1752, 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.) |