Let define procedure for converting second order theory to first order:
- Take any second order theory with equality
- Invent sort Bool' and new fresh constants F' and T', of sort Bool'
- Create fresh sort CC
- Replace each proposition P(x) (where x : XX) except equality to P'(x) == T' where P' : XX -> Bool'
- Replace each connective to respective function to Bool'
- For each first order function f : XX -> YY define fresh constant c : CC. We call it the key of function f.
- 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)
- 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
- 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?
- 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?