= 27d567bc2d48d9f40e9ccc20ea370b15)
JoshuaZ comments on [LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing" - Less Wrong Discussion
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)
Comments (46)
I think there's a definitional issue here. Eugine is using "proof checker" to mean an algorithm that given a sequence of statements in an axiomatic system verifies that the proof is formally valid. You seem to mean by proof checker something like a process that goes through listing all valid statements in the system along with a proof of the statement.
JoshuaZ: No, I mean the former. The problem is that you have enough rules of inference to allow you to extract all logical consequences of your axioms, then that set of rules of inference is going to be too complicated to explain to any computer. (i.e. the rules of inference are non-recursive.)
Isn't that more a consequence of the stronger statement that you just can't write down all valid inferences in the second-order system?