You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: