zwarich

After a long discussion on the Lean Zulip, Mario Carneiro has shown that the Calculus of Inductive Constructions (in its full version w/ large elimination of Acc) + Excluded Middle proves that ZF is consistent:
https://arxiv.org/abs/2609.23143
It is fairly simple to show that Aczel’s type of sets as well-founded trees is a model of ZF without Replacement, and even a bit further, that the iterative hierarchy V_alpha exists for all ordinals alpha, but Replacement seems very analogous to Unique Choice, and there is (as far as I am aware) no syntactic construction that can show the relative consistency of UC (or LEM) over CiC w/ large elimination of Acc.

Instead, the proof of consistency roughly proceeds by dichotomy on whether the image of a set by a functional relation is sufficiently bounded. If it is, the set can be constructed, thus establishing the Axiom of Replacement and the consistency of ZF; otherwise the ranks of the sets show that V_alpha for their limit alpha is already a model of ZF.

This is an amusing trick in that it answers the question in presence of LEM, but doesn’t shed any light on the relationship between Unique Choice and Replacement (or stronger type-theoretic choice principles and Collection).

I don't even eat dumplings anymore, I just buy into a dumpling REIT

After playing around with various attempts to construct models of ZF (or IZF) in the Calculus of Inductive Constructions, I can say that CiC (even with LEM) is severely deficient compared to ZF/IZF in terms of what can be done without assuming some form of Choice. I think that Lean's banishment of these problems by just assuming Choice throughout the ecosystem might be no small part of its appeal to mathematicians.

The latest Lean soundness hole (https://github.com/leanprover/lean4/issues/14576), which also affects alternative implementations of the kernel, is proof that God only ever intended for us to use W-types, and certainly not nested inductives.

I’ve seen a number of people speak about a representation of datatypes in ML where a datatype is given by a module with an abstract type and its constructors. Obviously, this is missing some additional information to define pattern matching, e.g. a recursor. Has anyone actually worked out all of the details?

we need to consider deceleration

@joe@f.duriansoftware.com @tjammer@mastodon.gamedev.place Mathematica had it right all along: use [] for function calls.

@joe@f.duriansoftware.com It cracked me up to learn that even Java has switch expressions now.

I think my current aesthetic preference is for every construct to work as an expression, and to treat blocks as a distinct form of expression that needs to end with a yield of a value rather than just implicitly returning the final value. Implicitly returning the last value imposes a lot of syntactic restrictions, especially when you're using the Fortress/Swift approach for reducing the need for semicolons.

@joe@f.duriansoftware.com Is there another way to support both relative enum .constructor(...) syntax and Swift-style semicolon avoidance while implicitly returning the last expression? That was the main constraint forcing me to have some sort of marker keyword for the last expression.

@joe@f.duriansoftware.com I also thought of that, but if you have two separate projection operators in your language (which is an acceptable choice) then :: would probably have the same problem as .. I guess you could do it without having :: as a "static" projection operator, but it would be a bit weird.

I think Rust is still debating whether to support _::Constructor(...), along with companion _ { ... } instead of Struct { ... }. I don't think they could make ::Constructor(...) work because of the extern prelude. I think I also saw someone who wanted Zig's .{ ... } for structs.

@joe@f.duriansoftware.com What syntax were you proposing, do { ... } or something else?