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).
> 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.
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).