2
$\begingroup$

Let define procedure for converting second order theory to first order:

  1. Take any second order theory with equality
  2. Invent sort Bool' and new fresh constants F' and T', of sort Bool'
  3. Create fresh sort CC
  4. Replace each proposition P(x) (where x : XX) except equality to P'(x) == T' where P' : XX -> Bool'
  5. Replace each connective to respective function to Bool'
  6. For each first order function f : XX -> YY define fresh constant c : CC. We call it the key of function f.
  7. For each sort XX and YY, if source theory contained any functions XX -> YY, define new function applyXXYY : CC -> XX -> YY such that if c is key for f then applyXXYY(c,x) = f(x)
  8. For each first order function f applied to second order function g replace f by its key: g(f) replace to g(c) where c is a key for f
  9. Each expression with variable containing first order function applied to argument replace application to variable by application to applyXXYY(variable) (where XX and YY are respective to sort of f). So, definition g(x,f,y) := x*f(y)+1-q(f) become g(x,c,y) := x*apply(c,y)+1-q(c)

Items 6..9 is well known amongst functional programmers as defunctionalization process (roughly).

So, SOL is more expressive than FOL (in strict Felleisen/VanRoy sense) but strictly equal in power. Is it correct?

Questions:

  • Are Second Order Logic really equivalent to First Order Logic?
  • Are really any logic of some order can be lowered to FOL?
  • Can any higher order Logic be converted to equivalent first order logic?
Improve this question
$\endgroup$
2
  • $\begingroup$ I believe you need to make some assumptions that your input theory is finitely presentable for this to work. You might need to make some further 'finitary' assumptions as well. This works for functional programs explicitly because higher-order programs are restricted to be finite, to take finite input, to produce finite output (i.e. to terminate). Without those assumptions, things are bound to break, somewhere. The expressiveness is really a statement about Kolmogorov complexity, not computing power. $\endgroup$
    – Jacques Carette
    Commented Jul 2, 2010 at 19:02
  • $\begingroup$ About expressiveness. I've used word expressiveness in the meaning as in Felleisen work "On the Expressive Power of Programming Languages". Approximately, same expressiveness is merely that if language A is capable to express any program that language B may express without massive global changes. Such a massive global changes is measure of expressivenes, roughly. Can you give pointer to definition of expressiveness in the sense that you mean? $\endgroup$
    – Vag
    Commented Jul 2, 2010 at 19:13

1 Answer 1

Reset to default
4
$\begingroup$

The answer to your question is that it depends on what semantics you want to use for higher-order logic.

  • If you use full higher-order semantics, then you cannot reduce your theory to a first-order theory. In these semantics, the higher-order quantifiers range over all objects of the appropriate type, and so a model only has to specify the domain of discourse for individuals (elements of the base type).

  • If you use Henkin semantics, then you can replace your higher-order theory with a completely equivalent multi-sorted first-order theory, using the process you are describing in which you add numerous "Apply" symbols. In Henkin semantics, a model has to provide a separate domain of discourse for each type of quantifier. So it is possible, in a particular Henkin model, that a higher-order quantifier does not range over all objects of its type, only over the ones that were included in that model.

Full higher-order semantics are much more powerful than Henkin semantics. For example, there is a categorical axiomatization of the natural numbers in full second-order semantics, but Henkin semantics are subject to the Lowenheim-Skolem theorem just like first-order semantics. (This is because Henkin semantics really are just first-order semantics.)

One canonical reference for this is Shapiro's Foundations without foundationalism.

Improve this answer
$\endgroup$
0

You must log in to answer this question.

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