Besides all this, Tarski gives a deductive system for LGTC, as required of every language. Suffice it to say that it is a version of a typical simple theory of finite types, with axioms and rules for the connectives and quantifiers, axioms of comprehension and extensionality for all orders, and an axiom of infinity. Tarski observes that LGTC suffices, with the help of some tricks, to develop all the mathematics that can be developed in the simple theory of finite types, even though it has formally fewer types of variables.