User:Jon Awbrey/SCRATCHPAD

Greek

  ἐν ἀρχῇ

  Ἐν ἀρχῇ ἦν ὁ λόγος  

Πάτερ ἡμῶν ὁ ἐν τοῖς οὐρανοῖς· ἁγιασθήτω τὸ ὄνομά σου·

ἐλθέτω ἡ βασιλεία σου·

LOGOS

Epigraph Formats

	'Tis a derivative from me to mine, And only that I stand for.
	— Winter's Tale, 3.2.43–44

	Out of the dimness opposite equals advance . . . .      Always substance and increase, Always a knit of identity . . . . always distinction . . . .      always a breed of life.
	— Walt Whitman, Leaves of Grass, [Whi, 28]

On either side the river lie
Long fields of barley and of rye,
That clothe the wold and meet the sky;
And thro' the field the road runs by
	To many-tower'd Camelot;
And up and down the people go,
Gazing where the lilies blow
Round an island there below,
	The island of Shalott.
		— Tennyson, The Lady of Shalott, [Ten, 17]

The most valuable insights are arrived at last; but the most valuable insights are methods.

— Nietzsche, The Will to Power, [Nie, S469, 261]

The power of form, the will to give form to oneself. "Happiness" admitted as a goal. Much strength and energy behind the emphasis on forms. The delight in looking at a life that seems so easy. — To the French, the Greeks looked like children.

— Nietzsche, The Will to Power, [Nie, S94, 58]

In every sort of project there are two things to consider: first, the absolute goodness of the project; in the second place, the facility of execution.           In the first respect it suffices that the project be acceptable and practicable in itself, that what is good in it be in the nature of the thing; here, for example, that the proposed education be suitable for man and well adapted to the human heart.           The second consideration depends on relations given in certain situations — relations accidental to the thing, which consequently are not necessary and admit of infinite variety.

— Rousseau, Emile, or On Education, [Rou-1, 34–35]

Blockquote Formats

Now, I ask, how is it that anything can be done with a symbol, without reflecting upon the conception, much less imagining the object that belongs to it? It is simply because the symbol has acquired a nature, which may be described thus, that when it is brought before the mind certain principles of its use — whether reflected on or not — by association immediately regulate the action of the mind; and these may be regarded as laws of the symbol itself which it cannot as a symbol transgress. (Peirce, CE 1, 173).

The information of a term is the measure of its superfluous comprehension. That is to say that the proper office of the comprehension is to determine the extension of the term. …           Every addition to the comprehension of a term, lessens its extension up to a certain point, after that further additions increase the information instead. …           And therefore as every term must have information, every term has superfluous comprehension. And, hence, whenever we make a symbol to express any thing or any attribute we cannot make it so empty that it shall have no superfluous comprehension.           I am going, next, to show that inference is symbolization and that the puzzle of the validity of scientific inference lies merely in this superfluous comprehension and is therefore entirely removed by a consideration of the laws of information.

(Peirce, CE 1, 467).

a.	The theories of the soul (psyche) handed down by our predecessors have been sufficiently discussed; now let us start afresh, as it were, and try to determine (diorisai) what the soul is, and what definition (logos) of it will be most comprehensive (koinotatos).
b.	We describe one class of existing things as substance (ousia), and this we subdivide into three: (1) matter (hyle), which in itself is not an individual thing, (2) shape (morphe) or form (eidos), in virtue of which individuality is directly attributed, and (3) the compound of the two.
c.	Matter is potentiality (dynamis), while form is realization or actuality (entelecheia), and the word actuality is used in two senses, illustrated by the possession of knowledge (episteme) and the exercise of it (theorein).
d.	Bodies (somata) seem to be pre-eminently substances, and most particularly those which are of natural origin (physica), for these are the sources (archai) from which the rest are derived.
e.	But of natural bodies some have life (zoe) and some have not; by life we mean the capacity for self-sustenance, growth, and decay.
f.	Every natural body (soma physikon), then, which possesses life must be substance, and substance of the compound type (synthete).
g.	But since it is a body of a definite kind, viz., having life, the body (soma) cannot be soul (psyche), for the body is not something predicated of a subject, but rather is itself to be regarded as a subject, i.e., as matter.
h.	So the soul must be substance in the sense of being the form of a natural body, which potentially has life. And substance in this sense is actuality.
i.	The soul, then, is the actuality of the kind of body we have described. But actuality has two senses, analogous to the possession of knowledge and the exercise of it.
j.	Clearly (phaneron) actuality in our present sense is analogous to the possession of knowledge; for both sleep (hypnos) and waking (egregorsis) depend upon the presence of the soul, and waking is analogous to the exercise of knowledge, sleep to its possession (echein) but not its exercise (energein).
k.	Now in one and the same person the possession of knowledge comes first.
l.	The soul may therefore be defined as the first actuality of a natural body potentially possessing life; and such will be any body which possesses organs (organikon).
m.	(The parts of plants are organs too, though very simple ones: e.g., the leaf protects the pericarp, and the pericarp protects the seed; the roots are analogous to the mouth, for both these absorb food.)
n.	If then one is to find a definition which will apply to every soul, it will be "the first actuality of a natural body possessed of organs".
o.	So one need no more ask (zetein) whether body and soul are one than whether the wax (keros) and the impression (schema) it receives are one, or in general whether the matter of each thing is the same as that of which it is the matter; for admitting that the terms unity and being are used in many senses, the paramount (kyrios) sense is that of actuality.
p.	We have, then, given a general definition of what the soul is: it is substance in the sense of formula (logos), i.e., the essence of such-and-such a body.
q.	Suppose that an implement (organon), e.g. an axe, were a natural body; the substance of the axe would be that which makes it an axe, and this would be its soul; suppose this removed, and it would no longer be an axe, except equivocally. As it is, it remains an axe, because it is not of this kind of body that the soul is the essence or formula, but only of a certain kind of natural body which has in itself a principle of movement and rest.
r.	We must, however, investigate our definition in relation to the parts of the body.
s.	If the eye were a living creature, its soul would be its vision; for this is the substance in the sense of formula of the eye. But the eye is the matter of vision, and if vision fails there is no eye, except in an equivocal sense, as for instance a stone or painted eye.
t.	Now we must apply what we have found true of the part to the whole living body. For the same relation must hold good of the whole of sensation to the whole sentient body qua sentient as obtains between their respective parts.
u.	That which has the capacity to live is not the body which has lost its soul, but that which possesses its soul; so seed and fruit are potentially bodies of this kind.
v.	The waking state is actuality in the same sense as the cutting of the axe or the seeing of the eye, while the soul is actuality in the same sense as the faculty of the eye for seeing, or of the implement for doing its work.
w.	The body is that which exists potentially; but just as the pupil and the faculty of seeing make an eye, so in the other case the soul and body make a living creature.
x.	It is quite clear, then, that neither the soul nor certain parts of it, if it has parts, can be separated from the body; for in some cases the actuality belongs to the parts themselves. Not but what there is nothing to prevent some parts being separated, because they are not actualities of any body.
y.	It is also uncertain (adelon) whether the soul as an actuality bears the same relation to the body as the sailor (ploter) to the ship (ploion).
z.	This must suffice as an attempt to determine in rough outline the nature of the soul.
	(Aristotle, On the Soul, 2.1)

Ordered List Formats

1. Item 1
1. Item a
1. Item i
2. Item ii
3. Item iii
2. Item b
3. Item c
2. Item 2
1. Item a
1. Item i
2. Item ii
3. Item iii
2. Item b
3. Item c
3. Item 3

Mathematical Symbols

\(\curlyvee\)	\curlyvee
\(\curlywedge\)	\curlywedge
\(\lessdot\)	\lessdot
\(\gtrdot\)	\gtrdot
\(:\!\lessdot\)	:\!\lessdot
\(:\!\gtrdot\)	:\!\gtrdot
\(\colon\!\lessdot\)	\colon\!\lessdot
\(\colon\!\gtrdot\)	\colon\!\gtrdot
\($\)	$	NB. Idiosyntax of WikiTeX
\($\!\)	$\!	NB. Idiosyntax of WikiTeX
\(\$\)	\$

Cactus TeX

