  The second idea makes Martin-Löf’s approach strongly differ from all other definitions of proof-theoretic validity. The crucial difference, for example, to Prawitz’s procedure is that it is not metalinguistic in character, where “metalinguistic” means that propositions and candidates of proofs are specified first and then, by means of a definition in the metalanguage, it is fixed which of them are valid and which are not. Rather, propositions and proofs come into play only in the context of demonstrations. For example, if we assume that something is a proof of an implication A → B, we need not necessarily show that both A and B are well-formed propositions outright, but, in addition to knowing that A is a proposition, we only need to know that B is a proposition provided that A has been proved. Being a proposition is expressed by a specific form of judgement, which is established in the same system of demonstration which is used to establish that a proof of a proposition has been achieved.