diff options
Diffstat (limited to 'Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex')
-rw-r--r-- | Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex index 1585ba504c8..4feb646eb9f 100644 --- a/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex +++ b/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex @@ -1 +1,30 @@ -\textcolor{red}{TODO: metatheory documentation}
\ No newline at end of file +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 |