\(\begin{array}{l} \texttt{ } \\ \texttt{~} \\ \texttt{()} \\ \texttt{(~)} \\ \texttt{(( ))} \\ \texttt{( )( )} \\ \texttt{a b c} \\ \texttt{a~b~c} \\ \texttt{a(a)~=~(~)} \\ \texttt{a((b)(c))~=~((ab)(ac))} \\ \end{array}\)

\(\begin{array}{l} \texttt{d}^2 \texttt{x} \\ \texttt{d}^\text{2} \texttt{x} \\ \texttt{d}^\texttt{2} \texttt{x} \\ \end{array}\)

\(\texttt{uv~(du~dv) ~+~ u(v)~(du (dv)) ~+~ (u)v~((du) dv) ~+~ (u)(v)~((du)(dv))}\)

\(\texttt{uv} \cdot \texttt{(du~dv)} + \texttt{u(v)} \cdot \texttt{(du (dv))} + \texttt{(u)v} \cdot \texttt{((du) dv)} + \texttt{(u)(v)} \cdot \texttt{((du)(dv))}\)

\(\begin{matrix} \bar{(} \ldots \bar{)} & \bar{|} \ldots \bar{|} \\ \\ \dot{(} \ldots \dot{)} & \dot{|} \ldots \dot{|} \\ \\ \hat{(} \ldots \hat{)} & \hat{|} \ldots \hat{|} \\ \\ \check{(} \ldots \check{)} & \check{|} \ldots \check{|} \\ \\ \tilde{(} \ldots \tilde{)} & \tilde{|} \ldots \tilde{|} \\ \\ \downharpoonleft \ldots \downharpoonright & \upharpoonleft \ldots \upharpoonright \\ \\ \overline{(} \ldots \overline{)} & \overline{|} \ldots \overline{|} \\ \\ \underline{(} \ldots \underline{)} & \underline{|} \ldots \underline{|} \\ \\ \overline{\underline{(}} \ldots \overline{\underline{)}} & \overline{\underline{|}} \ldots \overline{\underline{|}} \\ \\ \end{matrix}\)

\(\begin{array}{lllll} {}^{_\sim}\!X & = & U - X & = & \{ \, u \in U : \underline{(} u \in X \underline{)} \, \}. \end{array}\)

\(\begin{array}{lllll} {}^{_\sim}\!X & = & U - X & = & \{ \, u \in U : \tilde{(} u \in X \tilde{)} \, \}. \end{array}\)

\[X = \{\ (\!|u|\!)(\!|v|\!),\ (\!|u|\!) v,\ u (\!|v|\!),\ u v\ \} \cong \mathbb{B}^2.\]

\[X = \{\ \underline{(u)(v)},\ \underline{(u)~v},\ \underline{u~(v)},\ \underline{u~v}\ \} \cong \mathbb{B}^2.\]

\[X = \{\!\] (u)(v)\(,\) (u)v\(,\) u(v)\(,\) uv \(\} \cong \mathbb{B}^2.\)

\[X = \{\!\] (u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)

\(X = \{\!\) (u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)

\(X = \{\!\) (u)(v) , (u)v ,  u(v) , uv \(\} \cong \mathbb{B}^2.\)

Examples of Logical Orbits

Version 1

\(\begin{array}{ccc} \texttt{u}' & = & \texttt{((u)(v))} \\ \texttt{v}' & = & \texttt{((u,~v))} \end{array}\)

\(\begin{matrix} \text{Orbit 1} \\ \text{Initial Point :}~ (u, v) = (1, 1) \end{matrix}\)

\(\begin{array}{c|cc} t & u & v \\ \\ 0 & 1 & 1 \\ 1 & 1 & 1 \\ 2 & '' & '' \\ \end{array}\)

\(\begin{matrix} \text{Orbit 2} \\ \text{Initial Point :}~ (u, v) = (0, 0) \end{matrix}\)

\(\begin{array}{c|cc} t & u & v \\ \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 2 & 1 & 0 \\ 3 & 1 & 0 \\ 4 & '' & '' \\ \end{array}\)

Version 2

\(\text{Orbit 1. Intitial Point :}~ (u, v) = (1, 1)\)

\(\begin{array}{c|cc|cc|cc|cc|cc|c} t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\ \\ 0 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 1 & 1 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 4 & '' & '' & '' & '' & '' & '' & '' & '' & '' & '' & \ldots \\ \end{array}\)

\(\text{Orbit 2. Intitial Point :}~ (u, v) = (0, 0)\)

\(\begin{array}{c|cc|cc|cc|cc|cc|c} t & u & v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\ \\ 0 & 0 & 0 & 0 & 1 & 1 & 0 & 0 & 1 & 1 & 0 & \ldots \\ 1 & 0 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & 1 & \ldots \\ 2 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 3 & 1 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 & \ldots \\ 4 & '' & '' & '' & '' & '' & '' & '' & '' & '' & '' & \ldots \\ \end{array}\)

Version 3

\(\text{Orbit 1}\!\)

\(\begin{array}{c|cc|cc|} t & u & v & du & dv \\[8pt] 0 & 1 & 1 & 0 & 0 \\ 1 & '' & '' & '' & '' \\ \end{array}\)

\(\text{Orbit 2}\!\)

\(\begin{array}{c|cc|cc|cc|} t & u & v & du & dv & d^2 u & d^2 v \\[8pt] 0 & 0 & 0 & 0 & 1 & 1 & 0 \\ 1 & 0 & 1 & 1 & 1 & 1 & 1 \\ 2 & 1 & 0 & 0 & 0 & 0 & 0 \\ 3 & '' & '' & '' & '' & '' & '' \\ \end{array}\)

Type Markers

Composer P

\(\begin{array}{l} ((x \underset{A}{:} ~y \overset{B}{\underset{A}{:}}) \underset{B}{:} ~z \overset{C}{\underset{B}{:}}) \underset{C}{:} \end{array}\)

\(\begin{array}{l} ((x \overset{A}{:} ~y \overset{B}{\underset{A}{:}}) \overset{B}{:} ~z \overset{C}{\underset{B}{:}}) \overset{C}{:} \end{array}\)

\(\begin{array}{l} ((x \overset{A}{\Uparrow} ~y \overset{B}{\underset{A}{\Uparrow}}) \overset{B}{\Uparrow} ~z \overset{C}{\underset{B}{\Uparrow}}) \overset{C}{\Uparrow} \end{array}\)

\(\begin{array}{l} ((x \underset{A}{\Downarrow} ~y \overset{A}{\underset{B}{\Downarrow}}) \underset{B}{\Downarrow} ~z \overset{B}{\underset{C}{\Downarrow}}) \underset{C}{\Downarrow} \end{array}\)

\(\begin{array}{l} ((x \overset{ }{\underset{A}{\Downarrow}} ~ y \overset{A}{\underset{B}{\Downarrow}} ) \overset{ }{\underset{B}{\Downarrow}} ~ z \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{A}{\underset{B}{\Downarrow}} ~ (z \overset{B}{\underset{C}{\Downarrow}} ~ P \overset{B \Rightarrow C}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \end{array}\)

Transposer T

\(\begin{array}{l} (y \overset{ }{\underset{B}{\Downarrow}} ~ (x \overset{ }{\underset{A}{\Downarrow}} ~ z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ) \overset{B}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \\ \\ = \\ \\ (x \overset{ }{\underset{A}{\Downarrow}} ~ (y \overset{ }{\underset{B}{\Downarrow}} ~ (z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~ T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}} ) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}} ) \overset{A}{\underset{C}{\Downarrow}} ) \overset{ }{\underset{C}{\Downarrow}} \end{array}\)

Over And Under Setting

1. The conjunction \(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if every one of the \(q_j\!\) is true.

   \(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) is true  \(\Leftrightarrow\)  \(q_j\!\) is true for every \(j \in J.\)

2. The surjunction \(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if exactly one of the \(q_j\!\) is untrue.

   \(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) is true  \(\Leftrightarrow\)  \(q_j\!\) is untrue for unique \(j \in J.\)

Equation Sequences

\(\begin{array}{lll} [| \downharpoonleft s \downharpoonright |] & = & [| F |] \\[6pt] & = & F^{-1} (\underline{1}) \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ s ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) = \underline{1} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} = \underline{1} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{exclusive~or}~ y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \operatorname{just~one~true~of}~ x, y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{not~equal~to}~ y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \nLeftrightarrow y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \neq y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x + y ~\}. \end{array}\)

