Right: automated proof checking is not really “generally doable” in an axiomatic system—how hard it is depends entirely on the axiomatic system under discussion.
Right: automated proof checking is not really “generally doable” in an axiomatic system—how hard it is depends entirely on the axiomatic system under discussion.