Basic proof theory - Troelstra, A.S (Cambridge tracts in theoretical computer science, 2000)