The basic concept is that of Formal systems: a rigorously specified language with some (zero or more) axioms (initial formulas) and rules of inference (prescriptions how to derive new formuals from already derived ones). What counts is the respective "expressive capability".
Propositional calculus has a very limited expressive capability, but it is very useful for pedagogical reason, because with it it is possible to show the basic concept and properties of formal systems : syntax, semantics, consistency, completeness, etc.
First order logic is much more useful because it has a poweful expressive capability: with it we can formalize many (quite) all of mathematical thpories, like set theory and arithmetic.
First-order logic (FOL) is made of a language (the so called f-o language) with the quantifiers : ? and ?, rules of inference: like Modus Ponens and Generalization, and (zero or more) logical axioms.
A first-order theory is manufactured "on top" of FOL adding specific non-logical symbols and axioms: see PA for first-order Peano arithmetic or ZF for Zermelo-Fraenkel Set Theory.
In the case of set theory, for example, we have a single non-logical symbol, viz. the binary relation "in" (∈) and several non-logical axioms, like e.g. the Null axiom: ?x?y ? (y ∈ x).
Starting from the non-logical axioms and using the machinery of the "underlying logic", i.e. logical axioms and rules of inference, we can derive new formulas of the thory that are the specific mathematical theorems of the theory.
Intuitionistic type theory (aka constructive type theory or Martin-L?f type theory)
is a formal logical system and philosophical foundation for constructive mathematics. It is a full-scale system which aims to play a similar role for constructive mathematics as Zermelo-Fraenkel Set Theory does for classical mathematics. [...] The main idea is that mathematical concepts such as elements, sets and functions are explained in terms of concepts from programming such as data structures, data types and programs.
MLTT, as well as the historical Type Theory, developed by Alfred North Whitehead and Bertrand Russell’s into Principia Mathematica (1910-1913), and its modern versions, are formal systems which includes first-order logic, but are more expressive in a practical sense: they are well suited to the formalization of mathematics.
A good textbook regarding Mathematical Logic: Dirk van Dalen Logic and Structure (2004, Springer).
For MLTT and similar, see e.g. L.Crosilla, Constructive TYpe Theory and Giuseppe Primiero, Information and knowledge: A constructive type-theoretical approach (2008, Springer).
See also L.Crosilla, The entanglement of logic and set theory, constructively.
