## Friday, September 23, 2011

### 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

## Wednesday, September 21, 2011

### 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