[loicd]

> That doesn’t mean “X is valid”; if something follows from the axioms of set theory then it holds in all models of set theory

Yes, I was being elliptic. That should read "X is valid in set theory". The point being that it is a notion of validity (ie valid in all models of set theory) rather than a notion of satisfiability (ie valid in a particular model of set theory).

[denotational]

For some reason the "reply" buttons past a certain level of nesting were missing for me, but that appears no longer to be the case, so I'm moving a previous comment here

The notion of relative validity is just semantic entailment, no? I have never seen that referred to in terms of validity, which has been reserved strictly for formulae that are true in all models, not in some class of models.

I’m a Platonist, and I suspect most mathematicians fall towards that end of the spectrum, so I disagree that most Mathematicians see ZFC as the arbiter of truth. They certainly aren’t doing formal proofs in ZFC, and in fact I suspect that most non-logician mathematicians would have difficulty reciting the axioms of ZFC.

That’s not to say I don’t appreciate proof theory and the desire to work in an axiomatic framework, indeed in a past life I spent most of my time formalising various things in Coq, but I don’t think it’s relevant to fundamental mathematical truth, which I believe exists outside of axiomatisation (and I think most mathematicians would agree).

[Timon3]

> For some reason the "reply" buttons past a certain level of nesting were missing for me, but that appears no longer to be the case, so I'm moving a previous comment here

If I understand correctly, HN throttles reply speed by hiding the reply button for some time after a comment was posted. The deeper the thread the longer this timeout gets.