From 958437abfc71342ac2b84a451c989e6eb20b7643 Mon Sep 17 00:00:00 2001 From: p Date: Fri, 29 Nov 2024 22:18:45 -0500 Subject: partially unbreak innperseqs diagram --- essays/post_formalism_memories.otx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'essays/post_formalism_memories.otx') 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. -- cgit v1.2.3