Substitution operator on non-wff tvars

[Adam Bliss]

Continuing with my experiment from the earlier thread, I have added what I called ax-12a to peano_min.ghi:

stmt (ax-12a () ((A x)) (-> (= x A) (-> ph (A. x (-> (= x A) ph)))))

... and it seems to be working well to enable general theorems regarding substitutions on wffs, such as "sbn". I'm now thinking about how to handle substitution on non-wff tvars, such as the "nat" kind from peano.ghi. 

I think I pretty much understand the Theory of Classes chapter on metmath/set.mm. To recapitulate, they assert that all maths can be done with only setvars (which correspond to "vars" and not "tvars" in ghilbert; i.e. you cannot substitute a compound term into them) and wffs (which correspond to "tvars" and not "vars"; i.e. you cannot quantify over them). Atop this they add "class metavariables",  which can be mechanically eliminated, using some statements that straddle the line between axioms and definitions.

I don't know whether set.mm has a substitution operator that takes class metavariables, but I think I can see how it would be done: e.g. defining a class substitution operator [/]c in terms of the class equality operator =c by means of an axiom like this:

   (=c ([/]c x A ({|} y ph)) ({|} y ([/] x A ph))

(where for simplicity let's say x and y are distinct vars; I'm sure a bundled version could be worked out with sufficient effort.) Then again, perhaps such an operator isn't really necessary, since for any actual use-case you could quickly convert the classes in question back to wff-form?

Now this seems fine for metamath / set.mm, but leaves me unsatisfied in the context of ghilbert / peano.gh. I think I can do roughly the same thing using the machinery in "naive_set.ghi" to define "kind set" (which is really a class) and the axiomatic terms {|}  (nat var x wff tvar -> set tvar) and iota (set tvar -> nat tvar), but it doesn't feel right. I'm not sure my aversion to this is valid or even comprehensible, but here's an attempt to describe the reasons:

1. This machinery seems unparsimonious. Peano arithmetic is really "about" nats, not sets, and requiring us to move into sets and back just to define a fundamental operation like substitution on a nat tvar feels wrong. (I am working on an alternate version which skips the "set" kind, and directly defines (iota x ph) instead of (iota ({|} x ph) , but it doesn't feel a whole lot better....)

2. I far prefer ghilbert's approach to definitional soundness, and hate to introduce new mechanically-eliminable terms through axioms if I can avoid it. (I appreciate that ax-12a violates this principle in some ways, but it seems much more palatable an axiom to me than the ones in naive_set.ghi.)

3. Ghilbert's interface format allows tvars of every kind. wff tvars are not priviliged (right?) ; even though the peano_min axioms only produce stmts of kind wff,  other theories might be different.  Shouldn't there be a way to prove in-language substitution theorems on these arbitrary-kind tvars without requiring a special axiomatic term that first moves the discourse back to wffs? (I'm especially unsure whether this question even makes sense. But if it does, maybe this is another argument for reducing all usage of quantifiable vars down to a single universal lambda term, and supporting beta-reduction in the ghilbert-level semantics, rather than trying to shoehorn it into every theory?) 

I strongly suspect that this has all been discussed before somewhere, probably decades ago, but I'm having trouble finding it. Can anyone point me towards some writing on ways to do in-language substitution on non-wff tvars? Or does anyone have personal thoughts on this topic they'd be willing to share? 

Thanks,

--Adam

[Adam Bliss]

PS:

On Sat, Apr 20, 2019, 13:49 Adam Bliss <abl...@gmail.com> wrote:

>But if it does, maybe this is another argument for reducing all usage of quantifiable vars down to a single universal lambda term, and supporting beta-reduction in the ghilbert-level semantics, rather than trying to shoehorn it into every theory?) 

Contrariwise, is this whole thing a reason to abandon my attempt to use in-language general theorems about substitution, and instead to embrace rwffs intead of ax-12, and use extralinguistic automation to perform each concrete substitution step?

[Mario Carneiro]

I will return to this topic in more depth later, but for now I will point you to my project metamath zero, and specifically the handling of substitution in peano.mm0 (https://github.com/digama0/mm0/blob/master/examples/peano.mm0#L37-L38 , also see definitions "sbs" and "sbn" later down). In that file, I define "PA with classes" in a manner exactly equivalent to set.mm's "ZFC with classes". The handling of definitions is very similar to ghilbert.

In an earlier version of the file, I used (iota x ph) as a definite descriptor; later I retrofitted the classes in and now the same operator is called "the A" where "A" is a set (a subset of nat).

--
You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ghilbert+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.