We’ve also seen that proofs in formal systems can be considered as a type of non-deterministic computation. We can therefore try to use the recipe on them. This will work if the axioms and rules of inference are of an appropriate type. We have to be able to write expressions which check whether a number is the encoding of an axiom of the system, and whether a number is the encoding of a statement which follows, via the rules of inference of the system, from one or more other statements whose encoding is given. The pattern matching capabilities of concatenation make this fairly straightforward for most systems though. A rule like ``From statements \({ P }\) and \({ Q }\) we can deduce the statement \({ ( P ∧ Q ) }\). Also, from any statement of the form \({ ( P ∧ Q ) }\) we can deduce the statement \({ P }\) and the statement \({ Q }\)’’, for example, is very easily expressed. Although it requires considerably more effort we can also express fairly complicated rules, like the rules for quantifiers in our system for first order logic, including their restrictions in certain cases to substituting only new parameters for variables.
In this way we can show that the encoded statements of theorems of first order logic form an arithmetic set. I didn’t exactly make this easy though. We don’t have any axioms but we have a lot of rules of inference and some of them are fairly complex. The task would be much easier with a more traditional axiomatic system, like a first order version of Nicod. This is why those systems aren’t merely a historical relic. Although it’s painful to prove things in them, it’s easier to prove things about them.