12,089
edits
Changes
Directory:Jon Awbrey/Papers/Differential Propositional Calculus (view source)
Revision as of 17:08, 27 May 2008
, 17:08, 27 May 2008→Differential Propositions: prep table
Introduce a suitably generic definition of the extended universe of discourse:
Introduce a suitably generic definition of the extended universe of discourse:
: Let <math>U = X_1 \times \ldots \times X_k</math> and <math>\operatorname{E}U = U \times \operatorname{d}U = X_1 \times \ldots \times X_k \times \operatorname{d}X_1 \times \ldots \times \operatorname{d}X_k.</math>
: For <math>U = X_1 \times \ldots \times X_k</math>,
: let <math>\operatorname{E}U = U \times \operatorname{d}U = X_1 \times \ldots \times X_k \times \operatorname{d}X_1 \times \ldots \times \operatorname{d}X_k.</math>
For a proposition <math>f : X_1 \times \ldots \times X_k \to \mathbb{B},</math> the (first order) enlargement of <math>f\!</math> is the proposition <math>\operatorname{E}f : \operatorname{E}U \to \mathbb{B}</math> that is defined by:
For a proposition <math>f : X_1 \times \ldots \times X_k \to \mathbb{B},</math> the (first order) enlargement of <math>f\!</math> is the proposition <math>\operatorname{E}f : \operatorname{E}U \to \mathbb{B}</math> that is defined by:
|
|
|-
|-
| f<sub>0</sub> || f<sub>0000</sub> || 0 0 0 0 || ( ) || false || 0
| f<sub>0</sub>
| f<sub>0000</sub>
| 0 0 0 0
| ( )
| false
| 0
|-
|-
| f<sub>1</sub> || f<sub>0001</sub> || 0 0 0 1 || (x)(y) || neither x nor y || ¬x ∧ ¬y
| f<sub>1</sub>
| f<sub>0001</sub>
| 0 0 0 1
| (x)(y)
| neither x nor y
| ¬x ∧ ¬y
|-
|-
| f<sub>2</sub> || f<sub>0010</sub> || 0 0 1 0 || (x) y || y and not x || ¬x ∧ y
| f<sub>2</sub>
| f<sub>0010</sub>
| 0 0 1 0
| (x) y
| y and not x
| ¬x ∧ y
|-
|-
| f<sub>3</sub> || f<sub>0011</sub> || 0 0 1 1 || (x) || not x || ¬x
| f<sub>3</sub>
| f<sub>0011</sub>
| 0 0 1 1
| (x)
| not x
| ¬x
|-
|-
| f<sub>4</sub> || f<sub>0100</sub> || 0 1 0 0 || x (y) || x and not y || x ∧ ¬y
| f<sub>4</sub>
| f<sub>0100</sub>
| 0 1 0 0
| x (y)
| x and not y
| x ∧ ¬y
|-
|-
| f<sub>5</sub> || f<sub>0101</sub> || 0 1 0 1 || (y) || not y || ¬y
| f<sub>5</sub>
| f<sub>0101</sub>
| 0 1 0 1
| (y)
| not y
| ¬y
|-
|-
| f<sub>6</sub> || f<sub>0110</sub> || 0 1 1 0 || (x, y) || x not equal to y || x ≠ y
| f<sub>6</sub>
| f<sub>0110</sub>
| 0 1 1 0
| (x, y)
| x not equal to y
| x ≠ y
|-
|-
| f<sub>7</sub> || f<sub>0111</sub> || 0 1 1 1 || (x y) || not both x and y || ¬x ∨ ¬y
| f<sub>7</sub>
| f<sub>0111</sub>
| 0 1 1 1
| (x y)
| not both x and y
| ¬x ∨ ¬y
|-
|-
| f<sub>8</sub> || f<sub>1000</sub> || 1 0 0 0 || x y || x and y || x ∧ y
| f<sub>8</sub>
| f<sub>1000</sub>
| 1 0 0 0
| x y
| x and y
| x ∧ y
|-
|-
| f<sub>9</sub> || f<sub>1001</sub> || 1 0 0 1 || ((x, y)) || x equal to y || x = y
| f<sub>9</sub>
| f<sub>1001</sub>
| 1 0 0 1
| ((x, y))
| x equal to y
| x = y
|-
|-
| f<sub>10</sub> || f<sub>1010</sub> || 1 0 1 0 || y || y || y
| f<sub>10</sub>
| f<sub>1010</sub>
| 1 0 1 0
| y
| y
| y
|-
|-
| f<sub>11</sub> || f<sub>1011</sub> || 1 0 1 1 || (x (y)) || not x without y || x → y
| f<sub>11</sub>
| f<sub>1011</sub>
| 1 0 1 1
| (x (y))
| not x without y
| x → y
|-
|-
| f<sub>12</sub> || f<sub>1100</sub> || 1 1 0 0 || x || x || x
| f<sub>12</sub>
| f<sub>1100</sub>
| 1 1 0 0
| x
| x
| x
|-
|-
| f<sub>13</sub> || f<sub>1101</sub> || 1 1 0 1 || ((x) y) || not y without x || x ← y
| f<sub>13</sub>
| f<sub>1101</sub>
| 1 1 0 1
| ((x) y)
| not y without x
| x ← y
|-
|-
| f<sub>14</sub> || f<sub>1110</sub> || 1 1 1 0 || ((x)(y)) || x or y .|| x ∨ y
| f<sub>14</sub>
| f<sub>1110</sub>
| 1 1 1 0
| ((x)(y))
| x or y
| x ∨ y
|-
|-
| f<sub>15</sub> || f<sub>1111</sub> || 1 1 1 1 || (( )) || true || 1
| f<sub>15</sub>
| f<sub>1111</sub>
| 1 1 1 1
| (( ))
| true
| 1
|}
|}
<br>
<br>