Assigning Meaning to open terms

In that second post, I pointed out that ITT allows you to prove ∀n, n + 0 = 0 + n, but does not allow you to use this fact to prove (n ⇒ n + 0) = (n ⇒ 0 + n). The reason for this gap is because the proof of ∀n, n + 0 = 0 + n is not a proof of one equality (about n + 0). Instead, it is a proof of 1 + 0 = 0 + 1, 2 + 0 = 0 + 2, and so on: many equality proofs, none of which mention a variable. Because of that, ITT doesn't allow you to rewrite under the binder.¹ [¹ Because ITT only allows you to rewrite by equalities, and it's impossible to choose the right equality to rewrite under the binder, since the value of the binder is undetermined.]

The key problem, in other words, is that ITT allows us to prove facts about ∀n, n + 0 = 0 + n, but that's still quite different from proving facts about n + 0 = 0 + n. ITT never allows us to prove things like that, and in fact treats them as syntactically invalid.

But I think there's a way to avoid that.

As I argue in my modal first-order post, you can think of the universal and existential quantifiers not as introducing variables, but as changing them. From this point of view, every variable always has a value, even when not bound by a quantifier; it's just that the value is unknown. The programming versino of this is a variable that has been declared but not written to, leading it to have undefined value.

The intended semantics here are modal. There is a set of contexts to interpret formulas in, where a context is an assignment of valid values to variables. A formula is true if it evaluates to true in all contexts. That lets us assign truth values to formulas like x = x (always true) and y = z (not always true and not always false).

Then the universal quantifier means changing the quantified variable (to an unknown value). So ∀x, P is true if P is true after changing x to some unknown value, but keeping the other variables the same.

Right now, this interpretation only really fits first-order logic, since it doesn't handle questions of types and constructivity. I'm not sure how to extend the interpretation to the full ITT, but it seems like it should be possible.

So far, I've only defined an interpretation for open terms. Some of them interpret as true, sure, but what sort of proof rules could be used to prove them? For example, how would you prove x = x?

One answer, of course, is that many things like equality could be axiomatized directly using open terms. Then something like x = x is an axiom, so trivial to prove.

Another answer is that, under certain assumptions, local reasoning suffices. For example, if φ[x, y] contains no free variables other than x and y, then if ∀x ∀y, φ[x, y] is true locally then φ[x, y] is true globally. I think the local-to-global principle could potentially be related to the notion of computation (which you think of happening only at a particular context).

The local-to-global rule above is admissible, but it avoids cases where contexts contain things other than just variables. For example, if there is a notion of time as well as a notion of variable values, it may be that something true right now for all possible values of x and y, but that doesn't mean that it is an eternal, timeless truth. So choosing these local-to-global principles is tricky.

I can't think of other natural ways to establish facts about open terms, but I'm happy to hear suggestions.

The other question for open terms is how you use them. Here the answer is easier; their use is identical to normal closed terms, with the only difference that there are now terms like n + 0 = 0 + n, which are an equality that can be used to rewrite under binders. The only tricky bit here is that variable binding happens not only when handling universal quantifiers but in any term at all.