I have been trying to define the notion of a product of second-order classes using (finitary) second-order and if needed third-order logic. It seems to be possible to define the product of finitely many classes, because I can just express this using a finite second-order sentence. The problem is that, when I try to define an infinite product, I seem to need to be able to refer to an indexed family of classes. More specifically, so that I can use an infinite index class. But something tells me this should not be possible to do in higher-order logic, because intuitively, it seems to involve some circularity. Do you know if it is possible? Also, someone suggested me that type theory should help me with this problem, and if so, do you know why?
Add a comment
|