It doesn't seem odd at all, we have an expectation of the calculator, and if it fails to fulfill that expectation then we start to doubt that it is, in fact, what we thought it was (a working calculator).
Except that if you examine the workings of a calculator that does agree with us, you're much much less likely to find a wiring fault (that is, that it's implementing a different algorithm).
if (a) [a reasonable human would agree implements arithmetic] and (b) [which disagrees with us on whether 2+2 equals 4] both hold, then (c) [The human decides she ve was mistaken and needs to fix the machine]. If the human can alter the machine so as to make it agree with 2+2 = 4, then and only then will the human feel justified in asserting that it implements arithmetic.
If the only value for which the machine disagrees with us is 2+2, and the human adds a trap to detect the case "Has been asked 2+2", which overrides the usual algorithm and just outputs 4... would the human then claim they'd "made it implement arithmetic"? I don't think so.
I'll try a different tack: an implementation of arithmetic can be created which is general and compact (in a Solomonoff sense) - we are able to make calculators rather than Artificial Arithmeticians. Clearly not all concepts can be compressed in this manner, by a counting argument. So there is a fact-of-the-matter that "these {foo} are the concepts which can be compressed by thus-and-such algorithm" (For instance, arithmetic on integers up to N can be formalised in O(log N) bits, which grows strictly slower than O(N); thus integer arithmetic is compressed by positional numeral systems). That fact-of-the-matter would still be true if there were no humans around to implement arithmetic, and it would still be true in Ancient Rome where they haven't heard of positional numeral systems (though their system still beats the Artificial Arithmetician).
I'll look over it, but given what you say here I'm not confident that it won't be an attempt at a resurrection of Platonism.
What's wrong with resurrecting (or rather, reformulating) Platonism? Although, it's more a Platonic Formalism than straight Platonism.
If the only value for which the machine disagrees with us is 2+2, and the human adds a trap to detect the case "Has been asked 2+2", which overrides the usual algorithm and just outputs 4... would the human then claim they'd "made it implement arithmetic"? I don't think so.
Well, this seems a bit unclear. We are operating under the assumption that the set up looks very similar to a correct set up, close enough to fool a reasonable expert. So while the previous fault would cause some consternation and force the expert to lower his pr...
I've mentioned in comments a couple of times that I don't consider formal systems to talk about themselves, and that consequently Gödelian problems are irrelevant. So what am I actually on about?
It's generally accepted in mathematical logic that a formal system which embodies Peano Arithmetic (PA) is able to talk about itself, by means of Gödel numberings; statements and proofs within the system can be represented as positive integers, at which point "X is a valid proof in the system" becomes equivalent to an arithmetical statement about #X, the Gödel number representing X. This is then diagonalised to produce the Gödel sentence (roughly, g="There is no proof X such that the last line of X is g", and incompleteness follows. We can also do things like defining □ ("box") as the function from S to "There is a proof X in PA whose last line is S" (intuitively, □S says "S is provable in PA"). This then also lets us define the Löb sentence, and many other interesting things.
But how do we know that □S ⇔ there is a proof of S in PA? Only by applying some meta-theory. And how do we know that statements reached in the meta-theory of the form "thus-and-such is true of PA" are true of PA? Only by applying a meta-meta-theory. There is no a-priori justification for the claim that "A formal system is in principle capable of talking about other formal systems", which claim is used by the proof that PA can talk about itself. (If I remember correctly, to prove that □ does what we think it does, we have to appeal to second-order arithmetic; and how do we know second-order arithmetic applies to PA? Either by invoking third-order arithmetic to analyse second-order arithmetic, or by recourse to an informal system.)
Note also that the above is not a strange loop through the meta-level; we justify our claims about arithmeticn by appeal to arithmeticn+1, which is a separate thing; we never find ourselves back at arithmeticn.
Thus the claim that formal systems can talk about themselves involves ill-founded recursion, what is sometimes called a "skyhook". While it may be a theorem of second-order arithmetic that "the strengthened finite Ramsey theorem is unprovable in PA", one cannot conclude from second-order arithmetic alone that the "PA" in that statement refers to PA. It is however provable in third-order arithmetic that "What second-order arithmetic calls "PA" is PA", but that hasn't gained us much - it only tells us that second- and third-order arithmetic call the same thing "PA", it doesn't tell us whether this "PA" is PA. Induct on the arithmetic hierarchy to reach the obvious conclusion. (Though note that none of this prevents the Paris-Harrington Theorem from being a theorem of n-th order arithmetic ∀n≥2)
What, then, is the motivation for the above? Well, it is a basic principle of my philosophy that the only objects that are real (in a Platonic sense) are formal systems (or rather, syntaxes). That is to say, my ontology is the
setclass of formal systems. (This is not incompatible with the apparent reality of a physical universe; if this isn't obvious, I'll explain why in another post.) But if we allow these systems to have semantics, that is, we claim that there is such a thing as a "true statement", we start to have problems with completeness and consistency (namely, that we can't achieve the one and we can't prove the other, assuming PA). Tarski's undefinability theorem protects us from having to deal with systems which talk about truth in themselves (because they are necessarily inconsistent, assuming some basic properties), but if systems can talk about each other, and if systems can talk about provability within themselves (that is, if analogues to the □ function can be constructed), then nasty Gödelian things end up happening (most of which are, to a Platonist mathematician, deeply unsatisfying).So instead we restrict the ontology to syntactic systems devoid of any semantics; the statement ""Foo" is true" is meaningless. There is a fact-of-the-matter as to whether a given statement can be reached in a given formal system, but that fact-of-the-matter cannot be meaningfully talked about in any formal system. This is a remarkably bare ontology (some consider it excessively so), but is at no risk from contradiction, inconsistency or paradox. For, what is "P∧¬P" but another, syntactic, sentence? Of course, applying a system which proves "P∧¬P" to the 'real world' is likely to be problematic, but the paradox or the inconsistency lies in the application of the system, and does not inhere in the system itself.
EDIT: I am actually aiming to get somewhere with this, it's not just for its own sake (although the ontological and epistemological status of mathematics is worth caring about for its own sake). In particular I want to set up a framework that lets me talk about Eliezer's "infinite set atheism", because I think he's asking a wrong question.
Followed up by: The Apparent Reality of Physics