Per Martin-Löf: Assertion and request

Abstract: Think of the content of an assertion as something that is to be done: let us call it a task. Peirce’s explanation of the speech act of assertion as the assuming of responsibility then takes the form: by making an assertion, you assume the responsibility, or duty, of performing the task which constitutes the content of the assertion when requested to do so by the hearer. Thus a duty on the part of the speaker appears as a right on the part of the hearer to request the speaker to perform his duty: this is an instance of what is called the correlativity of rights and duties, a fundamental principle of deontological ethics which can be traced back to Bentham. In logic, it appears as the correlativity of assertions and requests. Since nothing but assertions appear in the usual inference rules of logic, there arises the question of what the rules are that govern the correlative requests. In the case of constructive type theory, they turn out to be the rules which bring the meaning explanations for the various forms of assertion to formal expression. Thus, in analogy with Gentzen’s dictum that the propositional operations, the connectives and the quantifiers, are defined by their introduction rules, we may say that the forms of assertion are defined by their associated request rules.