Return to Answer

Such constructions are interesting! However, they are often done with PA instead of ZFC (see note). For an interesting discussion, I recommend Torkel Franzén's book Inexhaustibility: a non-exhaustive treatment (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent blog article by Mike O'Connor.

Note: The following is explained in Mike O'Connor's article, but I think I need to clarify why ZFC is not the ideal base theory to do this and why PA is a better candidate.

The idea is that Con(T) is usually understood as an arithmetical statement. More precisely, given a recursive presentation of the theory T the statement Con(T) is arithmetical formalization of "there is no proof of a contradiction from T" which is encoded using Gödel numbers for proofs and formulas. (This is the messy part of Gödel's Theorem.) This is why PA, or more generally any recursively axiomatizable extension of PA, which provide a more natural environment for the analysis of arithmetical statements. For example, instead of ZFC, you may as well use the purely arithmetical part of ZFC.

There is also an even more fundamental problem with transfinite iterates. Given a recursive presentation of a theory T, the iterates T₀ = T, T₁ = T₀ + Con(T₀), T₂ = T₁ + Con(T₁), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of T_ω or T_ω+ω+3 but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of ordinal notations than in terms of proper ordinals. Ordinal notations can go pretty far up, but there are clear limitations.

These difficulties and their implications are discussed in great detail in Franzén's book. As Mike O'Connor explains, it is natural to go further and extend to subsystems of second-order arithmetic, but there and, more generally, in set theory the appropriate principles to study are reflection principles and large cardinal axioms which have better semantic interpretations.

Such constructions are interesting! However, they are often done with PA instead of ZFC (see note). For an interesting discussion, I recommend Torkel Franzén's book Inexhaustibility: a non-exhaustive treatment (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent blog article by Mike O'Connor.

Note: The following is explained in Mike O'Connor's article, but I think I need to clarify why ZFC is not the ideal base theory to do this and why PA is a better candidate.

The idea is that Con(T) is usually understood as an arithmetical statement. More precisely, given a recursive presentation of the theory T the statement Con(T) is arithmetical formalization of "there is no proof of a contradiction from T" which is encoded using Gödel numbers for proofs and formulas. (This is the messy part of Gödel's Theorem.) This is why PA, or more generally any recursively axiomatizable extension of PA, provides a more natural environment for the analysis of such statements. For example, instead of ZFC, you may as well use the purely arithmetical part of ZFC.

There is also an even more fundamental problem with transfinite iterates. Given a recursive presentation of a theory T, the iterates T₀ = T, T₁ = T₀ + Con(T₀), T₂ = T₁ + Con(T₁), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of T_ω or T_ω+ω+3 but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of ordinal notations than in terms of proper ordinals. Ordinal notations can go pretty far up, but there are clear limitations.

These difficulties and their implications are discussed in great detail in Franzén's book. As Mike O'Connor explains, it is natural to go further and extend these to subsystems of second-order arithmetic, but there and in set theory the appropriate principles to study are reflection principles and large cardinal axioms which have better semantic interpretations and take advantage of their richer surroundings.

Such constructions are interesting! However, they are often done with PA instead of ZFC (see note). For an interesting discussion, I recommend Torkel Franzén's book Inexhaustibility: a non-exhaustive treatment (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent blog article by Mike O'Connor.

Note: The following is explained in Mike O'Connor's article, but I think I need to emphasize why ZFC is not the ideal base theory to do this and why PA is a better candidate.

The problem is that Con(T) is usually understood as an arithmetical statement. More precisely, given a recursive presentation of the theory T the statement Con(T) is arithmetical formalization of "there is no proof of a contradiction from T" which is encoded using Gödel numbers for proofs and formulas. (This is the messy part of Gödel's Theorem.) Analyzing such arithmetical statements in ZFC is overkill, PA is a much more appropriate theory for doing this, but there is an even more fundamental problem.

  Given a recursive presentation of a theory T, the iterates T₀ = T, T₁ = T₀ + Con(T₀), T₂ = T₁ + Con(T₁), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of T_ω or T_ω+ω+3 but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of ordinal notations than in terms of proper ordinals. Ordinal notations can go pretty far up, but there are clear limitations.

These difficulties and their implications are discussed in great detail in Franzén's book. As Mike O'Connor explains, it is natural to go further and extend to subsystems of second-order arithmetic, but there and, more generally, in set theory the appropriate principles to study are reflection principles and large cardinal axioms.

Such constructions are interesting! However, they are often done with PA instead of ZFC (see note). For an interesting discussion, I recommend Torkel Franzén's book Inexhaustibility: a non-exhaustive treatment (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent blog article by Mike O'Connor.

Note: The following is explained in Mike O'Connor's article, but I think I need to clarify why ZFC is not the ideal base theory to do this and why PA is a better candidate.

The idea is that Con(T) is usually understood as an arithmetical statement. More precisely, given a recursive presentation of the theory T the statement Con(T) is arithmetical formalization of "there is no proof of a contradiction from T" which is encoded using Gödel numbers for proofs and formulas. (This is the messy part of Gödel's Theorem.) This is why PA, or more generally any recursively axiomatizable extension of PA, which provide a more natural environment for the analysis of arithmetical statements. For example, instead of ZFC, you may as well use the purely arithmetical part of ZFC.

There is also an even more fundamental problem with transfinite iterates. Given a recursive presentation of a theory T, the iterates T₀ = T, T₁ = T₀ + Con(T₀), T₂ = T₁ + Con(T₁), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of T_ω or T_ω+ω+3 but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of ordinal notations than in terms of proper ordinals. Ordinal notations can go pretty far up, but there are clear limitations.

These difficulties and their implications are discussed in great detail in Franzén's book. As Mike O'Connor explains, it is natural to go further and extend to subsystems of second-order arithmetic, but there and, more generally, in set theory the appropriate principles to study are reflection principles and large cardinal axioms which have better semantic interpretations.

Such constructions are interesting! However, they are often done with PA instead of ZFC. For an interesting discussion, I recommend Torkel Franzén's book Inexhaustibility: a non-exhaustive treatment (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent blog article by Mike O'Connor.

Such constructions are interesting! However, they are often done with PA instead of ZFC (see note). For an interesting discussion, I recommend Torkel Franzén's book Inexhaustibility: a non-exhaustive treatment (Lecture Notes in Logic 16, ASL, 2004). You can also read this excellent blog article by Mike O'Connor.

Note: The following is explained in Mike O'Connor's article, but I think I need to emphasize why ZFC is not the ideal base theory to do this and why PA is a better candidate.

The problem is that Con(T) is usually understood as an arithmetical statement. More precisely, given a recursive presentation of the theory T the statement Con(T) is arithmetical formalization of "there is no proof of a contradiction from T" which is encoded using Gödel numbers for proofs and formulas. (This is the messy part of Gödel's Theorem.) Analyzing such arithmetical statements in ZFC is overkill, PA is a much more appropriate theory for doing this, but there is an even more fundamental problem.

Given a recursive presentation of a theory T, the iterates T₀ = T, T₁ = T₀ + Con(T₀), T₂ = T₁ + Con(T₁), etc. Can be continued into the transfinite, but only to a limited extent. It is easy to give a recursive presentation of T_ω or T_ω+ω+3 but there are only countably many ordinals for which this works. Indeed, these iterates are better defined in terms of ordinal notations than in terms of proper ordinals. Ordinal notations can go pretty far up, but there are clear limitations.

These difficulties and their implications are discussed in great detail in Franzén's book. As Mike O'Connor explains, it is natural to go further and extend to subsystems of second-order arithmetic, but there and, more generally, in set theory the appropriate principles to study are reflection principles and large cardinal axioms.