What kinds of variables range over proofs?

Question

I hope this question does not seem to obscure...

Consider the standard inference rule schema for, say, conjunction:

Rule (ConjunctionIntroduction)
  Premises
    P
    Q
  Conclusion
    P∧Q

If we are working intuitionistically, this is really a shorthand for the following (as far as my understanding goes):

Rule (ConjunctionIntroduction)
  Premises
    ρ ⊢ p::P
    σ ⊢ q::Q
  Conclusion
    ρ,σ ⊢ r::P∧Q

That is, rather than just stating that P holds, we state that there is a context ρ in which the proof p is a proof of P. And so on for the other premise and the conclusion.

Now P and Q are (what I would call) "metavariables" or "propositional variables". And ρ and σ are what I would call "context variables". So if I had to explicitly instruct a verifier, rather than hope that it could work out the various kinds of variables at play, I would prepend the following declarations:

Metavariables P,Q
Contexts ρ,σ

But what about the variables which range over proofs? Up until now I've also considered them metavariables, but this is clearly wrong. Consider the following:

Type NaturalNumber
...
Variable n:NaturalNumber

On the left of the type assertion we have a (normal, say) variable, the value of which would be a term or an expression. And on the right there is a type. But if I wanted to consider such assertions more generally, I would have to invent type variables to range over types:

Variable x
TypeVariable T
...
x:T    

Clearly type variables and (normal) variables aren't the same at all.

Up until now I haven't considered the kinds of variables needed to range over proofs. In fact it's worse, I've been conflating them with metavariables. However, the example of variables versus type variables shows me I've been wrong. Googling around, however, I don't see the notion proof variables anywhere. So what should I call them? Or are others also conflating these two kinds of variables? Or have a got something else completely wrong?

I'm tempted to just do this...

Metavariables P,Q
Contexts ρ,σ
Proofs p,q,r

...and leave it at that. Should I?

By the way, I know I should strictly write ContextVariables for Contexts and ProofVariables for Proofs but I think the intention is clear.

Answer 1

It is not common in the mathematical logic tradition to have variables that range over proofs.

The kind of rules you envisage are most commonly encountered in the context of the Curry-Howard correspondence, where the objects that encode proof structure are terms of the lambda calculus. Accordingly, metavariables that range over these could be called term variables. It is common to use the letters $M, N,$ etc. for these variables.

For your "context" variables $\rho$ and $\sigma$, one most often sees upper-case Greek letters, starting with $\Gamma, \Delta, \ldots$.

So in fully decorated form, your conjunction introduction rule could look like $$ \frac{\Gamma\vdash M:P \qquad\qquad \Delta\vdash N:Q}{\Gamma, \Delta \vdash \langle M,N\rangle : P \land Q } $$

(Beware that there are many minor stylistic variations possible here. The choices in the above example may have a slight computer-science bias, since that's where I'm coming from, but mathematical logicians should still find it reasonably familiar).

Answer 2

Let me go full formal on you.

Consider these data type declarations of the syntax for the typed lambda calculus in Agda.

data TType : Set where
    TTVar : Nat -> TType                    -- α
    _=>_ : TType -> TType -> TType          -- τ → τ
    Forall : TType -> TType                 -- ∀α. τ

mutual
    data TExpr : Set where
        TVal : TValue -> TExpr              -- v
        TApp : TExpr -> TExpr -> TExpr      -- f x
        TTyApp : TExpr -> TType -> TExpr    -- e[τ]
        TVar : Nat -> TExpr                 -- x

    data TValue : Set where
        TLambda : TType -> TExpr -> TValue  -- λx:τ.e
        TTyLambda : TExpr -> TValue         -- Λτ.e
        TConst : Nat -> TValue              -- c

In this case, Agda itself is a the metalanguage. A type variable would be a value of the form TTVar n for some natural number n¹. A term variable would be a value of the form TVar n for some natural number n.

A type metavariable is a variable of Agda of type TType. An expression metavariable is a variable of Agda of type TExpr. Finally, a value metavariable is a variable of Agda of type TValue. (Also, there are natural number metavariables.)

Of course, for a different object language there would be different data types describing the syntax, but a metavariable is always the same thing in this context: a variable of Agda of some given type. That is, a variable of the metalanguage. Other notions of "variable", if any, will depend on the object language.

As to your final question of whether you should write ContextVariables or Contexts, etc., it's up to you. I would probably lean toward just Contexts etc. I consider a variable of Agda (i.e. a metavariable) of type TExpr to "be" an expression (i.e. value of type TExpr) just as much as a concrete value. If I was talking about a function in the Agda code, I would not say "this function takes an expression metavariable" but that it "takes an expression". Even when informally writing about e.g. the typed lambda calculus, I would say "given terms $M$ and $N$, $\langle M,N\rangle$ is a term". The only case where I think I would prefer something like ContextVariables is if Contexts introduced constants of the metalanguage, and it was also necessary to explicitly state which symbols were variables (of the metalanguage) or not.

¹ And now the discussion potentially involves meta-metavariables...