Predicate Calculus Functions

[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

[Thierry Arnoux]

Hi Scott,

I'm not sure which axiomatization you're talking about, I found a Coq paper with an axiomatization of the hereditarily finite sets which I believe can be done very similarly to set.mm, using wff's and setvar's, but defining an "adjunction" predicate instead of the membership predicate, and formulating the axioms with those. That paper does not include any axiom about equality, but you'll probably need some axiom of the form ` |- ( x = y -> ( x . z ) = ( y . z ) ) `

In any case, Mario is also using terms in his HOL database.

BR,
_
Thierry

[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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CACKrHR955QXpsPnTFD7V%3DG9B_RJhJUO9VWPUSO%2BOHUeZ9xw98g%40mail.gmail.com.

[Scott Fenton]

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 <ma...@kenkubota.de> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/AB116B71-BE9E-4C98-8B53-9DC5A7BDCCBC%40kenkubota.de.

[Scott Fenton]

Sorry, ax-6

On Aug 15, 2021, at 12:10 PM, Scott Fenton <sct...@gmail.com> wrote:



[Norman Megill]

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.