10
$\begingroup$

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?

$\endgroup$
3
  • 2
    $\begingroup$ In everyday mathematics we choose notation to make the ideas easier to read and write about. Nothing more formal than the kind you illustrate is needed, or even wise. To study formal logic you do need more formalism. $\endgroup$
    – Ethan Bolker
    Jul 18, 2016 at 14:08
  • 3
    $\begingroup$ Notation is redefined all the time and the reason this (usually) doesn't end in utter confusion is human's remarkable ability to pick up on the current context. This is especially apparent when listening to experts in fields you are not familiar with. What they say and write is (taken literally) quite often gibberish, but actually makes perfect sense to anyone familiar with the common notation and abuses thereof. So, what I'm saying is that you're asking the wrong question. We can formalize all these things (in very different ways), but we shouldn't - unless there is reason to. $\endgroup$
    – Stefan Mesken
    Jul 18, 2016 at 18:53
  • 2
    $\begingroup$ A huge thumbs down to the above comment. We do need to formalize the things, for example in order to be able to create automatic verification systems and theorem provers. Other applications could include parsers for latex formulae to faciliate the search for some senior professors. The question perfectly makes sense, in my opinion. $\endgroup$
    – Sergey Dovgal
    May 11, 2020 at 18:01

2 Answers 2

Reset to default
16
$\begingroup$

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

$\endgroup$
4
  • $\begingroup$ Can you provide references for the concepts "full abbreviation power" and "definitorial expansion", please. $\endgroup$
    – Rob Arthan
    Jul 19, 2016 at 23:21
  • 1
    $\begingroup$ @RobArthan: You asked me this before in a comment and I already did tell you where they came from, but you didn't reply. "A Concise Introduction to Mathematical Logic" by Wolfgang Rautenberg uses the term "definitorial extension of T" for the extension of T by adding new predicate symbols or function symbols defined by a formula. It also says that in less formalized theories the ability to introduce such new symbols can be regarded as a mechanism for "abbreviation of explicit definitions". It gives the same conditions as I did. However it does not concern internal creation of new symbols. $\endgroup$
    – user21820
    Jul 20, 2016 at 4:52
  • $\begingroup$ @RobArthan: That is why originally I used the term "full abbreviation power" to refer to the innate capability of the formal system to create on the fly new symbols with defining axioms, and as I said before the term itself had already been in use on FOM (see cs.nyu.edu/pipermail/fom/2015-September/019136.html and cs.nyu.edu/pipermail/fom/2015-July/018851.html for example). $\endgroup$
    – user21820
    Jul 20, 2016 at 4:56
  • $\begingroup$ @RobArthan: By the way Rautenberg puts "definitorial expansion" as a synonym of "definitorial extension". In my answer I chose the former because the latter sounds too much like an actual extension of the formal system, but I'm talking about full abbreviation power within the formal system. Notice that full abbreviation power essentially prevents non-intrinsic blowups, and so is a pragmatic necessity for any practical formal system. $\endgroup$
    – user21820
    Jul 20, 2016 at 5:00
2
$\begingroup$

Shortly, from a formal perspective, introducing new notation amount to expanding the language of the formal system (theory) you are working on, adding some axioms that in some way provide a definition for the new symbols.

The new symbols can be predicate or operation-symbols.

For predicate-symbols the new axioms are logical equivalences between the introduced predicate and some formula of the old language (i.e. statements of the form $P(x) \iff \varphi(x)$, where $P$ is the new predicate).

For operation-symbols the defining axioms can either be equations (identifying the new operation with an operation we could already represent with operation-symbols of the old language) or logical equivalence of the form $f(x)=y \iff \varphi(x,y)$, where $f$ is the new operation-symbol and $\varphi(x,y)$ is a (provable) functional formula of the old language.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .