> > 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). >
I wasn't clear but that's what I meant. We have no formal proof in Heyting arithmetic, but since the logic is intuitionistic, we have to trace back the use of only a few axioms and "see" that they are "artefacts" of earlier contructions which are more general than needed for the present purposes. It'll be easier when the website is updated (I guess the page you're talking about was locally generated on your computer, since I can't access http://us2.metamath.org/ileuni/bezout.html ?). 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. > Yes, there is some work to do toward modularity of databases. With Norm's addition of the command WRITE SOURCE <file> /SPLIT, and provided we have the good tags in iset.mm, we can produce a file ifol.mm that can then be included by $[ ifol.mm $] at the beginning of other databases. On top of that, one can state for instance Peano's axioms, or Tarski's axioms of elementary geometry, etc. (One caveat is that we will want a logic with terms, which are not provided anymore since there are no class terms, so we'll need to strengthen the "denotation axiom" E. x x = y to E. x x = A, but this can be added as an intermediate layer ifol-terms.mm which includes ifol.mm). Benoît -- 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/d8baf20d-5f4f-4b3f-adc0-a16fb52fdcccn%40googlegroups.com.
