Figure 1
First option – Determinate states.
Figure 2
Second option – A non-determinate state between determinates ones.
Figure 3
Continuous change.
Figure 4
Indeterminate instantiation (P3) and corresponding indeterminate type-identity (between P1 and P3).
Figure 5
Indeterminate type-identity (between P1* and P3*) without indeterminate instantiation.
| 1 | ∇(Pa≡Pb) | Assumption | |
| 2 | λX [∇ (Pa≡X)] Pb | 1 | Second-order type-property abstraction from 1 |
| 3 | ~∇(Pa≡Pa) | Assumption | |
| 4 | ~λX [∇ (Pa≡X)] Pa | 3 | Second-order type-property abstraction from 3 |
| 5 | ~(Pa≡Pb) | 1, 3 | Indiscernibility of Identical Powers from 2 and 4 |
| 6 | ⊥ | 1, 3 | Contradiction from 1 and 5 |