Logic - 2022-03-29

« first day (2050 days earlier) ← previous day next day → last day (1061 days later) »

user21820

14:27

in Discussion between user21820 and Trebor, 2 days ago, by user21820

@Trebor: Oh and here's an unrelated question: The author of this PDF on CIC said "Impredicative systems are powerful but also very fragile in the sense that impredicativity does not interact very well with other features leading rapidly to inconsistent systems.". Do you agree, or do you actually think there is absolutely nothing wrong with impredicative Prop?

in Discussion between user21820 and Trebor, 2 days ago, by Trebor

@user21820 Maybe there's something wrong. That's debatable. But there's nothing wrong to claim that impredicative Set and Prop is dangerous.

in Discussion between user21820 and Trebor, 2 days ago, by Trebor

Personally I am very slightly in favor of predicative Prop.

in Discussion between user21820 and Trebor, 22 hours ago, by user21820

@Trebor: I think I have a better understanding of the issue of impredicative Prop, and I'd like to tell you what I think and hear your view on it. I think whether or not there is a problem with impredicative Prop depends on what we intend it to mean. In the PDF on CIC that I had quoted above, it seems that they would like to interpret "Π(x:A) . B" as a 'finished' type, and so the rule ( ( Γ ⊢ A : Type[i] ) ; ( Γ , x : A ⊢ B : Prop ) ⊢ ( Γ ⊢ Π(x:A) . B : Prop ) ) is indeed problematic.

in Discussion between user21820 and Trebor, 22 hours ago, by user21820

In particular, if we imagine each universe as being constructed (by an abstract generative process) based on the lower universes, then we have to finish Prop before we can construct Type[1], but the impredicative rule essentially breaks that. In particular, if every type is intended to be some kind of collection/set, then "Π(x:A) . B" may never be finished if A = Type[1], simply because Type[1] may never be finished.

in Discussion between user21820 and Trebor, 22 hours ago, by user21820

To evade an outright problem, one might think of the universes as being generated not necessarily in order of their hierarchy. But then one must accept that any type T may never be finished at any point; its membership may never stabilize. This applies even if ( T : Prop ) simply because of the impredicative rule. This implies that we cannot view membership in T classically, and so LEM would be completely unjustifiable.

in Discussion between user21820 and Trebor, 21 hours ago, by user21820

So basically, impredicative Prop plus LEM would be as bad as the impredicativity in full ZFC, because the situation is analogous there where set membership is boolean and hence the cumulative hierarchy cannot be used to justify full specification or full replacement. However, this argument does not imply any problem with plain CoC with impredicative Prop, as long as one is careful to never view a type as a fixed collection.

in Discussion between user21820 and Trebor, 21 hours ago, by Trebor

Hmm I think that's about right. But I can't be sure for ZFC, because apart from beginner facts I don't know a lot.

in Discussion between user21820 and Trebor, 21 hours ago, by Trebor

Oh I think I do know what you mean. It's probably correct.

4 hours later…

user21820

18:39

A: What is the trade-off to accepting impredicative propositions?

I think this is mainly not a question about usability, but rather a form of discomfort so as to the foundational status of theories incorporating impredicativity. Indeed, as you mentioned, impredicativity greatly increases the logical power of your system. While this is a blessing when you are tr...

Q: Proof-theoretic comparison table?

I read this CSTheory SE post, which suggests that it is often not clear what variant of MLTT or CIC is being referred to. But I would like to know the proof-theoretic strengths of the various underlying foundational systems for more 'constructive' proof assistants such as Agda, Coq, Lean. For exa...