Checking proofs in the metamathematics of first order logic

purl.stanford.edu/dd609fp0649