[Date Prev][Date Next] [Chronological] [Thread] [Top]

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



Dear Bob,

I do not consider myself a real master of the subject, still I would like make some remarks.

Robert Boyer wrote:

possibly inconsistent set theory, or even on a possibly
dubious first order logic, whose semantics are
generally based on set theory.

Why you think that first order logic is dubious (PRA is a first order theory, isn't it?).

At least we know that first order logic is consistent.
It is true that the proof of consistency may be based on set theory (just consider formulae valid in one element model) but one can do without set theory. Just add to the theory a constant X and an axiom
      for x holds x = X
then eliminate quantifiers and the whole problem is reduced to the propositional calculus.

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

All the best,
Andrzej