[Agda] Postulating double-negated consistent axioms without breaking canonicity?

[Andreas Abel]

On 26.05.11 11:27 AM, Nils Anders Danielsson wrote:
> On 2011-05-26 11:19, Andreas Abel wrote:
>> If you say that if all your axioms are negative, consistency implies
>> canonicity, I would find that plausible. Your axiom "em" still looks
>> ugly to me.
>
> Why? If I understood you correctly, then your irrelevant projections
> correspond to postulates without computational meaning. Do you consider
> this feature to be ugly as well?

Just because I find em in *Set*, be it double negated, funny.  Set is 
about computational stuff.  Currently, of course, there is no Prop in 
Agda, so there is little alternative for what you want to do.

Irrelevance is one way to separate computational content form proofs, 
Prop another.  Maybe the empty type is also a means to achieve this.  If 
we prove that we can erase terms of the empty type without altering 
reduction, we might be able to formally justify your approach.

>> As a research project, I suggest to try and add a classical,
>> impredicative, proof-irrelevant universe Prop to Agda. Maybe that would
>> allow you to do your stuff?
>
> The axiom Ulf suggested is apparently inconsistent in the presence of
> impredicativity, so I guess not. Furthermore I would postulate a
> universe-polymorphic version of the axiom.

I am not so sure about the inconsistency of impredicativity and 
classical logic in *Prop*, a universe of proof-irrelevant propositions. 
  At least, that would be new to me.

   http://coq.inria.fr/V8.1/faq.html#htoc38

says:

   31  What standard axioms are inconsistent with Coq?

   The axiom of unique choice together with classical logic (e.g. 
excluded-middle) are inconsistent in the variant of the Calculus of 
Inductive Constructions where Set is impredicative.

   As a consequence, the functional form of the axiom of choice and 
excluded-middle, or any form of the axiom of choice together with 
predicate extensionality are inconsistent in the Set-impredicative 
version of the Calculus of Inductive Constructions.

   The main purpose of the Set-predicative restriction of the Calculus 
of Inductive Constructions is precisely to accommodate these axioms 
which are quite standard in mathematical usage.

   The Set-predicative system is commonly considered consistent by 
interpreting it in a standard set-theoretic boolean model, even with 
classical logic, axiom of choice and predicate extensionality added.

So, the concern is only with impredicative Set, not with impredicative Prop.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/