= 27d567bc2d48d9f40e9ccc20ea370b15)
CronoDAS comments on No coinductive datatype of integers - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (138)
In first-order logic, if a statement is logically valid - is true in all models - then there exists a (finite) proof of that statement. Second-order logic, however, is incomplete; there is no proof system that can prove all logically valid second-order statements.
So if you can reduce something to first-order logic, that's a lot better than reducing it to second-order logic.
Well, now you are exhibiting the IMHO regrettable tendency that the more mathematical LWers exhibit of putting way too much focus on incompleteness uncomputability and other negative results that have negligible chance of actually manifesting unless you are specifically looking for pathological cases or negative results.
I use second-order logic all the time. Will work fine for this purpose.
Yeah, you're probably right...
I still do not see how first-order logic relates in any way to cousin_it's statement in grandparent of grandparent.
Just because second-order logic is incomplete does not mean we must restrict ourselves to first-order logic.
I think I recall reading somewhere that you only need first-order logic to define Turing machines and computer programs in general, which seems to suggest that "not expressible in first order logic" means "uncomputable"... I could just be really confused about this though...
Anyway, for some reason or other I had the impression that "not expressible in first order logic" is a property that might have something in common with "hard to explain to a machine".
ADDED. relates -> supports or helps to illuminate