One one hand metamath shows that yes, any reasonable logic (and many exotic ones) can be implemented as via the (meta)rule of substitution.

… On the other hand, in Lean and Coq I think judgmental equality is handled as a single rule by just normalizing both sides. Substitution can be used to implement each step of normalization, but I think that would be turning one proof step in Lean or Coq into an arbitrarily large proof in the Metamath style.

… Nonetheless, I though Metamath zero, both uses a Metamath substitute system and also is able to check Lean term proofs. Maybe I’m missing something here, but I’m not sure how it would work unless (1) I’m mistaken and Lean stores all steps of of judgmental equality or (2) MM0 uses something like a tactic to implement all the steps of Lean’s judgmental equality.

Two more points: (1) Metamath and MM0 show that substitution is actually quite fast. (2) When you say “implement” a proof assistant, it is unclear how much you are talking about the underlying logical kernel or all the features (including that some ITPs are also programming languages). It is also unclear how much you will allow automation and tooling to be built on top of substitution. Metamath has little tooling, but MM0 shows you can add a lot if you like.

I guess using nbe is a kind of "substitution-free" implementation of lambda calculus

@ice1000 I guess using nbe is a kind of "substitution-free" implementation of lambda calculus The way I read that is, if one stops at the Lambda-calculus level and does not look behind the currents that makes sense. However in implementing code it quickly becomes apparent that there is much one needs to not only consider but implement that is left out in the papers and such. See How to deal with Binders. Continued.

@ice1000 Also in implementing Lambda-calculus, I don't see how one can not do it without β-reduction which needs substitution or a term rewrite which can then be done with substitution.

I started writing an answer, but it is hard since it is not clear what you mean by "substitution". For example, is the metamath approach to substitution ok for you? If so, I think the answer is obviously that every kernel is reimplementable with substitution. They show how to do it in practice, but in theory you can just implement any Turing machine using a similar calculus. If you have a more restrictive definition of substitution (and more importantly what you mean by "only need substitution"), then I'd have to see what you mean.

@JasonRute For example, is the metamath approach to substitution ok for you? Yes.

@JasonRute I have not yet tired to implement at Metamath engine but from I have read and see I could literally drop my current Prolog substitution library into for build the core and it would work without change.

@JasonRute If the nLab entry for syntactic substitution helps you can reference that. (ref). Wno-all even added to the tag info to pin the meaning of the tag in place.

@JasonRute I hope you see the not in the question. can not be derived from substitution?

The problem with that nLab entry (and the wiki page) is that while I think logicians agree what substitution is, they probably don't have an entry on what it means to derive a set of rules from substitution. As much as metamath says that substitution is the only rule, I think really what metamath is doing is making a bunch of rules and derived rules and then applying them with substitution. So really if metamath is ok, the question is more "are there any proof assistant kernels which can not be derived from a set of rules instantiated via substitution."

@JasonRute I was not aware of the line of thinking. I will look into understanding this and probably be asking some questions. This could take days as I like to dig in deep. Thanks. If you have some references to look at please note them.

Metamath basically just shoves the responsibility to the axioms. Systems like CoC do not have any axioms, and use rules instead. I think this difference is inessential.

IMHO this question is ill-defined. What's "only"? To implement substitution you first need formulas. So it's not only substitutions -- You also have the concept of formulas! You need to clearly describe what exactly to include and what to exclude.

@Trebor Thanks for being honest. To implement substitution you first need formulas. My main reference for the definition of substitution is from Term Rewriting and All That by Franz Baader and Tobias Nipkow p. 38 but many don't have that book handy and it is not accessible for free. When you say formula is this to require that substitution needs variables?

@Trebor Would just noting variables are needed clear up the question or is there more you are seeking?

I think the trick with NbE is to use the metalanguage's substitution rather than defining your own on the object language. I don't know whether this covers every use case of substitution in a proof assistant, but it seems like a promising route for an answer.

Of interest: Normalisation by evaluation NbE

@mudri metalanguage's substitution The way I read that is any programming language used would have a substitution method or function. Is that what you mean? Another reading is that a meta language is created from the programming language and that has substitution. Is that what you mean? If it is neither please explain.

@GuyCoder My way of speaking was somewhat loose, though it leads to a good slogan. If the metalanguage is functional, we will usually think of its semantics as being given by a small step operational semantics, including β-rules defined via substitution. In practice, we'll probably compile metalanguage programs into machine code such that no substitution actually happens (e.g, using stack frames to pass arguments). See the meaning of app (s, t) in particular (in the linked Wikipedia page), where if S is a λ-expression, we will get a β-reduction.

@mudri My way of speaking was somewhat loose I am so guilty of that at times I have to confess it often to be absolved.

@mudri If the metalanguage is functional I know this well, see: Code and resources for "Handbook of Practical Logic and Automated Reasoning" I am Eric noted at the top of the page.

@mudri In going from β-rules to substitution how do you deal with lambda terms modulo convertibility? E.g. How to deal with Binders?

@mudri we'll probably compile metalanguage programs into machine code such that no substitution actually happens Does this mean you have not implemented code yet and at least run test cases?

@GuyCoder I don't really understand what you're asking in your penultimate comment. NbE is a normalisation methodology, meaning that it maps convertible terms to equal terms (up to α-equivalence). This gives you “modulo convertibility” for free. The specific representation of binders is, to some extent, a separate concern, as long as deciding α-equivalence on it is easy enough. IIRC, de Bruijn levels are performant in practice.

@GuyCoder For your last comment, to be specific I'll talk about the NbE procedure listed on the Wikipedia page. The metalanguage is Standard ML, and the object language is STλC with functions and products. Notice that there is no definition of substitution (on the object language) listed. The place where we could imagine substitution happening is in the metalanguage, where reduction of Standard ML may be implemented by repeatedly applying operational rules to the program until no more apply. This is what we tend to do when reasoning about SML programs. (contd)

However, I would expect that real SML implementations don't use term rewriting to run programs, and instead compile any terms to bit representations and machine code instructions. Thus, when you run the executable of your NbE algorithm created by your SML compiler, no substitution really happens. There's clearly no substitution directly on object language terms – because we never defined it – and there's no substitution on ML terms because it doesn't happen to be implemented that way. The only substitution is in the reference semantics of SML, which we don't run directly.

@mudri Thanks. I really like that you comments include the definitions, The metalanguage is Standard ML, and the object language is STλC