Stream: Miscellaneous

Topic: Why is UIP not a lemma

walker (Dec 12 2022 at 15:04):

when we say that x: nat We know for sure that x can only be either O or S x' where x' is another nat, that is because nat has two constructors, and we simply do case analysis on both cases

Why cannot we say thing for identity type and say there is only one case and thus prove UIP ?

Goal forall A (x y :A) (p1 p2 : x = y), p1 = p2.
Proof.
destruct p1.
Fail destruct p2.
(* Cannot instantiate metavariable P of type "forall a : A, x = a -> Prop" with
abstraction "fun (x : A) (p2 : x = x) => eq_refl = p2" of incompatible type
"forall x : A, x = x -> Prop".
*)

That should have worked and I fail to understand what is the problem!

Gaëtan Gilbert (Dec 12 2022 at 15:56):

instead of tactics try to write the match terms out, with full return annotations

Paolo Giarrusso (Dec 12 2022 at 16:21):

Note that UIP _is_ provable for nat — in fact, for any type with decidable equality

Paolo Giarrusso (Dec 12 2022 at 16:23):

and that general statement is called Hedberg's theorem

Paolo Giarrusso (Dec 12 2022 at 16:23):

I've never learned to _write_ that proof (for nat or in general), but both stdlib and stdpp have proofs of this idea (with different packagings)

Pierre-Marie Pédrot (Dec 12 2022 at 16:24):

the proof of Hedberg's theorem is not that hard, basically you rectify the wrong equality in the return clause

Pierre-Marie Pédrot (Dec 12 2022 at 16:27):

you have a way to produce a canonical inhabitant of equality from any proof of equality.

Paolo Giarrusso (Dec 12 2022 at 16:27):

stdlib's statement is UIP_dec (in theories/Logic/Eqdep_dec.v), stdpp's statement is eq_pi (stdpp/stdpp/proof_irrel.v)

Li-yao (Dec 12 2022 at 18:11):

Besides becoming an expert in dependent pattern-matching to convince yourself that you can't do it, note that it took until 1996 to confirm UIP isn't derivable, so it's no wonder it's not that obvious https://ncatlab.org/nlab/files/HofmannStreicherGroupoidInterpretation.pdf

Paolo Giarrusso (Dec 12 2022 at 18:26):

I'm sure @Li-yao knows, but understanding dependent pattern matching (and any syntactic reasoning) only explains why _this proof_ (or similar?) won't work — UIP is indepedent, so Hofmann and Streicher needed a countermodel to UIP

Li-yao (Dec 12 2022 at 18:42):

Is there no hope for a purely syntactic proof?

Paolo Giarrusso (Dec 12 2022 at 19:30):

I googled "syntactic independence proofs" and learned that at least one exists: https://dpt-info.di.unistra.fr/~narboux/slides/Herbrand-Euclid-vulgarization.pdf. Slide 9 has a toy example, but I didn't get through the real thing yet (work calls)

Stefan Monnier (Dec 12 2022 at 19:56):

Can't we do something like what Boulier et al. did in their "next 700 models" paper: define a new Eq type whose refl constructor carries an additional dummy Boolean, and then define the usual/normal constructor and eliminator on top of it?

Paolo Giarrusso (Dec 12 2022 at 20:23):

that's still a (syntactic) model, but I imagine it could work

Li-yao (Dec 12 2022 at 20:43):

That seems to be what's happening in the proof of Theorem 5.1 of Hofmann&Streicher.

Gaëtan Gilbert (Dec 12 2022 at 21:42):

since equality of nats has uip, enriching every Eq with a bool can't work I think

Pierre-Marie Pédrot (Dec 12 2022 at 23:47):

^ this. You need to preserve this additional structure everywhere, so it's very non-trivial (if doable).

Pierre-Marie Pédrot (Dec 12 2022 at 23:50):

I am not aware of a syntactic model of MLTT with one universe + ¬ UIP, i.e. one where we interpret conversion as some decidable conversion in a target type theory, and it looks very hard to do.

