HF set theory – Re: [Metamath] Predicate Calculus Functions

[Ken Kubota]

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 <sct...@gmail.com>: 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 metamath+unsubscr...@googlegroups.com. 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/AB116B71-BE9E-4C98-8B53-9DC5A7BDCCBC%40kenkubota.de.