Newer
Older
In this section we look more closely at the examples from section \ref{sec:pheno} and how each can be represented
using theory graphs.
But first, we look at the aspects common to all examples to form an intuition of the theory graphs structures that are needed.
The examples in section \ref{sec:pheno} are each slightly different but they have fundamental common aspects.
First, each paper starts with establishing a common ground on which the results of the paper are built. This leverages the literature in two ways.
\begin{itemize}
\item Firstly, concepts from the literature are used to conveniently build up the local definitions. From the theory graphs perspective
\item Secondly, properties of locally introduced concepts are \emph{adopted} from the literature. Mathematically, this is justified by
and (implicit or explicit) subsumption between the local definition and that used by the referenced theorem.
From the theory graph perspective this function as a theory morphism that induces the properties locally due to its truth-preserving semantics.
Therefore, a paper corresponds, not to a single theory, but to a theory pattern that leads to a theory of the main contxribution of the paper.
Secondly, the notion of ``literature'' and the existence of concepts beyond a particular definition (so that equivalent definitions imply one is
talking about the same platonic concept) are common to all examples. We believe that what happens in mathematical practice is that definition and foundational
choices are abstracted away as implementation details and the important concepts and their properties are used as an interface to each theory (in the mathematical sense,
e.g. group theory). But this is precisely the situation that realms try to capture in theory graphs. Therefore, we maintain that, from a theory graph perspective, informal
mathematical papers refer (and contribute to) realms rather than individual theories.
\subsection{Realms in Informal Mathematics}
Figure \ref{fig:rec-gen} shows the general case for the representation of a paper as part of a theory graph (although simplified to one recap reference for the paper).
The ``literature'' for the mathematical theory to which the paper contributes is represented as a realm with a face and several pillars.
The paper references a document within the field, that is naturally part of a pillar and grounds the recap theory.
The main content of the paper is a theory in itself that includes the recap theory and is a conservative extension of it.
The view $v$ ensures that the paper can make use of concepts and theorems from the realm, as they can be accessed via $v$. In informal mathematics $v$ is usually not explicitly
given, but it may or may not be justified. In case it is not we call $v$ a \emph{postulated} view.
The relation $r$ is between the recap and the cited paper is left unspecified at this point as we distinguish several cases below.
%Mathematical papers re-introduce concepts with the implied assumption of semantic equivalence in the context of the paper.
%I.e. every statement in the paper holds for the original definition too, but not necessarily the converse.
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,3.5) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-3,0) {Recap};
\node[thy] (pcont) at (-3,2) {Paper Content};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[->] (citp) to node[below] {$\cn{r}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
We recognize four special cases for recaps based on the nature of $r$ and discuss each individually below.
First we have to decide the home theory of the symbols that the recap introduces.
If the home is the cited theory then $r$ is an import then we have a \emph{plain recap} (\ref{rc:pl}) .
Otherwise, we have new symbols in the recap theory that are somehow related with the ones in the cited one.
In that situation we have three subcases depending on the relation between the recap and cited theory:
\emph{equivalence recap} (\ref{rc:eq}), \emph{specialization recap} (\ref{rc:sp}) and \emph{generalization recap} (\ref{rc:ge}).
One situation is that of plain recaps where the relation $r$ is an inclusion into the recap from the cited paper.
Typically the include $r$ is a conservative extension of the cited paper.
For instance the \emph{covers of the multiplicative group} from example \ref{ex:covers} directly uses the concept from the cited paper,
but gives a concise verbalization of its definition. This allows it to make use of the result in \cite{covers-2} which acts as a conservative
extension of \cite{covers-13}. The situation is shown in figure \ref{fig:rec-covers}
Note that, if $r$ is conservative, then we have a \textbf{pillar extension} for the realm justifies the new paper becoming part of the realm's literature.
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,3.5) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-3,0) {\cn{CACF}};
\node[thy] (pcont) at (-3,2) {\cn{MToCACF}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\node[thy] (r) at (2,3) {Realm Face};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[conservative,red] (citp) to node[below] {$\cn{r}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\end{tikzpicture}
\caption{Publication graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers}
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-3,-3.7) rectangle (5,3.5) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-2.5,-3.5) rectangle (1.5,1.8) {};
%p2
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-3.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
\node (p1-name) at (-2,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-1.5,-1) {\cn{CACF}};
\node[thy] (pcont) at (-1.5,0) {\cn{MToCACF}};
\node[thy] (top1) at (-0.5,1) {$\top$};
\node[thy] (tcdots1) at (0.5,-0.5) {$\cdots$};
\node[thy] (citp) at (-0.5,-2) {Cited Paper};
\node[thy] (top2) at (3.5,1) {$\top$};
\node[thy] (bot2) at (3.5,-3) {$\bot$};
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[conservative,red] (citp) to node[below] {$\cn{r}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (tcdots1);
\draw[conservative] (tcdots1) to (top1);
\draw[conservative] (pcont) to (top1);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\end{tikzpicture}
\caption{Aggregation graph for plain recaps (using Example \ref{ex:covers})}\label{fig:rec-covers}
\end{figure}
\paragraph{Special Case: Equivalence Recap} \label{rc:eq}
Another common situation is that of equivalence recaps where the relation $r$ is an equivalence (isomorphism) between the two theories.
We can represent the relation $r$, in this case, as two views $v_{to}$ and $v_{from}$, one in each direction between the recap and the cited paper that
ensure their isomorphism. Then, the view $v$ is induced by $v_{from} \circ v_1$ modulo conservativity.
Moreover, the contribution of the paper carries over to the realm via the view $v_{to}$.
This occurs, for instance, in example \ref{ex:mnets} where this intuition is explicitly written down in the paper as ``There are several equivalent ways to
define multinets.'' (although not proved). Moreover, examples \ref{ex:quant} and \ref{ex:calculi} also fit in this category.
In fact it is the most common situation in the sample papers we studied.
The implicit or explicit equivalence of the local definitions in the recap theory that the view $v$ from the face exists and therefore that theorems from the mathematical
field can be used in the paper. In case the equivalence is implicit we speak of a \emph{postulated} view, i.e. one where the assigned expressions are (partially) informal.
A flexiformal system can still reason about the meaning travel induced by a postulated view but cannot look into assigned objects and e.g. proof check them.
\end{oldpart}
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,3.5) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-3,0) {\cn{MNets}};
\node[thy] (pcont) at (-3,2) {\cn{ICMnets}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[view,red, bend left = 15] (citp) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 15] (recap) to node[below] {$\cn{v_{to}}$} (citp);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\caption{Publication graph for equivalence recaps (using Example \ref{ex:mnets})}\label{fig:rec-mnets}
Note that adding an equivalent definition corresponds to a \textbf{realm extension}, where the face is fixed, and the view from the face to the current
theory can be postulated. Therefore, in figure \ref{fig:rec-mnets} the paper effectively extends the realm (or the current pillar) as introduced in section \ref{sec:prel}.
This corresponds to the mathematical practice of ``contributing to'' a field (or mathematical theory). This resulting realm after knowledge aggregation
is shown in Figure \ref{fig:rec-mnets-aggr}, where the new paper contributes a new pillar to the realm. The equivalence is ensured by $v_{from}$ and $v_{to}$ as
we take into account conservativity to reduce them to the $\bot$ theory.
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4,-1.7) rectangle (5,3.5) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-3.5,-1.5) rectangle (-1.5,1.8) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
\node (p3-name) at (-2.8,1.6) {$\mathit{Pillar_{n+1}}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (pcont) at (-2.5,1) {\cn{ICMnets}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {Cited Paper};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\node[thy] (r) at (0.5,3) {Realm Face};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[view,red, bend left = 15] (bot1) to node[below] {$\cn{v_{from}}$} (recap);
\draw[view,red, bend left = 15] (recap) to node[below] {$\cn{v_{to}}$} (bot1);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\end{tikzpicture}
\caption{Aggregation graph for equivalence recaps (using Example \ref{ex:mnets})}\label{fig:rec-mnets-aggr}
\end{figure}
\paragraph{Special Case: Specialization Recap} \label{rc:sp}
Thirdly, we have the case where $r$ is a specialization relation that can be represented as a view $v_{from}$ from the cited theory to the recap.
Same as in the previous case, this ensures the existence of $v$ as $v_{from} \circ v_1$ modulo conservativity.
However it does not directly contribute the paper results back to the (same) realm as they concern a special case of the concepts in the realm.
This is the case in example \ref{ex:atm} where the definition from the paper is a specialization of the one in the literature.
In \ref{CalStai:natm09}, the definition of the accelerated Turing machine involves a concrete step size ($2^{-n}$),
whereas the definition it recaps allows arbitrary sequences of step sizes as long as their
sum remains finite. Thus we have the situation in Figure~\ref{fig:rec-atm}. Theory \cn{ATM}
contains the (opaque) sentence (\ref{lq:atm}), but there cannot be a view from \cn{ATM} to
\cn{atm} as that is more general. But we do have a view to \cn{atm(2^{-n})}, which
naturally arises in treatments of accelerated Turing machines as an example. That special case forms a realm of its own. \ednote{expand on this}
\ednote{@MK the old version of the ATM case is below as oldpart, the second part I removed because it doesn't fit
precisely but there are some interesting things there, we should talk about it}
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,3.5) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-6,-0.5) rectangle (-4,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
%realm2
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-3.5,-2.3) rectangle (-1.5,-1) {};
\node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
\node (r2-name) at (-2.1,-2.1) {$\mathit{Realm_2}$};
\node (p-name) at (-4.5,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-5,0) {\cn{ATM}};
\node[thy] (pcont) at (-5,2) {\cn{ATMhalt}};
\node[thy] (citpex) at (-2.5,-1.5) {$\cn{atm}(2^{-n})$};
\draw[view] (recap) to node[above] {$\cn{v_{to}}$} (citpex);
\draw[include] (citp) to (citpex);
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {atm};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\node[thy] (r) at (2,3) {Realm Face};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[view,red] (citp) to node[below] {$\cn{v_{from}}$} (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\end{tikzpicture}
\caption{Publication graph for specialization recaps (using Example \ref{ex:atm})}\label{fig:rec-atm}
Finally, we have the case where $s$ is a plain (partial) include that does not entail conservativity and therefore does not entail
the existence $v$. In that case we call $v$ a \emph{postulated} view and the recap itself an \emph{adoption}.
This is the case in example \ref{ex:course} where the recap theory \cn{SET} includes only the symbols $\in$ and $\{\cdot,\cdot\}$ from
the formal development \cn{ZFset}, but not their axioms. Instead the symbols are ``defined'' by alluding to the literature (common knowledge).
We claim this verbalization effectively postulates the existence of $v$, by implying that the semantics of the two symbols is compatible with that
given in the literature (which we represent as a realm).
\begin{figure}[ht]\centering
\begin{tikzpicture}
%realm
\draw[draw=blue!40, fill=gray!4,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-1,-1.7) rectangle (5,3.5) {};
%p-paper
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-4.5,-0.5) rectangle (-1.5,2.8) {};
%p1
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (-0.5,-1.5) rectangle (1.5,1.8) {};
\draw[draw=blue!40, fill=gray!10,rectangle, rounded corners, inner sep=10pt, inner ysep=20pt] (2.5,-1.5) rectangle (4.5,1.8) {};
\node (r-name) at (4.5,3.3) {$\mathit{Realm}$};
\node (p-name) at (-2,2.6) {$\mathit{Paper}$};
\node (p1-name) at (0,1.6) {$\mathit{Pillar_1}$};
\node (p2-name) at (4.0,1.6) {$\mathit{Pillar_n}$};
\node[thy] (recap) at (-3,0) {\cn{SET}};
\node[thy] (pcont) at (-3,2) {\cn{SETOPS}};
\node[thy] (top1) at (0.5,1) {$\top$};
\node[thy] (citp) at (0.5,0) {\cn{ZFset}};
\node[thy] (bot1) at (0.5,-1) {$\bot$};
\node[thy] (r) at (2,3) {Realm Face};
\draw[view] (r) to node[above] {$\cn{v}$} (pcont);
\draw[view] (r) to node[left] {$\cn{v_1}$} (top1);
\draw[view] (r) to node[right] {$\cn{v_2}$} (top2);
\draw[pinclude,red] (citp) to (recap);
\draw[conservative] (recap) to (pcont);
\draw[conservative] (bot1) to (citp);
\draw[conservative] (citp) to (top1);
\draw[view, bend left = 15] (bot2) to (bot1);
\draw[view, bend left = 15] (bot1) to (bot2);
\end{tikzpicture}
\caption{Publication graph for generalization/unspecified recaps (using Example \ref{ex:course})}\label{fig:rec-slides}
