Label and reference logic #49
Description
The following labeling and reference logic should be the default semantics.
Numbering
- Chapter numbering: arabic numerals
- Section numbering: arabic numerals
- Appendix numbering: uppercase latin letters
- Paragraph numbering: arabic numerals
- Item blocks and labeled displayed lines at depth 0: lowercase latin letters (or customized labels)
- Item blocks and labeled displayed lines at depth 1: arabic numerals (or customized labels)
- Item blocks and labeled displayed lines at depth 2: roman numerals (or customized labels)
- Item blocks and labeled displayed lines at depth >2: undefined (or customized labels)
Label parts:
- A chapter numbered by a numeral
N:N - A section numbered by a numeral
N:N - An appendix numbered by a letter
L:L - A paragraph numbered by numeral
N:N - An item block or a labeled displayed line numbered by an expression E:
⌜(E)⌝
Labels
- A chapter numbered by a numeral
N:⌜Chapter N⌝ - A section numbered by a numeral
N:⌜Section N⌝ - An appendix numbered by a letter
L:⌜Appendix L⌝ - An ordinary paragraph numbered by a numeral
N:'¶'followed by a non-breaking space, followed by the parents' label parts separated by dots, followed byN(example:'¶ 2.A.3'labels the third paragraph of the first appendix of the second chapter) - A paragraph tagged with a tag with as semantic value an expression
E, and numbered by a numeralN:'E'followed by a non-breaking space, followed by the parents' label parts separated by dots, followed byN(examples:'Fact 2.3'labels a paragraph tagged'FCT'which is the third paragraph of either chapter 2 or section 2—depending on whether the document is made up of chapters or sections;'Definition 3'labels a paragraph tagged'DEF'in a document made up only of paragraphs.) - An item block or a displayed line with label part an expression
E:E(examples:'(a)'is an uncustomized label of, for example, the first item block or numbered display line of a paragraph;'(1)'is an uncustomized label of the first item block or numbered displayed line inside an item block at depth 0)
Global references
TODO
Local references
TODO
Examples
A section with ordinary and tagged paragraphs, and custom-labeled display lines
source
§ SEC:intro
Introduction
¶ PAR:intro
Some facts about inductively defined structures seem not to admit
“straightforward” induction proofs. In such cases, a
“non-straightforward” induction proof seems “necessary”. A curious
one, or one fond of precision, or anyone with any other motivation,
might then wonder whether there is a way to precisely and sensibly
state, and prove, that this or that fact does not admit a
straightforward induction proof.
¶ DEF:basel
b : ℕ → ℚ
(B) b(0) ≔ 1 DEF:basel_base_case
(R) b(n+1) ≔ b(n)+(n+2)⁻² DEF:basel_rec_case
¶ RMK
[DEF:basel] is by (successor) recursion on the natural numbers.
[] [DEF:basel_base_case] is the the base case.
[] [DEF:basel_rec_case] is the the recursive case.
¶ FCT:basel
For each n:
b(n) < 2.
¶
[FCT:basel] is a simplification of *the Basel problem*, which ask for
a closed-form expression of the infinite sum:
1 1 1 1
─── + ─── + ─── + ─── + ⋯
1² 2² 3² 4²
Euler (1740) solved this problem and the sum is π²/6 (≈ 1.64).
semantics
§ 1 Introduction
────────────
¶ 1.1 Some facts about inductively defined structures seem not to admit
“straightforward” induction proofs. In such cases, a
“non-straightforward” induction proof seems “necessary”. A curious
one, or one fond of precision, or anyone with any other motivation,
might then wonder whether there is a way to precisely and sensibly
state, and prove, that this or that fact does not admit a
straightforward induction proof.
¶ 1.2 DEFINITION
b : ℕ → ℚ
(B) b(0) ≔ 1
(R) b(n+1) ≔ b(n)+(n+2)⁻²
¶ 1.3 REMARK Definition 1.2 is by (successor) recursion on the natural
numbers.
(a) 1.2(B) is the the base case.
(b) 1.2(R) is the the recursive case.
¶ 1.4 FACT For each n:
b(n) < 2.
¶ 1.5 Fact 1.4 is a simplification of t̲h̲e̲ ̲B̲a̲s̲e̲l̲ ̲p̲r̲o̲b̲l̲e̲m̲, which ask for a
closed-form expression of the infinite sum:
1 1 1 1
─── + ─── + ─── + ─── + ⋯
1² 2² 3² 4²
Euler (1740) solved this problem and the sum is π²/6 (≈ 1.64).
Same example as above, but a an appendix inside a chapter instead of a section
source
CH
§ APP:intro
Introduction
¶ PAR:intro
Some facts about inductively defined structures seem not to admit
“straightforward” induction proofs. In such cases, a
“non-straightforward” induction proof seems “necessary”. A curious
one, or one fond of precision, or anyone with any other motivation,
might then wonder whether there is a way to precisely and sensibly
state, and prove, that this or that fact does not admit a
straightforward induction proof.
¶ DEF:basel
b : ℕ → ℚ
(B) b(0) ≔ 1 DEF:basel_base_case
(R) b(n+1) ≔ b(n)+(n+2)⁻² DEF:basel_rec_case
¶ RMK
[DEF:basel] is by (successor) recursion on the natural numbers.
[] [DEF:basel_base_case] is the the base case.
[] [DEF:basel_rec_case] is the the recursive case.
¶ FCT:basel
For each n:
b(n) < 2.
¶
[FCT:basel] is a simplification of *the Basel problem*, which ask for
a closed-form expression of the infinite sum:
1 1 1 1
─── + ─── + ─── + ─── + ⋯
1² 2² 3² 4²
Euler (1740) solved this problem and the sum is π²/6 (≈ 1.64).
semantics
CHAPTER 1
═════════
§ 1.A Introduction
────────────
¶ 1.A.1 Some facts about inductively defined structures seem not to admit
“straightforward” induction proofs. In such cases, a
“non-straightforward” induction proof seems “necessary”. A curious
one, or one fond of precision, or anyone with any other motivation,
might then wonder whether there is a way to precisely and sensibly
state, and prove, that this or that fact does not admit a
straightforward induction proof.
¶ 1.A.2 DEFINITION
b : ℕ → ℚ
(B) b(0) ≔ 1
(R) b(n+1) ≔ b(n)+(n+2)⁻²
¶ 1.A.3 REMARK Definition 1.A.2 is by (successor) recursion on the natural
numbers.
(a) 1.A.2(B) is the the base case.
(b) 1.A.2(R) is the the recursive case.
¶ 1.A.4 FACT For each n:
b(n) < 2.
¶ 1.A.5 Fact 1.A.4 is a simplification of t̲h̲e̲ ̲B̲a̲s̲e̲l̲ ̲p̲r̲o̲b̲l̲e̲m̲, which ask for a
closed-form expression of the infinite sum:
1 1 1 1
─── + ─── + ─── + ─── + ⋯
1² 2² 3² 4²
Euler (1740) solved this problem and the sum is π²/6 (≈ 1.64).
Local and global cross-references
source
§
Example of local and global cross-references
¶
[] ITM:a
This item is labeled ‘ITM:a’.
[] ITM:a_i
This item is labeled ‘ITM:a_i’.
[] ITM:a_ii
This item is labeled ‘ITM:a_ii’.
[] This is a reference to the item labeled ‘ITM:a_i’:
[ITM:a_i].
[] This is another reference to the item labeled ‘ITM:a_i’:
[ITM:a_i].
¶ PAR:itm_ref
This is yet another reference to the item labeled ‘ITM:a_i’:
[ITM:a_i].
¶ FCTS
We have:
[] FCT:something
A fact labeled ‘FCT:something’.
[] FCT:some_other
Some other fact!
This is a reference to the fact labeled ‘FCT:something’:
[FCT:something]. This one is local.
¶ PAR:fct_ref
This is another such reference: [FCT:something]. This one is global.
¶
Note the difference between the global reference in [PAR:itm_ref] and
the one in [PAR:fct_ref]: only one uses the phrasing ‘── of ──’;
the other is a fact in its own right and is better referred to as
such.
semantics
§ 1 Example of local and global cross-references
────────────────────────────────────────────
¶ 1.1 (a) This item is labeled ‘ITM:a’.
(1) This item is labeled ‘ITM:a_i’.
(2) This item is labeled ‘ITM:a_ii’.
(3) This is a reference to the item labeled ‘ITM:a_i’: (1).
(b) This is another reference to the item labeled ‘ITM:a_i’:
(a)(1).
¶ 1.2 This is yet another reference to the item labeled ‘ITM:a_i’: (a)(1)
of ¶ 1.1.
¶ 1.3 FACTS We have:
(a) A fact labeled ‘FCT:something’.
(b) Some other fact!
This is a reference to the fact labeled ‘FCT:something’: Fact (a).
This one is local.
¶ 1.4 This is another such reference: Fact 1.3(a). This one is global.
¶ 1.5 Note the difference between the global reference in ¶ 1.2 and the
one in ¶ 1.4: only one uses the phrasing ‘── of ──’; the other is a
fact in its own right and is better referred to as such.