After my talk on "Tests, Games, and Martin-Löf's Meaning Explanations for 
Intuitionistic Type Theory" some of us went on to discuss meaning explanations 
by email. After this discussion Steve Awodey encouraged us to make it available 
on the UF wiki. What follows is obtained by "linearizing" the many simultaneous 
"threads" of this email discussion. Unfortunately, this linearization is not 
perfect, and as a consequence it sometimes seems more disjoined than it actually was.

Peter

DO THE MEANING EXPLANATIONS APPLY BOTH TO INTENSIONAL AND EXTENSIONAL TYPE THEORY?
==================================================================================

PETER DYBJER: Meaning explanations play an equally big role for intensional as for 
extensional type theory.

MIKE SHULMAN: Okay; that's not what I took away from your talk and from our
discussions today.  I thought you said that the meaning explanation
only explains the extensional identity types, and over lunch I
understood how that is, because the recursive part of the definition
says that the identity types literally contain only refl.  It sounded
to me as though there might be things you could do to get an
intensional theory, like building a notion of witnesses for equality
into the starting notion of computation like Bob was suggesting, but
that they aren't part of the "standard" meaning explanation.  Is that
not right?

PETER: Intensional type theory is a subtheory of extensional type theory 
(at least "morally") which results from removing the rule of "identity reflection" 
and the rule of "uniquness of identity proofs" and keeping the rule for the 
eliminator "J". So all rules of intensional type theory are validated by the 
meaning explanations. Because of the absence of "identity reflection" and 
"uniquness of identity proofs" intensional type theory has other models, 
but they are "non-standard".

The meaning explanations are as central to the present version of intensional 
type theory as they are for the extensional version. When introducing the 
logical framework with a distinction between "sets" and "types" Per Martin-Löf 
added meaning explanations to the logical framework level.

In my talk I emphasized that the meaning explanations validate extensional type 
theory. It was one of the aims of my talk to bring extensional type theory into 
the discussion here at IAS, where extensions of type theory, even undecidable 
ones, are discussed anyway. It's important to know about extensional type theory, 
and in what sense it is constructively valid, even if you don't want to use it.

