In the mmset.html ref. [KalishMontague], p. 81 footnote says: "The fact that (B7') [our ax-6] can be replaced by the weaker axiom (B7) [our ax-6v] is stated implicitly in the abstract [5], where also the rather obvious possibility is mentioned of extending the approach to predicate logic with operation symbols and individual constants."
Ref. 5 is: [5] Montague, R. and Kalish, D. Formulations of the predicate calculus with operation symbols and.descriptive phrases (abstract). Bull. Amer. Math. Soc., 62 (1956),261. The pdf for this is provided by the 1st Google hit. I didn't study it carefully and don't know if or how easily it can be adapted to Metamath, nor whether it can be made metalogically (scheme) complete in our sense. Norm On Sunday, August 15, 2021 at 12:42:25 PM UTC-4 Scott Fenton wrote: > Sorry, ax-6 > > On Aug 15, 2021, at 12:10 PM, Scott Fenton 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 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: > > 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 > > <https://groups.google.com/d/msgid/metamath/CACKrHR955QXpsPnTFD7V%3DG9B_RJhJUO9VWPUSO%2BOHUeZ9xw98g%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > > > -- > 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 > > <https://groups.google.com/d/msgid/metamath/AB116B71-BE9E-4C98-8B53-9DC5A7BDCCBC%40kenkubota.de?utm_medium=email&utm_source=footer> > . > > -- 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/ef69b8d4-ee34-4b91-b01a-3a9eb28f71c0n%40googlegroups.com.
