summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex
diff options
context:
space:
mode:
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.tex31
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