\(\begin{array}{lll} [| F^\$ (p, q) |] & = & [| \underline{(}~p~,~q~\underline{)}^\$ |] \\[6pt] & = & (F^\$ (p, q))^{-1} (\underline{1}) \\[6pt] & = & \{~ x \in X ~:~ F^\$ (p, q)(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \underline{(}~p~,~q~\underline{)}^\$ (x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \underline{(}~p(x)~,~q(x)~\underline{)} ~\} \\[6pt] & = & \{~ x \in X ~:~ p(x) + q(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ p(x) \neq q(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \upharpoonleft P \upharpoonright (x) ~\neq~ \upharpoonleft Q \upharpoonright (x) ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P ~\nLeftrightarrow~ x \in Q ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P\!-\!Q ~\operatorname{or}~ x \in Q\!-\!P ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P\!-\!Q ~\cup~ Q\!-\!P ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P + Q ~\} \\[6pt] & = & P + Q ~\subseteq~ X \\[6pt] & = & [|p|] + [|q|] ~\subseteq~ X \end{array}\)

Multiline TeX Formats

\( \begin{cases} a \\ b \\ c \\ \begin{cases} d \\ e \\ f \\ \end{cases} \\ g \\ h \\ i \\ \end{cases} \)

\(\begin{alignat}{2} x & = (y - z)(y + z) \\ & = y^2 - z^2 \\ \end{alignat}\)

\(\begin{align} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \begin{align} \underset{o \in O}{\operatorname{Conj}} \\ & \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) & = \\ & \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) & \\ \end{align} \\ & & \} & \\ \end{align}\)

\(\begin{align} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\ & & \} & \\ \end{align}\)

\(\begin{align} \operatorname{F2.2a.} \quad \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\ & & \} & \\ \end{align}\)

\(\begin{array}{lllll} \operatorname{F2.2a.} & \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & & \underset{o \in O}{\operatorname{Conj}}~ (\upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o)) \\ & & & \} & \\ \end{array}\)

Box Displays

Formal Grammars

\(\mathfrak{C} (\mathfrak{P}) : \text{Grammar 1}\!\)

\(\mathfrak{Q} = \varnothing\)

\(\begin{array}{rcll} 1. & S & :> & m_1 \ = \ ^{\backprime\backprime} \operatorname{~} ^{\prime\prime} \\ 2. & S & :> & p_j, \, \text{for each} \, j \in J \\ 3. & S & :> & \operatorname{Conc}^0 \ = \ ^{\backprime\backprime\prime\prime} \\ 4. & S & :> & \operatorname{Surc}^0 \ = \ ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime} \\ 5. & S & :> & S^* \\ 6. & S & :> & ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, S \, \cdot \, ( \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S \, )^* \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime} \\ \end{array}\)

\(\mathfrak{C} (\mathfrak{P}) : \text{Grammar 2}\!\)

\(\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}\)

\(\begin{array}{rcll} 1. & S & :> & \varepsilon \\ 2. & S & :> & m_1 \\ 3. & S & :> & p_j, \, \text{for each} \, j \in J \\ 4. & S & :> & S \, \cdot \, S \\ 5. & S & :> & ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime} \\ 6. & T & :> & S \\ 7. & T & :> & T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S \\ \end{array}\)

\(\mathfrak{C} (\mathfrak{P}) : \text{Grammar 3}\!\)

\(\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}\)

\(\begin{array}{rcll} 1. & S & :> & R \\ 2. & S & :> & F \\ 3. & S & :> & S \, \cdot \, S \\ 4. & R & :> & \varepsilon \\ 5. & R & :> & m_1 \\ 6. & R & :> & p_j, \, \text{for each} \, j \in J \\ 7. & R & :> & R \, \cdot \, R \\ 8. & F & :> & ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime} \\ 9. & T & :> & S \\ 10. & T & :> & T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S \\ \end{array}\)

\(\mathfrak{C} (\mathfrak{P}) : \text{Grammar 4}\!\)

\(\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T' \, ^{\prime\prime} \, \}\)

\(\begin{array}{rcll} 1. & S & :> & \varepsilon \\ 2. & S & :> & S' \\ 3. & S' & :> & m_1 \\ 4. & S' & :> & p_j, \, \text{for each} \, j \in J \\ 5. & S' & :> & ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime} \\ 6. & S' & :> & S' \, \cdot \, S' \\ 7. & T & :> & \varepsilon \\ 8. & T & :> & T' \\ 9. & T' & :> & T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S \\ \end{array}\)

\(\mathfrak{C} (\mathfrak{P}) : \text{Grammar 5}\!\)

\(\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}\)

\(\begin{array}{rcll} 1. & S & :> & \varepsilon \\ 2. & S & :> & S' \\ 3. & S' & :> & m_1 \\ 4. & S' & :> & p_j, \, \text{for each} \, j \in J \\ 5. & S' & :> & S' \, \cdot \, S' \\ 6. & S' & :> & ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime} \\ 7. & S' & :> & ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime} \\ 8. & T & :> & ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \\ 9. & T & :> & S' \\ 10. & T & :> & T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \\ 11. & T & :> & T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \, \cdot \, S' \\ \end{array}\)

\(\mathfrak{C} (\mathfrak{P}) : \text{Grammar 6}\!\)

\(\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}\)

\(\begin{array}{rcll} 1. & S & :> & \varepsilon \\ 2. & S & :> & S' \\ 3. & S' & :> & R \\ 4. & S' & :> & F \\ 5. & S' & :> & S' \, \cdot \, S' \\ 6. & R & :> & m_1 \\ 7. & R & :> & p_j, \, \text{for each} \, j \in J \\ 8. & R & :> & R \, \cdot \, R \\ 9. & F & :> & ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime} \\ 10. & F & :> & ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime} \\ 11. & T & :> & ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \\ 12. & T & :> & S' \\ 13. & T & :> & T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \\ 14. & T & :> & T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \, \cdot \, S' \\ \end{array}\)

Proof Schemata

Definition 1

Variant 1

			\(\text{Definition 1}\!\)
	\(\text{If}\!\)	\(Q \subseteq X\)
	\(\text{then}\!\)	\(\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}\)
	\(\text{such that:}\!\)
	\(\text{D1a.}\!\)	\(\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q\)	\(\forall x \in X\)

Variant 2

\(\text{Definition 1}\!\)

\(\text{If}\!\) \(Q ~\subseteq~ X\)   \(\text{then}\!\) \(\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}\)   \(\text{such that:}\!\)

\(\operatorname{D1a.}\) \(\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q\) \(\forall x \in X\)

Rule 1

			\(\text{Rule 1}\!\)
	\(\text{If}\!\)	\(Q \subseteq X\)
	\(\text{then}\!\)	\(\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}\)
	\(\text{and if}\!\)	\(x \in X\)
	\(\text{then}\!\)	\(\text{the following are equivalent:}\!\)
	\(\text{R1a.}\!\)	\(x \in Q\)
	\(\text{R1b.}\!\)	\(\upharpoonleft Q \upharpoonright (x)\)

Rule 2

			\(\text{Rule 2}\!\)
	\(\text{If}\!\)	\(f : X \to \underline\mathbb{B}\)
	\(\text{and}\!\)	\(x \in X\)
	\(\text{then}\!\)	\(\text{the following are equivalent:}\!\)
	\(\text{R2a.}\!\)	\(f(x)\!\)
	\(\text{R2b.}\!\)	\(f(x) = \underline{1}\)

Rule 3

Variant 1

			\(\text{Rule 3}\!\)
	\(\text{If}\!\)	\(Q \subseteq X\)
	\(\text{and}\!\)	\(x \in X\)
	\(\text{then}\!\)	\(\text{the following are equivalent:}\!\)
	\(\text{R3a.}\!\)	\(x \in Q\)	\(\text{R3a : R1a}\!\)
			\(::\!\)
	\(\text{R3b.}\!\)	\(\upharpoonleft Q \upharpoonright (x)\)	\(\text{R3b : R1b}\!\) \(\text{R3b : R2a}\!\)
			\(::\!\)
	\(\text{R3c.}\!\)	\(\upharpoonleft Q \upharpoonright (x) = \underline{1}\)	\(\text{R3c : R2b}\!\)

