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?