In justifying a rule of inference of a logical system one must assume that the judgements serving as premisses and conclusion in any application of the rule are meaningful. (Without meaning, anything goes, and the question of justification does not arise.) In contemporary logic, meaning is usually assumed to be provided by an interpretation in a model. Such a model is, however, presented in a mathematical language whose meaning itself may be in need of explanation. For instance, a model-theoretic proposition of the form "M models t = u" is defined to mean "the interpretation of t and the interpretation of u are identical elements of M". To the question of what this definiens, in its turn, means model theory provides no answer. In effect, this is a question about the meaning of the language of set theory, and that is not a purely mathematical question, but also in part a philosophical one. A typical answer consists in the reference to some conception of set, such as the iterative conception. Per Martin-Löf's meaning explanations serve a similar role for his constructive type theory, a constructive alternative to classical set theory. His meaning explanations are, however, much more precise, and developed in much more detail, than similar projects for other formal systems.
In this course we will, firstly, try to get clear about the nature and role of these meaning explanations. The ways in which meaning explanations differ from systems of model-theoretic semantics will be emphasized. Secondly, we will look at a novel formulation of the meaning explanations in terms of dialogues. This formulation of the meaning explanations has been motivated, at least in part, by a dialogical, or interactive, account of assertion, in which the speech act of assertion is explained together with the speech act of request. The knowledge possessed by an assertor is spelled out in dialogue rules that lay down what the assertor must do in response to a request for justification. For the forms of judgement employed in type theory it turns out that these rules, when properly understood, replicate the meaning explanations, albeit in a different formulation.
Topics related to this course can be found here and here. Here are the slides.