A question on the formality of a theory I've just about finished reading Mathematical Logic, Kleene, and I had a question about how theories are formed in formal logic.  
Throughout the beginning of the book he builds propositional and predicate calculus.  And I was under the impression that when building a theory, we use a set of axioms (of meaningless symbols) in the predicate calculus for instance.  And for a theorem $C$ in a theory $T$ we write $T\vdash{C}$.  
But then he builds a formal system $N$ for number theory. Where $\vdash{C}$ in $N$ if and only if $\forall{A_1},...,\forall{A_n}\vdash{C}$ in predicate calculus where $\forall{A_1},...,\forall{A_n}$ are closed forms of the non-logical axioms of $N$.
My Question is:

When operating in and practicing formal logic, do we use predicate calculus with a set of axioms behind the $"\vdash"$ sign or do we build a whole language for that theory?  And if it translates back to predicate calculus, why do we build languages?

For example, do we build a language for $ZFC$ or do we just operate in predicate calculus?
 A: FOL is the natural logic environment to formalize mathematical theories.
Propositional calculus, instead, is only a "toy": it is based on a very simplified model of language that is not useful to develop interesting theories, but can be used efficiently to study the basic properties of a formal system : consistency, completeness, etc.
With FOL we have the "logical engine", i.e. the syntax of the language with axioms and rules, and we usually study it in a similar way to the study of propositional calculus, in order to understand the basic meta-logic properties.
When we study "pure" FOL, we define the derivability relation ($\vdash$), where : 

$\vdash \varphi$ means : "formula $\varphi$ is derivable in the calculus", and $\Gamma \vdash \varphi$ means : "formula $\varphi$ is derivable in the calculus form the set $\Gamma$ of assumptions".

With it we prove the fundamental Soundness and Completeness Theorem :

$\Gamma \vdash \varphi \text {  iff  } \Gamma \vDash \varphi$.

In addition to the study of "pure" predicate logic, we are interested to add to the "logical engine" suitable non-logical constants, like $\in$ ("in"), the binary relation of set theory, or $+$ and $\times$ ("plus" and "times"), the basic arithmetical operations, with suitable axioms that govern their behaviour.
Thus, according to the specific mathematical symbols and axioms introduced, we have different mathematical theories; when the collection of axioms is the first-order version of Peano's axioms, we have Kleene's theory $\text N$ (aka : $\mathsf {PA}$), i.e. first-order theory of arithmetic.
The same for $\mathsf {ZF}$, i.e. Zermelo-Fraenkel Set Theory.

See also List of first-order theories.
