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