Very nice post!

Bug: Higher-order logic (a standard term) means "infinite-order logic" (not a standard term), not "logic of order greater 1" (also not a standard term). (For whatever reason, neither the Wikipedia nor the SEP entry seem to come out and say this, but every reference I can remember used the terms like that, and the usage in SEP seems to imply it too, e.g. "This second-order expressibility of the power-set operation permits the simulation of higher-order logic within second order.")

so AFAIK it's theoretically possible that I'm the first to spell out that idea in exactly that way

I remember explaining the Axiom of Choice in this way to a fellow undergraduate on my integration theory course in late 2000. But of course it never occurred to me to write it down, so you only have my word for this :-)

I've seen some (old) arguments about the meaning of axiomatizing which did not resolve in the answer, "Because otherwise you can't talk about numbers as opposed to something else," so AFAIK it's theoretically possible that I'm the first to spell out that idea in exactly that way, but it's an obvious-enough idea and there's been enough debate by philosophically inclined mathematicians that I would be genuinely surprised to find this was the case.

If memory serves, Hofstadter uses roughly this explanation in GEB.

I think philosophers who think that the categoricity of second-order Peano arithmetic allows us to refer to the natural numbers uniquely tend to also reject the causal theory of reference, precisely because the causal theory of reference is usually put as requiring all reference to be causally guided. Among those, lots of people more-or-less think that references can be fixed by some kinds of description, and I think logical descriptions of this kind would be pretty uncontroversial.

OTOH, for some reason everyone in philosophy of maths is allergic to second-order logic (blame Quine), so the categoricity argument doesn't always hold water. For some discussion, there's a section in the SEP entry on Philosophy of Mathematics.

(To give one of the reasons why people don't like SOL: to interpret it fully you seem to need set theory. Properties basically behave like sets, and so you can make SOL statements that are valid iff the Continuum Hypothesis is true, for example. It seems wrong that logic should depend on set theory in this way.)

A few points:

i) you don't actually need to jump directly to second order logic in to get a categorical axiomatization of the natural numbers. There are several weaker ways to do the job: Lomegaomega (which allows infinitary conjunctions), adding a primitive finiteness operator, adding a primitive ancestral operator, allowing the omega rule (i.e. from the infinitely many premises P(0), P(1), ... P(n), ... infer AnP(n)). Second order logic is more powerful than these in that it gives a quasi categorical axiomatization of the universe of sets (i.e. of any two models of ZFC_2, they are either isomorphic or one is isomorphic to an initial segment of the other).

ii) although there is a minority view to the contrary, it's typically thought that going second order doesn't help with determinateness worries (i.e. roughly what you are talking about with regard to "pinning down" the natural numbers). The point here is that going second order only works if you interpret the second order quantifiers "fully", i.e. as ranging over the whole power set of the domain rather than some proper subset of it. But the problem is: how can we rule out non-full interpretations of the quantifiers? This seems like just the same sort of problem as ruling out non-standard models of arithmetic ("the same sort", not the same, because for the reasons mentioned in (i) it is actually more stringent of a condition.) The point is if you for some reason doubt that we have a categorical grasp of the natural numbers, you are certainly not going to grant that we can enforce a full interpretation of the second order quantifiers. And although it seems intuitively obvious that we have a categorical grasp of the natural numbers, careful consideration of the first incompleteness theorem shows that this is by no means clear.

iii) Given that categoricity results are only up to isomorphism, I don't see how they help you pin down talk of the natural numbers themselves (as opposed to any old omega_sequence). At best, they help you pin down the structure of the natural numbers, but taking this insight into account is easier said than done.

What about Steven Landsburg's frequent crowing on the Platonicity of math and how numbers are real because we can "directly perceive them"? How does this relate to it?

EDIT: Well, he replies here.

It so happens that the three "big lies" death mentions are all related to morality/ethics, which is a hard question. But let me take the conversation and change it a bit:

