Q:

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

A:

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.

