Ok, right. I think I didn't fully appreciate your point before. So the fact that a particular many-sorted first-order logic with extra axioms is proof-theoretically equivalent to (a given proof system for) 2nd-order logic should make me stop asking whether we should build machines with one or the other, and start asking instead whether the many-sorted logic with extra axioms is any better than plain first-order logic (to which the answer appears to be yes, based on our admittedly 2nd-order reasoning). Right?

It seems to me like this discussion has gotten too far into either/or "winning". The prevalance of encodings in mathematics and logic (e.g. encoding the concept of pairing in set theory by defining (a, b) to be the set {{a}, {a, b}}, the double negation encoding of classical logic inside intuitionist logic, et cetera) means that the things we point to as "foundations" such as the ZF axioms for set theory are not actually foundational, in the sense of necessary and supporting. ZF is one possible system which is sufficiently strong to encode the things that we want to do. There are many other systems which are also sufficiently strong, and getting multiple perspectives on a topic by starting from different alternative "foundations" is probably a good thing. You do not have to choose just one!

Another way to look at it is - the things that we call foundations of mathematics are like the Planck length - yes, according to our current best theory, that's the smallest, most basic element. However, that doesn't mean it is stable; rather, it's cutting edge (admittedly, Planck length is more at the cutting edge of physics than foundations of mathematics are at a cutting edge of mathematics). The stable things are more like cubits and inches - central, human-scale "theorems" such that if a new alternative foundation of mathematics contradicted them, we would throw away the foundation rather than the theorem. Some candidate "cubit" or "inch" theorems (really, arguments) might be the infinitude of primes, or the irrationality of the square root of 2.

Friedman and Simpson have a program of "Reverse Mathematics", studying in what way facts that we normally think of as theorems, like the Heine-Borel theorem, pin down things that we normally think of as logic axioms, such as induction schemas. I really think that Simpson's paper "Partial Realizations of Hilbert's Program" is insightful and helpful to this discussion: http://www.math.psu.edu/simpson/papers/hilbert.ps

Lakatos's "Proofs and Refutations" is also helpful, explaining in what sense a flawed and/or informal argument is helpful - Note that Lakatos calls arguments proofs, even when they're flawed and/or informal, implicitly suggesting that everyone calls their arguments proofs until the flaws are pointed out. I understand he retreated from that philosophical position later in life, but that pre-retreat philosophical position might still be tenable.

I think I agree. This gives me the feeling that every time the discussion revolves around models, it is getting off the point. We can touch proof systems. We can't touch models.

We can say that models are part of our pebblecraft...

The question, though, is whether we should trust particular parts of our pebblecraft. Should we prefer to work with first-order logic, or 2nd-order logic? Should we believe in such a thing as a standard model of the natural numbers? Should we trust proofs which make use of those concepts?

This and previous articles in this series emphasize attaching meaning to sequences of symbols via discussion and gesturing toward models. That strategy doesn't seem compatible with your article regarding sheep and pebbles. Isn't there a way to connect sequences of symbols to sheep (and food and similar real-world consequences) directly via a discipline of "symbolcraft"?

I thought pebblecraft was an excellent description of how finitists and formalists think about confusing concepts like uncountability or actual infinity: Writing down "... is uncountably infinite ..." is part of our pebblecraft, and we have some confidence that when we get to the bottom line of the formal argument, we'll be able to interpret the results "in the usual way". The fact that someone (perhaps an alien) might watch our pebblecraft and construe us (in medias res) to be referring to (abstract, mathematical) things other than the (abstract, mathematical) things that we usually construe ourselves to be referring to doesn't stop the pebblecraft magic from working.

Something I've been wondering for a while now: if concepts like "natural number" and "set" can't be adequately pinned down using first-order logic, how the heck do we know what those words mean? Take "natural number" as a given. The phrase "set of natural numbers" seems perfectly meaningful, and I feel like I can clearly imagine its meaning, but I can't see how to define it.

