Line 626:
Line 626:
: ''e''<sub>1</sub> ''e''<sub>2</sub> ''e''<sub>3</sub> means "''e''<sub>1</sub> and ''e''<sub>2</sub> and ''e''<sub>3</sub>".
: ''e''<sub>1</sub> ''e''<sub>2</sub> ''e''<sub>3</sub> means "''e''<sub>1</sub> and ''e''<sub>2</sub> and ''e''<sub>3</sub>".
−
The bound connectives are written as lists of ''k'' expressions (''e''<sub>1</sub>, …, ''e''<sub>''k''</sub>), where the parentheses and commas are considered to be parts of the connective notation. In text presentations the parentheses will be superscripted, as <sup>(</sup>''e''<sub>1</sub>, …, ''e''<sub>''k''</sub><sup>)</sup>, to avoid confusion with other uses. The bound connective is interpreted to mean that just one of the ''k'' listed expressions is false. That is, <sup>(</sup>''e''<sub>1</sub>, …, ''e''<sub>''k''</sub><sup>)</sup> is true if and only if exactly one of the expressions ''e''<sub>1</sub>, …, ''e''<sub>''k''</sub> is false. In particular, for ''k'' = 1 and 2:
+
The bound connectives are written as lists of ''k'' expressions (''e''<sub>1</sub>, …, ''e''<sub>''k''</sub>), where the parentheses and commas are considered to be parts of the connective notation. In text presentations the parentheses will be superscripted, as <sup>(</sup>''e''<sub>1</sub>, …, ''e''<sub>''k''</sub><sup>)</sup>, to avoid confusion with other uses. The bound connective is interpreted to mean that just one of the ''k'' listed expressions is false. That is, <sup>(</sup>''e''<sub>1</sub>, …, ''e''<sub>''k''</sub><sup>)</sup> is true if and only if exactly one of the expressions ''e''<sub>1</sub>, …, ''e''<sub>''k''</sub> is false. In particular, for ''k'' = 1 and 2, we have:
−
<pre>
+
:{| cellpadding="4"
−
(e1) means "not e1".
+
| (''e''<sub>1</sub>)
−
+
| means
−
(e1,e2) means "e1 xor e2", "e1 + e2",
+
| not ''e''<sub>1</sub>.
−
+
|
−
or "e1 neq e2", "e1 =/= e2".
+
|-
−
</pre>
+
| (''e''<sub>1</sub>, ''e''<sub>2</sub>)
+
| means
+
| ''e''<sub>1</sub> xor ''e''<sub>2</sub>,
+
| ''e''<sub>1</sub> + ''e''<sub>2</sub>,
+
|-
+
|
+
| or
+
| ''e''<sub>1</sub> neq ''e''<sub>2</sub>,
+
| ''e''<sub>1</sub> ≠ ''e''<sub>2</sub>.
+
|}
A remaining sample of typical expressions will finish illustrating the use of this calculus.
A remaining sample of typical expressions will finish illustrating the use of this calculus.