Small Talks: Tarski's metatheorem and Applied Logics

[Sonnet Nguyen <Sonnet.Nguyen@fuw.edu.pl>]

Hi all,
Tarski's theorem is One of most facinating mathematical theorems which I
have learnt during my stydying math in Warsaw.  Tarski, great Polish
mathematician, livied at the (golden time of polish mathematical
school) same time with other greatest Polish mathematicians like: Stefan
Banach, K. Kuratowski,  Lukasiewicz, Sierpinski, Schauder, Mazur, etc.  

Let turn back to Tarski's metatheorem, which says that:
Each (logical) formula in the language of ordered, closed (in the real
sense) fields is equivalent to an open formula with the same free
variables.

(Remind here that open formula is a formula without quantifiers, i.e. 
symbol "for every", "existence"; i.e. " \forall " and "\exists".)

For example: the formula F(a,b,c): exists x (ax^{2}+bx+c=0) 
             is equivalent to the open formula 
                         FO(a,b,c): b^{2}-4ac >= 0;

So, Tarski's theorem is simply a theorem "eliminating" quantifiers. 
Problem of eliminating quantifiers is very "classical" and it plays
(From theoretical point of views!) important rule in both science (i.e.
logics, AI) and technology (electronics).

Tarski's theorem is really "nice" and "simple" but this "metatheorem"
has no direct application to life ...  
(Probably for this reason, it's weekly known!)    

Hope my talks do not bore You. 
enjoys,
SN
---------------------------------------------------------
|    Sonnet Nguyen,  Polish Acad. of Scie.              |
---------------------------------------------------------