Constructivism and Metamathematics

Abstract

This paper discusses the problem of availability of constructive metamathematics for constructive theories. Since intuitionism is usually considered as the most important kind of constructivism, we have the following question: Is it possible to give intuitionistically acceptable proofs of metamathematical theorems? This issue is illustrated by the completeness theorem for intuitionistic predicate logic and the consistency of arithmetic. The conclusion is that hitherto collected evidence justifies the claim that the universal intuitionistic metamathematics is very problematic.