4 ms·

Thank you so much for taking the time to reply. I now realized that I confused "syntactic" and "semantic" completeness. I agree on your points; my first up th

Thank you so much for taking the time to reply. I now realized that I confused "syntactic" and "semantic" completeness. I agree on your points; my first up there was ignoring a bit of the context (it was late...) and not meant to "motivate" the multitude of proof assistants by incompleteness theorem. As a programming language person, I am quite convinced there will never, ever be an agreement on a common formal language (even if there was or is agreement on foundations it should be based upon) - it is the same as for programming languages. This is more due to human nature rather than technical factors, and if we conceive logic as a linguistic activity, then we can see how foundations and the corresponding ergonomic language logic are related, maybe two sides of the same coin. "Foundations" in the context of mathematics appear (to me at least) as something technical and interchangeable. Is there a venue for discussions on logics like these outside of the occasional logic-related HN threads? : )

dwohnitmok 6y ago
> As a programming language person, I am quite convinced there will never, ever be an agreement on a common formal language (even if there was or is agreement on foundations it should be based upon) - it is the same as for programming languages. This is more due to human nature rather than technical factors, and if we conceive logic as a linguistic activity, then we can see how foundations and the corresponding ergonomic language logic are related, maybe two sides of the same coin. "Foundations" in the context of mathematics appear (to me at least) as something technical and interchangeable. I strongly agree. The formalization of mathematics bears strong resemblances to programming (and is in deep theoretical senses the same endeavor) so it would be hardly surprising for the same social phenomena to show up. As an aside I think the relationship between the halting problem and real-world programming languages is a good heuristic for the effect that Godel's incompleteness theorems have on formalization of mathematics (e.g. very little in programming language development is directly attributable to the halting problem and its existence doesn't spell the doom of programming, but it's always there in the background). > Is there a venue for discussions on logics like these outside of the occasional logic-related HN threads? : ) There's the Foundations of Mathematics (FOM) mailing list: https://cs.nyu.edu/mailman/listinfo/fom https://cs.nyu.edu/mailman/listinfo/fom, but it's geared towards cutting edge and very technical research rather than more layman discussions of the sort found on HN. Otherwise I don't know of one unfortunately.

dwohnitmok 6y ago

> As a programming language person, I am quite convinced there will never, ever be an agreement on a common formal language (even if there was or is agreement on foundations it should be based upon) - it is the same as for programming languages. This is more due to human nature rather than technical factors, and if we conceive logic as a linguistic activity, then we can see how foundations and the corresponding ergonomic language logic are related, maybe two sides of the same coin. "Foundations" in the context of mathematics appear (to me at least) as something technical and interchangeable. I strongly agree. The formalization of mathematics bears strong resemblances to programming (and is in deep theoretical senses the same endeavor) so it would be hardly surprising for the same social phenomena to show up. As an aside I think the relationship between the halting problem and real-world programming languages is a good heuristic for the effect that Godel's incompleteness theorems have on formalization of mathematics (e.g. very little in programming language development is directly attributable to the halting problem and its existence doesn't spell the doom of programming, but it's always there in the background). > Is there a venue for discussions on logics like these outside of the occasional logic-related HN threads? : ) There's the Foundations of Mathematics (FOM) mailing list: https://cs.nyu.edu/mailman/listinfo/fom https://cs.nyu.edu/mailman/listinfo/fom, but it's geared towards cutting edge and very technical research rather than more layman discussions of the sort found on HN. Otherwise I don't know of one unfortunately.