 Ad 3: Open proofs are justified by considering their closed instances. These closed instances are obtained by replacing their open assumptions with closed proofs of them, and their open variables with closed terms. For example, a proof of B from A is considered valid, if every closed proof, which is obtained by replacing the open assumption A with a closed proof of A, is valid. In this way, open assumptions are considered to be placeholders for closed proofs, for which reason we may speak of a substitutional interpretation of open proofs.