Hi Robert,
> 1) It seems that the total amount of thms is different from my past
> analysis, I had 1186 from the previous function you just pushed into
> Opentheory but I got 1,214 theorems running this one. Have I missed
> anything?
I'll answer this one on the other thread, since it's more OpenTheory specific.
> 2) I am not familiar with AXIOM OF INFINITY, does it have anything to do
> with identifying if a proof is classical or intuitionistic?
The axiom of infinity is used to construct the natural numbers, so
seeing (3) in the derivation is an indication that the proof involved
the natural numbers in some way.
> 3) {(1) (2) (3)} means it is not 1, nor 2, nor 3 I guess?
Sorry, I should have explained the notation. This means that the
theorem used all 3 axioms in its proof.
Cheers,
Joe
------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
