Is Gödelian Model-based Deductive Reasoning Computational?

Abstract

I advance herein the view that the reasoning required to prove Godelian incompleteness theorems is not, contrary to what some have said, achieved by today's automated theorem provers.