Hi all, I'm working on founded recursion (recursion when R Fr A as opposed to R We A) and I'm encountering some machinery trouble. Specifically, I'd like to use +c to prove a bunch of properties, but my relationships may be proper classes. Furthermore, I'd like the logic to be prior to the real numbers, as I'm going to use it in my surreal number development, which logically contains an isomorphic set of reals. I'm using df-trpred at the moment to work around it, but that's clunky. Anyone have any definitional ideas I could go on here?
Thanks, Scott -- 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/CACKrHR_rciExCZT_kwu0FadgRH%3DZwa7EdorbS1Eo2QyoR2%3DBfQ%40mail.gmail.com.
