It actually does make sense, and is an important idea in complexity theory. In general, the problem of proving an arbitrary claim in ZFC isn't computable (this

It actually does make sense, and is an important idea in complexity theory. In general, the problem of proving an arbitrary claim in ZFC isn't computable (this is just Godel's incompleteness theorem). if you confine your claims to smaller languages, you get smaller complexity classes. For instance, the problem of proving things in the propostional calculus is called BSAT, and is the quintessential NP complete problem. In general a nice way of thinking about what NP is are the set of formula that have polynomial time checkable proofs.