This is known as higher-order abstract syntax.
First solution: Use Haskell's lambda.
A datatype could look like:
data Prop
= Not Prop
| And Prop Prop
| Or Prop Prop
| Impl Prop Prop
| Equiv Prop Prop
| Equals Obj Obj
| ForAll (Obj -> Prop)
| Exists (Obj -> Prop)
deriving (Eq, Ord)
data Obj
= Num Integer
| Add Obj Obj
| Mul Obj Obj
deriving (Eq, Ord)
You can write a formula as:
ForAll (\x -> Exists (\y -> Equals (Add x y) (Mul x y))))
This is described in detail in in The Monad Reader article. Highly recommended.
Second solution:
Use strings like
data Prop
= Not Prop
| And Prop Prop
| Or Prop Prop
| Impl Prop Prop
| Equiv Prop Prop
| Equals Obj Obj
| ForAll String Prop
| Exists String Prop
deriving (Eq, Ord)
data Obj
= Num Integer
| Var String
| Add Obj Obj
| Mul Obj Obj
deriving (Eq, Ord)
Then you can write a formula like
ForAll "x" (Exists "y" (Equals (Add (Var "x") (Var "y")))
(Mul (Var "x") (Var "y"))))))
The advantage is that you can show the formula easily (it's hard to show a Obj -> Prop
function). The disadvantage is that you have to write changing names on collision (~alpha conversion) and substitution (~beta conversion). In both solutions, you can use GADT instead of two datatypes:
data FOL a where
True :: FOL Bool
False :: FOL Bool
Not :: FOL Bool -> FOL Bool
And :: FOL Bool -> FOL Bool -> FOL Bool
...
-- first solution
Exists :: (FOL Integer -> FOL Bool) -> FOL Bool
ForAll :: (FOL Integer -> FOL Bool) -> FOL Bool
-- second solution
Exists :: String -> FOL Bool -> FOL Bool
ForAll :: String -> FOL Bool -> FOL Bool
Var :: String -> FOL Integer
-- operations in the universe
Num :: Integer -> FOL Integer
Add :: FOL Integer -> FOL Integer -> FOL Integer
...
Third solution: Use numerals to represent where the variable is bound, where lower means deeper. For example, in ForAll (Exists (Equals (Num 0) (Num 1))) the first variable will bind to Exists, and second to ForAll. This is known as de Bruijn numerals. See I am not a number - I am a free variable.