  where the brackets indicate the possibility to discharge occurrences of the assumption A. The open assumptions of a derivation are those assumptions on which the end-formula depends. A derivation is called closed, if it has no open assumption, otherwise it is called open. If we deal with quantifiers, we have to consider open individual variables (sometimes called “parameters”), too. Metalogical features crucial for proof-theoretic semantics and for the first time systematically investigated and published by Prawitz (1965) include: