Aaronson is using a slightly less common definition of soundness (arithmetical soundness) than the usual one you'll see. Usually we talk about the soundness of entire logical systems (e.g. the soundness of first-order logic) rather than particular theories within that system.
Here arithmetical soundness is tightly coupled to the idea of Godel encodings of theorems and proofs. That is a system like ZFC does not have a direct notion of theorems and proofs. Instead a statement such as `Con(ZFC)` is actually a statement about the (non-)existence of a certain natural number fulfilling certain conditions. More specifically `Con(F)` is usually a statement stating that the natural number corresponding to a Godel encoding of a proof of a clearly contradictory statement (e.g. `1 = 0`) does not exist, whereas `Not(Con(F))` is a statement that such a Godel encoding does exist (which usually makes `Not(Con(F))` the more fundamental statement of the two and `Con(F)` is really `Not(Incon(F))` but I digress).
Arithmetical soundness requires the notion of "standard natural numbers." In particular, as stated elsewhere in this thread, first-order Peano Arithmetic can be satisfied by many different models, only one of which we designate as our familiar "standard natural numbers."
Arithmetical soundness then is the property that natural numbers which satisfy the conditions of these statements encoded via Godel encodings are all standard natural numbers. So for example `Not(Con(F))` corresponds to a statement about the existence of a natural number. If `F` is "truly" consistent then `Not(Con(F))` can only be satisfied by a non-standard natural number. On the other hand if `F` is "truly" inconsistent then `Not(Con(F))` can be satisfied by a standard natural number.
You've noticed that I've put the word "truly" in quote marks. This is for two reasons:
1. The usual way to rigorously define "truly" is to appeal to some standard model. Hence the arrow of definition should be going the other way; the concept of a standard natural number that underlies arithmetical soundness is what lets talk about "true" consistency.
2. Whether it makes sense to talk about "the" standard model of a given theory or whether there are multiple possible standard models becomes a matter of philosophy. The former position corresponds to essentially a version of Platonism. The latter position is what is often known as the "multiverse" theory of mathematical logic. Through the philosophical viewpoint of the latter, we can never say absolutely whether a given theory is arithmetically unsound or not, only that it is arithmetically unsound relative to a given model of the natural numbers.
Here arithmetical soundness is tightly coupled to the idea of Godel encodings of theorems and proofs. That is a system like ZFC does not have a direct notion of theorems and proofs. Instead a statement such as `Con(ZFC)` is actually a statement about the (non-)existence of a certain natural number fulfilling certain conditions. More specifically `Con(F)` is usually a statement stating that the natural number corresponding to a Godel encoding of a proof of a clearly contradictory statement (e.g. `1 = 0`) does not exist, whereas `Not(Con(F))` is a statement that such a Godel encoding does exist (which usually makes `Not(Con(F))` the more fundamental statement of the two and `Con(F)` is really `Not(Incon(F))` but I digress).
Arithmetical soundness requires the notion of "standard natural numbers." In particular, as stated elsewhere in this thread, first-order Peano Arithmetic can be satisfied by many different models, only one of which we designate as our familiar "standard natural numbers."
Arithmetical soundness then is the property that natural numbers which satisfy the conditions of these statements encoded via Godel encodings are all standard natural numbers. So for example `Not(Con(F))` corresponds to a statement about the existence of a natural number. If `F` is "truly" consistent then `Not(Con(F))` can only be satisfied by a non-standard natural number. On the other hand if `F` is "truly" inconsistent then `Not(Con(F))` can be satisfied by a standard natural number.
You've noticed that I've put the word "truly" in quote marks. This is for two reasons:
1. The usual way to rigorously define "truly" is to appeal to some standard model. Hence the arrow of definition should be going the other way; the concept of a standard natural number that underlies arithmetical soundness is what lets talk about "true" consistency.
2. Whether it makes sense to talk about "the" standard model of a given theory or whether there are multiple possible standard models becomes a matter of philosophy. The former position corresponds to essentially a version of Platonism. The latter position is what is often known as the "multiverse" theory of mathematical logic. Through the philosophical viewpoint of the latter, we can never say absolutely whether a given theory is arithmetically unsound or not, only that it is arithmetically unsound relative to a given model of the natural numbers.