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 34582, ax-luk2 34583 and ax-luk3 34584. I rather copy this
system than use luk-1 1647 to luk-3 1649, 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.) |