= 27d567bc2d48d9f40e9ccc20ea370b15)
Also, of course, to put this in the context of the original post, if we're talking about second order logic, then of course there can be no automated proof-checkers.
You appear to be confused here. The rest of your post is good.
In response to
comment
by
on
[LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing"
In response to
comment
by
on
[LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing"
I should have said this more carefully. If one allows enough rules of inference so that all the logical consequences of the axioms can be proved, then there are no automated proof checkers. So you can have proof checkers, but only at the cost of restricting the system so that not all logical consequences (i.e. implications that are true in every model) can be proved.
In response to
comment
by
on
[LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing"
Why do you imagine that the introduction of an axiomatic system would address this problem?
Because then the problem is not "Does this non-axiomatized stuff obey that theorem ?" but "Does that theorem follow from these axioms ?". One is a pure logic problem, and proofs may be checked by automated proof-checkers. The other directly or indirectly relies on the mathematician's intuition of the non-axiomatized subject in question, and can't be checked by automated proof-checkers.
In response to
comment
by
on
[LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing"
Because then the problem is not "Does this non-axiomatized stuff obey that theorem ?" but "Does that theorem follow from these axioms ?". One is a pure logic problem, and proofs may be checked by automated proof-checkers. The other directly or indirectly relies on the mathematician's intuition of the non-axiomatized subject in question, and can't be checked by automated proof-checkers.
Except insofar as the mathematicians, unknown to each other, have different ideas of what constitutes a valid rule of inference.
A logical system is a mathematical obect. If the problem is that different mathematicians might think they're talking about the same object when they're really talking about different ones, then I don't see why logical systems, out of all mathematical objects, should be particularly exempt from this problem.
Also, of course, to put this in the context of the original post, if we're talking about second order logic, then of course there can be no automated proof-checkers.
In response to
[LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing"
mathematicians from Pythagoras through Dedekind had absolutely no problem talking about numbers in the absence of the Peano axioms.
So, they were lucky. It could have been that that-which-Pythagoras-calls-number was not that-which-Fibonacci-calls-numbers.
Are there absolutely no examples of cases where mathematicians disagreed about some theorem about some not-yet-axiomatized subject, and then it turns out the disagreement was because they were actually talking about different things?
(I know of no such examples, but I would be surprised it none exist)
In response to
comment
by
on
[LINK] Steven Landsburg "Accounting for Numbers" - response to EY's "Logical Pinpointing"
Plasmon:
<i>So, they were lucky. It could have been that that-which-Pythagoras-calls-number was not that-which-Fibonacci-calls-numbers.</i>
Why do you imagine that the introduction of an axiomatic system would address this problem?
In response to
Logical Pinpointing
Thanks for posting this. My intended comments got pretty long, so I converted them to a blog post <a href="http://www.thebigquestions.com/2012/11/14/accounting-for-numbers/">here</a>. The gist is that I don't think you've solved the problem, partly because second order logic is not logic (as explained in my post) and partly because you are relying on a theorem (that second order Peano arithmetic has a unique model) which relies on set theory, so you have "solved" the problem of what it means for numbers to be "out there" only by reducing it to the question of what it means for sets to be "out there", which is, if anything, a greater mystery.
= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
= f037147d6e6c911a85753b9abdedda8d){kind=logo}
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.)