[...] but we have no guarantee at all that our formal system contains the full empirical or quasi-empirical stuff in which we are really interested and with which we dealt in the informal theory. There is no formal criterion as to the correctness of formalization.
ETA: When I first read this remark, I couldn’t decide whether it was terrifying, or just a very abstract specification of a deep technical problem. I currently think it’s both of those things.
Cox’s theorem seems to reduce the gap between the formal and the informal, by deriving probability theory from axioms that seem easier to informally assess.
Yes, and that is to me one of the main attractions of Bayesianism; but nevertheless, there is still a jump there between our informal considerations and formal means, and that ineradicable jump is what Perlis is talking about.
-- Imre Lakatos, “What Does a Mathematical Proof Prove?”
ETA: When I first read this remark, I couldn’t decide whether it was terrifying, or just a very abstract specification of a deep technical problem. I currently think it’s both of those things.
--Alan Perlis, Epigrams in Programming
Cox’s theorem seems to reduce the gap between the formal and the informal, by deriving probability theory from axioms that seem easier to informally assess.
Yes, and that is to me one of the main attractions of Bayesianism; but nevertheless, there is still a jump there between our informal considerations and formal means, and that ineradicable jump is what Perlis is talking about.
Link appears to be broken.
Fixed, thanks.