"So we can believe the big ones?"

Yes. Anger. Happiness. Pain. That sort of thing.

"They're not the same at all!"

You think so? Then take the universe and grind it down to the finest powder and sieve it through the finest sieve and then show me one atom of happiness, one molecule of pain.

In this version, the final argument is still correct -- if I take the universe and grind it down to a sieve, I will not be able to say "woo! that carbon atom is an atom of happiness". Since the penultimate question of this meditation was "Is there anything else", at least I can answer that question.

Clearly, we want to talk about happiness for many reasons -- even if we do not value happiness in itself (for ourselves or others), predicting what will make humans happy is useful to know stuff about the world. Therefore, it is useful to find a way that allows us to talk about happiness. Happiness, though, is complicated, so let us put it aside for a minute to ponder something simpler: a solar system. I will simplify here, a solar system is one star and a bunch of planets rotating around it. Though solar systems effect each other through gravity or radiation, most of the effects of the relative motions inside a solar system comes from inside itself, and this pattern repeats itself throughout the galaxy. Much like happiness, being able to talk about solar systems is useful -- though I do not particularly value solar systems in and of themselves, it's useful to have a concept of "a solar system", which describes things with commonalities, and allows me to generalize.

If I grind the universe, I cannot find an atom that is a solar system atom -- grinding the universe down destroys the "solar system" useful pattern. For bounded minds, having these patterns leads to good predictive strength without having to figure out each and every atom in the solar system.

In essence, happiness is no different than solar system -- both are crude words to describe common patterns. It's just that happiness is a feature of minds (mostly human minds, but we talk about how dogs or lizards are happy, sometimes, and it's not surprising -- those minds are related algorithms). I cannot say where every atom is in the case of a human being happy, but some atom configurations are happy humans, and some are not.

So: at the very least, happiness and solar systems are part of the causal network of things. They describe patterns that influence other patterns.

Mercy is easier than justice and duty. Mercy is a specific configuration of atoms behaving a human in a specific way -- even though the human feels they are entitled to cause another human hurt ("feeling entitled" is a set of specific human-mind-configurations, regardless of whether "entitlement" actually exists), but does not do so (for specific reasons, etc. etc.). In short, mercy describes specific patterns of atoms, and is part of causal networks.

Duty and justice -- I admit that I'm not sure what my reductionist metaethics are, and so it's not obvious what they mean in the causal network.

This depends a lot on your definition of meaningfulness. Justice and mercy are subjective values and not predictive or descriptive statements about reality. But in my opinion subjective values are meaningful, in fact they're meaning itself and the only reason I consider descriptive statements about reality to be meaningful is that they help me achieve subjective values. I believe that subjective values are objectively valuable, or that the concept of objective value would make no sense, whichever you prefer. Changes in my beliefs cannot change my fundamental values and my fundamental values are motivational in a way that beliefs are not, so I consider the fundamental values to be of prior importance.

RE: Stability of logic. Logic might not be stable or it might change later, we don't have any way of knowing and the question isn't useful and believing in logic makes me happy and gives me rewards.

I've thought about this for a while, and I feel like you can replace "Fantasy" and "Lies" with "Patterns" in that dialogue, and have it make sense, and it also appears to be an answer to your questions. That being said, it also feels like a sort of a cached thought, even though I've thought about it for a while. However, I can't think of a better way to express it and all of the other thoughts I had appeared to be significantly lower caliber and less clear.

Considering that, I should then ask "Why isn't 'Patterns' the answer?'

The statement that the world is just is a lie. There exist possible worlds that are just - for instance, these worlds would not have children kidnapped and forced to kill - and ours is not one of them.

Thus, justice is a meaningful concept. Justice is a concept defined in terms of the world (pinned-down causal links) and also irreducibly normative statements. Normative statements do not refer to "the world". They are useful because we can logically deduce imperatives from them. "If X is just, then do X." is correct, that is:

