Could Frege's Ontology be a Henkin Model?
Frege uses second-order quantification in both his formal and informal works. So far, I have always assumed that his second-order logic is standard second-order logic. But couldn't it also be second-order logic with Henkin semantics, which would in fact be a kind of first-order logic (compact, complete and skolem-löwenheimish)? Unfortunately, I know far too little about second-order logic to answer this question.
Are there any second-order statements that are satisfiable in standard semantics, but not in Henkin semantics? (I guess there must be: Wouldn't second-order logic with standard semantics have to be complete otherwise? Not sure.) If so, do any of Frege's theorems belong to these?
It is easy to show that the (second order) comprehension principle holds in Frege's system (of the Grundgesetze, without Axiom 5):
For any formula A with x free, P x(Px A)
I think that this is also a key idea in Frege's semantics: Every sentence S from which a "proper name" has been removed, denotes a function F such that for all objects o denoted by a name n, S(x/n) is true iff F(o). But perhaps from this it doesn't follow, as Adam Rieger supposes in his Analysis paper (10/2002), that there are more functions than objects. This would of course be true in the standard semantics of second order logic, but not in a Henkin semantics. And I guess that 1) the comprehension principle is also satisfiable in a Henkin semantics, and 2) in such a model the second-order domain need not be larger than the first-oder domain. I would rather like to know this instead of guessing...
How, by the way, does Frege introduce real numbers? There are not enough formulas to give rise to aleph-1 functions via the comprehension schema, and hence also not enough to establish aleph-1 extensions of functions via axiom 5. Unfortunately I have no clue about what goes on in the wallpaper parts of Grundgesetze, vol.2.
[Update: Ignore that last question. Obviously with both Axiom 5 and the Comprehension Principle Cantor's proof can be carried out.]
[Another Update: I replied to this posting here. (Pingback server still broken...)]