Skip to main content
Proof Assistants Beta

Return to Answer

corrected conservativity result
Source Link
François G. Dorais
François G. Dorais
  • 635
  • 3
  • 13

This is not possible because Lean's Prop is impredicative. Restricting to Type 0 is close but not exactly the same as working in ZFC.

For example, Con(ZFC) (formalized in a typical Gödelian manner) is an arithmetical proposition that only talks about Nat, which lives in Type 0. So this is within the scope of "restricting to Type 0".

It so happens that there is a model of ZFC that lives in Type 1. This means that Con(ZFC) must be true in Lean: there is no model of Lean where Con(ZFC) is false. But there is no way to tell that the truth of Con(ZFC) depends on the existence of some Type 1 object because Prop is impredicative.

As far as I can tell, Lean's type theory (with Choice) is conservative over ZFC + ∀n Con∪ {Con(ZFC + there are at least n inaccessibles) : n = 0,1,2,...} for arithmetical statements.

This is not possible because Lean's Prop is impredicative. Restricting to Type 0 is close but not exactly the same as working in ZFC.

For example, Con(ZFC) (formalized in a typical Gödelian manner) is an arithmetical proposition that only talks about Nat, which lives in Type 0. So this is within the scope of "restricting to Type 0".

It so happens that there is a model of ZFC that lives in Type 1. This means that Con(ZFC) must be true in Lean: there is no model of Lean where Con(ZFC) is false. But there is no way to tell that the truth of Con(ZFC) depends on the existence of some Type 1 object because Prop is impredicative.

As far as I can tell, Lean's type theory (with Choice) is conservative over ZFC + ∀n Con(ZFC + there are at least n inaccessibles) for arithmetical statements.

This is not possible because Lean's Prop is impredicative. Restricting to Type 0 is close but not exactly the same as working in ZFC.

For example, Con(ZFC) (formalized in a typical Gödelian manner) is an arithmetical proposition that only talks about Nat, which lives in Type 0. So this is within the scope of "restricting to Type 0".

It so happens that there is a model of ZFC that lives in Type 1. This means that Con(ZFC) must be true in Lean: there is no model of Lean where Con(ZFC) is false. But there is no way to tell that the truth of Con(ZFC) depends on the existence of some Type 1 object because Prop is impredicative.

As far as I can tell, Lean's type theory (with Choice) is conservative over ZFC ∪ {Con(ZFC + there are at least n inaccessibles) : n = 0,1,2,...} for arithmetical statements.

Source Link
François G. Dorais
François G. Dorais
  • 635
  • 3
  • 13

This is not possible because Lean's Prop is impredicative. Restricting to Type 0 is close but not exactly the same as working in ZFC.

For example, Con(ZFC) (formalized in a typical Gödelian manner) is an arithmetical proposition that only talks about Nat, which lives in Type 0. So this is within the scope of "restricting to Type 0".

It so happens that there is a model of ZFC that lives in Type 1. This means that Con(ZFC) must be true in Lean: there is no model of Lean where Con(ZFC) is false. But there is no way to tell that the truth of Con(ZFC) depends on the existence of some Type 1 object because Prop is impredicative.

As far as I can tell, Lean's type theory (with Choice) is conservative over ZFC + ∀n Con(ZFC + there are at least n inaccessibles) for arithmetical statements.