> Let X →Y denote the set of functions from X to Y. Let X ×Y denote the set of binary relations over X and Y . Let D be a domain that is the union of integers Z and functions Z → Z. Boolean values are essentially integers. To make it clear, we use T for non-zero integers, which represent the true value, and F for zero, which represents the false value. You can't use symbols without first defining them. You have defined X->Y without first saying what X and Y are. XxY is *not* the set of binary relations over X and Y. A binary relation is a subset of XxY. A set of binary relations would be a subset of 2^(XxY) --- i.e., a set, each of whose elements is a subset of XxY. That is not what you mean. Here is a correct way to write this part: Let X and Y be sets. X->Y denotes the set of functions from X to Y. X\times Y denotes the Cartesian product of X and Y, i.e., the set of ordered pairs (x,y), with x\in X and y\in Y. Let \Z denote the set of integers. [Do you also want the set of natural numbers, \N = {0,1,...} ?] The set \D is a little weird. Maybe it would help if it had the symbol Z in it somewhere. Like \D_{\Z}. And what is a "domain"? Just say Let \[ \D_{\Z} = \Z \cup (\Z->\Z). \] What do you mean Boolean values are essentially integers? This is just vague. I would delete it. What do you mean we use T for non-zero integers? That is also vague. Is T the set of all non-zero integers, or one particular non-zero integer? Which one? I don't see the point (yet) of this notational choice. >The notion sequence is a finite enumerated collection of elements... Let me try to rewrite this: Let S be a set. The set of all finite sequences of elements of S is denoted S^*. Let $\xi=s_0s_1\cdots s_{n-1}$ be an element of S^*. The \emph{length} of $\xi$, denoted $|\xi|$, is $n$. The empty sequence, i.e., the unique element of S^* of length $0$, is denoted $\epsilon$. If $\zeta=s'_0\cdots s'_{m-1}$ is also an element of $S^*$, then the \emph{concatenation} of $\xi$ and $\zeta$, denoted $\xi\circ\zeta$, is the sequence $s_0\cdots s_{n-1}s'_0\cdots s'_{m-1}$. Note $|\xi\circ\zeta|=|\xi|+|\zeta|$. If |\xi|\geq 1, define $\head(\xi)=s_0$ and $\tail(\xi)=s_{n-1}$. (Note $\head(epsilon)$ and $\tail(\epsilon)$ are undefined.) >A substitution notation, t[a′/a], denotes the result of substituting all appear- ances of a with a′ in t. What is t? Is it a sequence? If that's the case then say something like: If \zeta\inS^* and a, a'\in S, then \zeta[a'/a] denotes... If this is more general, then I guess it is a kind of meta-notation and you should explain it. Like, there will be various structures, including sequences and ..., and this notation will also denote substituting all occurrences of a with a' in t. > A patching notation, f [a 􏰀→ b], denotes a function... Again you have used symbols f, a, and b without first defining them. Say Let X and Y be sets and f:X->Y. Let a\in X and b\in Y. Then f[a\mapsto b] denotes the function from X to Y defined by \[ f[a\mapsto b](x) = { b if x=a ... f(x) otherwise \] for all x\in X. >Notation A,B,... encodes the meaning that if A, B, ... are all valid, then C is... This is called an \emph{inference rule} and A, B, C are sentences in some logic. A, B, ... are the \emph{premises} of the rule. C is the \emph{conclusion}. It means, if you have derived A, B, ..., then you can derive C. Note in particular that I don't think you can say "valid". "valid" is defined by the formula holding (evaluating to true) over all models. If the inference system is sound, then anything you can derive is valid. If the inference system is not sound, you can derive invalid formulas. They are just separate concepts. >Logic operators are used by their typical forms,... Propositional and first order logical operators are written as follows: \wedge denotes \emph{and}, ... ---- It turns out you do use \N and in fact more: > ... N=0. Then you can use the functional override notation s[i\mapsto x], and it makes sense. It is the result of replacing element i with x. That is what you will then use when stating the semantics of a[i]=x. Define: X^* = \bigcup_{n\geq 0} (\N^{