@LinearChristmas agree on vdash

@LinearChristmas I don't know if I've ever heard that about replacement, but it doesn't seem immediately implausible and I agree that it wouldn't be enough.

@LinearChristmas Sure, it's true that we aren't in general guaranteed a satisfaction predicate for proper classes (and that we never have one for V). My point was just that your worry about reflection is implicitly premised on the soundness theorem, which wouldn't make a whole lot of sense if there weren't a way to formalize satisfaction.

I guess, more to the point, at least in ZFC, there's no way to talk about proper classes, so a binary "is a model of" is out of the question right away. What we could maybe hope for (but can't have), is that for each proper class C, there is a formula $F_C(x)$ that expresses "x is a sentence and C satisfies x." That's what I mean by a satisfaction predicate for a proper class in the previous.