formalization of tautology There is no Tarski definition of true, that is there is no formula Tr such that Tr(A) <\--> A. My question is if there is a formula Taut such that Taut(A)<\-->"A is a tautology" Thank you Martin

Yes, there is a 'Tautology' predicate. A statement is a tautology if and only if it can be derived from an empty set of premises, and we can describe that using the typical Godel numbering and associated predicates. It is a special case of the 'provable-from-recursive-set-of-axioms-A' predicate that we know exists, as in this case $A$ is empty.