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

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?

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.
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).