  Formally, this definition has to be relativized to the atomic system considered, and to the set of justifications (proof reductions) considered. Furthermore, proofs are here understood as candidates of valid proofs, which means that the rules from which they are composed are not fixed. They look like proof trees, but their individual steps can have an arbitrary (finite) number of premisses and can eliminate arbitrary assumptions. The definition of validity singles out those proof structures which are ‘real’ proofs on the basis of the given reduction procedures.