Variant 2

\(\operatorname{Rule~3}\)

\(\text{If}\!\) \(Q ~\subseteq~ X\)     \(\text{and}\!\) \(x ~\in~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R3a.}\) \(x ~\in~ Q\) \(\operatorname{R3a~:~R1a}\)       \(::\!\)   \(\operatorname{R3b.}\) \(\upharpoonleft Q \upharpoonright (x)\) \(\operatorname{R3b~:~R1b}\) \(\operatorname{R3b~:~R2a}\)       \(::\!\)   \(\operatorname{R3c.}\) \(\upharpoonleft Q \upharpoonright (x) ~=~ \underline{1}\) \(\operatorname{R3c~:~R2b}\)

Corollary 1

			\(\text{Corollary 1}\!\)
	\(\text{If}\!\)	\(Q \subseteq X\)
	\(\text{and}\!\)	\(x \in X\)
	\(\text{then}\!\)	\(\text{the following statement is true:}\!\)
	\(\text{C1a.}\!\)	\(x \in Q ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}\)	\(\text{R3a} \Leftrightarrow \text{R3c}\)

Rule 4

			\(\text{Rule 4}\!\)
	\(\text{If}\!\)	\(Q \subseteq X ~\text{is fixed}\)
	\(\text{and}\!\)	\(x \in X ~\text{is varied}\)
	\(\text{then}\!\)	\(\text{the following are equivalent:}\!\)
	\(\text{R4a.}\!\)	\(x \in Q\)
	\(\text{R4b.}\!\)	\(\downharpoonleft x \in Q \downharpoonright\)
	\(\text{R4c.}\!\)	\(\downharpoonleft x \in Q \downharpoonright (x)\)
	\(\text{R4d.}\!\)	\(\upharpoonleft Q \upharpoonright (x)\)
	\(\text{R4e.}\!\)	\(\upharpoonleft Q \upharpoonright (x) = \underline{1}\)

Logical Translation Rule 0

\(\text{Logical Translation Rule 0}\!\)

\(\text{If}\!\) \(s_j ~\text{is a sentence about things in the universe X}\)   \(\text{and}\!\) \(p_j ~\text{is a proposition about things in the universe X}\)   \(\text{such that:}\!\)     \(\text{L0a.}\!\) \(\downharpoonleft s_j \downharpoonright ~=~ p_j, ~\text{for all}~ j \in J,\)   \(\text{then}\!\) \(\text{the following equations are true:}\!\)

\(\text{L0b.}\!\) \(\downharpoonleft \operatorname{Conc}_j^J s_j \downharpoonright\) \(=\!\) \(\operatorname{Conj}_j^J \downharpoonleft s_j \downharpoonright\) \(=\!\) \(\operatorname{Conj}_j^J p_j\)   \(\text{L0c.}\!\) \(\downharpoonleft \operatorname{Surc}_j^J s_j \downharpoonright\) \(=\!\) \(\operatorname{Surj}_j^J \downharpoonleft s_j \downharpoonright\) \(=\!\) \(\operatorname{Surj}_j^J p_j\)

Logical Translation Rule 1

\(\text{Logical Translation Rule 1}\!\)

\(\text{If}\!\) \(s ~\text{is a sentence about things in the universe X}\)   \(\text{and}\!\) \(p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}\)   \(\text{such that:}\!\)     \(\text{L1a.}\!\) \(\downharpoonleft s \downharpoonright ~=~ p\)   \(\text{then}\!\) \(\text{the following equations hold:}\!\)

