With all of the axioms expressible in primitive recursive terms, we can start on what it means for something to be provable.
We'll define what it means for some statement x to be an immediate consequence of some statements y and z.