In the discussions following Landon's Guest Post @» Butterflies and Wheels (on the value in philosophical training) there is an exchange between Landon and Harald Hanche-Olsen on the question of whether Logic is a branch of Philosophy or Mathematics. I make no claim on logic per se, but the Boolean Algebra which models its basics is a branch of mathematics and that relatively trivial bit is all that has relevance to computers - which is what Landon was on about, but that is not what I want to look at here.
Further down in that exchange the question of Godel's proofs came up (though that definitely has nothing to do with real computers!) and Landon made some claims that I had to dispute. (In particular he denied the relevance of the well known restriction to systems which include a model for the natural numbers). This led me to revisit the little book by Nagel and Newman - and actually there is still a gap in my understanding. On page 78 N&N show how the statement that formula x is a leading part of formula y corresponds to the Godel number for x being a factor in that for y. So far so good, but on page 79 they assert that there is a similar but more complicated arithmetic characterization of the statement that number z is the Godel number for a proof of the statement with Godel number x. This seems quite plausible but I have never checked it. It could be considered an 'exercise' but it might be a hard one to actually carry out in detail. But that's not the issue I want to address here either.
In order to point out the silliness of claiming that the restriction to systems which include the natural numbers is irrelevant it is of course necessary to identify a mathematical system which does not include them. Simple Boolean Algebra is one - whose consistency is in fact provable. But given Landon's position, that might not be an effective example. Other algebraic structures naturally come to mind - except for the awkwardness that they are often (though probably not essentially so) set up in terms of a "set" of objects and so it might look at least superficially as if the axioms therefore presuppose those of ZF set theory which does include a model of the natural numbers (and on to just about everything else). Then I thought "aha the existence of Finite Geometries must show that the Euclidean axioms don't imply the ability to construct a full model of the Natural numbers". But fortunately I checked before posting and noted that only the incidence axioms were listed - which is fine for my purposes but raises the question of whether the standard Euclidean geometry could have been used as an example. If I had thrown out my first thought there, it would not have taken an expert to see that I was wrong (or at least hadn't thought carefully enough about which of the often not clearly itemized axioms I was referring to). Anyone with even the slightest familiarity with high school Euclidean Geometry could have said "But Euclidean geometry allows you to construct the mid-point between any two points, and if you then construct the mid-point between that and one of the first two, and so on then don't you get an infinite sequence of distinct points which could be identified with the ordinal numbers?" and I would have had to stop and think about what goes into that mid-point construction which has been left out of the axioms in terms of which finite models do exist.
In mathematics, and actually I suspect in other disciplines as well, it is often newcomers who make the major advances because those new to the field are less encumbered by either repeatedly reinforced preconceptions or masses of irrelevant detail. If I can be excused a bit of a play on words: they may be expert but they are not yet experts.