\(\text{L1b}_{00}.\!\) \(\downharpoonleft \operatorname{false} \downharpoonright\) \(=\!\) \((~)\) \(=\!\) \(\underline{0} ~:~ X \to \underline\mathbb{B}\)   \(\text{L1b}_{01}.\!\) \(\downharpoonleft \operatorname{not}~ s \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright)\) \(=\!\) \((p) ~:~ X \to \underline\mathbb{B}\)   \(\text{L1b}_{10}.\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(p ~:~ X \to \underline\mathbb{B}\)   \(\text{L1b}_{11}.\!\) \(\downharpoonleft \operatorname{true} \downharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(\underline{1} ~:~ X \to \underline\mathbb{B}\)

Geometric Translation Rule 1

\(\text{Geometric Translation Rule 1}\!\)

\(\text{If}\!\) \(Q \subseteq X\)   \(\text{and}\!\) \(p ~:~ X \to \underline\mathbb{B}\)   \(\text{such that:}\!\)     \(\text{G1a.}\!\) \(\upharpoonleft Q \upharpoonright ~=~ p\)   \(\text{then}\!\) \(\text{the following equations hold:}\!\)

\(\text{G1b}_{00}.\!\) \(\upharpoonleft \varnothing \upharpoonright\) \(=\!\) \((~)\) \(=\!\) \(\underline{0} ~:~ X \to \underline\mathbb{B}\)   \(\text{G1b}_{01}.\!\) \(\upharpoonleft {}^{_\sim} Q \upharpoonright\) \(=\!\) \((\upharpoonleft Q \upharpoonright)\) \(=\!\) \((p) ~:~ X \to \underline\mathbb{B}\)   \(\text{G1b}_{10}.\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(p ~:~ X \to \underline\mathbb{B}\)   \(\text{G1b}_{11}.\!\) \(\upharpoonleft X \upharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(\underline{1} ~:~ X \to \underline\mathbb{B}\)

Logical Translation Rule 2

\(\text{Logical Translation Rule 2}\!\)

\(\text{If}\!\) \(s, t ~\text{are sentences about things in the universe}~ X\)   \(\text{and}\!\) \(p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}\)   \(\text{such that:}\!\)     \(\text{L2a.}\!\) \(\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q\)   \(\text{then}\!\) \(\text{the following equations hold:}\!\)

\(\text{L2b}_{0}.\!\) \(\downharpoonleft \operatorname{false} \downharpoonright\) \(=\!\) \((~)\) \(=\!\) \((~)\)   \(\text{L2b}_{1}.\!\) \(\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)\) \(=\!\) \((p)(q)\!\)   \(\text{L2b}_{2}.\!\) \(\downharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright\) \(=\!\) \((p) q\!\)   \(\text{L2b}_{3}.\!\) \(\downharpoonleft \operatorname{not}~ s \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright)\) \(=\!\) \((p)\!\)   \(\text{L2b}_{4}.\!\) \(\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)\) \(=\!\) \(p (q)\!\)   \(\text{L2b}_{5}.\!\) \(\downharpoonleft \operatorname{not}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft t \downharpoonright)\) \(=\!\) \((q)\!\)   \(\text{L2b}_{6}.\!\) \(\downharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright)\) \(=\!\) \((p, q)\!\)   \(\text{L2b}_{7}.\!\) \(\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)\) \(=\!\) \((p q)\!\)   \(\text{L2b}_{8}.\!\) \(\downharpoonleft s ~\operatorname{and}~ t \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright\) \(=\!\) \(p q\!\)   \(\text{L2b}_{9}.\!\) \(\downharpoonleft s ~\operatorname{is~equivalent~to}~ t \downharpoonright\) \(=\!\) \(((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright))\) \(=\!\) \(((p, q))\!\)   \(\text{L2b}_{10}.\!\) \(\downharpoonleft t \downharpoonright\) \(=\!\) \(\downharpoonleft t \downharpoonright\) \(=\!\) \(q\!\)   \(\text{L2b}_{11}.\!\) \(\downharpoonleft s ~\operatorname{implies}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright))\) \(=\!\) \((p (q))\!\)   \(\text{L2b}_{12}.\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(p\!\)   \(\text{L2b}_{13}.\!\) \(\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright\) \(=\!\) \(((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)\) \(=\!\) \(((p) q)\!\)   \(\text{L2b}_{14}.\!\) \(\downharpoonleft s ~\operatorname{or}~ t \downharpoonright\) \(=\!\) \(((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))\) \(=\!\) \(((p)(q))\!\)   \(\text{L2b}_{15}.\!\) \(\downharpoonleft \operatorname{true} \downharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(((~))\)

Geometric Translation Rule 2

\(\text{Geometric Translation Rule 2}\!\)

\(\text{If}\!\) \(P, Q \subseteq X\)   \(\text{and}\!\) \(p, q ~:~ X \to \underline\mathbb{B}\)   \(\text{such that:}\!\)     \(\text{G2a.}\!\) \(\upharpoonleft P \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft Q \upharpoonright ~=~ q\)   \(\text{then}\!\) \(\text{the following equations hold:}\!\)

\(\text{G2b}_{0}.\!\) \(\upharpoonleft \varnothing \upharpoonright\) \(=\!\) \((~)\) \(=\!\) \((~)\)   \(\text{G2b}_{1}.\!\) \(\upharpoonleft \overline{P} ~\cap~ \overline{Q} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright)\) \(=\!\) \((p)(q)\!\)   \(\text{G2b}_{2}.\!\) \(\upharpoonleft \overline{P} ~\cap~ Q \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright\) \(=\!\) \((p) q\!\)   \(\text{G2b}_{3}.\!\) \(\upharpoonleft \overline{P} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright)\) \(=\!\) \((p)\!\)   \(\text{G2b}_{4}.\!\) \(\upharpoonleft P ~\cap~ \overline{Q} \upharpoonright\) \(=\!\) \(\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright)\) \(=\!\) \(p (q)\!\)   \(\text{G2b}_{5}.\!\) \(\upharpoonleft \overline{Q} \upharpoonright\) \(=\!\) \((\upharpoonleft Q \upharpoonright)\) \(=\!\) \((q)\!\)   \(\text{G2b}_{6}.\!\) \(\upharpoonleft P ~+~ Q \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright)\) \(=\!\) \((p, q)\!\)   \(\text{G2b}_{7}.\!\) \(\upharpoonleft \overline{P ~\cap~ Q} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright)\) \(=\!\) \((p q)\!\)   \(\text{G2b}_{8}.\!\) \(\upharpoonleft P ~\cap~ Q \upharpoonright\) \(=\!\) \(\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright\) \(=\!\) \(p q\!\)   \(\text{G2b}_{9}.\!\) \(\upharpoonleft \overline{P ~+~ Q} \upharpoonright\) \(=\!\) \(((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright))\) \(=\!\) \(((p, q))\!\)   \(\text{G2b}_{10}.\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(q\!\)   \(\text{G2b}_{11}.\!\) \(\upharpoonleft \overline{P ~\cap~ \overline{Q}} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright))\) \(=\!\) \((p (q))\!\)   \(\text{G2b}_{12}.\!\) \(\upharpoonleft P \upharpoonright\) \(=\!\) \(\upharpoonleft P \upharpoonright\) \(=\!\) \(p\!\)   \(\text{G2b}_{13}.\!\) \(\upharpoonleft \overline{\overline{P} ~\cap~ Q} \upharpoonright\) \(=\!\) \(((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright)\) \(=\!\) \(((p) q)\!\)   \(\text{G2b}_{14}.\!\) \(\upharpoonleft P ~\cup~ Q \upharpoonright\) \(=\!\) \(((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))\) \(=\!\) \(((p)(q))\!\)   \(\text{G2b}_{15}.\!\) \(\upharpoonleft X \upharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(((~))\)

Value Rule 1

Editing Note. There are several versions of this Rule in the last couple of drafts I can find. I will try to figure out what's at issue here as I mark them up.

Variant 1

\(\text{Value Rule 1}\!\)

\(\text{If}\!\) \(v, w ~\in~ \underline\mathbb{B}\)   \(\text{then}\!\) \(^{\backprime\backprime} v = w \, ^{\prime\prime} ~\text{is a sentence about pairs of values}~ (v, w) \in \underline\mathbb{B}^2,\)     \(\downharpoonleft v = w \downharpoonright ~\text{is a proposition} ~:~ \underline\mathbb{B}^2 \to \underline\mathbb{B},\)   \(\text{and}\!\) \(\text{the following are identical values in}~ \underline\mathbb{B}:\)

\(\text{V1a.}\!\) \(\downharpoonleft v = w \downharpoonright (v, w)\)   \(\text{V1b.}\!\) \(\downharpoonleft v \Leftrightarrow w \downharpoonright (v, w)\)   \(\text{V1c.}\!\) \(\underline{((}~ v ~,~ w ~\underline{))}\)

Variant 2

\(\text{Value Rule 1}\!\)

\(\text{If}\!\) \(v, w ~\in~ \underline\mathbb{B}\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\text{V1a.}\!\) \(v = w\!\)   \(\text{V1b.}\!\) \(v \Leftrightarrow w\)   \(\text{V1c.}\!\) \(\underline{((}~ v ~,~ w ~\underline{))}\)

Variant 3

A rule that allows one to turn equivalent sentences into identical propositions:

\((s ~\Leftrightarrow~ t) \quad \Leftrightarrow \quad (\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright)\)

Consider the following pair of expressions:

\(\downharpoonleft v ~=~ w \downharpoonright (v, w)\)

\(\downharpoonleft v(x) ~=~ w(x) \downharpoonright (x)\)

\(\text{Value Rule 1}\!\)

\(\text{If}\!\) \(v, w ~\in~ \underline\mathbb{B}\)   \(\text{then}\!\) \(\text{the following are identical values in}~ \underline\mathbb{B}:\)

\(\text{V1a.}\!\) \(\downharpoonleft v = w \downharpoonright\)   \(\text{V1b.}\!\) \(\downharpoonleft v \Leftrightarrow w \downharpoonright\)   \(\text{V1c.}\!\) \(\underline{((}~ v ~,~ w ~\underline{))}\)

Variant 4

\(\text{Value Rule 1}\!\)

\(\text{If}\!\) \(f, g ~:~ X \to \underline\mathbb{B}\)   \(\text{and}\!\) \(x ~\in~ X\)   \(\text{then}\!\) \(\text{the following are identical values in}~ \underline\mathbb{B}:\)

\(\text{V1a.}\!\) \(\downharpoonleft f(x) ~=~ g(x) \downharpoonright\)   \(\text{V1b.}\!\) \(\downharpoonleft f(x) ~\Leftrightarrow~ g(x) \downharpoonright\)   \(\text{V1c.}\!\) \(\underline{((}~ f(x) ~,~ g(x) ~\underline{))}\)

Variant 5

\(\text{Value Rule 1}\!\)

\(\text{If}\!\) \(f, g ~:~ X \to \underline\mathbb{B}\)   \(\text{then}\!\) \(\text{the following are identical propositions on}~ X:\)

\(\text{V1a.}\!\) \(\downharpoonleft f ~=~ g \downharpoonright\)   \(\text{V1b.}\!\) \(\downharpoonleft f ~\Leftrightarrow~ g \downharpoonright\)   \(\text{V1c.}\!\) \(\underline{((}~ f ~,~ g ~\underline{))}^\$\)

Evaluation Rule 1

\(\operatorname{Evaluation~Rule~1}\)

\(\text{If}\!\) \(f, g ~:~ X \to \underline\mathbb{B}\)   \(\text{and}\!\) \(x ~\in~ X\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{E1a.}\) \(f(x) ~=~ g(x)\) \(\operatorname{E1a~:~V1a}\)   \(::\!\)   \(\operatorname{E1b.}\) \(f(x) ~\Leftrightarrow~ g(x)\) \(\operatorname{E1b~:~V1b}\)   \(::\!\)   \(\operatorname{E1c.}\) \(\underline{((}~ f(x) ~,~ g(x) ~\underline{))}\) \(\operatorname{E1c~:~V1c}\) \(\operatorname{E1c~:~$1a}\)   \(::\!\)   \(\operatorname{E1d.}\) \(\underline{((}~ f ~,~ g ~\underline{))}^\$ (x)\) \(\operatorname{E1d~:~$1b}\)

Definition 2

Variant 1

\(\operatorname{Definition~2}\)

\(\text{If}\!\) \(P, Q ~\subseteq~ X\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{D2a.}\) \(P ~=~ Q\)     \(\operatorname{D2b.}\) \(x \in P ~\Leftrightarrow~ x \in Q\) \(\forall x \in X\)

Variant 2

\(\operatorname{Definition~2}\)

\(\text{If}\!\) \(P, Q ~\subseteq~ X\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{D2a.}\) \(P ~=~ Q\)   \(\operatorname{D2b.}\) \(\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)\)

Definition 3

Variant 1

\(\operatorname{Definition~3}\)

\(\text{If}\!\) \(f, g ~:~ X \to Y\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{D3a.}\) \(f ~=~ g\)     \(\operatorname{D3b.}\) \(f(x) ~=~ g(x)\) \(\forall x \in X\)

Variant 2

\(\operatorname{Definition~3}\)

\(\text{If}\!\) \(f, g ~:~ X \to Y\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{D3a.}\) \(f ~=~ g\)   \(\operatorname{D3b.}\) \(\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))\)

