There is a section of set.mm (currently 1.8.3) which proves statements of predicate logic which are theorems in set.mm but axioms in iset.mm.
We should do the same for propositional logic (this would be a good beginner project if anyone wants to get started with metamath, but if no one picks it up, I eventually will).
Here's a summary of the situation from Gérard Lang:
Four of them are already provided as follows: axia1 is simpl
(443), axia2 is simple (447), axia3 is pm3.2 (434) and axin2 is pm2.21
(100).
Concerning the two last axioms ax-in1 and ax-io, [Gérard Lang] only found partial
results like pm2.02 (160) for ax-in1, and jao (498) and prth (554), but
no exact proof of theorems axin1 and axio.
jkingdon
commented
6 years ago
There is a section of set.mm (currently 1.8.3) which proves statements of predicate logic which are theorems in set.mm but axioms in iset.mm.
We should do the same for propositional logic (this would be a good beginner project if anyone wants to get started with metamath, but if no one picks it up, I eventually will).
Here's a summary of the situation from Gérard Lang:
Four of them are already provided as follows: axia1 is simpl (443), axia2 is simple (447), axia3 is pm3.2 (434) and axin2 is pm2.21 (100). Concerning the two last axioms ax-in1 and ax-io, [Gérard Lang] only found partial results like pm2.02 (160) for ax-in1, and jao (498) and prth (554), but no exact proof of theorems axin1 and axio.