Excluded middle w/o definite descriptions in theory of constructions

Date: Wed Oct 17 14:26:02 GMT+0100 1990

  Berardi Stefano
  Dipartimento di Informatica
  Universita' di Torino
  Pier della Francesca, Corso Svizzera 185, Torino
  Recently, J. P. Seldin posted in type net a paper about the consistency
  of an extension of Pure Construction Calculus. In this paper, J. Seldin
  extends the syntactic proof of :
  "Intuitionistic (Higher Order) Logic strongly normalizes =>
   Classical (Higher Order) Arithmetic is consistent"

  to a proof of a more complex statement :

  "Pure Construction Calculus strongly normalizes =>
   Classical Arithmetic is consistent with Construction Calculus"
  Seldin concludes that Excluded Middle, in P.C.C., does not imply proof
  irrelevance (all types have at most one element), since it would imply
  0 = 1, which is inconsistent with Arithmetic.
  Seldin's result, however, is interesting in itself. It shows one possible way
  to extend Pure Construction Calculus to a theory strong enough to deduce all
  interesting mathematical statement :
  a theory (P.C.C. + Classical Arithmetic) we could use as a base  for
  automatic proof-checking.

  I would like to contribute to the discussion on such topic, briefly
  introducing a semantic proof of the same result I announced at last Jumelage
  Meeting at Edimburgh.
  In such Meeting I introduced a family of models for PCC, which I called "Type
  Irrelevance Models", which satisfy the following  axioms :
  - Extensionality (both for function-types and function-terms);
  - Excluded Middle;
  - Infinite axioms (all Peano Axioms but Induction);

  I could add, now, that in such strange models Induction is false :
  you may find a polymorphic integer x : Int which is not a natural
  number, i.e. not of the form {0, S0, SS0, SSS0, ...}
  and moreover definite descriptions are false, i.e. :
  there are A, B : Prop and R : A -> B -> Prop, such that
   "for all a : A there is a unique b : B such that R(a,b)"
   is true, but
   "there is an f : A -> B, such that, for all a : A, we have R(a,f(a))"
   is false

  (as also Seldin remarks, Induction is useful but not strictly needed,
   since we may bound a quantification on Int to those integer which are
   natural numbers, i.e. in {0, S0, SS0, SSS0, ...})

  The existence of such family of models implies the consistency of :
  P.C.C. + Classical Arithmetic + Extensionality axioms + negations of
  Induction and definite descriptions.

  Roughly speaking a "Type irrelevance" model is defined from any extensional
  lambda model M, by interpreting an inhabited proposition as M and a non
  inhabited proposition as the empty set. A proposition "for all a in A, B(a)"
  is interpreted as M iff either B(a) is M, for all a in M, or A is empty.
  Thus, Prop becomes a two-element set, {empty set, M}.
  The other elements of Type are interpreted set-theorically as function spaces
  (with domain either M, or another element of Type).
  The proofs are interpreted by erasing every type information in them, and
  then interpreting the resulting untyped term in M.
  The relation a : A is interpreted set-theorically as "a is an element of A".
  Remark that, if A : Prop, then a : A implies that A is (interpreted as) M.

  Since we have only two possible values for a propositions, corresponding
  to the truth values true and false, Excluded Middle comes for free.
  Extensionality holds for a function type since the model is set-theorical,
  and for a function term since M is extensional.
  The Infinite axioms are equivalent, in PCC, at the fact "there is some type
  with at least two elements". This latter fact holds because M is a type,
  and it has at least two elements.
  The negations of Induction and definite descriptions come by a cardinality
  argument, after an easy analysis of the model.

  A "Type Irrelevance" model defines a maximal consistent extension of PCC,
  a theory which is much on the line of Classical (extensional) Mathematic,
  but still have some pathologies (it is not difficult to show that, for each
  A : Prop, each f : A -> A has a fixed point).
  They are not the only interesting maximal consistent extensions of PCC.
  For instance, we might extend PCC with Predicative (in Prop only) Strong
  Sums, Infinite axioms and Induction. We may find a maximal consistent
  extension of such theory using the Partial Equivalence Relation Model
  built on the untyped term model.
  In such a model, of course, both Excluded Middle and Extensionality for
  function types are false.
  This theory is very far from usual Mathematics, still it is closer than
  the previous one to Martin-Lof ideas, and could be an alternative
  Logical Framework to mechanize proof-checking.
  I have no definitive opinion about the right way to use PCC as Logical
  Framework, and any suggestion about it would be very welcome.
                                        Torino, 8 Ottobre 1990
                                        Stefano Berardi