Pierre-Marie Pédrot (Dec 12 2022 at 23:50):

even doing a groupoid model is going to break the definitional J rule for refl.

walker (Dec 13 2022 at 14:14):

Gaëtan Gilbert said:

instead of tactics try to write the match terms out, with full return annotations

I guess this is even more reason to learn the match .. with...

Gaëtan Gilbert (Dec 13 2022 at 14:48):

you can also try to write it using

Definition eq_match {A:Type} (x:A) (P : forall y, x = y -> Type)
  (v:P x eq_refl)
  y
  (e:x = y)
  : P y e
  := match e with eq_refl => v end.

which provides the full power of matching on eq (the autogenerated eq_rect is not dependent enough because of a generation heuristic when the inductive is Prop)

Xuanrui Qi (Dec 15 2022 at 05:56):

I don't think you can prove independence results syntactically, but I'm not an expert either

Pierre-Marie Pédrot (Dec 15 2022 at 11:23):

Indeed you can, that's the whole point of syntactic models.

Paolo Giarrusso (Dec 15 2022 at 13:40):

Beyond syntactic models — which _are_ models — I linked earlier a pure proof-theoretic approach — that is, one that does _not_ construct a model (https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Why.20is.20UIP.20not.20a.20lemma/near/315443781). I point this out because, like @Xuanrui Qi , I didn't know this was possible.

Pierre-Marie Pédrot (Dec 15 2022 at 13:41):

For this kind of results to hold, you still need some form of cut elimination / strong normalization, and for this you will never escape from a model somewhere.

Paolo Giarrusso (Dec 15 2022 at 13:45):

Good point: "there exists an unprovable statement in X" implies "X is consistent". And if your theory extends PA, a consistency proof can't be formalizable purely in PA — so it can't be _purely_ proof-theoretic/syntactic.

Paolo Giarrusso (Dec 15 2022 at 13:46):

Right? And logical relations and syntactic models escape that by exceeding PA

Paolo Giarrusso (Dec 15 2022 at 13:49):

But I haven't studied this "properly" — I learned this point about PA from "Proofs and Types", but I might miss something. And whether "syntactic proofs" implies "formalizable in PA" (or even PRA?) is super-hazy

Pierre-Marie Pédrot (Dec 15 2022 at 13:50):

I'm not sure what you mean, but ultimately everything is syntactic. Semantics is just the syntax in the meta-theory. The point about syntactic models is that they are better behaved as they lower the requirement of the expressivity of the meta by becoming a relative proof of consistency (or whatever).

Pierre-Marie Pédrot (Dec 15 2022 at 13:51):

It's very easy to reach confusing situations in this kind of discussion, since the very notion of "syntactic" is just like "truth", it's not absolute but relative to some ambient theory.

Paolo Giarrusso (Dec 15 2022 at 15:10):

I agree it's relative, so for this discussion I can choose the ambient metatheory to be about a (Platonist?) world with genuinely uncountable objects.

Paolo Giarrusso (Dec 15 2022 at 15:11):

people are free to choose strict finitism/formalism, but that's philosophy outside the maths: for the actual maths I prefer things that people can agree regardless of their philosophy.

Paolo Giarrusso (Dec 15 2022 at 15:13):

Regardless, "you can/cannot construct a syntactic model using only PA" should be a precise question?

Paolo Giarrusso (Dec 15 2022 at 15:14):