Do the right thing.

I was going to say that yes, I think there is another kind of thing that can be meaningfully talked about, and "justice" and "mercy" and "duty" have something to do with that sort of thing, but a more prototypical example would be "This court has jurisdiction". Especially if many experts were of the opinion that it didn't, but the judge disagreed, but the superior court reversed her, and now the supreme court has decided to hear the case.

But then I realized that there was something different about that kind of "truth": I would not want an AI to assign a probability to the proposition The court did, in fact, have jurisdiction (nor to, oh, It is the duty of any elected official to tell the public if they learn about a case of corruption, say). I think social constructions can technically be meaningfully talked about among humans, and they are important as hell if you want to understand human communication and behavior, but I guess on reflection I think that the fact that I would want an AI to reason in terms of more basic facts is a hint that if we are discussing epistemology, if we're discussing what sorts of thingies we can know about and how we can know about them, rather than discussing particular properties of the particularly interesting thingies called humans, then it might be best to say that "The judge wrote in her decision that the court had jurisdiction" is a meaningful statement in the sense under consideration, but "The court had jurisdiction" is not.

The map is not the territory. We discuss reality on many levels, but there is only one underlying level. Justice, duty and the like are abstractions; we use the same symbol in multiple places to define certain patterns. You don't get two identical 'happinesses', like you get two identical atoms. It's useful for us though, to talk about this abstraction at the macro level and not the micro, and it's meaningful, given that we're assuming the same axioms. I think, stuff that causes other stuff is reality, and if we assume certain axioms that correspond to reality, any new truthful statements and concepts deduced are meaningful because they also correspond to reality. Everything there is covered. Things that exists, and things we think exists.

So far we've talked about two kinds of meaningfulness and two ways that sentences can refer; a way of comparing to physical things found by following pinned-down causal links, and logical reference by comparison to models pinned-down by axioms. Is there anything else that can be meaningfully talked about? Where would you find justice, or mercy?

You find them inside counterfactual statements about the reactions of an implied hypothetical representative human, judging under under implied hypothetical circumstances in which they have access to all relevant knowledge. There is clearly justice if a wide variety of these hypothetical humans agree that there is, under a wide variety of these hypothetical circumstances; there is clearly not justice if they agree that there is not. If the hypothetical people disagree with each other, then the definition fails.

Talking about things like justice, mercy and duty is meaningful, but the meanings are intermediated by big, complex webs of abstractions which humans keep in their brains, and the algorithms people use to manipulate those webs. They're unambiguous only to the extent to which people successfully keep those webs in sync with each other. In practice, our abstractions mainly work by combining bags of weak classifiers and feature-weighted similarity to positive and negative examples. This works better for cases that are similar to the training set, worse for cases that are novel and weird, and better for simpler abstractions and abstractions built on simpler constituents.

In people's brains, and in papers written by philosophy students.

