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/2578823F-F060-4A10-8BC6-6E43E7BD3D95%40gmail.com.
