diff options
author | p <grr@lo2.org> | 2024-11-29 22:18:45 -0500 |
---|---|---|
committer | p <grr@lo2.org> | 2024-11-29 22:18:45 -0500 |
commit | 958437abfc71342ac2b84a451c989e6eb20b7643 (patch) | |
tree | a442fcba060599f316a1ab6e21f4f7720e28769b | |
parent | 9bdfeb8a204fbbce701fd75a19fc94b19ae06adb (diff) | |
download | blueprint-958437abfc71342ac2b84a451c989e6eb20b7643.tar.gz |
partially unbreak innperseqs diagram
-rw-r--r-- | essays/innperseqs.diag.otx | 63 | ||||
-rw-r--r-- | essays/post_formalism_memories.otx | 2 |
2 files changed, 34 insertions, 31 deletions
diff --git a/essays/innperseqs.diag.otx b/essays/innperseqs.diag.otx index 4a07122..f352adb 100644 --- a/essays/innperseqs.diag.otx +++ b/essays/innperseqs.diag.otx @@ -1,20 +1,24 @@ -\newcommand{\innprow}[4]{ - \parbox{2.25in}{ - \parbox{0.35in}{\includegraphics[scale=0.25]{img/time#1}} - \parbox{0.5in}{#2:} - \parbox{1.25in}{ - \parbox{1.25in}{#3} - - \parbox{1.25in}{#4}}}\vskip 0.5em} - -\begin{figure} -{\centering - \parbox{0.15in}{\rotatebox[origin=c]{90}{\ - {\footnotesize Successive bands represent the vague outer ring at successive times as it fades in toward the small bright light.}}}\begin{minipage}{1.5in} - \imgw{1.3in}{img/innperseqs}\vskip 0.1em {\centering\small small bright light \par} - \end{minipage}\begin{minipage}{2in} -\dq{Sentences} at -\vskip 1em +\def\innprow#1#2#3#4{ + \hbox to 1.5in{ + \picw=0.3in\inspic{time#1.png}% + \hskip 0.1in plus 0.1in% + #2:% + \hskip 0.1in plus 0.1in% + \vbox{ + \hbox to 1in{#3}\nl + \hbox to 1in{#4}}} + \vskip 0.5em} + +\midinsert +\hbox to \hsize{{\leftskip=0pt plus1fil\rightskip=0pt plus1fil + \hbox to 0.2in{\rotbox{90}{{\typoscale[800/] Successive bands represent the vague outer ring at successive times as it fades in toward the small bright light.}}}% +% + \hskip 0.2in% + \vbox{\picw=1.3in\inspic{innperseqs.png}\vskip 0.1em% + \hbox to 1.5in{\typoscale[900/] small bright light \par}} +% + \vbox{\leftskip=0pt \typoscale[900/] + \dq{Sentences} at\vskip 1em \innprow{1}{$time_1$}{$a_1 a_2 a_3 a_4 a_5 a_6 a_7 b$}{$a_1,a_2 \rightarrow\ b$} @@ -30,21 +34,20 @@ \vskip 2em -\dq{Axioms} \\ +\dq{Axioms} \nl \hskip 1em $a_1 a_2 a_3 a_4 a_5 a_6 a_7$ \vskip 2em -Innperseq \\ -$(a_3,a_2,a_1)$ \\ -$(b,a_3)$ \\ -$(c,a_5,a_4)$ \\ -$(d,b,a_6)$ \\ -$(e,c,a_7)$ \\ -$(f,e,d)$ \\ +Innperseq \nl +$(a_3,a_2,a_1)$ \nl +$(b,a_3)$ \nl +$(c,a_5,a_4)$ \nl +$(d,b,a_6)$ \nl +$(e,c,a_7)$ \nl +$(f,e,d)$ \nl $(g)$ - \end{minipage}\par} - \vskip 1em - \caption{Example instance of \sysname{Innperseqs.}} - \label{innperdiag} -\end{figure} + \par}}} + \cskip + \caption/f[innperdiag] Example instance of \sysname{Innperseqs.} +\endinsert
\ No newline at end of file diff --git a/essays/post_formalism_memories.otx b/essays/post_formalism_memories.otx index f5885d4..74f4377 100644 --- a/essays/post_formalism_memories.otx +++ b/essays/post_formalism_memories.otx @@ -126,7 +126,7 @@ An \term{innperseq} is a sequence of sequences of sentences on one radius satisf * The last sequence has one member. \enditems} -% \input innperseqs.diag.otx +\input essays/innperseqs.diag.otx In diagram \ref[innperdiag], different positions of the vague outer ring at different times are suggested by different shadings. The outer segment moves \dq{down the page.} The figure is by no means an innperseq, but is supposed to help explain the definition. In \sysname{Innperseqs,} a conventional proof would be redundant unless all the statements were on the same radius. And even if the weakest axiom were chosen (the initial outer endpoint), this axiom would imply the initial inner endpoint, and from there the theorem could be reached immediately. In other words, to use the standard definition of \dq{\term{proof}} in \sysname{Innperseqs} would result in an uninteresting derivation structure. Thus, a more interesting derivation structure is defined, the \dq{\term{innperseq.}} The interest of an \dq{\term{innperseq}} is to be as elaborate as the many restrictions in its definition will allow. Proofs are either disregarded in \sysname{Innperseqs}; or else they are identified with innperseqs, and lack Property 8. \sysname{Innperseqs} makes the break with the proof-theorem structure of formalist mathematics. |