  One might investigate how far one gets by considering elimination rules rather than introduction rules as a basis of proof-theoretic semantics. Some ideas towards a proof-theoretic semantics based on elimination rather than introduction rules have been sketched by Dummett (1991, Ch. 13), albeit in a very rudimentary form. A more precise definition of validity based on elimination inferences is due to Prawitz (1971; 2007; see also Schroeder-Heister 2015). Its essential idea is that a closed proof is considered valid, if the result of applying an elimination rule to its end formula is a valid proof or reduces to one. For example, a closed proof of an implication A → B is valid, if, for any given closed proof of A, the result of applying modus ponens