michaelrabenberg
commented
2 months ago I'd be very interested to see the output of such an exercise, as I imagine would many BFO users. (I feel like we corresponded about this a long time ago but things intervened and I lost track.) At any rate:
One potential complication occurs to me (apologies if this is obvious but just wanted to make it explicit): Suppose there happen to be two logically equivalent axioms in BFO FOL--call them "A1" and "A2"--but neither is a theorem of the rest of BFO FOL. Then each will end up being marked as a theorem during such an exercise, absent some suitable intervention. It'd presumably be important to ensure that in a case like that, at least one of A1 and A2 doesn't get simply get treated as a theorem in certain ways (e.g., by being treated in certain contexts as an inessential component of BFO FOL).
A simple way to take care of this, I assume, would be to run a test for logical equivalence first.
Distinguish axioms from theorems in the BFO FOL. I've code that tries to prove each formula from the rest. Take the ones that are proven and mark them as theorems.