Sorry, ax-6 > On Aug 15, 2021, at 12:10 PM, Scott Fenton <[email protected]> wrote: > > > That and the paper it references are actually what I was working from! HF > theory employs terms, so I was wondering, for instance, if ax-5 would need to > be rephrased to work with terms. > >>> On Aug 15, 2021, at 12:02 PM, Ken Kubota <[email protected]> wrote: >>> >> >> I’m not sure whether this helps, but Larry Paulson's presentation employs HF >> set theory: >> https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf >> >> Kind regards, >> >> Ken Kubota >> >> ____________________________________________________ >> >> Ken Kubota >> https://doi.org/10.4444/100 >> >> >> >>> Am 15.08.2021 um 01:11 schrieb Scott Fenton <[email protected]>: >>> >>> Hi all, >>> >>> Has anyone done research into predicate calculus terms/functions and >>> metalogical completeness? I'm interested in formalizing hereditarily finite >>> set theory, but its standard presentation comes with terms. >>> >>> 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/CACKrHR955QXpsPnTFD7V%3DG9B_RJhJUO9VWPUSO%2BOHUeZ9xw98g%40mail.gmail.com. >> >> -- >> 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/AB116B71-BE9E-4C98-8B53-9DC5A7BDCCBC%40kenkubota.de.
-- 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/C6DB797B-9092-4880-8FD3-6013D5E10543%40gmail.com.
