EQ 2: Textual Replacement

prev: Table of Precedences


E [x := R] or \(E _{R} ^{x} \) denotes an expression that is the same as E, but with all the occurrences of x replaced by "(R)". Unnecessary parentheses maybe removed after substitution.

e.g: (z + y) [z := 5] becomes ((5) + y) becomes (by removing unnecessary parentheses) (5 + y)

If x is a list of *distinct* \( x_1, x_2,...x_n\) of variables and R a list \(R_1\ , R_2 , ... R_n\) of expressions then \(E _{R} ^{x} \) denotes the *simultaneous* replacement in E of the variables of x by corresponding expressions of R, each expression being enclosed by parentheses.

(z + y) [z,y := 5,6] becomes ((5) + (6)) becomes (by removing unnecessary parentheses) (5 + 6)

next: Inference Rules

EQ 1: Precedences

Precedences (from high to low)

(1) [x := e] (Textual Substitution)

(2) . (function application)

(3) Unary Prefix Operators + - \( \neg \) # ~ \( \mathcal { P } \)

(4) **

(5) \( \ast \) / \( \div \) mod gcd

(6) + - \( \cup \) \( \cap \) \( \times \) \( \circ \) \( \bullet \)

(7) \( \downarrow \) \( \uparrow \)

(8) #

(9) \( \triangleright \) \( \triangleleft \) ^

(10) = < > \( \epsilon \) \( \subset \) \( \subseteq \) \( \supset \) \( \supseteq \) |

(11) \( \vee \) \( \wedge \)

(12) \( \Rightarrow \) \( \Leftarrow \)

(13) \( \equiv \)

Notes: All non associative prefix binary operators associate to the left, except ** , \( \triangleleft \) and \( \Rightarrow \) which associate to the right.


All operators on lines 10, 12 and 13 may have a slash / through them to denote negation.

Thus b \( \not\equiv \) c is equivalent to \( \neg \) ( b \( \equiv \) c )


A core subset of the above, omitting unnecessary symbols, which is used to prove the theorems of the logic itself is as follows

(a) [x := e] (Textual Substitution)

(b) . (function application)

(c) \( \neg \)

(d) \( \ast \) /

(e) =

(f) \( \vee \) \( \wedge \)

(g) \( \Rightarrow \) \( \Leftarrow \)

(h) \( \equiv \)

prev: next: Textual Substitution

Testing Latex Rendering

Just some random text


\[ 1 + \frac{q^2}{(1-q)}+\frac{q^6}{(1-q)(1-q^2)}+\cdots =


\prod_{j=0}^{\infty}\frac{1}{(1-q^{5j+2})(1-q^{5j+3})},

\quad\quad \text{for} |q|<1. \]


\[ \begin{aligned}

\nabla \times \vec{\mathbf{B}} -\, \frac1c\, \frac{\partial\vec{\mathbf{E}}}{\partial t} & = \frac{4\pi}{c}\vec{\mathbf{j}} \\ \nabla \cdot \vec{\mathbf{E}} & = 4 \pi \rho \\

\nabla \times \vec{\mathbf{E}}\, +\, \frac1c\, \frac{\partial\vec{\mathbf{B}}}{\partial t} & = \vec{\mathbf{0}} \\


\nabla \cdot \vec{\mathbf{B}} & = 0 \end{aligned}

\]


embedded latex

More MathJax tests. Embedding formulae inside sentences

The formula \( \prod_{j=0}^{\infty}\frac{1}{(1-q^{5j+2})(1-q^{5j+3})}, \quad\quad \text{for} |q|<1. \) embedded in the middle of a sentence

This expression \(\sqrt{3x-1}+(1+x)^2\) is an example of an inline equation.



The question is Prove Universal Instantiation i.e

Prove \( (\forall x |: P) \Rightarrow P [ x := E ] \)

LHS \( \hspace{2 cm } (\forall x |: P) \)

= \( \hspace{0.5 cm } \) notation expansion

\( \hspace{2 cm } (\forall x | true : P) \)

= \( \hspace{0.5 cm } \) true \( \equiv a \vee \neg a \)

\( \hspace{2 cm } (\forall x | (x = E) \vee (x \neq E) : P) \)

= \( \hspace{0.5 cm } \) Axiom: Range Split \( (\star | R \vee S: P) \equiv (\star | R : P) \star (\star | S : P) \) here \( \star = \wedge. \) notated as \( \forall \)


\( \hspace{2 cm } (\forall x | (x = E) : P) \wedge (\forall x | (x \neq E) : P) \)

\( \Rightarrow \hspace{0.5 cm } Theorem: a \wedge b \Rightarrow a \)

\( \hspace{2 cm } (\forall x | (x = E) : P) \)

= \( \hspace{0.5 cm } \) Single Point Axiom \( (\star y | (y = F) : Q) \equiv \) Q [ y := F ]

\( \hspace{2 cm } \) P [ x := E ] = RHS.
QED