 One can thus provide a proof-theoretic semantics for a language (Schroeder-Heister 1991). When presenting his system of natural deduction, Gentzen remarked that the introduction rules for the logical expressions represent their “definitions,” and the elimination rules are consequences of those definitions (Gentzen 1933). For example, the introduction rule for conjunction dictates that a conjunction \(A \amp B\) may be inferred from both conjuncts \(A\) and \(B\), and this rule captures the meaning of the connective. Conversely, the elimination rule for conjunction says that from \(A \amp B\) one may infer both \(A\) and \(B\). The universal quantifier rules tell us that from the universally quantified claim \(\forall xFx\) we can infer any instance \(Fa\), and we can infer \(\forall xFx\) from the instance \(Fa\), provided that no other assumption has been made involving the name \(a\). Under certain requirements, one can show that the elimination rule is validated by the introduction rule.