[Prev][Next][Index][Thread]
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
ITALY
stefano@itoinfo.bitnet
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