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