0
$\begingroup$

I was reading this blog posting and the following claim was made:

...[T]here's tricks for making second-order logic encode any proposition in third-order logic and so on. If there's a collection of third-order axioms that characterizes a model, there's a collection of second-order axioms that characterizes the same model. Once you make the jump to second-order logic, you're done - so far as anyone knows (so far as I know) there's nothing more powerful than second-order logic in terms of which models it can characterize.

I think I've heard similar claims before -- that second-order logic provides us all the resources we could have for characterizing models.

Is this claim correct? What is the theorem associated with this claim?

$\endgroup$
2
  • $\begingroup$ I have been taught that second order logic is nothing more hat first-order (multi-sorted) logic. $\endgroup$ Apr 29, 2015 at 6:09
  • $\begingroup$ @PrimoPetri That is true for second-order logic restricted to Henkin models (as opposed to full models). With Henkin semantics, SOL is no more expressive than FOL. Once you move to full models (which differ from the Henkin models in allowing the second-order quantifers to range over the full powerset of the domain) you get a logic which is more expressive. It's also incomplete. In the SEP article linked to in Jonny's answer, this is discussed in sections 2 and 3. Your claim is true of what they call the "General Semantics" (section 3). $\endgroup$
    – Dennis
    Apr 29, 2015 at 12:24

1 Answer 1

3
$\begingroup$

I believe the result you are looking for is mentioned here: http://plato.stanford.edu/entries/logic-higher-order/#4

More specifically, we have the following result of Hintikka (1955): For each formula φ of higher-order logic (in a language with finitely many non-logical symbols), we can effectively find a sentence ψ of second-order logic (in the language of equality) such that φ is valid if and only if ψ is valid.

The basic notion is that the powerset operation is definable in second order logic, which allows for the simulation of higher order logics.

$\endgroup$

You must log in to answer this question.

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