How could we formalize the introduction of new notation?

What I am thinking about is how in a textbook/proof/theorem/discussion/definition one states that from now on a new notation will be used in the appropriate scope.

Example:

Let $V^*$ denote the dual of a vector space $V$

although the above is a widely accepted notation, we could always choose to redefine it (however ill-advised that is)

Let $G$ be a group with group operation $(x,y)\mapsto (x,y)+$

stating that i will be using a post-fix notation.

Also there is a function application notation $(f,x)\mapsto f(x)$, but we may override it, as is done when considering sequences $(a,n)\mapsto a_n$.

$\textbf{Question}$: How can this "introduction of new notation" be formalized?

Solution 1:

What you may be looking for in your formal system is variously called full abbreviation power or definitorial expansion. Basically, it comprises rules that allows you to create on the fly new symbols extending the original language. We need one type of rule for each kind of symbol: $\def\eq{\leftrightarrow}$

1. For each $k$-parameter sentence $φ$ over the current language, you can add a new predicate symbol $P$ and the axiom $\forall x_{1..k}\ ( P(x_{1..k}) \eq φ(x_{1..k}) )$.

2. For each $(k+1)$-parameter sentence $φ$ over the current language such that you have proven "$\forall x_{1..k}\ \exists! y\ ( φ(x_{1..k},y) )$", you can add a new function symbol $f$ and the axiom $\forall x_{1..k} \forall y\ ( f(x_{1..k}) = y \eq φ(x_{1..k},y) )$.

3. For each $1$-parameter sentence $φ$ over the current language such that you have proven "$\exists y\ ( φ(y) )$", you can add a new constant symbol $c$ and the axiom $φ(c)$.

You can choose whether or not to have scoping for new symbols. In mathematical practice we do have implicit scoping. For instance we use the same symbol with different meanings depending on the context. This can be formalized easily, and is very well known to all programmers, since their programs reuse symbols all the time. It is also arguably best to scope new symbols as narrowly as possible, so that it is only defined where it is needed.

You can add full abbreviation power (with or without scoping) to any first-order formal system, and the resulting system will be conservative over the original. The reason is that in any model of the original system one can interpret the new symbols according to their defining sentences and then then added axioms become mere tautologies.

To cater to notation beyond first-order logic, such as summation symbols and subscripts and lines, one would need significantly more. In a text-based environment all we need is rewrite rules and a means of specifying precedence rules. This is very well studied and has been applied ever since the invention of programming languages. Some proof assistants support extensive rewrite rules to facilitate such notation introduction, but most are still based on ASCII. To support totally arbitrary notation, one would need some mechanism for describing graphics! One way to do that is to allow rewrite rules to specify LaTeX macros. I think this has been implemented in a few proof assistants, but I can't recall which ones at the moment...