(I confess I've never learned how "syntactic" proof theory can be carried out in PA, but finitists seem adamant they did).

Patrick Nicodemus (Dec 15 2022 at 16:09):

Pierre-Marie Pédrot said:

For this kind of results to hold, you still need some form of cut elimination / strong normalization, and for this you will never escape from a model somewhere.

What do you mean by this? I would say the opposite. To me, ordinal analysis is relatively far from model theory.

Paolo Giarrusso (Dec 15 2022 at 19:53):

And ordinal analysis hasn't been brought up. EDIT: I was wrong here

Paolo Giarrusso (Dec 15 2022 at 19:54):

more helpfully: at least as I understand from Wikipedia, Coq's infinitely more powerful than the systems ordinal analysis studies — so we don't know "how infinitely"

Paolo Giarrusso (Dec 15 2022 at 19:56):

I'm not an expert, but that's what I gather from

Most theories capable of describing the power set of the natural numbers have proof-theoretic ordinals that are so large that no explicit combinatorial description has yet been given.

and from the fact that Coq can go quite a bit beyond nat -> Prop
https://en.wikipedia.org/wiki/Ordinal_analysis#Theories_with_larger_proof-theoretic_ordinals

Paolo Giarrusso (Dec 15 2022 at 19:59):

back to the topic, most proofs of strong normalization proceed by logical relations (or one of the twenty other names for it), which are ways to construct models. For systems powerful enough (like System F, and even more so for Coq), we can _prove_ that pure proof theory (anything formalizable in PA) isn't sufficient: I think System T is already too powerful.

Paolo Giarrusso (Dec 15 2022 at 20:00):

(technically, logical relations are often built on operational semantics for term reduction — but the logical relation remains rather semantic)

Paolo Giarrusso (Dec 15 2022 at 20:02):

but corrections welcome — I understand the "logical relations" part much better than the ordinal analysis part

Paolo Giarrusso (Dec 15 2022 at 20:15):

looking at https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof I owe @Patrick Nicodemus an apology for my comment. It's fair to say that some cut elimination proofs involve ordinal analysis, but I think the ones we are discussing do not.

Paolo Giarrusso (Dec 15 2022 at 20:17):

to prove consistency of System F's impredicativity, for instance, instead of using a different system, we map object-language impredicativity to meta-language impredicativity (tho in some proofs you can use a slightly weaker form).

Patrick Nicodemus (Dec 15 2022 at 20:40):

Paolo Giarrusso said:

(I confess I've never learned how "syntactic" proof theory can be carried out in PA, but finitists seem adamant they did).

Gentzen's proof is something like: we define a linear ordering "<_C" on natural numbers, C for "complexity" which we, working outside the formalism, can "easily see" is an embedding of a certain countable ordinal into N. Then we associate to each proof a measure of its complexity which is an element of this ordinal. We prove that all the various reductions strictly reduce the complexity, so that a sequence of reductions of a proof term gives a sequence of decreasing elements of the ordinal. Since the ordinal is well founded, the sequence of reductions must eventually terminate.

All of this coding, and the proof that the translation from (terms, $<_{\beta,\eta,\dots}$) into $(\mathbb{N}, <_C)$ is an order homomorphism, can be done in primitive recursive arithmetic. That is what finitists mean by saying it is a finitistic proof of consistency. However, one cannot prove in PA that the embedded ordinal is actually well-founded. More specifically, for any definable binary relation $R$ on $\mathbb{N}$ one can formulate the accessibility predicate $Acc_R(n)$ and then ask if all natural numbers are accessible, or all natural numbers $n$ such that $R(n,m)$ for some fixed $m$ (so an initial segment of the ordering), and for our 'ordinal' we cannot prove this. Thus, this is where incompleteness rears its head.

So it is a finitistic proof except that one needs an extremely strong induction principle to carry it out.

Paolo Giarrusso (Dec 15 2022 at 21:31):

I've often wondered how that principle compares with structural induction on PA_ω proof trees — those are infinitely branching trees, so structural induction on them is transfinite

Paolo Giarrusso (Dec 15 2022 at 23:54):

see e.g. http://lists.seas.upenn.edu/pipermail/types-list/2018/001985.html.

structural induction is, in a precise sense, equivalent to ordinal induction

also https://www.cs.bham.ac.uk/~mhe/papers/ordinals/ordinals.html#8626 seems to encode ε₀ using

data B : Set where
 Z : B
 S : B → B
 L : (ℕ → B) → B

where L makes this an infinitely branching node, similarly to what we see in PA_ω

Paolo Giarrusso (Dec 15 2022 at 23:54):

either way, thanks for the explanation!

Last updated: Jun 05 2023 at 09:01 UTC