I'm doing some research on second order logic and I'd like to write down a proof for the following argument:

argument 1

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
    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.
    – d-cmst
    Commented Apr 3, 2013 at 21:00
  • 1
    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
    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.
    – Dennis
    Commented Apr 3, 2013 at 21:10
  • 1
    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

1 Answer 1


Here's a proof relying on a translation of second-order logic into set theory.

Read "Px" as enter image description here and likewise for Qx. What the condition requires then, is that P is a subset of Q, so http://latex.codecogs.com/gif.latex?$P%20\subseteq%20Q$.

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 enter image description here, but clearly this doesn't follow from P being a subset of Q.

Here is a description of a countermodel (well really, a whole class of countermodels since I don't specify a domain): suppose that our model assigns the same members to P and Q, so that P=Q. In that case it will be true that P is a subset of Q but it will be false that P is a member of Q, since no set is a member of itself.

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .