# 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. Commented Apr 3, 2013 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. Commented Apr 3, 2013 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. Commented Apr 3, 2013 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. Commented Apr 3, 2013 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. Commented Apr 4, 2013 at 21:59