For example, if your order of proof enumeration is unlucky enough, you could find U’=”return 1000″ with no dependence on A at all, then two-box and make that equation true.
I wonder if reflection on your own inference system could make things like this go away...
I wonder if reflection on your own inference system could make things like this go away...
That would be cool. How?