(Note: this is my first post. I may be wrong, and if so am curious as to how. Anyway, I figure it's high time that my beliefs stick their neck out. I expect this will hurt, and apologize now should I later respond poorly.)

This may be the answer to a different question, but...

I play lots of role-playing games. Role-playing games are like make-believe; events in them exist in a shared counter-factual space (in the players' imagination). Make-believe has a problem: if two people imagine different things, who is right? (This tends to end with a bunch of kids arguing about whether the fictional T-Rex is alive or dead).

Role-playing games solve this problem by handing authority over various facets of the game to different things. The protagonists are controlled by their respective players, the results of choices by dice and rules, and most of the fictional world by the Game Master.*

So, in a role-playing game, when you ask what is true[RPG], you should direct that question to the appropriate authority. Basically, truth[RPG] is actually canon (in the fandom sense; TV Trope's page is good, but comes with the usual where-did-my-evening-go caveats).

Similarly, if we ask "where did Luke Skywalker go to preschool?", we're asking a question about canon.

That said, even canon needs to be internally consistent. If someone with authority were to claim that Tatooine has no preschools, then we can conclude that Luke Skywalker didn't go to preschool. If an authority claims two inconsistent things, we can conclude that the authority is wrong (namely, in the mathematical sense the canon wouldn't match any possible model).

I've long felt that ideas like morality and liberty are a variety of canon.

Specifically, you can have authorities (a religion or philosopher telling you stuff), and those authorities can be provably wrong (because they said something inconsistent), but these ideas exists in a kind of shared imaginary space. Also, people can disagree with the canon and make up their own ideas.

Now, that space is still informed by reality. Even in fiction, we expect gravity to drop off as the square of distance, and we expect solid objects to be unable to pass through each other.** With ideas, we can state that they are nonsensical (or, at minimum, not useful) if they refers to real things which don't exist. A map of morality is a map of a non-real thing, but morality must interface with reality to be useful, so anywhere the interface doesn't line up with reality, morality (or its map) is wrong.

*This is one possible breakdown. There are many others.

**In most games/stories, anyway. At first glance I'd expect morality to be better bound to reality, but I suppose there's been plenty of people who's moral system boiled down to "don't do anything Ma'at would disapprove of", backed up with concepts like the literal weight of sin (vs. the weight of a feather).

Justice - The quality of being "just" or "fair". Humans call a situation fair when everyone involved is happy afterwards, without having had their desires forcibly thwarted (e.g. being strapped into a chair and hooked into a morphine drip) along the way.

Mercy - Compassionate or kindly forbearance shown toward an offender, an enemy, or other person in one's power. Humans choose to engage in actions characterized this way on a daily basis.

Duty - Something that one is expected or required to do by moral or legal obligation. Legal duties certainly exist; Earth is not an anarchy.

Justice, mercy, and duty are only words. The important question to ask is whether or not they are useful. I certainly think they are; I use each of those words at least once a week. Once the symbols have been replaced by substance, it is clear that we should not be looking for those things in single atoms, but very large collections of them we call "humans", or slightly smaller (but still very large) collections we call "human brains".

And as far as we know, atoms are not arranged in configurations that have the properties we ascribe to the tooth fairy.

They exist in the same sense that numbers exist, or that meaningful existence exists, or that meaningfulness exists.

Once you grind the universe into powder, none of those things exists anymore.

Justice, mercy, duty, etc are found by comparison to logical models pinned down by axioms. Getting the axioms right is damn tough, but if we have a decent set we should be able to say "If Alex kills Bob under circumstances X, this is unjust." We can say this the same way that we can say "Two apples plus two apples is four apples." I can't find an atom of addition in the universe, and this doesn't make me reject addition.

Also, the widespread convergence of theories of justice on some issues (eg. Rape is unjust.) suggests that theories of justice are attempting to use their axioms to pin down something that is already there. Moral philosophers are more likely to say "My axioms are leading me to conclude rape is a moral duty, where did I mess up?" than "My axioms are leading me to conclude rape is a moral duty, therefore it is." This also suggests they are pinning down something real with axioms. If it was otherwise, we would expect the second conclusion.

"Justice" and "mercy" can be found by looking at people, and in particular how people treat each other. They're physical things, although they're really complicated kinds of physical things.

I would find them under the category of patterns.

A neural network is very good at recognising patterns; and human brains run on a neural network architecture. Given a few examples of what a word does or does not mean, we can quickly recognise the pattern and fit it into our vocabulary. (Apparently, this can be used in language classes; the teacher will point to a variety of objects, indicating whether they are or are not vrugte, for example; and it won't take that many examples before the student understands that vrugte means fruit but not vegetables).

Justice and mercy are not patterns of objects, but rather patterns of action. The man killed his enemy, but has a wife and children to support; sending him to Death Row might be just, but letting him have some way of earning money while imprisoned might be merciful. Similarly, happy, sad, and angry are emotional patterns; a person acts in this way when happy, and acts in that way when sad.

Right, response to the meditation:

It gets rather difficult talking about human mental constructs, let's begin by asking myself where would I find justice/mercy; almost immediately (which means that I need to do some more thinking) I find that I think of human emotional constructs as a side effect of society and it's group mindset,

You think so? Then take the universe and grind it down to the finest powder and sieve it through the finest sieve and then show me one atom of justice, one molecule of mercy.

• Susan and Death, in Hogfather by Terry Pratchett

I would find that by grinding down the universe to it's component molecules would completely fail to find any number of things that humanity finds important; Humanity for one, to me rationalism is, above all the study of the universe and what it contains. And yet when it comes to most psychological phenomenon the models start to break down, does this mean that a more refined model would be equally unable to describe the phenomenon, not necessarily. Because as rationalists one of our key teachings is that we can observe something by studying it's causes and effects; justice and mercy exists insofar as we as humans can comprehend their nature. They exist because we can determine the differences between a universe where they exist and the ones where they don't exist.

-reposted in the right section

Mathematics is a system for building abstract statements that can be mapped to reality. The axioms of a mathematical (or other axiomatic) model define the conditions that a system (such as a pair of apples in the real universe) must satisfy in order for the abstract model to be applicable as well as providing a schema for mapping the abstract model to the concrete system.

There are other kinds of abstractions we could meaningfully talk about and they need not be defined as precisely as an axiomatic model like mathematics. An abstract model could be defined as a relationship between abstract ideas that can be mapped to a concrete system by pinning down each of its constituent abstractions to a concrete member of the system.

An abstract model may be predictive, meaning it has an if-then structure: if some relation between abstract members holds then the model predicts that some other relation will also hold. Such a predictive model may be true or false for any given concrete system that it is applied to. The standard we expect of a mathematical model is that it is valid (true for all concrete systems that it can be applied to), yet an abstract model need not meet so high a standard for it to be useful. We can imagine much fuzzier abstract models that are true only some of the time but can be useful by providing general-purpose rules that allow us to infer information about the actual state of a concrete system that matches the criteria of the model. If we know the probability of an abstract predictive model being correct we can use it wherever it is applicable to inform the construction of causal models. If we consider causal models to operate in the realm of first order logic where we can quantify over and describe relationships between the basic units of cause and effect in our universe, an abstract model lives in the realm of higher order logic and can describe the relationships between causal relations and lower order abstract models.

An abstract model need not be predictive to be useful. It may be defined to be applicable only where the entire relation it describes holds. In this case it simply acts as a reusable symbol that is useful for representing a model of a concrete system more compactly as in the way a function in a computer program factors out reusable logic, or a word in human language factors out a reusable abstract idea.

Justice and Mercy are both fuzzy abstract models. To the extent that people agree on their definitions they are meaningful for communicating a particular relationship between pinned-down abstractions. For example, Justice may be defined (simplistically) as describing a relationship between human deeds and subsequent events such that deeds labelled 'bad' result in punishment and deeds labelled 'good' result in reward. The particular deed and subsequent event as well as the definitions of good, bad, punishment and reward are all component abstractions of the abstract model called Justice which must be pinned down in a concrete system in order for the concept of Justice to be applied in that system.

Justice may also be used as a predictive model if you formulate it as a prediction from a good/bad deed to a future reward/punishment event (or vice versa) and it would be useful for constructing a causal model of any particular concrete system to the extent that this predicted relationship matches the actual underlying nature of that system.

Note: none of this is based on any formal study of logic outside of this Epistemology sequence so some of the terminology in this post was invented by me just now.

Er, yes? I mean it's not like we're born knowing that cars behave like integers and outlet electricity doesn't, since neither of those things existed ancestrally.

The fact that one apple added to one apple invariably gives two apples....

It's almost a tautology. What we have is an iterated identification. There are two objects that are named "apple," they are identical in identification, but separate and distinct. This appears in time. I'm counting my identifications. The universality of 1+1 = 2 is a product of a single brain design. For an elephant, the same "problem" might be "food plus food equals food."

It seems to me like there are at least two possible definitions of "reality". One is "the set of all true statements" (such as "the sky is blue", "salt dissolves in water", and "2 + 2 = 4"), and the other is "the set of all 'aspects of the world'"—things like "in world W, there is an electron at point p and time t", whose truth could, in principle, be varied independently of all other "aspects of the world".

The choice of definition seems more or less arbitrary.

I couldn't agree more. The timelessness of maths should be read negatively, as indepence of anything else, not as dependence on a timeless realm.

What if 2 + 2 varies over something other than time that nonetheless correlates with time in our universe? Suppose 2 + 2 comes out to 4 the first 1 trillion times the operation is performed by humans, and to 5 on the 1 trillion and first time.

I suppose you could raise the same explanation: the definition of 2 + 2 makes no reference to how many times it has been applied. I believe the same can be said for any other reason you may give for why 2 + 2 might cease to equal 4.

I love the elegance of this answer, upvoting.

"- try pondering this one. Why does 2 + 2 come out the same way each time? Never mind the question of why the laws of physics are stable - why is logic stable? Of course I can't imagine it being any other way, but that's not an explanation."

I have recently had a thought relevant to the topic; an operation that is not stable.

In certain contexts, the operation d is used, where XdY means "take a set of X fair dice, each die having Y sides (numbered 1 to Y), and throw them; add together the numbers on the uppermost faces". Using this definition, 2d2 has value '2' 25% of the time, value '3' 50% of the time, and value '4' 25% of the time. The procedure is always identical, and so there's nothing in the process which makes any reference to time, but the result can differ (though note that 'time' is still not a parameter in that result). If the operation '+' is replaced by the operation 'd' - well, then that is one other way that can be imagined.

Edited to add: It has been pointed out that XdY is a constant probability distribution. The unstable operation to which I refer is the operation of taking a single random integer sample, in a fair manner, from that distribution.

Yeah, but I've found the previous posts much more useful for coming up with clear explanations aimed at non-LWers, and I presume they'd make a better introduction to some of the core LW epistemic rationality than just throwing "The Simple Truth" at them.

In my opinion, Causal Diagrams and Causal Models is far superior to Timeless Causality.

I am not saying that there is anything wrong with "Timeless Causality", or any of Eliezer's old posts, but this sequence goes into enough depth of explanation that even someone who has not read the older sequences on Less Wrong would have a good chance of understanding it.

I think this is his way of connecting numbers to the previous posts. If "a property" is defined as a causal relation, which all properties are, then I think this makes sense. It doesn't provide some sort of ultimate metaphysical justification for numbers or properties or anything, but it clarifies connections between the two and such a justification isn't really possible anyways.

I'm assuming full semantics for second-order logic (for any collection of numbers there is a corresponding property being quantified over) so the axioms have a semantic model provably unique up to isomorphism, there are no nonstandard models, the Completeness Theorem does not hold and some truths (like Godel's G) are semantically entailed without being syntactically entailed, etc.

I'm not sure that adding the conjunction (R(x,y,z)&R(x,y,w)->z=w) would have made things clearer...I thought it was obvious the hypothetical mathematician was just explaining what kind of steps you need to "taboo addition"

I'd say that your "non-well-defined function on fractions" isn't actually a function on fractions at all; it's a function on fractional expressions that fails to define a function on fractions.

I agree that the use of S here was confusing. Also, there is one too many right parens.

But isn't P1 required by "And every property true at 0, and for which P(Sx) is true whenever P(x) is true, is true of all numbers."?

We can try to write that down as "For all x, there is an n such that x = S(S(...S(0)...)) repeated n times."

The two problems that we run into here are: first, that repeating S n times isn't something we know how to do in first-order logic: we have to say that there exists a sequence of repetitions, which requires quantifying over a set. Second, it's not clear what sort of thing "n" is. It's a number, obviously, but we haven't pinned down what we think numbers are yet, and this statement becomes awkward if n is an element of some other chain that we're trying to say doesn't exist.

I'm a little confused as to which of two positions this is advocating:

1. Numbers are real, serious things, but the way that we pick them out is by having a categorical set of axioms. They're interesting to talk about because lots of things in the world behave like them (to some degree).

2. Mathematical talk is actually talk about what follows from certain axioms. This is interesting to talk about because lots of things obey the axioms and so exhibit the theorems (to some degree).

I read it as (1), with a side order of (2). Mathematical talk is also about what follows from certain axioms. The axioms nail it down so that mathematicians can be sure what other mathematicians are talking about.

Both of these have some problems. The first one requires you to have weird, non-physical numbery-things.

Not weird, non-physical numbery-things, just non-physical numbery-things. If they seem weird, maybe it's because we only noticed them a few thousand years ago.

Not only this, but they're a special exception to the theory of reference that's been developed so far, in that you can refer to them without having a causal connection.

No more than a magnetic field is a special exception to the theory of elasticity. It's just a phenomenon that is not described by that theory.

In contrast with my esteemed colleague RichardKennaway, I think it's mostly #2. Before the Peano axioms, people talking about numbers might have been talking about any of a large class of things which discrete objects in the real world mostly model. It was hard to make progress in math past a certain level until someone pointed out axiomatically exactly which things-that-discrete-objects-in-the-real-world-mostly-model it would be most productive to talk about.

Concordantly, the situation of pre-axiom speakers is much like that of people from Scotland trying to talk to people from the American South and people from Boston, when none of them knows the rules of their grammar. Edit: Or, to be more precise, it's like two scots speakers as fluent as Kawoomba talking about whether a solitary, fallen tree made a "sound," without defining what they mean by sound.

What about "both ways simultaneously, the distinction left ambiguous most of the time because it isn't useful"?

I would read this:

axioms pin down that we're talking about numbers as opposed to something else.

as:

axioms pin down that we're talking about some system that behaves like numbers as opposed to something else.

Lots of things in both real and imagined worlds behave like numbers. It's most convenient to pick one of them and call them "The Numbers" but this is really just for the sake of convenience and doesn't necessarily give them elevated philosophical status. That would be my position anyway.

I'm not sure exactly what Eliezer intends, but I'll put in my two cents:

A proof is simply a game of symbol manipulation. You start with some symbols, say '(', ')', '¬', '→', '↔', '∀', '∃', 'P', 'Q', 'R', 'x', 'y', and 'z'. Call these symbols the alphabet. Some sequences of symbols are called well-formed formulas, or wffs for short. There are rules to tell what sequences of symbols are wffs, these are called a grammar. Some wffs are called axioms. There is another important symbol that is not one of the symbols you chose - this is the '⊢' symbol. A declaration is the '⊢' symbol followed by a wff. A legal declaration is either the '⊢' symbol followed by an axiom or the result of an inference rule. An inference rule is a rule that declares that a declaration of a certain form is legal, given that certain declarations of other forms are legal. A famous inference rule called modus ponens is part of a formal system called first-order logic. This rule says: "If '⊢ P' and '⊢ (P → Q)' (where P and Q are replaced with some wffs) are valid declarations, then '⊢ Q' is also a valid declaration." By the way, a formal system is just a specific alphabet, grammar, set of axioms, and set of inference rules. You also might like to note that if '⊢ P' (where P is replaced with some wff) is a valid declaration, then we also call P a theorem. So now we know something: In a formal system, all axioms are theorems.

The second thing to note is that a formal system does not necessarily have anything to do with even propositional logic (let alone first- or second-order logic!). Consider the MIU system (open link in WordPad, on Windows), for example. It has four inference rules for just messing around with the order of the letters, 'M', 'I', and 'U'! That doesn't have to do with the real world or even math, does it?

The third thing to note is that, though a formal system can tell us what wffs are theorems, it cannot (directly) tell us what wffs are not theorems. And hence we have the MU puzzle. This asks whether "MU" is a theorem in the MIU system. If it is, then you only need the MIU system to demonstrate this, but if it is not, you need to use reasoning from outside of that system.

As other commenters have already noted, mathematicians are not thinking about ZFC set theory when they prove things (that's not a bad thing; they'd never manage to prove any new results if they had to start from foundations for every proof!). However, mathematicians should be fairly confident that the proofs they create could be reduced down to proofs from the low-level axioms. So Eliezer is definitely right to be worried when a mathematician says "A proof is a social construct – it is what we need it to be in order to be convinced something is true. If you write something down and you want it to count as a proof, the only real issue is whether you’re completely convincing.". A proof is a social construct, but it is one, very, very specific kind of social construct. The axioms and inference rules of first-order Peano arithmetic are symbolic representations of our most fundamental notion of what the natural numbers are. The reason for propositional logic, first-order logic, second-order logic, Peano arithmetic, and the scientific method is that humans have little things called "cognitive biases". We are convinced by way too many things that should be utterly unconvincing. To say that a proof is a convincing social construct is...technically...correct (oh how it pains me to say that!)...but that very vague part of what it means for something to be a proof seems to imply that a proof is the utter antithesis of what it was meant for! A mathematical proof should be the most convincing social construct we have, because of how it is constructed.

First-order Peano arithmetic has just a few simple axioms, and a couple simple inference rules, and its symbols have a clear intended interpretation (in terms of the natural numbers (which characterize parts of the web of causality as already explained in the OP)). The truth of a few simple axioms and validity of a couple simple inference rules can be evaluated without our cognitive biases getting in the way. On the other hand, it's probably not a good idea to make "There is a prime number larger than any given natural number." an axiom of a formal system about the natural numbers, because it is not an immediate part of our intuitive understanding of how causal systems that behave according to the rules of the natural numbers behave. We as humans would have to be very, very, confused if a theorem of first-order Peano arithmetic (because we are so sure that its axioms are true and its inference rules are valid) turned out to be the negation of another theorem of Peano arithmetic, but not so confused if the same happened for ZFC set theory, because we do not so readily observe infinite sets in our day-to-day experience. The axioms and inference rules of first-order Peano arithmetic more directly correspond to our physical reality than those of ZFC set theory do (and the axioms and inference rules of the MIU system have nothing to do with our physical reality at all!). If a contradiction in first-order Peano arithmetic were found, though, life would go on. First-order Peano arithmetic does have a lot to do with our physical reality, but not all of it does. It inducts to numbers like 3^^^3 that we will probably never interact with. The ultrafinitists would be shouting "Told you so!"

Now I have said enough to give my direct response to the comment I am replying to. First of all, the dichotomy between "logic" and "mathematics" can be dissolved by referring to "formal systems" instead. A formal system is exactly as entwined with reality as its axioms and inference rules are. In terms of instrumental rationality, the more exotic theorems of ZFC set theory (and MIU) really don't help us, unless we intrinsically enjoy considering the question "What if there were (even though we have no evidence that this is the case) a platonic realm of sets? How would it behave?"

When used as means to an end, the point of a formal system is to correct for our cognitive biases. In other words, the definition of a proof should state that a proof is a "convincing demonstration that should be convincing", to begin with. I suspect Eliezer is so concerned with the Peano axioms because computer programs happen to evidently behave in a very, very mathematical way, and he believes that eventually a computer program will decide the fate of humanity. I share his concerns; I want a mathematical argument that the General Artificial Intelligence that will be created will be Friendly, not anything that might "convince" a few uninformed government officials.