Q:

Definition and meaning of "Proof Schema", "Class Sign"

I'm a newbie in advanced mathematics, and I'm trying to understand Godel's theorem. I came across these two words which I couldn't understand clearly.
"Proof Schema" and "Class-Sign"
Can anybody provide me definition of these, and describe what these term mean in simple words? 
It's from Kurt Godel's book (translated into English) "On Formally Undecidable Propositions of Principia Mathematica and Related Systems".. by Dover publications.. I'll just quote lines where it's introduced (Page No 39)- 
"It can be shown that "formula", "proof-schema", and "provable formala" are definable in the system of PM.
Class-Sign: 
"A formula of PM with just one free variable, and that of the type of natural numbers(class of classes), we shall designate a 'class-sign'..
Thank you

A:

By "proof schema" Gödel just means a formal proof. You can see this quite clearly from the context: a formula is a finite sequence of natural numbers, each of which codes one of the symbols of the formula, while a proof schema is a finite sequence of finite sequences of natural numbers, in other words a finite sequence of codes of formulae.
The basic idea of Gödel coding is very simple: take the symbols of a formal language (the alphabet) and represent each symbol by a natural number in such a way that given any string of such symbols we can produce a finite sequence of symbols which represent them (encoding); and given any natural number there is an effective procedure by which we can calculate which symbol it represents (decoding).
A "class sign" is what we would normally in English call a predicate: a formula with one free variable $\varphi(x)$ whose extension is the class of objects $\left\{ x : \varphi(x) \right\}$. Since we're only considering natural numbers here the extension in question will of course be a set, that is, the set of natural numbers $n$ such that $\varphi(n)$. (Being fussy, we might say that a class sign is a unary predicate since it has only one free variable; one can have predicates of any finite arity.)
Defining these things in a precise manner is key to the method of arithmetisation, whereby logical notions are shown to be expressible in the language of arithmetic, and thus sentences in that language can be constructed which refer to themselves. This is called the method of diagonalisation.

