| 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 38098, ax-luk2 38099 and ax-luk3 38100. I rather copy this
system than use luk-1 1688 to luk-3 1690, 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.) |
