FOM: 'Logical parsimony' of intuitionistic mathematics

[Torkel Franzen]

  Neil Tennant says:

  >By "logical parsimony" I meant simply that the deducibility relation of
  >the system in question was a sub-relation of the classical deducibility
  >relation. That's all!

  Yes, I was just being difficult, objecting to this terminology as
tendentious and misleading.

  >My parsimonious grandmother used to make all sorts of careful distinctions
  >between brown paper bags, and used Christmass wrappings, and rubber bands.
  >Each could serve very specific purposes when "recycled".

  The intuitionistic granny, however, collects a huge variety of
carefully labeled paper bags and rubber bands which neither she nor
anybody else can put to any use, although she cannily points out
that situations in which they would come in useful can be imagined.
For example, a certain type of rubber band is specifically intended
for jury-rigging a broken antenna in a visiting alien from outer space.

  William Tait remarks:

  >I'm not convinced of this. The constructive distinction between \exists 
  >and \neg \forall \neg, though these are equivalent,is important because 
  >the axiom of choice in the form
  >(*) \forall x \exists y A(x,y) \implies \exists F \forall x A(x, F(x))
  >is a consequence of the constructive meaning of the logical constants. 
  >But I would add that this conception of the logical constants is not 
  >wedded to the constructive conception of mathematics.

  I didn't mean to suggest that it is true of every intuitionistic
logical distinction that it corresponds to nothing in mathematical
knowledge or reasoning. On the contrary, a distinction between
constructive and non-constructive arguments and results is traditional
and important in mathematics. But intuitionistically we have to
distinguish between e.g. (x)(Ey)P(x,y) (P a primitive recursive
predicate, the quantifiers ranging over N), --(x)(Ey)P(x,y) and
(x)--(Ey)P(x,y) without having a single example of a P for which we
can prove (intuitionistically) one but not all of the three statements.

---
Torkel Franzen