Finding a material on the construction of mathematical logic I am taking a 'mathematical logic' course this semester, but the material we are given seems a bit superficial as it goes directly to the methods to simplify formulas. What I'm looking for is a material that talks about the construction of logic (from basic set theory maybe?) that is a little bit more rigorous than our course and that starts from zero. I have been searching on the internet, but I can't seem to find anything interesting. It'd be nice if anyone could give me some links (in French or English) about that.
Thanks in advance.
 A: First we have to choose a meta-system to work in, in which any formal system that we wish to study is just an object. Many meta-systems are possible, but they must all have something equivalent to string manipulation and induction. Traditionally people choose a meta-system that has the same proving strength as ZFC, simply because much of modern mathematics can be expressed in ZFC. However, ZFC is way stronger than needed for almost all results in logic. So some people choose a different meta-system such as some kind of type theory.
Next we define a formal system as a language over some alphabet together with a collection of rules describing which strings can be derived. Note that the alphabet, language, rules and strings are all objects in the meta-system. When we reason about a formal system we are not in the formal system, and can talk about what strings it can and cannot derive, whereas in the formal system all we can do is to follow the rules to produce more derived strings.
If you use a ZFC-equivalent meta-system, for example, you would say that a formal system consists of a set of strings that is generated by the rules applied to the empty set. (Some of the rules might say that you can always derive certain strings, which are called axioms.) This generation process can be defined using induction and then you need some further tool in the meta-system to collect all the strings that can be derived in $k$ steps over all natural numbers $k$. This would be trivial in any ZFC-equivalent meta-system because we can take $\bigcup_{k\in\mathbb{N}} S_k$ where $S_k$ is the set of strings that can be derived in exactly $k$ steps. But many other meta-systems can do the same too, so you are not at all restricted to using a set theory for your meta-system.
Note that very often you will need the law of excluded middle in the meta-system. For instance if you want to prove that for any first-order theory $T$ either $T + φ$ or $T + \neg φ$ is consistent, you will necessarily have to invoke excluded middle or equivalent at some point. This is true even if $T$ is intuitionistic! In general, most logicians would have no qualms saying that either a formal system can prove a certain formula or it cannot, which already requires the meta-system to have excluded middle. Also note that because of this, some constructions that you perform in the meta-system will not be computable.
But still in many cases, the theorems you prove in your meta-system actually have some concrete representation in the real world (or so it seems so far), as programs in some generic programming language. For example:
(For any recursive first-order theory)


*

*There is a program to check whether the input (string) is a well-formed formula.

*There is a program to check whether the first input is a valid proof of the second input.

*There is a program that outputs a proof of the input if the proof exists (if not it may not halt).


Even better:

There is a program that, given any proof checker program (for any arbitrary formal system $T$) and string $φ$, outputs a $\Sigma_1$-sentence over PA that is true (under the standard interpretation) if and only if $φ$ is provable in $T$.

The above is true despite $T$ being unknown to the programmer, not to say the program (which is only given the proof checker program)! Furthermore, for some formal systems $T$, this is the best possible, as there may not be a program that always outputs "yes" or "no" as the correct answer to whether $φ$ is provable in $T$. Of course, for any single $φ$ there is a program that outputs the correct answer even if we cannot figure out what that program is. But there is no single program that can get the right answer or any arbitrary $T$ (given as a proof checker program) and string $φ$!