Variant 3

\(\operatorname{Definition~3}\)

\(\text{If}\!\) \(f, g ~:~ X \to Y\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{D3a.}\) \(f ~=~ g\)   \(\operatorname{D3b.}\) \(\prod_x^X~ (f(x) ~=~ g(x))\)

Definition 4

\(\operatorname{Definition~4}\)

\(\text{If}\!\) \(Q ~\subseteq~ X\)   \(\text{then}\!\) \(\text{the following are identical subsets of}~ X \times \underline\mathbb{B}:\)

\(\operatorname{D4a.}\) \(\upharpoonleft Q \upharpoonright\)   \(\operatorname{D4b.}\) \(\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright\)

Definition 5

Variant 1

\(\operatorname{Definition~5}\)

\(\text{If}\!\) \(Q ~\subseteq~ X\)   \(\text{then}\!\) \(\text{the following are identical propositions:}\!\)

\(\operatorname{D5a.}\) \(\upharpoonleft Q \upharpoonright\)   \(\operatorname{D5b.}\) \(\begin{array}{lcl} f & : & X \to \underline\mathbb{B} \\ f(x) & = & \downharpoonleft x \in Q \downharpoonright \quad (\forall x \in X) \end{array}\)

Variant 2

\(\operatorname{Definition~5}\)

\(\text{If}\!\) \(Q ~\subseteq~ X\)   \(\text{then}\!\) \(\text{the following are identical propositions:}\!\)

\(\operatorname{D5a.}\) \(\upharpoonleft Q \upharpoonright\)   \(\operatorname{D5b.}\) \(\begin{array}{ccccl} f & : & X & \to & \underline\mathbb{B} \\ f & : & x & \mapsto & \downharpoonleft x \in Q \downharpoonright \end{array}\)

Variant 3

\(\operatorname{Definition~5}\)

\(\text{If}\!\) \(Q ~\subseteq~ X\)   \(\text{then}\!\) \(\text{the following are identical propositions} ~:~ X \to \underline\mathbb{B}\)

\(\operatorname{D5a.}\) \(\upharpoonleft Q \upharpoonright\)   \(\operatorname{D5b.}\) \(\downharpoonleft x \in Q \downharpoonright\)

Definition 6

\(\operatorname{Definition~6}\)

\(\text{If}\!\) \(\text{each string}~ s_j, ~\text{as}~ j ~\text{ranges over the set}~ J,\)     \(\text{is a sentence about things in the universe}~ X~\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{D6a.}\) \(\overset{J}{\underset{j}{\forall}}~ s_j\)   \(\operatorname{D6b.}\) \(\operatorname{Conj}_j^J s_j\)

Definition 7

\(\operatorname{Definition~7}\)

\(\text{If}\!\) \(s, t ~\text{are sentences about things in the universe}~ X\)   \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{D7a.}\) \(s ~\Leftrightarrow~ t\)   \(\operatorname{D7b.}\) \(\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright\)

Rule 5

\(\operatorname{Rule~5}\)

\(\text{If}\!\) \(P, Q ~\subseteq~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R5a.}\) \(P ~=~ Q\) \(\operatorname{R5a~:~D2a}\)       \(::\!\)   \(\operatorname{R5b.}\) \(\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)\) \(\operatorname{R5b~:~D2b}\) \(\operatorname{R5b~:~D7a}\)       \(::\!\)   \(\operatorname{R5c.}\) \(\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright)\) \(\operatorname{R5c~:~D7b}\) \(\operatorname{R5c~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{R5d.}\) \(\begin{matrix} \{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in P \downharpoonright \\ = \\ \{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright \end{matrix}\) \(\operatorname{R5d~:~\_\_?\_\_}\) \(\operatorname{R5d~:~D5b}\)       \(::\!\)   \(\operatorname{R5e.}\) \(\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright\) \(\operatorname{R5e~:~D5a}\)

Rule 6

\(\operatorname{Rule~6}\)

\(\text{If}\!\) \(f, g ~:~ X \to Y\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R6a.}\) \(f ~=~ g\) \(\operatorname{R6a~:~D3a}\)       \(::\!\)   \(\operatorname{R6b.}\) \(\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))\) \(\operatorname{R6b~:~D3b}\) \(\operatorname{R6b~:~D6a}\)       \(::\!\)   \(\operatorname{R6c.}\) \(\operatorname{Conj_x^X}~ (f(x) ~=~ g(x))\) \(\operatorname{R6c~:~D6b}\)

Rule 7

\(\operatorname{Rule~7}\)

\(\text{If}\!\) \(p, q ~:~ X \to \underline\mathbb{B}\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R7a.}\) \(p ~=~ q\) \(\operatorname{R7a~:~R6a}\)       \(::\!\)   \(\operatorname{R7b.}\) \(\overset{X}{\underset{x}{\forall}}~ (p(x) ~=~ q(x))\) \(\operatorname{R7b~:~R6b}\)       \(::\!\)   \(\operatorname{R7c.}\) \(\operatorname{Conj_x^X}~ (p(x) ~=~ q(x))\) \(\operatorname{R7c~:~R6c}\) \(\operatorname{R7c~:~P1a}\)       \(::\!\)   \(\operatorname{R7d.}\) \(\operatorname{Conj_x^X}~ (p(x) ~\Leftrightarrow~ q(x))\) \(\operatorname{R7d~:~P1b}\)       \(::\!\)   \(\operatorname{R7e.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}\) \(\operatorname{R7e~:~P1c}\) \(\operatorname{R7e~:~$1a}\)       \(::\!\)   \(\operatorname{R7f.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ p ~,~ q ~\underline{))}^\$ (x)\) \(\operatorname{R7f~:~$1b}\)

Rule 8

\(\operatorname{Rule~8}\)

