Checking proofs in the metamathematics of first order logic.