Re: [mizar] [gmane.comp.science.types.announce] [Agda] CFP: Dependently Typed Programming (FI Special Issue)

[Freek Wiedijk <freek@cs.ru.nl>]

Andrzej:

>Why you think that first order logic is dubious

One might say that the intuitionists think that classical
first order logic is dubious :-)  However, that is not the
right way to look at it: classical first order logic is a
subsystem of constructive first order logic (the subsystem
consisting of the negative statements, i.e., the statements
that are equivalent to formulas of the form "not A[]".)

>(PRA is a first order theory, isn't it?).

That is true, but I still experience PRA in the style of
nqthm/ACL2 as weaker than first order logic, as in those
systems you don't seem to have first class existential
quantifiers.

>Actually I do not know what 'semantics` means, if it is
>not based on set theory.

Neither do I, but I'm certain that the term is used by
type theorists, and that in that case they _don't_ consider
themselves to be doing set theory.  (I guess that when they
talk about semantics they "just" interpret one theory in
another one.)

Freek