# Lowering order of theory

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?
-
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. – Jacques Carette Jul 2 '10 at 19:02
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? – Vag Jul 2 '10 at 19:13