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?
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 :
With it we prove the fundamental Soundness and Completeness Theorem :
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.