On January 11, 2022 8:11:02 AM PST, Benoit <[email protected]> wrote:
I think one can say without too much of a stretch that the proof is in Heyting arithmetic (Peano's axioms do not appear as axioms in iset.mm, but if one traces back your proofs, one can probably convince oneself that this is the case) so there are no questions about its constructive nature (I mean: there is no issue about predicativity or IZF versus CZF).
Hmm my assumption is that this sort of proof works in CZF or Heyting arithmetic but I'm not sure that the iset.mm proof convinces us of that. If you look at the "This theorem was proved from axioms" list at the bottom of the page for bezout you see ax-caucvg and I assume that's not because ax-caucvg is needed to prove results about integers, but because we somehow drag in absolute value or something else (and I think if we wanted to avoid it we probably could prove some absolute value theorems for rationals without ax-caucvg).
If people are interested in this sort of thing, there's definitely work that can be done in iset.mm similar to the work that has been done in the past for set.mm - reducing the use of axioms where not needed. I'm not exactly the expert on what axioms are needed for what, much less what would be needed to make iset.mm more realistically cover systems smaller than IZF (whether CZF - outside the section where it currently lives in iset.mm - or the various systems of second-order arithmetic or even first-order arithmetic). So some of this would probably be best done by totally restating some of the axioms (or even switching away from something built on propositional and predicate logic and sets, as iset.mm is), but I'm being quite vague about "some of this" simply because I don't know.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/a6a120e5-d6c7-74b9-b56d-ea15409ea4a4%40panix.com.
