FEATURE: [Distinguish axioms from theorems in the BFO FOL]

[alanruttenberg]

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.

[michaelrabenberg]

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.