Re: Dick Lipton & Ken Regan • (1) • (2)
Putting all thought of the Frankl Conjecture out of our minds for the moment, let’s return to the proposition in Example 1 and work through its differential analysis from scratch.
Example 1
 |
(1) |
Consider the proposition 
The enlargement 
Given that
Difficulties of notation in differential logic are greatly eased by introducing the family of minimal negation operators on finite numbers of boolean variables. For our immediate purposes we need only the minimal negation operators on one and two variables.
- The minimal negation operator on one variable
is notated with monospace parentheses as
and is simply another notation for the logical negation
- The minimal negation operator on two variables
is notated with monospace delimiters as
and is simply another notation for the exclusive disjunction
In this notation the previous expression for
A canonical form for 
For example, in the case 
![\begin{array}{lll} \mathrm{E}f(1, 1, 1, \mathrm{d}p, \mathrm{d}q, \mathrm{d}r) & = & (1 + \mathrm{d}p)(1 + \mathrm{d}q)(1 + \mathrm{d}r) \\[4pt] & = & \lnot\mathrm{d}p \land \lnot\mathrm{d}q \land \lnot\mathrm{d}r \\[4pt] & = & \texttt{(} \mathrm{d}p \texttt{)(} \mathrm{d}q \texttt{)(} \mathrm{d}r \texttt{)} \end{array}](https://s0.wp.com/latex.php?latex=%5Cbegin%7Barray%7D%7Blll%7D++%5Cmathrm%7BE%7Df%281%2C+1%2C+1%2C+%5Cmathrm%7Bd%7Dp%2C+%5Cmathrm%7Bd%7Dq%2C+%5Cmathrm%7Bd%7Dr%29++%26+%3D+%26+%281+%2B+%5Cmathrm%7Bd%7Dp%29%281+%2B+%5Cmathrm%7Bd%7Dq%29%281+%2B+%5Cmathrm%7Bd%7Dr%29++%5C%5C%5B4pt%5D++%26+%3D+%26+%5Clnot%5Cmathrm%7Bd%7Dp+%5Cland+%5Clnot%5Cmathrm%7Bd%7Dq+%5Cland+%5Clnot%5Cmathrm%7Bd%7Dr++%5C%5C%5B4pt%5D++%26+%3D+%26+%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dp+%5Ctexttt%7B%29%28%7D+%5Cmathrm%7Bd%7Dq+%5Ctexttt%7B%29%28%7D+%5Cmathrm%7Bd%7Dr+%5Ctexttt%7B%29%7D++%5Cend%7Barray%7D&bg=ffffff&fg=000000&s=1 "\begin{array}{lll} \mathrm{E}f(1, 1, 1, \mathrm{d}p, \mathrm{d}q, \mathrm{d}r) & = & (1 + \mathrm{d}p)(1 + \mathrm{d}q)(1 + \mathrm{d}r) \\[4pt] & = & \lnot\mathrm{d}p \land \lnot\mathrm{d}q \land \lnot\mathrm{d}r \\[4pt] & = & \texttt{(} \mathrm{d}p \texttt{)(} \mathrm{d}q \texttt{)(} \mathrm{d}r \texttt{)} \end{array}")
Collecting the cases yields the boolean expansion of
Step 1
![\begin{smallmatrix} & p q r \cdot f(1 + \mathrm{d}p, 1 + \mathrm{d}q, 1 + \mathrm{d}r) & + & p q \tilde{r} \cdot f(1 + \mathrm{d}p, 1 + \mathrm{d}q, 0 + \mathrm{d}r) & + & p \tilde{q} r \cdot f(1 + \mathrm{d}p, 0 + \mathrm{d}q, 1 + \mathrm{d}r) & + & p \tilde{q} \tilde{r} \cdot f(1 + \mathrm{d}p, 0 + \mathrm{d}q, 0 + \mathrm{d}q) \\[4pt] + & \tilde{p} q r \cdot f(0 + \mathrm{d}p, 1 + \mathrm{d}q, 1 + \mathrm{d}r) & + & \tilde{p} q \tilde{r} \cdot f(0 + \mathrm{d}p, 1 + \mathrm{d}q, 0 + \mathrm{d}r) & + & \tilde{p} \tilde{q} r \cdot f(0 + \mathrm{d}p, 0 + \mathrm{d}q, 1 + \mathrm{d}r) & + & \tilde{p} \tilde{q} \tilde{r} \cdot f(0 + \mathrm{d}p, 0 + \mathrm{d}q, 0 + \mathrm{d}q) \end{smallmatrix}](https://s0.wp.com/latex.php?latex=%5Cbegin%7Bsmallmatrix%7D++%26++p+q+r+%5Ccdot+f%281+%2B+%5Cmathrm%7Bd%7Dp%2C+1+%2B+%5Cmathrm%7Bd%7Dq%2C+1+%2B+%5Cmathrm%7Bd%7Dr%29++%26+%2B+%26++p+q+%5Ctilde%7Br%7D+%5Ccdot+f%281+%2B+%5Cmathrm%7Bd%7Dp%2C+1+%2B+%5Cmathrm%7Bd%7Dq%2C+0+%2B+%5Cmathrm%7Bd%7Dr%29++%26+%2B+%26++p+%5Ctilde%7Bq%7D+r+%5Ccdot+f%281+%2B+%5Cmathrm%7Bd%7Dp%2C+0+%2B+%5Cmathrm%7Bd%7Dq%2C+1+%2B+%5Cmathrm%7Bd%7Dr%29++%26+%2B+%26++p+%5Ctilde%7Bq%7D+%5Ctilde%7Br%7D+%5Ccdot+f%281+%2B+%5Cmathrm%7Bd%7Dp%2C+0+%2B+%5Cmathrm%7Bd%7Dq%2C+0+%2B+%5Cmathrm%7Bd%7Dq%29++%5C%5C%5B4pt%5D++%2B+%26++%5Ctilde%7Bp%7D+q+r+%5Ccdot+f%280+%2B+%5Cmathrm%7Bd%7Dp%2C+1+%2B+%5Cmathrm%7Bd%7Dq%2C+1+%2B+%5Cmathrm%7Bd%7Dr%29++%26+%2B+%26++%5Ctilde%7Bp%7D+q+%5Ctilde%7Br%7D+%5Ccdot+f%280+%2B+%5Cmathrm%7Bd%7Dp%2C+1+%2B+%5Cmathrm%7Bd%7Dq%2C+0+%2B+%5Cmathrm%7Bd%7Dr%29++%26+%2B+%26++%5Ctilde%7Bp%7D+%5Ctilde%7Bq%7D+r+%5Ccdot+f%280+%2B+%5Cmathrm%7Bd%7Dp%2C+0+%2B+%5Cmathrm%7Bd%7Dq%2C+1+%2B+%5Cmathrm%7Bd%7Dr%29++%26+%2B+%26++%5Ctilde%7Bp%7D+%5Ctilde%7Bq%7D+%5Ctilde%7Br%7D+%5Ccdot+f%280+%2B+%5Cmathrm%7Bd%7Dp%2C+0+%2B+%5Cmathrm%7Bd%7Dq%2C+0+%2B+%5Cmathrm%7Bd%7Dq%29++%5Cend%7Bsmallmatrix%7D&bg=ffffff&fg=000000&s=1 "\begin{smallmatrix} & p q r \cdot f(1 + \mathrm{d}p, 1 + \mathrm{d}q, 1 + \mathrm{d}r) & + & p q \tilde{r} \cdot f(1 + \mathrm{d}p, 1 + \mathrm{d}q, 0 + \mathrm{d}r) & + & p \tilde{q} r \cdot f(1 + \mathrm{d}p, 0 + \mathrm{d}q, 1 + \mathrm{d}r) & + & p \tilde{q} \tilde{r} \cdot f(1 + \mathrm{d}p, 0 + \mathrm{d}q, 0 + \mathrm{d}q) \\[4pt] + & \tilde{p} q r \cdot f(0 + \mathrm{d}p, 1 + \mathrm{d}q, 1 + \mathrm{d}r) & + & \tilde{p} q \tilde{r} \cdot f(0 + \mathrm{d}p, 1 + \mathrm{d}q, 0 + \mathrm{d}r) & + & \tilde{p} \tilde{q} r \cdot f(0 + \mathrm{d}p, 0 + \mathrm{d}q, 1 + \mathrm{d}r) & + & \tilde{p} \tilde{q} \tilde{r} \cdot f(0 + \mathrm{d}p, 0 + \mathrm{d}q, 0 + \mathrm{d}q) \end{smallmatrix}")
Step 2
![\begin{smallmatrix} & p q r \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)(} \mathrm{d}q \texttt{)(} \mathrm{d}r \texttt{)} & + & p q \texttt{(} r \texttt{)} \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)(} \mathrm{d}q \texttt{)} \mathrm{d}r & + & p \texttt{(} q \texttt{)} r \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)} \mathrm{d}q \texttt{(} \mathrm{d}r \texttt{)} & + & p \texttt{(} q \texttt{)(} r \texttt{)} \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)} \mathrm{d}q \, \mathrm{d}r \\[4pt] + & \texttt{(} p \texttt{)} q r \,\cdot\, \mathrm{d}p \texttt{(} \mathrm{d}q \texttt{)(} \mathrm{d}r \texttt{)} & + & \texttt{(} p \texttt{)} q \texttt{(} r \texttt{)} \,\cdot\, \mathrm{d}p \texttt{(} \mathrm{d}q \texttt{)} \mathrm{d}r & + & \texttt{(} p \texttt{)(} q \texttt{)} r \,\cdot\, \mathrm{d}p \, \mathrm{d}q \texttt{(} \mathrm{d}r \texttt{)} & + & \texttt{(} p \texttt{)(} q \texttt{)(} r \texttt{)} \,\cdot\, \mathrm{d}p \, \mathrm{d}q \, \mathrm{d}r \end{smallmatrix}](https://s0.wp.com/latex.php?latex=%5Cbegin%7Bsmallmatrix%7D++%26++p+q+r+%5C%2C%5Ccdot%5C%2C++%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dp+%5Ctexttt%7B%29%28%7D+%5Cmathrm%7Bd%7Dq+%5Ctexttt%7B%29%28%7D+%5Cmathrm%7Bd%7Dr+%5Ctexttt%7B%29%7D++%26+%2B+%26++p+q+%5Ctexttt%7B%28%7D+r+%5Ctexttt%7B%29%7D+%5C%2C%5Ccdot%5C%2C++%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dp+%5Ctexttt%7B%29%28%7D+%5Cmathrm%7Bd%7Dq+%5Ctexttt%7B%29%7D+%5Cmathrm%7Bd%7Dr++%26+%2B+%26++p+%5Ctexttt%7B%28%7D+q+%5Ctexttt%7B%29%7D+r+%5C%2C%5Ccdot%5C%2C++%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dp+%5Ctexttt%7B%29%7D+%5Cmathrm%7Bd%7Dq+%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dr+%5Ctexttt%7B%29%7D++%26+%2B+%26++p+%5Ctexttt%7B%28%7D+q+%5Ctexttt%7B%29%28%7D+r+%5Ctexttt%7B%29%7D+%5C%2C%5Ccdot%5C%2C++%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dp+%5Ctexttt%7B%29%7D+%5Cmathrm%7Bd%7Dq+%5C%2C+%5Cmathrm%7Bd%7Dr++%5C%5C%5B4pt%5D++%2B+%26++%5Ctexttt%7B%28%7D+p+%5Ctexttt%7B%29%7D+q+r+%5C%2C%5Ccdot%5C%2C++%5Cmathrm%7Bd%7Dp+%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dq+%5Ctexttt%7B%29%28%7D+%5Cmathrm%7Bd%7Dr+%5Ctexttt%7B%29%7D++%26+%2B+%26++%5Ctexttt%7B%28%7D+p+%5Ctexttt%7B%29%7D+q+%5Ctexttt%7B%28%7D+r+%5Ctexttt%7B%29%7D+%5C%2C%5Ccdot%5C%2C++%5Cmathrm%7Bd%7Dp+%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dq+%5Ctexttt%7B%29%7D+%5Cmathrm%7Bd%7Dr++%26+%2B+%26++%5Ctexttt%7B%28%7D+p+%5Ctexttt%7B%29%28%7D+q+%5Ctexttt%7B%29%7D+r+%5C%2C%5Ccdot%5C%2C++%5Cmathrm%7Bd%7Dp+%5C%2C+%5Cmathrm%7Bd%7Dq+%5Ctexttt%7B%28%7D+%5Cmathrm%7Bd%7Dr+%5Ctexttt%7B%29%7D++%26+%2B+%26++%5Ctexttt%7B%28%7D+p+%5Ctexttt%7B%29%28%7D+q+%5Ctexttt%7B%29%28%7D+r+%5Ctexttt%7B%29%7D+%5C%2C%5Ccdot%5C%2C++%5Cmathrm%7Bd%7Dp+%5C%2C+%5Cmathrm%7Bd%7Dq+%5C%2C+%5Cmathrm%7Bd%7Dr++%5Cend%7Bsmallmatrix%7D&bg=ffffff&fg=000000&s=2 "\begin{smallmatrix} & p q r \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)(} \mathrm{d}q \texttt{)(} \mathrm{d}r \texttt{)} & + & p q \texttt{(} r \texttt{)} \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)(} \mathrm{d}q \texttt{)} \mathrm{d}r & + & p \texttt{(} q \texttt{)} r \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)} \mathrm{d}q \texttt{(} \mathrm{d}r \texttt{)} & + & p \texttt{(} q \texttt{)(} r \texttt{)} \,\cdot\, \texttt{(} \mathrm{d}p \texttt{)} \mathrm{d}q \, \mathrm{d}r \\[4pt] + & \texttt{(} p \texttt{)} q r \,\cdot\, \mathrm{d}p \texttt{(} \mathrm{d}q \texttt{)(} \mathrm{d}r \texttt{)} & + & \texttt{(} p \texttt{)} q \texttt{(} r \texttt{)} \,\cdot\, \mathrm{d}p \texttt{(} \mathrm{d}q \texttt{)} \mathrm{d}r & + & \texttt{(} p \texttt{)(} q \texttt{)} r \,\cdot\, \mathrm{d}p \, \mathrm{d}q \texttt{(} \mathrm{d}r \texttt{)} & + & \texttt{(} p \texttt{)(} q \texttt{)(} r \texttt{)} \,\cdot\, \mathrm{d}p \, \mathrm{d}q \, \mathrm{d}r \end{smallmatrix}")
To be continued …
Resources
- Differential Logic : Introduction
- Differential Propositional Calculus
- Differential Logic and Dynamic Systems
Pingback: Frankl, My Dear : 6 | Inquiry Into Inquiry
Pingback: Frankl, My Dear : 9 | Inquiry Into Inquiry
Pingback: Survey of Differential Logic • 1 | Inquiry Into Inquiry