I’m still worried about the word “model”. You talk about models of second-order logic, but what is a model of second-order logic? Classically speaking, it’s a set, and you do talk about ZF proving the existence of models of SOL. But if we need to use set theory to reason about the semantic properties of SOL, then are we not then working within a first-order set theory? And hence we’re vulnerable to unexpected “models” of that set theory affecting the theorems we prove about SOL within it.
It seems like you’re treating “model” as if it were a fundamental concept, when in fact the way it’s used in mathematics is normally embedded within some set theory. But this then means you can’t robustly talk about “models” all the way down: at some point your notion of model bottoms out. I don’t think I have a solution to this, but it feels like it’s a problem worth addressing.
My response to this situation is to say that proof theory is more fundamental and interesting than model theory, and pragmatic questions (which the dialog attempted to ask) are more important than model-theoretic questions. However, to some extent, the problem is to reduce model-theoretic talk to more pragmatic talk. So it isn’t surprising to see model-theoretic talk in the post (although I did feel that the discussion was wandering from the point when it got too much into models).
I’m still worried about the word “model”. You talk about models of second-order logic, but what is a model of second-order logic? Classically speaking, it’s a set, and you do talk about ZF proving the existence of models of SOL. But if we need to use set theory to reason about the semantic properties of SOL, then are we not then working within a first-order set theory? And hence we’re vulnerable to unexpected “models” of that set theory affecting the theorems we prove about SOL within it.
It seems like you’re treating “model” as if it were a fundamental concept, when in fact the way it’s used in mathematics is normally embedded within some set theory. But this then means you can’t robustly talk about “models” all the way down: at some point your notion of model bottoms out. I don’t think I have a solution to this, but it feels like it’s a problem worth addressing.
My response to this situation is to say that proof theory is more fundamental and interesting than model theory, and pragmatic questions (which the dialog attempted to ask) are more important than model-theoretic questions. However, to some extent, the problem is to reduce model-theoretic talk to more pragmatic talk. So it isn’t surprising to see model-theoretic talk in the post (although I did feel that the discussion was wandering from the point when it got too much into models).