How to test a second order logic argument for validity

I'm doing some research on second order logic and I'd like to write down a proof for the following argument: where `x` is a first order variable and `P` and `Q` are predicate symbols.

A plain english instance of the argument would be something like

All men are mortals, so the property of being human has the property of being mortal

This looks an invalid argument to me, but I'd like a formal proof of its invalidity. I'm looking, for example, for a way to extend the finite universe method to second order arguments, but any formal proof would be good, either semantic or syntactic.

• Are you working from some particular textbook? It would help to know some of the details of the system you're working within. – Dennis Apr 3 '13 at 20:51
• @Dennis I'm now in the process of searching for a textbook which provides a (simple) second order logic system. I asked here before finding it because maybe it was trivial to extend some first order method and someone already knew how to do it. I will update the quesion as soon as I find a system suited for the task. If you have advices on textbooks please share them, they're very welcome. – Nico Boni Apr 3 '13 at 21:00
• My first concern is that Q(P) might not be well-formed depending on how the recursive definition of a well-formed formula is laid out. I would naturally read it as a predicating a third-order variable (Q) of P. – Dennis Apr 3 '13 at 21:02
• I gave a answer assuming a translation of second-order logic into set theory. I'm still not sure I understand what Q(P) means, though, so it might be way off-base. – Dennis Apr 3 '13 at 21:10
• 1. From the universal instantiation P(P)->Q(P) you cannot derive Q(P), don't you need P(P) as additional premise? 2. Which higher-order logic? In a predicative SOL with types P(P) is not allowed, you need an impredicative SOL with restricted comprehension principle - restricted, because otherwise you get the Paradox of Predication. – Eric '3ToedSloth' Apr 4 '13 at 21:59

Read "Px" as and likewise for Qx. What the condition requires then, is that P is a subset of Q, so .
Now, if Q(P) is to be read in the same way (which I think it shouldn't, it reads most naturally as a statement in third-order logic), then it states that , but clearly this doesn't follow from P being a subset of Q.