The best approach that comes to my mind: for all n, it's easy enough to define the concept "set of natural numbers less than n", so you simply need to take the limit of this concept as n approaches infinity. But the "limit of a concept" is not obviously a well-defined notion.

I'm concerned that you're pushing second order logic too hard, using a false fork - such and so cannot be done in first order logic therefore second-order logic. "Second order" logic is a particular thing - for example it is a logic based on model theory. http://en.wikipedia.org/wiki/Second-order_logic#History_and_disputed_value

There are lots of alternative directions to go when you go beyond the general consensus of first-order logic. Freek Wiedijk's paper "Is ZF a hack?" is a great tour of alternative foundations of mathematics - first order logic and the Zermelo-Frankel axioms for set theory turns out to be the smallest by many measures, but the others are generally higher order in one way or another. http://www.cs.ru.nl/~freek/zfc-etc/zfc-etc.pdf

"First order logic can't talk about finiteness vs. infiniteness." is sortof true in that first-order logic in a fixed language is necessarily local - it can step from object to object (along relation links) but the number of steps bounded by the size of the first-order formula. However, a standard move is to change the language, introducing a new sort of object "sets" and some axioms regarding relations between the old objects and the new objects such as inclusion, and then you can talk about properties of these new objects such as finiteness and infiniteness. Admittedly this standard move is informal or metatheoretic; we're saying "this theory is the same as that theory except for these new objects and axioms".

This is what the Zermelo-Frankel axioms do, and the vast majority of mathematics can be done within ZF or ZFC. Almost any time you encounter "finiteness" and "infiniteness" in a branch of mathematics other than logic, they are formalizable as first-order properties of first-order entities called sets.

"Does it matter if X" is not a question; "matter" is a two-place predicate (X matters to Y). What you seem to be worried about is the following: you need some set theory to talk about models of first-order logic. ZFC is a common axiomatization of set theory. But ZFC is itself a first-order theory, so it seems circular to use ZFC to talk about models of first-order logic. But if this is what you're worried about, you should just say so directly.

Does it matter if you don't have formal rules for what you're doing with models?

Do you expect what you're doing with models to be formalizable in ZFC?

Does it matter if ZFC is a first-order theory?

It may not be possible to draw a sharp line between things that exist from the things that do not exist. Surely there are problematic referents ("the smallest triple of numbers in lexicographic order such that a^3+b^3=c^3", "the historical jesus", "the smallest pair of numbers in lexicographic order such that a^3+24=c^2", "shakespeare's firstborn child") that need considerable working with before ascertaining that they exist or do not exist. Given that difficulty, it seems like we work with existence explicitly, as a theory; it's not "baked in" to human reasoning.

Guy Steele wrote a talk called "Growing a Language", where one of his points is that building hooks (such as functions) into the language definition to allow the programmer to grow the language is more important than building something that is often useful, say, complex numbers or a rich collection of string manipulation primitives. Maybe talking about the structure of "theories of X" would be valuable. Perhaps all theories have examples (including counterexamples as a specific kind of example) and rules (including definitions as a specific kind of example) - thats the kind of thing that I'm suggesting might be more like a hook.

One model for time travel might be a two dimensional piece of paper with a path or paths drawn wiggling around on it. If you scan a "current moment" line across the plane, then you see points dancing. If a line and its wiggles are approximately perpendicular to the line of the current moment, then the dancing is local and perhaps physical. Time travel would be sigmoid line, first a "spontaneous" creation of a pair of points, then the cancellation of one ("reversed") point with the original point.

An alternative story is of a line next to a loop - spontaneous creation of two "virtual" particles, one reversed, followed by those two cancelling.

Would J.K. Rowling's book be causal if we add to the lore that Time Turners are well understood to cause (unasked) "virtual bearers" very like their bearers? The virtual bearers could be reified by the real bearer using the time turner, or if they are not reified, they will "cancel" themselves by using their own, virtual, time turner.

I think this addition changes the time turner from a global / acausal constraint on possible universes to a local / causal constraint, but I could very well be mistaken. Note that the reversed person is presumably invisible, but persuasive - perhaps they are a disjunctive geas of some sort.