[Agda] Warning: this message contains amateur philosophy

[Peter Dybjer]

Hi Thorsten,

I realize this message is a bit outside the range of topics normally
discussed on the Agda-list ...

> Ouch! Are there any "objective concepts" in Mathematics? I had the
> impression this has all to do with our mind. Isn't this what
> intuitionism is all about? I didn't know that you had become a bold
> Platonist?
>
> Objective concepts: Kronecker suggested the natural numbers, otherwise
> you have to believe in some higher authority. Even the natural numbers
> are not really objective but based on a very broad agreement. My
> understanding of intuitionism (and hence predicativity) was that we
> carefully try to extend this agreement.

What I have in mind is the fact that the correctness (or incorrectness) of
a type theoretic judgement

a : A

is an objective fact. In the case of

a : N

this is clear. It is correct if the program a terminates with a natural
number (let's not worry about lazy natural numbers for the moment) and
whether or not this is the case is an objective fact.
This is what Martin-Löf style meaning explanations are all about, although
in general to establish the correctness of a judgement we have an
interactive process and not just "batch computation" of a. If A = Wx : B.
C
then a should compute to sup b c, and we then need the input to c, etc.

>> I propose the following plan of action when adding a new
>> construction to
>> Martin-Löf type theory (Agda).
>>
>> 1. Prove it consistent relative to set theory
>> 2. Give an informal but careful analysis why it is constructive,
>> that is,
>> why it satisfies Martin-Löf's style meaning explanations.
>> 3. Prove normalization and decidability of type-checking for the
>> extended
>> system.
>
> it seems we may have trouble at step 2.

We need to establish whether the resulting theory is correct in the sense
of the Martin-Löf style meaning explanations as explained above. Although
the set theoretic modelling in 1 is not sufficient to be sure about 2, it
may nevertheless be relevant for increasing our confidence.

Peter