Encoding first order formula (or its tree) into binary string?

Question

How to encode a first order formula into binary string, which I could give as input to Turing machine or program to do something with it (deciding is it satisfiable, or is concrete structure model for it, for example)?

I've read that I should first make a tree (which I know how to do) and then encode that tree, which I don't know how to do and I don't understand why I need to make that tree? Why don't just make binary number for every symbol which could appear in formula $( = , \vee, \wedge, <=>, =>, \exists, \forall...)$ and connect them into string for concrete formula?

Answer 1

There is one encoding scheme which is particularly obvious. Under this encoding scheme, the encoding of the formula $a \Rightarrow (b \Rightarrow a)$ is $$ a \Rightarrow (b \Rightarrow a). $$ A C program can parse this string into a tree if it needs to, but it's up to the program.

It is of course possible to think of many other encoding schemes, but unless you are interested in very weak complexity classes, the exact encoding scheme doesn't matter.

There is one fine point here: the alphabet is finite, but there could be formulas with arbitrarily many variables. There are many ways to solve this problem. For example, you can name variables in the form "$v$ + number", for example $v5$, $v107$, and so on. This uses only a finite alphabet (since we encode the number in decimal, using 10 symbols).