\(\text{If}\!\) \(s, t ~\text{are sentences about things in}~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R8a.}\) \(s ~\Leftrightarrow~ t\) \(\operatorname{R8a~:~D7a}\)       \(::\!\)   \(\operatorname{R8b.}\) \(\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright\) \(\operatorname{R8b~:~D7b}\) \(\operatorname{R8b~:~R7a}\)       \(::\!\)   \(\operatorname{R8c.}\) \(\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))\) \(\operatorname{R8c~:~R7b}\)       \(::\!\)   \(\operatorname{R8d.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))\) \(\operatorname{R8d~:~R7c}\)       \(::\!\)   \(\operatorname{R8e.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft t \downharpoonright (x))\) \(\operatorname{R8e~:~R7d}\)       \(::\!\)   \(\operatorname{R8f.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright (x) ~,~ \downharpoonleft t \downharpoonright (x) ~\underline{))}\) \(\operatorname{R8f~:~R7e}\)       \(::\!\)   \(\operatorname{R8g.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{R8g~:~R7f}\)

Rule 9

\(\operatorname{Rule~9}\)

\(\text{If}\!\) \(P, Q ~\subseteq~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R9a.}\) \(P ~=~ Q\) \(\operatorname{R9a~:~R5a}\)       \(::\!\)   \(\operatorname{R9b.}\) \(\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright\) \(\operatorname{R9b~:~R5e}\) \(\operatorname{R9b~:~R7a}\)       \(::\!\)   \(\operatorname{R9c.}\) \(\overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{R9c~:~R7b}\)       \(::\!\)   \(\operatorname{R9d.}\) \(\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{R9d~:~R7c}\)       \(::\!\)   \(\operatorname{R9e.}\) \(\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{R9e~:~R7d}\)       \(::\!\)   \(\operatorname{R9f.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}\) \(\operatorname{R9f~:~R7e}\)       \(::\!\)   \(\operatorname{R9g.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{R9g~:~R7f}\)

Rule 10

\(\operatorname{Rule~10}\)

\(\text{If}\!\) \(P, Q ~\subseteq~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R10a.}\) \(P ~=~ Q\) \(\operatorname{R10a~:~D2a}\)       \(::\!\)   \(\operatorname{R10b.}\) \(\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)\) \(\operatorname{R10b~:~D2b}\) \(\operatorname{R10b~:~R8a}\)       \(::\!\)   \(\operatorname{R10c.}\) \(\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright\) \(\operatorname{R10c~:~R8b}\)       \(::\!\)   \(\operatorname{R10d.}\) \(\overset{X}{\underset{x}{\forall}}~ \downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x)\) \(\operatorname{R10d~:~R8c}\)       \(::\!\)   \(\operatorname{R10e.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x))\) \(\operatorname{R10e~:~R8d}\)       \(::\!\)   \(\operatorname{R10f.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft x \in Q \downharpoonright (x))\) \(\operatorname{R10f~:~R8e}\)       \(::\!\)   \(\operatorname{R10g.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright (x) ~,~ \downharpoonleft x \in Q \downharpoonright (x) ~\underline{))}\) \(\operatorname{R10g~:~R8f}\)       \(::\!\)   \(\operatorname{R10h.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright ~,~ \downharpoonleft x \in Q \downharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{R10h~:~R8g}\)

Rule 11

\(\operatorname{Rule~11}\)

\(\text{If}\!\) \(Q ~\subseteq~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{R11a.}\) \(Q ~=~ \{ x \in X ~:~ s \}\) \(\operatorname{R11a~:~R5a}\)       \(::\!\)   \(\operatorname{R11b.}\) \(\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright\) \(\operatorname{R11b~:~R5e}\)       \(::\!\)   \(\operatorname{R11c.}\) \(\begin{array}{lcl} \upharpoonleft Q \upharpoonright & \subseteq & X \times \underline\mathbb{B} \\ \upharpoonleft Q \upharpoonright & = & \{ (x, y) \in X \times \underline\mathbb{B} ~:~ y = \, \downharpoonleft s \downharpoonright (x) \} \end{array}\) \(\operatorname{R11c~:~\_\_?\_\_}\) \(\operatorname{R11c~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{R11d.}\) \(\begin{array}{ccccl} \upharpoonleft Q \upharpoonright & : & X & \to & \underline\mathbb{B} \\ \upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x) \end{array}\) \(\operatorname{R11d~:~\_\_?\_\_}\) \(\operatorname{R11d~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{R11e.}\) \(\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)\) \(\operatorname{R11e~:~\_\_?\_\_}\) \(\operatorname{R11e~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{R11f.}\) \(\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright\) \(\operatorname{R11f~:~\_\_?\_\_}\)

Fact 1

Variant 1

\(\operatorname{Fact~1}\)

\(\text{If}\!\) \(P, Q ~\subseteq~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{F1a.}\) \(s \quad \Leftrightarrow \quad (P ~=~ Q)\) \(\operatorname{F1a~:~R9a}\)       \(::\!\)   \(\operatorname{F1b.}\) \(s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)\) \(\operatorname{F1b~:~R9b}\)       \(::\!\)   \(\operatorname{F1c.}\) \(s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{F1c~:~R9c}\)       \(::\!\)   \(\operatorname{F1d.}\) \(s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{F1d~:~R9d}\) \(\operatorname{F1d~:~R8a}\)       \(::\!\)   \(\operatorname{F1e.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright\) \(\operatorname{F1e~:~R8b}\) \(\operatorname{F1e~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{F1f.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright\) \(\operatorname{F1f~:~\_\_?\_\_}\) \(\operatorname{F1f~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{F1g.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}\) \(\operatorname{F1g~:~\_\_?\_\_}\) \(\operatorname{F1g~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{F1h.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{F1h~:~~\_\_?\_\_}\)

Variant 2

\(\operatorname{Fact~1}\)

\(\text{If}\!\) \(P, Q ~\subseteq~ X\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{F1a.}\) \(s \quad \Leftrightarrow \quad (P ~=~ Q)\) \(\operatorname{F1a~:~R9a}\)       \(::\!\)   \(\operatorname{F1b.}\) \(s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)\) \(\operatorname{F1b~:~R9b}\)       \(::\!\)   \(\operatorname{F1c.}\) \(s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{F1c~:~R9c}\)       \(::\!\)   \(\operatorname{F1d.}\) \(s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{F1d~:~R9d}\) \(\operatorname{F1d~:~R8a}\)       \(::\!\)   \(\operatorname{F1e.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright\) \(\operatorname{F1e~:~R8b}\) \(\operatorname{F1e~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{F1f.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright\) \(\operatorname{F1f~:~\_\_?\_\_}\) \(\operatorname{F1f~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{F1g.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}\) \(\operatorname{F1g~:~\_\_?\_\_}\) \(\operatorname{F1g~:~\_\_?\_\_}\)       \(::\!\)   \(\operatorname{F1h.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{F1h~:~~\_\_?\_\_}\)

Definition 8

\(\operatorname{Definition~8}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)   \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times I \, :\)

\(\operatorname{D8a.}\) \(L_{SI}\!\)   \(\operatorname{D8b.}\) \(\operatorname{Con}^L\)   \(\operatorname{D8c.}\) \(\operatorname{Con}(L)\)   \(\operatorname{D8d.}\) \(\operatorname{proj}_{SI}(L)\)   \(\operatorname{D8e.}\) \(\{ (s, i) \in S \times I ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}\)

Definition 9

\(\operatorname{Definition~9}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)   \(\text{then}\!\) \(\text{the following are identical subsets of}~ I \times S \, :\)

\(\operatorname{D9a.}\) \(L_{IS}\!\)   \(\operatorname{D9b.}\) \(\overset{\smile}{L_{SI}}\)   \(\operatorname{D9c.}\) \(\overset{\smile}{\operatorname{Con}^L}\)   \(\operatorname{D9d.}\) \(\overset{\smile}{\operatorname{Con}(L)}\)   \(\operatorname{D9e.}\) \(\operatorname{proj}_{IS}(L)\)   \(\operatorname{D9f.}\) \(\operatorname{Conv}(\operatorname{Con}(L))\)   \(\operatorname{D9g.}\) \(\{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}\)

Definition 10

\(\operatorname{Definition~10}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)   \(\text{then}\!\) \(\text{the following are identical subsets of}~ O \times S \, :\)

\(\operatorname{D10a.}\) \(L_{OS}\!\)   \(\operatorname{D10b.}\) \(\operatorname{Den}^L\)   \(\operatorname{D10c.}\) \(\operatorname{Den}(L)\)   \(\operatorname{D10d.}\) \(\operatorname{proj}_{OS}(L)\)   \(\operatorname{D10e.}\) \(\{ (o, s) \in O \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}\)

Definition 11

\(\operatorname{Definition~11}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)   \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times O \, :\)

\(\operatorname{D11a.}\) \(L_{SO}\!\)   \(\operatorname{D11b.}\) \(\overset{\smile}{L_{OS}}\)   \(\operatorname{D11c.}\) \(\overset{\smile}{\operatorname{Den}^L}\)   \(\operatorname{D11d.}\) \(\overset{\smile}{\operatorname{Den}(L)}\)   \(\operatorname{D11e.}\) \(\operatorname{proj}_{SO}(L)\)   \(\operatorname{D11f.}\) \(\operatorname{Conv}(\operatorname{Den}(L))\)   \(\operatorname{D11g.}\) \(\{ (s, o) \in S \times O ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}\)

Definition 12

\(\operatorname{Definition~12}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)   \(\text{and}\!\) \(x ~\in~ S\)   \(\text{then}\!\) \(\text{the following are identical subsets of}~ O \, :\)

\(\operatorname{D12a.}\) \(L_{OS} \cdot x\)   \(\operatorname{D12b.}\) \(\operatorname{Den}^L \cdot x\)   \(\operatorname{D12c.}\) \(\operatorname{Den}^L |_x\)   \(\operatorname{D12d.}\) \(\operatorname{Den}^L (-, x)\)   \(\operatorname{D12e.}\) \(\operatorname{Den}(L, x)\)   \(\operatorname{D12f.}\) \(\operatorname{Den}(L) \cdot x\)   \(\operatorname{D12g.}\) \(\{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}\)   \(\operatorname{D12h.}\) \(\{ o \in O ~:~ (o, x, i) \in L ~\operatorname{for~some}~ i \in I \}\)

Definition 13

\(\operatorname{Definition~13}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)   \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times I \, :\)

\(\operatorname{D13a.}\) \(\operatorname{Der}^L\)   \(\operatorname{D13b.}\) \(\operatorname{Der}(L)\)   \(\operatorname{D13c.}\) \(\{ (x, y) \in S \times I ~:~ \operatorname{Den}^L|_x = \operatorname{Den}^L|_y \}\)   \(\operatorname{D13d.}\) \(\{ (x, y) \in S \times I ~:~ \operatorname{Den}(L, x) = \operatorname{Den}(L, y) \}\)

Fact 2.1

\(\operatorname{Fact~2.1}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)     \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times I :\)

\(\operatorname{F2.1a.}\) \(\operatorname{Der}^L\) \(\operatorname{F2.1a~:~D13a}\)       \(::\!\)   \(\operatorname{F2.1b.}\) \(\operatorname{Der}(L)\) \(\operatorname{F2.1b~:~D13b}\)       \(::\!\)   \(\operatorname{F2.1c.}\) \(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \operatorname{Den}(L, x) ~=~ \operatorname{Den}(L, y) \\ \} & \\ \end{array}\) \(\operatorname{F2.1c~:~D13c}\) \(\operatorname{F2.1c~:~R9a}\)       \(::\!\)   \(\operatorname{F2.1d.}\) \(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright \\ \} & \\ \end{array}\) \(\operatorname{F2.1d~:~R9b}\)       \(::\!\)   \(\operatorname{F2.1e.}\) \(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \overset{O}{\underset{o}{\forall}}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) \\ \} & \\ \end{array}\) \(\operatorname{F2.1e~:~R9c}\)       \(::\!\)   \(\operatorname{F2.1f.}\) \(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \underset{o \in O}{\operatorname{Conj}}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) \\ \} & \\ \end{array}\) \(\operatorname{F2.1f~:~R9d}\)       \(::\!\)   \(\operatorname{F2.1g.}\) \(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) ~\underline{))} \\ \} & \\ \end{array}\) \(\operatorname{F2.1g~:~R9e}\)       \(::\!\)   \(\operatorname{F2.1h.}\) \(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright ~\underline{))}^\$ (o) \\ \} & \\ \end{array}\) \(\operatorname{F2.1h~:~R9f}\) \(\operatorname{F2.1h~:~D12e}\)       \(::\!\)   \(\operatorname{F2.1i.}\) \(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft L_{OS} \cdot x \upharpoonright ~,~ \upharpoonleft L_{OS} \cdot y \upharpoonright ~\underline{))}^\$ (o) \\ \} & \\ \end{array}\) \(\operatorname{F2.1i~:~D12a}\)

