Meta-mathematical reasoning

It's common in programming languages to write proofs about proofs. For example, when using a Gentzen-style deduction system for specifying a type system or a big-step operational semantics, we often write a proof by induction on the size of the proof tree of a derivation.

When proving type soundness, you can use a number of different dynamic semantics. It's sanest to attempt this with an operational semantics, but there are many flavors to choose from: big-step operational semantics, small-step semantics with compatibility rules for lifting the basic reductions into arbitrary evaluation contexts, small-step semantics with Gentzen-style rules for creating an inductive proof tree that lifts the reductions into evaluation contexts, or Felleisen-style small-step semantics where the evaluation contexts are reified as plain old mathematical objects.

The benefit of the latter is that it requires no meta-mathematical reasoning--this is not to say it's impossible to use any of the others to prove soundness, but it perhaps requires less subtlety to write a proof about ordinary objects than one about proofs.

It reminds me of what Andrew Pitts has been saying for a while about his and Gabbay's denotational framework for theories of binding. They originally formulated their theory by working in a different set theory (one invented in the early 20th century by Fraenkel and Mostowski), but discovered that this required a certain "meta-logical sophistication" that made their work less accessible:

[Pitts and Gabbay [2002]] expresses its results in terms of an axiomatic set theory, based on the classical Fraenkel-Mostowski permutation model of set theory. In my experience, this formalism impedes the take up within computer science of the new ideas contained in that article. There is an essentially equivalent, but more concrete description of the model as standard sets equipped with some simple extra structure. These so-called nominal sets are introduced by Pitts [2003], and I will use them here to express α-structural recursion and induction within "ordinary mathematics"...

From "Alpha-structural recursion and induction", p. 462

Again, I think the moral of the story is that when you place all the objects you want to reason about at the object level, you avoid the need for meta-reasoning, which can make your proofs simpler and more accessible.