How could we formalize the introduction of new notation?

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...

Tags:

Logic

Notation

Related

Calculation double Integral over Ball (optical size) What is the correct definition of a group? Intuition behind CW complexes Show $A\cap B \neq \varnothing \Rightarrow \operatorname{dist}(A,B) = 0$, and $\operatorname{dist}(A, B) = 0 \not\Rightarrow A\cap B \neq \varnothing$ Factoring polynomials with a 2nd degree coefficient greater than $1$ Combinatorial proof of $\sum_{k=0}^{n}(-1)^{k}\binom{n}{k}(l-k)^n=n!$, using inclusion-exclusion What are the subcategories of ordered sets / groups? If $K$ is compact and $C$ is closed in $\mathbb{R}^k$, prove that $K + C$ is closed using a "direct" proof $\int_{-\infty}^\infty \frac{\sin (t) \, dt}{t^4+1}$ must be zero and it isn't Prove that $\sum^{n-1}_{i=1}i^{(n-1)} \equiv -1$ (mod $n$) for all prime $n\in\mathbb{N}$. Proof of the summation $n!=\sum_{k=0}^n \binom{n}{k}(n-k+1)^n(-1)^k$? On the proof $\tan 70°-\tan 20° -2 \tan 40°=4\tan 10°$

Recent Posts