Fact 2.2

Variant 1

\(\operatorname{Fact~2.2}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{F2.2a.}\) \(\begin{array}{cccl} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \begin{array}{ccl} \underset{o \in O}{\operatorname{Conj}} \\ & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & ) & \\ \end{array} \\ & & \} & \\ \end{array}\) \(\operatorname{F2.2a~:~R11a}\)   \(::\!\)   \(\operatorname{F2.2b.}\) \(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \upharpoonleft & \{ & (x, y) \in S \times I ~: \\ & & & & \begin{array}{ccl} \underset{o \in O}{\operatorname{Conj}} \\ & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & ) & \\ \end{array} \\ & & & \} & \\ & & \upharpoonright & & \\ \end{array}\) \(\operatorname{F2.2b~:~R11b}\)   \(::\!\)   \(\operatorname{F2.2c.}\) \(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{cccl} \downharpoonleft & \underset{o \in O}{\operatorname{Conj}} \\ & & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & & ) & \\ \downharpoonright & & \\ \end{array} \\ & & \} & \\ \end{array}\) \(\operatorname{F2.2c~:~R11c}\)   \(::\!\)   \(\operatorname{F2.2d.}\) \(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{cccl} \underset{o \in O}{\operatorname{Conj}} \\ & \downharpoonleft & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & & ) & \\ & \downharpoonright & & \\ \end{array} \\ & & \} & \\ \end{array}\) \(\operatorname{F2.2d~:~Log}\)   \(::\!\)   \(\operatorname{F2.2e.}\) \(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{ccl} \underset{o \in O}{\operatorname{Conj}} \\ & \underline{((} & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & , & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & \underline{))} & \\ \end{array} \\ & & \} & \\ \end{array}\) \(\operatorname{F2.2e~:~Log}\)   \(::\!\)   \(\operatorname{F2.2f.}\) \(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{cll} \underset{o \in O}{\operatorname{Conj}} \\ & \underline{((} & \upharpoonleft \operatorname{Den}^L x \upharpoonright \\ & , & \upharpoonleft \operatorname{Den}^L y \upharpoonright \\ & \underline{))}^\$ & (o) \\ \end{array} \\ & & \} & \\ \end{array}\) \(\operatorname{F2.2f~:~$~}\)

Variant 2

\(\operatorname{Fact~2.2}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\begin{align} \operatorname{F2.2a.} \quad \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \underset{o \in O}{\operatorname{Conj}} \, (\upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \, = \, \upharpoonleft \operatorname{Den}^L y \upharpoonright (o)) \\ & & \} & \\ \end{align}\) \(\operatorname{F2.2a~:~R11a}\)   \(::\!\)   \(\operatorname{F2.2b.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright\) \(\operatorname{F2.2b~:~R11b}\)   \(::\!\)   \(\operatorname{F2.2c.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright\) \(\operatorname{F2.2c~:~R11c}\)   \(::\!\)   \(\operatorname{F2.2d.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright\) \(\operatorname{F2.2d~:~Log}\)   \(::\!\)   \(\operatorname{F2.2e.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright\) \(\operatorname{F2.2e~:~Log}\)   \(::\!\)   \(\operatorname{F2.2f.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright\) \(\operatorname{F2.2f~:~$~}\)

Fact 2.3

\(\operatorname{Fact~2.3}\)

\(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)     \(\text{then}\!\) \(\text{the following are equivalent:}\!\)

\(\operatorname{F2.3a.}\) \(\begin{array}{cccl} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \begin{array}{ccl} \underset{o \in O}{\operatorname{Conj}} \\ & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & ) & \\ \end{array} \\ & & \} & \\ \end{array}\) \(\operatorname{F2.3a~:~R11a}\)   \(::\!\)   \(\operatorname{F2.3b.}\) \(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \downharpoonleft & \underset{o \in O}{\operatorname{Conj}} \\ & & & & \begin{array}{cl} ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ ) & \\ \end{array} \\ & & \downharpoonright & & \\ \end{array}\) \(\operatorname{F2.3b~:~R11d}\)   \(::\!\)   \(\operatorname{F2.3c.}\) \(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{ccl} \downharpoonleft & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & ) & \\ \downharpoonright & & \\ \end{array} \\ & & & \\ \end{array}\) \(\operatorname{F2.3c~:~Log}\)   \(::\!\)   \(\operatorname{F2.3d.}\) \(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{ccl} \downharpoonleft & ( & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\ & = & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\ & ) & \\ \downharpoonright & & \\ \end{array} \\ & & & \\ \end{array}\) \(\operatorname{F2.3d~:~Def}\)   \(::\!\)   \(\operatorname{F2.3e.}\) \(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{cl} \underline{((} & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\ , & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\ \underline{))} & \\ \end{array} \\ & & & \\ \end{array}\) \(\operatorname{F2.3e~:~Log}\) \(\operatorname{F2.3e~:~D10b}\)   \(::\!\)   \(\operatorname{F2.3f.}\) \(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{cl} \underline{((} & \upharpoonleft L_{OS} \upharpoonright (o, x) \\ , & \upharpoonleft L_{OS} \upharpoonright (o, y) \\ \underline{))} & \\ \end{array} \\ & & & \\ \end{array}\) \(\operatorname{F2.3f~:~D10a}\)