summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex
blob: 4feb646eb9f742f1742be41e21c431ca00cd5efa (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
The \pkg{stex-metatheory} package contains \sTeX symbols so ubiquitous, that it is
virtually impossible to describe any flexiformal content without them, or that are
required to annotate even the most primitive symbols with meaningful
(foundation-independent) ``type''-annotations, or required for basic structuring
principles (theorems, definitions). As such, it serves as the default meta theory for any
\sTeX module.

We can also see the \pkg{stex-metatheory} as a foundation of mathematics in the sense of
\cite{rabe:future:15}, albeit an informal one (the ones discussed there are all formal
foundations). The state of the \pkg{stex-metatheory} is necessarily incomplete, and will
stay so for a long while: It arises as a collection of empirically useful symbols that are
collected as more and more mathematics are encoded in \sTeX and are classified as
foundational.

Formal foundations should ideally instantiate these symbols with their formal counterparts,
e.g. |isa| corresponds to a typing operation in typed setting, or the $\in$-operator in
set-theoretic contexts; |bind| corresponds to a universal quantifier in ($n$th-order)
logic, or a $\Pi$ in dependent type theories.

We make this theory part of the \sTeX collection due to the obiquity
of the symbols involved. Note however, that the metatheory is
for all practical purposes a ``normal'' \sTeX module, and the
symbols contained ``normal'' \sTeX symbols.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "../stex-manual"
%%% End:

%  LocalWords:  stex-metatheory th-order