THIERRY COQUAND: As Peter said in his talk, the meaning explanation can also be
seen as describing a realizability model for type theory (and this is a model
of both intensional and extensional theory).
As any model based on semantical ideas, it validates rules that are not derivable in the
formal system (for instance, any valid universal statement   Pi n:N. Id N (f n) 0
for f : N -> N will be validated in this model even if it is not provable in type theory.
Another rule validated in this model is 

  x: Id N 0 1 |-  5 : N -> N 

since  the type Id N 0 1 is empty; but this is not an argument for putting this rule
in the formal system...

One can give a similar realizability model which validates the rules
of intensional type theory and not extensional type theory by introducing
so called "neutral terms" in the computational model. For a type theory with
only N, S, 0 and natrec the result of a computation  instead of being only

 v ::= S(t) | 0 |  \x. t

(to simplify the discussion I don't consider the possible type values) like in the
closed term model, can now be

 v ::= S(t) | 0 | \ x. t | k
 k ::= Xn | app(k,t) | natrec(k,t,t)

where we have introduced variables X0,X1,… So a neutral term is a term
where the computation is "blocked" by a variable. Using these neutral terms
it is possible to define inductively when a term is normalizable.
(The definition is: Xi is normalizable, app(k,t) is normalizable if both k and t
are, natrec(k,t0,t1) is normalizable if k,t0,t1 are, S(t) is normalizable if t is,
0 is normalizable, and \x.t is normalizable if t(x/X0) => u and u is normalizable).
The definition of the model is then similar to the closed term realizability  model
but one adds to the clauses defining a type that -all- neutral normalizable terms
are in this type. For instance the clause of N becomes

 if A => N   and    if a => 0 then a:A
       if a => S(b) and b:A then a:A
       if a => k   and k normalizable  then k:A

The model is now a realizability model for intensional type theory, which
does not validate the extensionality rule. (This is one way to prove normalization for
type theory).

MIKE: Interesting, thanks!  But I have to say that I don't find that a
particularly compelling model of intensionality.

THIERRY: (This model was not intended  to be a compelling model of intensionality.)
The main point I wanted  to stress is that it is not so clear how to use the model
of closed terms as a justification for adding rules to type theory just because of their validity in
this model. Both the intensional rules and the extensional rules are justified in this model.
Which one to choose? As I wrote in my message, the model of closed terms also justifies rules like

 x: Id N 0 1 |-  5 : N -> N

that we clearly don't want to add. This example shows that some further discussions
are needed when adding to type theory a rule validated by this model.
 Maybe this point was clear already but I just wanted to bring it to the discussion.

BOB HARPER: 1. contrary to what thierry advocates, in nuprl we absolutely do take the 
meaning semantics as definitive, and allow any and all rules that are true under that 
interpretation.  in particular, it is both semantically valid and syntactically derivable 
that x in I(N,0,1) |- 1 in N->N, and all such similar things.  this is a feature, not a bug, 
in my opinion.  in nuprl the syntactic rules are merely codifications of standard practices 
for building proofs; it is the meaning semantics that DEFINES the theory.

2. thierry gave a fine example of how to give a meaning interpretation to itt that i suspect 
may have been misunderstood.  while it is true that the semantics given by peter validates 
both the rules of itt and the rules of ett, this is not the point of thierry's example.  
rather, he gives a _different_ meaning semantics for itt in which the operational semantics 
with which we start the discussion is defined for open terms, and which is then used to 
give a meaning-style interpretation of types.  this is a different enterprise from observing 
that peter's semantics validates the rules of itt.  maybe this was obvious, but as i read the 
discussion it seems that there might've been some confusion about this.

3. the nice thing about that example is that it shows that a meaning semantics need not 
force an "extensional" interpretation of identity; peter's does, but thierry's does not.  
but notice that in both cases the inhabitants of the identity type are determined solely 
by whatever the equality judgment means, which is to say that something is in Id_A(a,b) 
iff a=b in A, but the meaning of the latter judgment varies in the two interpretations.  
in this sense i think the emphasis on "equality reflection" as an expression of 
dimensionality is misleading.  the identity type always captures the equality 
judgment exactly; it's a question of what equality means that matters.

MIKE: You keep saying that, but I have to interpret it as a philosophical
statement of how you think a system *should* behave (rather than with
the meaning of "always" that I am used to), since it is not true in
the ordinary intensional MLTT.  Is it?

BOB: i don't know what is "ordinary mltt", because there are many useful and 
well-developed variations.

i think it is important not to confuse definitional equality with equality.  
if you do, then it looks as though the identity type in itt expresses something 
different than the equality given by the judgment, but that is because the equality 
given by the judgment is definitional equality (sameness of sense), not equality (sameness of reference).

in the judgmental formulation of 2dtt that dan and i gave we stressed this point by 
having a judgment of equality that is coextensive with the identity type, just as it 
is in nuprl.  but nuprl is one-dimensional, whereas our system is two-dimensional.  
so the dimensionality is not properly expressed by the relationship between the equality 
judgment and the identity type, because i claim (philosophically, programmatically) 
those two must always coincide, and they do in both the 1- and 2-dimensional cases 
with which i am familiar.

THIERRY: One further remark on the approach of taking the meaning semantics
for closed term as definitive. If we take an arithmetical statement which is true classically
but cannot be realized, for instance

 A =  forall n.   exists m T(n,n,m)   \/   not (exists m T(n,n,m))            T Kleene predicate

then we cannot have any proof of A. This implies that the judgement

  \lambda x.  0 :    not A = A -> emptytype

is valid (we can replace 0 by any expression) and so we have a proof of not A
and we get a system which is incompatible with classical logic (since A is true classically).

PS: Following Bob's message, it may indeed not be so clear that we want to forbid a priori rules like
        x:Id N 0 1 |- 5 : N -> N.
I found the NuPrl approach really nice since it is based
on a clear and simple semantics and follows it in a systematic way. 
I take features like the fact that we get rules like x:Id N 0 1 |- 5:N->N and the other point above
as signs/indications that we should take into account other semantics, but this is open to discussion.

THIERRY: One can then interpret my message as an argument why we cannot  assume
a fixed programming language -if-  we want to base the meaning explanation as
closed term realisability on this programming language (and this argument itself does
not use Church's thesis). 

 It is only if one wants to use this kind of semantics as definitive
(which is not my position) that assuming a fixed programming language is
essentially Church's thesis. For instance, Martin-Lof type theory is also
open ended, and it cannot be rejected a priori that all principles that we would
ever add to it can be expressed in a fixed programming language (e.g. induction-recursion
strong notion of universes, bar-induction,…)

BOB: Nice!  this is a good way to explain why open-endedness is so important to the meaning explanation.

Actually, this point confused me this morning, because i know the nuprl semantics to be consistent with 
classical logic, yet i wasn't quite able to see where the discrepancy arises.  i asked bob constable, 
who replied cogently as follows:

BOB CONSTABLE: You are right that (without the theory of partial types) the type theory of Nuprl, 
Constructive Type Theory (CTT), is consistent with classical mathematics, even with Bar Induction 
which we have recently added. Doug Howe has a set theoretic semantics that works for the theory 
without partial types and without the full recursive types -- which are extremely strong. 

The type A that Thierry is reasoning about is only known to be unrealizable if we accept 
Church's Thesis (CT).  We don't accept that in CTT.  If the reasoning is in the meta theory, 
using Church's Rule, then we might say that A is unrealizable based on an external analysis, 
but this is not expressible inside the theory and \x.0 is not a realizer inside for ~A.

BOB HARPER: it is a delicate point about the nature of the meaning semantics and the concept of 
"pre-mathematics" that peter has been defending.  the formula that thierry gave is indeed 
independent of HA viewed as a formal system, and if the meaning of the negation were given 
by provability in that formal system, then we would be in a situation where every unrealizable 
statement would be positively false.  but that is not the case.  the fact that thierry's A is 
unrealizable requires church's thesis, which we do not accept in the pre-mathematics 
(nor should we) in which the semantics is given.

PETER: I agree with the conclusion of this discussion that if you consider the 
"meaning explanations" as being about a fixed language of computable realizers, 
then we can justify anti-classical principles. Relating this to my talk, I see this 
as one of the "global" conditions that we do not want to assume in the "meaning explanations". 
The meaning of a judgement should only depend on its constituent terms, 
not on properties of the language in which it is embedded.


THE DISTINCTION BETWEEN "META-MATHEMATICAL" AND "PRE-MATHEMATICAL"
==================================================================
 
PETER:  Whereas realizability models are meta-mathematical in the sense 
that they presume a mathematical metalanguage, the meaning explanations are 
"pre-mathematical" in the sense that they explain the meaning of type theory 
only with reference to a primitive notion of computation.

MIKE: I still don't understand what "pre-mathematical" is supposed to mean.  It
sounded to me as though people were just saying that mathematics is
used to model/describe things in the real world that aren't themselves
mathematics.  Does "pre-mathematical" just refer to the process of
abstracting from something nonmathematical to come up with some
mathematics that we can use to describe it with?

PETER: I remember Per writing somewhere that he is doing logic in the tradition 
of the founding fathers of modern logic: Frege, Russell, Brouwer, ... who discussed 
the foundations of mathematics "from scratch". He contrasted this to the 
"meta-mathematical" tradition beginning with Tarski, which has taken over 
mathematical logic. In the beginning of his book "Intuitionistic Type Theory" 
(which will be cited later on) he distances himself from that tradition, 
where "mathematical logic is logic studied by mathematical methods, as a branch of 
mathematics." rather than as "foundations (or philosophy) of mathematics" which 
is what he does.

When a logician uses mathematical methods to study a logical system, he tacitly 
works in "mathematics" qua "set theory". (Of course, in some work one tries to 
limit the power of the metatheory. Thierry told me that Kleene's use of the 
word "metamathematics" actually meant using safe weak metatheories. Still it 
is "meta" in the sense that he assumes some mathematical framework.)

"Pre-mathematics", as I see it is to, refers as much as possible to simple, 
primitive "everyday", finite, concepts of "computation" and "observation". 
I do not want to pretend that the distinction between "pre-mathematics" and 
"meta-mathematics" is clear and crisp and uncontroversial. But that doesn't 
say that it is not there. We want to say something about the foundations of 
mathematics without some already accepted mathematical metalanguage.

MIKE: Anyway, it seems to me that the description of the meaning explanation
as an inductive-recursive definition makes perfect sense as a piece of
mathematics.

PETER: Indeed. That's what we do to construct the realizability model (the "PER-model").

MIKE: It makes sense as a piece of mathematics even if it can also be used 
informally as an argument for why type theory describes computation, or whatever 
you mean by "pre-mathematical".

PETER: If you look at the meaning explanation as giving rise to an 
inductive-recursive definition, viewed a formal concept in type theory 
(which can be understood set-theoretically) then you are taking the 
meta-mathematical viewpoint. One of the aims of my talk was to explain 
how these rules can be viewed as instructions for someone who wants to 
check the correctness of type-theoretic judgement by running tests and 
observe the result. This is something that can be done, without 
understanding what an inductive-recursive definition is or how 
it can be interpreted set-theoretically.

MIKE: I guess I have always figured that the reason modern logicians moved
to what you call "meta-mathematics" is that they realized you can't
get anywhere from nowhere.  You can't study the nature of logic
without having "somewhere to stand" with which to evaluate the
correctness of your statements about the nature of logic. 

PETER: But we would not have had predicate logic, set theory, type theory, 
intuitionistic logic, etc without the "pre-mathematical" considerations of 
Frege, Cantor, Russell, Brouwer, etc, in the first place.

MIKE: We wouldn't have modern physics and chemistry without the medieval
alchemists either, but that doesn't mean we still need to do alchemy.

PETER: Per is saying that there is still need for these foundational considerations.
His meaning explanations are intended to be an example of just that.

MIKE: That's the claim that I haven't heard any arguments in support of.

PETER: But intuitionistic type theory is the result of such thinking, isn't it? 
Per and Thierry have been deeply motivated by "pre-mathematical" thinking. 
Another example is Girard. He is trying to rebuild the foundations of logic, 
and although he makes good use of "meta-mathematics" the foundational thoughts 
are at the very core of his enterprise.

MIKE: I have always thought that one of the primary lessons of
twentieth-century mathematics and logic is that it's pointless to go
around looking for "the" foundation of mathematics, or trying to
justify a foundational system on purely philosophical grounds. 

PETER: It doesn't need to be on "purely" philosophical grounds. 
Per's work is a combination of his technical experience as a proof-theorist 
and his interest in the philosophy of mathematics. 

MIKE: We should take a pluralist conception: there are lots of systems that can
be foundational, with different properties and strengths and
relationships to each other, and they all have different uses.  Andrej
wrote about this recently:

http://math.andrej.com/2012/10/03/am-i-a-constructive-mathematician/

We now have the tools and the perspective to understand and study the
various worlds of mathematics formally.  Why do we still need to
waffle around at a pre-mathematical level?

PETER: Per's meaning explanations are actually very precise, but they 
would loose their importance for foundations if they were "only" an 
example of an inductive-recursive definition understood set-theoretically. 

MIKE: You keep saying "set-theoretically", but I've said that mathematics
doesn't need to be understood as meaning set theory.  Maybe we are
just confused about terminology: what you call "pre-mathematics" is
something that I would consider part of mathematics?

PETER: After having used the term "pre-mathematics" so many times, 
and within quotes, I start wondering whether it is a good term, 
or perhaps it confuses more than clarifies. I introduced it in a 
previous version of a talk on this topic. The purpose was to contrast 
Per's meaning explanations to the corresponding realizability model. 
I have continued using it, but now I'm not so sure it's a good one. 
Or perhaps the problem is not the terminology, but the deeper question 
whether the meaning explanations have a different status than other 
model constructions.

The word "meta-mathematics", on the other hand, has a precise meaning: 
the study of a logical theory from the point of view of a logical meta-theory. 
I keep mentioning set theory because it is the "default". If nothing else is 
mentioned and we want to say what it means to be rigorous axiomatically based 
mathematics, then we assume that it is set theory. 

MIKE: Maybe you do, but I don't.  I'm surprised to hear a comment like that
coming from anyone who studies constructive type theory.  Why should
we consider set theory to be the default?

PETER: Because it is the most widely accepted, and also the potentially 
strongest theory (with lots of knowledge about strong axioms)? What would you say?

MIKE: I don't see why there needs to be a default.  Although most
mathematics is much more naturally coded into type theory than into
classical \epsilon-based set theory, even if most mathematicians don't
realize that.

PETER: No, there does not need to be a default. I quite agree that most "meta-mathematics" 
is done informally, without any mention of what meta-theory is used. But it is 
important for the discussion that there is a meta-theory around, if only implicitly so. 

A remark: Thierry told me that Kleene insisted on using weak (even constructive) 
meta-theories. And clearly, there is a lot of interest in the question what 
strength we need in the meta-theory when proving some result.

More generally, we need to understand the relationship between mathematics and 
reality. There is something deeply unsatisfactory about the "unreasonable 
effectiveness of mathematics". 

MIKE: I'm not really convinced of that.  People invented mathematics with
the goal of describing reality, so why is it surprising that it
describes reality?

PETER: I think there is something special about computational foundations of 
mathematics, the broader enterprise of proof theorists who try to find the 
computational content of classical logic, set theory, etc. This very exciting 
enterprise goes much beyond purely intuitionist systems and is on its way to 
bridge the gap between mathematical practice and "meaning explanations" 
(taken in a broader sense). Intuitionistic type theory is just the system 
where the computational interpretation is most direct, and with that comes 
a connection to programming, and with that a connection to utility.

ANDREJ BAUER: While I am a great fan of realizability, I find it too limiting 
to understand logic only through the eyes of computation. As we know well 
geometry (if Mike. will forgive me for using that word) gives another kind of 
understanding, one in which truth must be "locally stable" rather than 
"comutationally witnessed". Some might think of it as an unintended interpretation, 
but it is not going away. We now even have a second non-comutational interpretation 
in terms of homototpy, which is not going away either. It is these new unforseen 
ways of understanding logic which are to me the primary reason for an open-ended 
system. But I want to go further: there is no a priori reason to think that there 
can be one logic/mathematics that fits all purposes. If we insist on being 
conservative with respect to all future discoveries, we shall never be able 
to commit to anything much.

PETER: Sometimes I think the very term "meaning explanation" is a bit unfortunate, 
it turns people like Mike off because it smells so much of philosophy. It's just 
something very simple and familiar to a programmer: it's about what happens when 
you run your programs and checks your results.

MIKE: Would you say, then, that the meaning explanation is about explaining
in what sense type theory is describing real-world programming?

But thinking about that has made me realize perhaps a little more
precisely what I am confused about.  It seems to me that there are two
completely different things going on:

1. Relating untyped notions of computation to typed ones.

2. Relating real-world notions of computation to mathematical ones.

PETER: I like this analysis, although I would rephrase 1 somewhat: 
"Relating untyped notions of computation to typing (or more generally to all the judgements)"

MIKE: We can have both typed and untyped notions of computation both in the
real world and in mathematics.  And it seems to me that if the end
result you want is to relate real-world, untyped notions of
computation to mathematical, typed ones, it would be simpler to first,
say, relate your starting point to a mathematical, untyped notion of
computation, and then do the remaining comparison inside of
mathematics.  Or to go around the other side of the commutative
square.

Moreover, on the surface, at least, the meaning explanation appears to
be only about relating untyped computation to type theory.  Which is
something that could happen entirely in mathematics --- or, I suppose
entirely in the real world.  So I think this is why I am confused that
everyone seems to be saying that the meaning explanation has something
to do with relating mathematics to the real world.

PETER: What the meaning explanations add to the mathematical aspects of the 
realizability model is the philosophical motivations why this is a good basis 
for the "constructive validity" of the system. 

MIKE: Is it correct, then, that the aspect of the discussion which can be
described as an inductive-recursive definition is the purely
mathematical aspect?

PETER: Yes.

MIKE: Okay.  I thought someone was saying that the part which looks
inductive-recursive should also be thought of as being
pre-mathematical or philosophical in some sense.  Now I guess I can
just ignore the philosophical talk about "constructive validity" and
be happy.  (-:

BOB: yes, but notice the discussion we had that involved subtleties such as 
the role of open-endedness and constructive reasoning at the level of the 
semantics.  these thoughts all come prior to formulating a definition (in the 
sense that peter was outlining) of type theory itself.  i don't think it's 
avoidable, or even desirable to try to avoid it, because you can't start 
from nothing and get something.

PETER: And note that Per says that he "certainly" does not do "mathematical logic 
as logic studied by mathematical methods, as a branch of mathematics" in his book 
(see citation below). But if you look at it purely meta-mathematically the whole 
book is a big inductive-recursive definition (with comments).

The philosophical discussions related to meaning explanations are quite open-ended, 
it's philosophy! In his talk at the meeting in Uppsala in 2009  in connection with 
his retirement, Per discussed "epistemological" vs "ontological" aspects of truth, 
and at the same meeting, his colleague in Stockholm Dag Prawitz discussed how Per's 
view of "epistemological" vs "ontological" aspects of truth and proof has changed 
over the years.

To demonstrate how Per has extended a rather technical account of the meaning 
explanations to excursions into philosophy, let me quote how little he he writes 
when he first introduces them in 1979 in "Constructive Mathematics and 
Computer Programming".

"In explaining what a judgement means, I shall limit myself to assumption 
free judgements. Once it has been explained what meanings they carry, the 
explantions can readily as to cover hypothetical judgements as well."

That's all. Then he goes on with what one can read meta-mathematically as the 
building of a mathematical model, although the purpose is clearly 
"pre-mathematical". There is hardly any philosophical discussion at all, 
except that the paper begins with quite a long discussion about the 
correspondence between constructive mathematics and computer programming.

In Per's book, based on lectures in Padova 1980, there is quite a bit 
more philosophical discussion. And then in his Siena lecture from 1983 
there is a real focus on philosophy. Many of his talks during the 1980s 
and 90s are rather non-technical and more philosophical, testifying to the 
open-ended nature of the "meaning explanations".

MIKE: The place that you stand doesn't have to be "set theory" -- it can be (and I
think often or even usually is) merely "informal mathematics" in the
sense that Peter Aczel has been advocating.  But why not allow
ourselves to be precise and use the tools of logical reasoning that
mathematics has laboriously developed over centuries, even when
studying mathematics as our object?

PETER: Sure, it doesn't have to be "set theory" and it can be "informal", 
but the term "meta" refers to the fact that you study a logical theory using 
the tools of a logical meta-theory. This reasoning can be informal, but it 
is only informal in the sense that the details of proofs and constructions 
in principle can be reduced to some formal meta-theory, for example set theory. 
(This point of view was expressed by Vladimir in the discussion the other day 
where he referred to ZF as the ultimate thing.) If there is no meta-theory around, 
either explicitly or implicitly, I don't think the word "meta-mathematical" 
is appropriate.

Moreover, I don't see "meta-mathematical" and "pre-mathematical" considerations 
as being mutually exclusive, rather they complement each other. Building a 
meta-mathematical model (like the realizability model) using the tools of 
set theory (inductive definitions as fixed points of monotone operators) 
helps clarifying the details of the meaning explanations. But that's not 
the whole story, you need a "pre-mathematical" story to explain why this 
is suitable as a foundation of constructive logical reasoning. 

MIKE: Why do you care?  People got into huge fights over this in the early
20th century, but haven't we outgrown that by now?  For lots of
mathematics, "classical" reasoning is useful and appropriate.  For
other purposes, you want to use a logic which is "constructive", but
the meaning of that can differ depending on the *reason* you want to
be "constructive".

PETER: And as it happens, (much of) classical reasoning is constructive ...

MIKE: If what you want is an internal language for a Grothendieck topos,
then you'll want with something extensional and with impredicative
powersets.  If you want all your proofs to be extractable into
programs that a computer can run, then you'll want something
different.  If you're Vladimir and you want to be able to define
semi-simplicial types in a particular way, maybe you want some strong
eta-rules for natural numbers.  But if you want to be able to
implement a practical proof assistant, then maybe you want decidable
type-checking.  Etc.

PETER: I don't mind all those systems which don't have computational content, 
or very indirect computational content, it's just that I can't programs in them. 
And I'm a very happy customer of classical set theory. I wouldn't dare doing 
advanced metatheory in Martin-Löf type theory, when I've tried to do that in a 
proof assistant, I've had too many type-checking problems ... Bishop says in 
his introduction to "Foundations of Constructive Analysis" something like 
"I don't want to deny the utility of classical mathematics, just as I don't 
want to deny the utility of unrigorous mathematics".

MIKE: Obviously, you may want more than one thing at once, which is great
but can be hard to achieve.  Dan Licata was saying something like this
to me the other day: a large part of the difficulty this year is that
we have different applications that are pulling in different
directions.  On the one hand, it's awesome that there *is* one system
that can have multiple applications, but there may be limits: one side
will eventually push it in a direction that's unacceptable for the
other side.  (But that's a digression from the current discussion.)

PETER: Interpretation in set theory does not itself provide a foundation for 
constructive logical reasoning. The fundamental problem of meta-mathematical 
analysis is that it can never be a foundation; the meta-theory always has to 
be stronger than the object-theory if we want to build models. To zoom in on 
a foundation pre-mathematical considerations are inevitable.

It is interesting to look at Per's papers (and the book) from this perspective. 
There is never any reference to set theoretic models. In his first paper about 
the inconsistent type theory, there is a normalization proof carried out in 
an inconsistent meta-theory. If he had tried to model this set-theoretically, 
he would have avoided this inconsistency. In his 1972 paper there is also a 
normalization proof using an inductive-recursive definition in the meta-theory. 

MIKE: Sounds to me like an argument against "pre-mathematics"...

PETER: It is an argument in favour of supplementing the "pre-mathematics" with 
"meta-mathematics".

Furthermore, Per does not explain how the inductive-recursive definition used 
in his normalization proof in his 1972 paper can be modelled set-theoretically, 
but relies on his "pre-mathematical" intuitions of "predicativity". It was 
Peter Aczel who later showed that such definitions indeed be modelled set-theoretically.

As I see it, the "meta-mathematical" and the "pre-mathematical" analysis of 
foundational problems are complemetary. It is not a question of either-or, 
we need both. For example, the "meta-mathematical" realizability models of 
type theory provide mathematical precision which complements the 
"pre-mathematical" foundational accounts provided by Per.

MIKE: I was not able to make much sense out of the meaning explanation until
someone said it was an inductive-recursive definition.  Why can't I
still say it is an inductive-recursive definition even if I am
describing it in some informal motivational way (and without caring to
specify a particular formal system in which to do my informal
mathematics) rather than constructing a realizability model?

PETER: It is perfectly fine to call it an "inductive-recursive definition" 
although to my ear this suggests that you work in a meta-theory where you 
have access to this notion. The meaning explanations do not only describe 
the model construction in a motivational way. They are supposed to explain 
why type theory is appropriate as a foundational system, where you can believe 
in the consistency in a direct way. What do the judgements "mean" in some more 
direct, primitive way? They are on the same level as Brouwer's motivations for 
the validity of the laws of logic, and of his rejection of excluded middle. 
And similarly on the same level as the writings of Kolmogorov. Just more 
evolved and precise, building on lambda calculus and computation to whnf.

Let me give some more examples of how I see the distinction between a 
"meta-mathematical" and a "pre-mathematical" understanding of some basic concepts.

Formal grammar:
- meta-mathematically this is a way to specify an inductively defined 
set of strings (the language generated by the grammar). This can be 
understood set-theoretically.
- pre-mathematically, it is a concrete prescriptions for how to generate 
strings. You apply the rules and a few seconds later you have generated 
a string.

Computation rules, e g the relation a => v of (big step) evaluation to 
canonical form in type theory.
- meta-mathematically, a specification of an inductively defined relation 
between terms and canonical forms,
- pre-mathematically, a concrete prescription for how to compute the term a, 
by performing a series of steps until you reach the canonical form v later on

MIKE: I'm still confused about what it means to consider the meaning
explanation as "pre-mathematical".  If it is not mathematics, then how
can it prove anything?

PETER: Let me cite the first paragraphs of Per's book "Intuitionistic 
Type Theory" (Bibilopolis), which so clearly sets out his project:

PER (CITED): "Mathematical logic and the relation between logic and 
mathematics have been interpreted in at least three different ways:
* mathematical logic as symbolic logic, or logic using mathematical symbolism;
* mathematical logic as foundations (or philosophy) of mathematics;
* mathematical logic as logic studied by mathematical methods, as a branch of 
mathematics.
We shall here mainly be interested in mathematical logic in the second sense. 
What we shall do is also mathematical logic in the first sense, but certainly 
not in the third."

PETER: What does the book "Intuitionistic Type Theory" contain? There are 
three kinds of things, essentially:
1. a presentation of the formal system of type theory, its syntax, judgements, 
and inference rules
2. philosophical (foundational) discussions of the meaning of the judgements 
("meaning explanations")
3. an informal justification of the inference rules wrt the meaning explanations

Now, 1 and 3 can be viewed as a piece of mathematics, as a reasonably detailed 
sketch of how to construct a realizability model, contrary to his claim in the 
quotation above. However, 2 is definitely not mathematics, it's philosophy, 
it's "pre-mathematics". Per probably thinks of 3 as well as pre-mathematics, 
it's not "logic studied by mathematical methods, as a branch of mathematics". 
Probably Mike's confusion is related to the status of 3, is it (meta-)mathematics 
or is it pre-mathematics?

BOB: 4. for me metamathematics may be distinguished from pre-mathematics as follows.  
both are an attempt to understand the foundations of mathematics.  what 
metamathematics does is to FORMALIZE a particular conception (maybe, Peano arithmetic 
or ZFC or something), and then studies this formalism using various techniques.  
for example, independence results are good examples of metamathematics.  
but the problem with metamathematics is that as soon as you formalize a body 
of mathematics, you're in a state of sin from which you cannot really recover.  
the point is that a formal system is defining a computably enumerable set of 
judgements, but the true judgments are nowhere near computably enumerable.  
indeed, goedel showed us how to derive true judgments that have a perfectly 
unproblematic pre-mathematical proof that are not derivable in the formal 
system (for anything like an interesting formal system).  this is not to 
say that metamathematics is pointless or anything like that, but it is to 
say that it's not a satisfactory way to go about formulating a true foundations 
for mathematics, it's rather a mathematical device that can be useful to a 
limited extent, but never definitive.

MIKE: Well, opinions may differ on whether what Goedel showed has anything
to do with "truth", or whether that notion is even meaningful.  But at
least, I would have thought that Goedel's theorem implies the need for
a pluralist conception of foundations, since no one system can ever
suffice for everything we might want.

THIERRY:  I am not sure of the implication.  I understand that from Goedel's theorem, 
for any given formal foundation, we know that we will be 
forced at some later point to add new principles to this
formal system, but does it mean that we -have- to be pluralist in the choice
of this formal system and to have a pluralist conception of foundations?

MIKE: No, you're probably right; it doesn't automatically imply that.  But
it at least suggests it as a possibility, and there's plenty of other
evidence in favor of pluralism.

THIERRY: (I am not sure Goedel himself was a pluralist)

MIKE: No, quite probably he was not.  But of course that has no bearing on
the implications of his theorem. 

I do think we should also add to the record some of the discussion
that we had at the reception on Monday.  In particular, the
realization I had that the reason the meaning explanation doesn't seem
to me to "explain" anything at a philosophical level is that (at least
in the version that you presented) the meaning explanation appears to
be about assigning types to untyped things -- but for me, this is not
something that requires explanation.  I see everything in nature as
naturally having a type (which is one of the many reasons that I
prefer type theory to classical set theory, and why I am surprised
that type theorists apparently think it needs explanation).

PETER: Yes, it may seem surprising that the foundation of type theory 
is based on an untyped language. But I suspect that there are differences 
of opinions about this - we should ask Per what his current position is 
in this matter for example. Somewhere in his writing he says something 
like "an object always comes with a type" just as you say above. But even 
if an object comes with a type, it's important that the computation of the 
object (term) returns a value of the right kind. This is what's called 
"type soundness" of programming languages - Milner's "well-typed programs 
cannot go wrong". In fact, the meaning explanations are nothing but 
type soundness + termination. But this gives what Per calls "simple 
minded consistency" in his book: there is no canonical object of the empty type.

MIKE: I was also thinking some more earlier this week about philosophy in
general.  I am not against all philosophy; in fact sometimes I quite
like philosophy.  The kind of philosophy that I don't see much use for
is the kind that is prescriptive or proscriptive, saying that only one
kind of mathematics is "correct" or "meaningful" or "justified" or
"valid", or that only one model is "standard" or "intended".  But it's
seemed to me that the philosophical aspect of discussions of meaning
explanations are of this sort, insisting that a mathematical system
can only be "justified" in some particular way.

PETER: Yes, I'm afraid that the meaning explanations are of this sort. 
The intention is to give a "standard" semantics. But it's quite clear 
that that doesn't stop all discussion - there is plenty of discussion 
of the "meaning" of the "meaning explanations". The aim of my talk is 
to question some aspects of the meaning explanations, and Per has been 
thinking about reformulating them.

MIKE: Put differently, I do believe that philosophy can have interesting and
useful input to mathematics, such as in suggesting new ideas,
structures, and systems.  And philosophy of mathematics can also be
interesting in its own right, especially when it takes mathematics
seriously.  But I don't think that mathematics needs any
"justification" from philosophy.