diff options
author | Norbert Preining <norbert@preining.info> | 2022-05-25 03:01:13 +0000 |
---|---|---|
committer | Norbert Preining <norbert@preining.info> | 2022-05-25 03:01:13 +0000 |
commit | f01a37f8311f33e32441d25bdadcda9dcdbd165d (patch) | |
tree | efb861dfafff09d4bef8024c85a11f8c8deaba76 /macros/latex/contrib/stex/doc/packages/stex-metatheory.tex | |
parent | 0c7d079315627312627c83bc9ce6f5e4f1b436f6 (diff) |
CTAN sync 202205250301
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages/stex-metatheory.tex')
-rw-r--r-- | macros/latex/contrib/stex/doc/packages/stex-metatheory.tex | 31 |
1 files changed, 30 insertions, 1 deletions
diff --git a/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex b/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex index 1585ba504c..4feb646eb9 100644 --- a/macros/latex/contrib/stex/doc/packages/stex-metatheory.tex +++ b/macros/latex/contrib/stex/doc/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 |