User carl mummert - MathOverflow

Answer by Carl Mummert for Reverse mathematics below RCA

2013-03-30T13:13:30Z

There is a large family of systems that go by names such as $\text{E-}\widehat{\text{PRA}}^\omega$. These are all somewhat related to the "System T" introduced by Gödel as part of this Dialectica interpretation. These systems are function-based, rather than set-based, and they are typically axiomatized in all finite types, although it would be easy enough to limit the collection of types. But they have a "feel" very much like PRA, in that the rules for creating functions of higher types by recursion are generalizations of the primitive recursion scheme in PRA. Comprehension is usually replaced, in these function-based settings, by fragments of the axiom of choice.

One aspect of this area is that, unlike reverse mathematics where there are five big systems that are each robust against minor changes, in the context of proof theory there are many different systems (e.g. $\text{PA}^\omega$, $\text{E-PA}^{\omega}$, $\text{E-}\widehat{\text{PA}}^{\omega}$, $\text{E-}\widehat{\text{PA}}^{\omega} \mathord{\upharpoonright}$ are different systems) and the fine details make a difference in the strengths. Moreover, different authors may use different notation for the same system.

The best references I know of for these systems are the books Applied Proof Theory by Kohlenbach and Metamathematical Investigation by Troelstra. Kohlenbach's book, in particular, has one of the most clear developments I have seen. There are a few papers online that have some information, such as

"Foundational and Mathematical Uses of Higher Types", Kohlenbach, http://brics.dk/RS/99/31/BRICS-RS-99-31.ps.gz
"Gödel's functional Interpretation", Avigad and Feferman, http://www.andrew.cmu.edu/~avigad/Papers/dialect.pdf

Answer by Carl Mummert for First-order vs second-order provability

2013-01-24T12:54:15Z

I assume that you mean the second-order system with both second-order induction and the full second-order comprehension scheme. There are many "second order variations" of Peano Arithmetic, with different strengths, so care is required to specify which one is intended. The second-order induction axiom on its own does not allow you to prove any new sentences of first-order arithmetic, compared to Peano Arithmetic, because every model of Peano Arithmetic extends to a model of $\mathsf{ACA}_0$, and that extended model satisfies the second-order induction axiom.

Regardless, there are not going to be any completely elementary principles of number theory that are provable in full second order arithmetic ($Z_2$) but not in PA, because of the well-known phenomenon that all elementary principles are already provable in PA. It is very difficult to find "natural" true mathematical statements that can be expressed in the language of PA but cannot be proved in PA. The Paris--Harrington principle is, in some sense, as good as it gets, which is the main reason the Paris--Harrington theorem is of interest.

Answer by Carl Mummert for Existential instantiation in Hilbert-style deduction systems

2012-12-21T20:51:42Z

For comparison, Enderton's textbook uses a Hilbert-style system. He derives EI in a form that is essentially what Emil Jeřábek calls Lemma 1', but as a metatheorem:

(EI) If $\Gamma, \phi(c) \vdash \psi$ where $c$ does not occur in $\Gamma$, $\phi(x)$, or $\psi$, then $$\Gamma, (\exists x)\phi(x) \vdash \psi,$$ and there is a deduction witnessing this fact that does not mention $c$.

Here we do not deduce $\phi(c)$ from $(\exists x) \phi(x)$, rather we assume $\phi(c)$ as a temporary hypothesis, for an appropriate $c$, knowing that we can later weaken that hypothesis to $(\exists x)\phi(x)$. But $\phi(c)$ does not appear on the right side of the turnstile in the metatheorem: it is never a conclusion, only a hypothesis.

Also, Enderton does define $\vDash$ via your "simple definition": $\phi \vDash \psi$ means that for every structure $M$ and variable assignment $a$, if $M$ satisfies $\phi$ with $a$ then $M$ satisfies $\psi$ with $a$. In particular, he points out the example that $Q(x) \not\vDash (\forall z) Q(z)$, where $Q$ is a unary relation symbol, and in this sense free variables are indeed not "implicitly universally quantified" in his definition. He is still able to prove that $\Gamma \vdash \phi$ if and only if $\Gamma \vDash \phi$, with no restrictions on free variables, by being careful with the logical axioms he assumes in his Hilbert-style system. He does get universal generalization as a metatheorem: if $\Gamma \vdash \phi(x)$ and $\Gamma$ does not mention $x$ then $\Gamma \vdash (\forall x)\phi(x)$.

This is quite different than the definition of $\vDash$ mentioned by Emil Jeřábek, in which $Q(x) \vDash (\forall z) Q(z)$. Let's call that "implicitly universally quantified". I have found in several cases that authors who are concerned with universal algebra or equational theories seem to prefer to use the definition in which free variables are implicitly universally quantified, while those who are concerned with model theory may not even define satisfaction or logical implication for formulas with free variables (instead they define what it means for a tuple of elements to satisfy a formula in a given structure, which is slightly different). All the definitions agree if we only consider sentences, of course.

Answer by Carl Mummert for Subscript 0 in Reverse Mathematics

2012-11-18T20:43:33Z

As the other answer points out, the subscript 0 means restricted induction. However, without the subscript 0, there are two conventions:

The older convention was that the systems without the subscript 0 have the full second-order induction scheme. Thus $\mathsf{ACA}$ is the system consisting of $\mathsf{ACA}_0$ plus the full induction scheme, and the same for e.g. $\mathsf{WKL}$ vs. $\mathsf{WKL}_0$. Historically, the systems with full induction were studied first (as in Feferman's article in the Handbook of Mathematical Logic), and the systems with restricted induction were of secondary interest. The restricted systems drew more interest once it was apparent how many mathematical results they can prove, so that in the context of reverse mathematics the systems with full induction seem less natural.
Some authors, however, use ACA to mean "Arithmetical Comprehension Axiom" and WKL to mean "Weak König's Lemma". For these authors, $\mathsf{ACA}_0$ is $\mathsf{RCA}_0$ plus "ACA". Similarly $\mathsf{WKL}_0$ means $\mathsf{RCA}_0$ plus "WKL". This terminology appears in various papers, even some published by respected proof theorists, and so you have to watch for it. Note that ACA here can be taken to be a single sentence "for all $X$ the Turing jump of $X$ exists" and similarly WKL is a single sentence.

For higher-order analogues, it is still a question whether restricted induction or full induction is included. Kohlenbach [1] has used notation such as $\mathsf{ACA}_0^\omega$ to refer to the analogue of $\mathsf{ACA}_0 $ formalized in arithmetic in all finite types. In this context, though, there are many different ways in which induction can be restricted. So notation like $\widehat{\mathsf{E\text{-}HA}}^\omega_\upharpoonright $ is used in the literature, where the hat and the harpoon refer to different sorts of restrictions. These notations are explained in Kohlenbach's Applied Proof Theory or in Troelstra's Metamathematical Investigations.

1: Ulrich Kohlenbach, "Higher Order Reverse Mathematics", Reverse Mathematics 2001, Lecture Notes in Logic, 2005, ftp://ftp.daimi.au.dk/BRICS/RS/00/49/BRICS-RS-00-49.pdf

Answer by Carl Mummert for Is there a general setting for self-reference?

2012-10-10T15:40:38Z

You might also be interested in Graham Priest's article "The Structure of the Paradoxes of Self-Reference", Mind 103 (1994) pp. 25-34. (Journal page ; JStor) and similar work by Priest. He has a general framework that he argues captures the various self-referential paradoxes. I believe he also discusses this in some of his other work and monographs.

Answer by Carl Mummert for Second-order term in first-order logic?

2012-08-22T18:12:13Z

I think that the spirit of this question, combined with the clarifications in comments, is:

What is it that makes first-order logic "first order"?

Unfortunately, the terms "first order" and "second order" get used to mean various things.

A formal but unsatisfying answer would say that first-order logic is a specific logic defined in, say, Mendelson's textbook, and any other logic is not "first order logic" strictly speaking. This is unsatisfying because we know there are many inessential variations of first-order logic - really there are many first-order logics that share a certain core. The question I quoted asks for a characterization of that core.

One common answer is that any logic in which we intend to have quantifiers over "functions" or "sets" is higher order. This is unsatisfying because, as Andrej Bauer points out, such theories can be syntactically expressed in multi-sorted first-order logic. There are many theories of "second order arithmetic", for example, which allow us to express set and function quantification but which are treated as first-order theories. Unfortunately, the terminology "second order" is established for these theories and cannot be avoided.

Recall that a logic consists of both a syntax and a semantics. The truly defining feature of a first-order logic is the semantics. First-order semantics begins with the notion of a structure (also called a model), as defined in every introductory textbook on first-order logic.

Consider how we would express function quantification in (multi-sorted) first-order logic, as in Andrej's answer. Each structure must interpret two sorts. It uses a set of individuals for the quantifiers over individuals and a separate set of functions for the quantifiers over functions. This set of functions, in an arbitrary structure, might be a proper subset of the collection of all functions on the set of individuals; nothing in the definition of a structure requires otherwise. Indeed some structures will have an infinite set of individuals but a finite set of functions.

Full second order semantics changes the class of allowable structures so that only those whose function set includes all the functions are allowed. This does not affect the syntax in any way, but it deeply changes the semantics. Because fewer structures are being considered, more formulas will be logically valid, and fewer will be satisfiable. Thus there are more categorical theories in these semantics, such as the well known categorical second-order axiomatizations of the natural numbers. Those same axiomatizations are syntactically fine in first-order logic, where the simple difference is that they are no longer categorical.

Thus the key difference between function quantification in multi-sorted first order logic (or type theory) and function quantification in full second-order semantics is not the existence of syntactic quantifier symbols that allow quantification over functions. The difference is in the meaning of those quantifiers, which derives from the way the semantics are defined. In the first-order case, we have little control over the range of quantifiers. In full second-order semantics, once the set of individuals is fixed, the range of the function quantifiers is also fixed. This distinction is only visible at the meta level, when we are studying the logic from the outside and can specify which interpretations are permissible. Nothing in the syntax of the logic tells us what collection of structures will be used to interpret it.

Answer by Carl Mummert for Does higher order arithmetic interpret the axiom of choice?

2012-08-03T03:49:03Z

There is quite a bit of this in Simpson's book Subsystems of Second Order Arithmetic in the specific context of second-order arithmetic. Here are three relevant results:

Corollary VII.5.11 (conservation theorems). Let $T_0$ be any one of the $L_2$-theories $\Pi^1_\infty\text{-CA}_0$, $\Pi^1_{k+1}\text{-CA}_0$, $\Delta^1_{k+2}\text{-CA}_0$, $0 ≤ k < \infty$. Let $\phi$ be any $\Pi^1_4$ sentence. Suppose that $\phi$ is provable from $T_0$ plus $\exists X \forall Y (Y ∈ L(X ))$. Then $\phi$ is provable from $T_0$ alone.

Here $\Pi^1_\infty\text{-CA}_0$ has the full comprehension scheme for second order arithmetic, and hence also the full induction scheme.

Theorem VII.6.16 ($\Sigma^1_{k+3}$ choice schemes). The following is provable in $\text{ATR}_0$. Assume $\exists X \forall Y (Y ∈ L(X ))$. Then:

$\Sigma^1_{k+3}\text{-AC}_0$ is equivalent to $\Delta^1_{k+3}\text{-CA}_0$ .

$\Sigma^1_{k+3}\text{-DC}_0$ is equivalent to $\Delta^1_{k+3}\text{-CA}_0$ plus $\Sigma^1_{k+3}\text{-IND}$ .

Strong $\Sigma^1_{k+3}\text{-DC}_0$ is equivalent to $\Pi^1_{k+3}\text{-CA}_0$ .

$\Sigma^1_\infty \text{-DC}_0$ ( $=\bigcup_{k < \omega} \Sigma^1_k\text{-DC}_0$ ) is equivalent to $\Pi^1_\infty\text{-CA}_0$ .

and

Corollary IX.4.12 (conservation theorem). For all $k <\omega$, $\Sigma^1_{k+3}\text{-AC}_0$ (hence also $\Delta^1_{k+3}\text{-AC}_0$ ) is conservative over $\Pi^1_{k+2}\text{-CA}_0$ for $\Pi^1_4$ sentences.

Answer by Carl Mummert for Z_2 versus second-order PA

2012-05-16T02:44:36Z

$Z_2$ as it is usually viewed is a first-order theory with two sorts, and as such is not categorical. The difference (apart from terminological issues) is entirely in the semantics that are used. In "full" second-order semantics, the set variables quantify over all subsets of the domain, while in first-order "Henkin" semantics each model has a domain for number variables and a second domain for set quantifiers to range over.

There are two things that you might mean by $PA_2$ (I realized this after writing the answer, so I have expanded it). The first option is to have $PA_2$ include the entire second-order induction scheme; let's call that $PA^s_2$. $PA^s_2$ and $ACA$ are indeed equiconsistent. Every model of $ACA$ is already a model of $PA^s_2$, and every model of $PA^2_2$ extends to a model of $ACA$ by just throwing in the definable sets. In fact, this extends any model of $PA^s_2$ to a model of $Z_2$, so these theories are equiconsistent. There is an issue that this could mean "equiconsistent in full second order semantics" or "equiconsistent in first-order semantics", but either way they are pairwise equiconsistent as long as the same semantics is used for both theories.

The other option is that $PA_2$ might just have the single second-order induction axiom $$ (\forall x)[0 \in X \land (\forall n)[n \in X \to n+1\in X] \to (\forall n) n \in X]. $$ Let's call that version $PA^i_2$. Now the semantics matters. In full second-order semantics, any model of $PA^i_2$ is a model of $PA^s_2$, so it extends to a model of $Z_2$. In first-order semantics, $PA^i_2$ is very weak, because without any comprehension axioms the single second-order induction axiom is not very strong in first-order semantics. $PA^i_2$ is (syntactically) a subtheory of $\mathsf{RCA}_0$, one of the weak systems of arithmetic considered in reverse mathematics, and so $PA^i_2$ has a much lower consistency strength than $Z_2$ in the first-order setting.

Answer by Carl Mummert for What is "Seetapun Enigma"?

2012-03-25T17:50:26Z

The question seems to be about the following special form of Ramsey's Theorem:

$\mathsf{RT}^2_2$: for every $2$-coloring of the unordered pairs from $\mathbb{N}$ there is an infinite subset of $\mathbb{N}$ for which all unordered pairs receive the same color.

which is a special case of

$\mathsf{RT}^n_k$: for every $k$-coloring of the unordered $n$-tuples from $\mathbb{N}$ there is an infinite subset of $\mathbb{N}$ for which all unordered $n$-tuples receive the same color.

The computability strength of infinite Ramsey's theorem was first studied by Jockusch (1972). When interpreted in modern terminology that didn't exist then, Jockusch's result is that $\mathsf{RT}^n_k$ is equivalent to $\mathsf{ACA}_0$ whenever $n \geq 3$ and $k \geq 2$. The equivalence is over the standard base system $\mathsf{RCA}_0$ which is assumed in the rest of this post. As a corollary, $\mathsf{ACA}_0$ proves $\mathsf{RT}^2_k$ for all $k \geq 2$.

Later, Hirst (1987) characterized the strength of principles of the form $\mathsf{RT}^1_k$. The separate results of Jockusch and Hirst leave a gap for exponent $2$, and in particular for $\mathsf{RT}^2_2$. The exact reverse mathematics strength of $\mathsf{RT}^2_2$ is somewhat mysterious, although I don't know that anyone calls it an "enigma". It has proven to be a particularly difficult open problem.

The first result was due to Seetapun (published as Seetapun and Slaman (1995)), who showed that $\mathsf{RT}^2_2$ does not imply $\mathsf{ACA}_0$. The fact that this seemingly weak result was all that could be obtained hints at the difficulty of finding the exact strength of $\mathsf{RT}^2_2$ with known methods. Seetapun's proof used an intricate forcing argument. The ideas behind this argument have been progressively clarified and extended, and are now well understood; the most recent paper on this is by Dzhafarov and Jockusch (2009).

The principle $\mathsf{WKL}_0$ says that every infinite subtree of $2^{<\mathbb{N}}$ has an infinite path. $\mathsf{WKL}_0$ is one of the "big five" systems of reverse mathematics, and is the natural comparison point for principles weaker than $\mathsf{ACA}_0$ such as $\mathsf{RT}^2_2$.

Cholak, Jockusch, and Slaman (2001) made the next significant progress on $\mathsf{RT}^2_2$. Among many other new results they showed that $\mathsf{RT}^2_2$ is not provable in $\mathsf{WKL}_0$, because $\mathsf{WKL}_0$ does not prove the principle $\mathsf{COH}$ which is provable from $\mathsf{RT}^2_2$. The principle $\mathsf{COH}$ is a formalized statement of a theorem from recursion theory about the existence of $r$-cohesive sets.

The results I have mentioned left the question open whether $\mathsf{RT}^2_2$ implies $\mathsf{WKL}_0$. This was recently solved by Liu in 2011. Liu showed in a still-unpublished paper that $\mathsf{RT}^2_2$ does not imply $\mathsf{WWKL}_0$, which is the restriction of $\mathsf{WKL}_0$ to trees of positive measure, and which is strictly weaker than $\mathsf{WKL}_0$. Thus, combining results, $\mathsf{RT}^2_2$ and $\mathsf{WKL}_0$ are mutually independent.

As I understand it, Liu proved this independently while a student at Central South University (China), without an advisor in logic or any graduate training in logic. Liu presented his result at the Reverse Mathematics workshop at University of Chicago in September 2011. The slides from that talk are available online, but they are quite technical. The proof uses another intricate forcing argument.

As I understand it, Liu's paper was submitted to a journal some time before the workshop, the results have been verified by referees, and the paper will be published once it is in final form.

Citations

Cholak, Peter A.; Jockusch, Carl G.; Slaman, Theodore A. On the strength of Ramsey's theorem for pairs. J. Symbolic Logic 66 (2001), no. 1, 1–55. MR1825173 (2002c:03094)
Dzhafarov, Damir D.; Jockusch, Carl G., Jr. Ramsey's theorem and cone avoidance. J. Symbolic Logic 74 (2009), no. 2, 557–578. MR2518811 (2010e:03052)
Hirst, Jeffry Lynn. Combinatorics in subsystems of second-order arithmetic. PhD Thesis, The Pennsylvania State University. 1987. 153 pp.
Jockusch, Carl G., Jr. Ramsey's theorem and recursion theory. J. Symbolic Logic 37 (1972), 268–280. MR0376319 (51 #12495)
Seetapun, David; Slaman, Theodore A. On the strength of Ramsey's theorem. Special Issue: Models of arithmetic. Notre Dame J. Formal Logic 36 (1995), no. 4, 570–582. MR1368468 (96k:03136)

Answer by Carl Mummert for Can infinity shorten proofs a lot?

2012-02-01T13:07:19Z

The axiom system PRA of "primitive-recursive arithmetic" is finitistic, but it has been known for a few decades that it has the same set of $\Pi^0_1$ consequences as the infinitistic theory $\text{WKL}_0$ of second-order arithmetic. In particular, there is a primitive recursive function $f$ that turns a formal proof of a $\Pi^0_1$ statement in $\text{WKL}_0$ into a proof in PRA. Roughly put, a $\Pi^0_1$ formula says that all natural numbers have some particular property, depending on the formula, where the property can be stated using a formula in the language of rings with no quantifiers.

The advantage of working in $\text{WKL}_0$ is that the proofs can be much shorter. I think this was always suspected, but Caldon and Ignjatovic recently established (pdf) a formal superexponential lower bound for $f$, at least on an infinite set of formulas. Their result is phrased for a different infinitary system, $I\Sigma^0_1$, that lies between PRA and $\text{WKL}_0$. $I\Sigma^0_1$ is a fragment of Peano arithmetic, unlike $\text{WKL}_0$; its main difference from PRA is that $I\Sigma^0_1$ allows direct universal quantification over the set of natural numbers during the proof, while PRA does not.

In their paper, the set of formulas for the lower bound is explicitly laid out. These may not be particularly concrete, because they relate to consistency statements.

If we expand PRA to allow for existential quantification, we can get a slightly larger theory in which $\Pi^0_2$ statements can be expressed. It is known that $\text{WKL}_0$ is still conservative over this larger theory for $\Pi^0_2$ statements. In 1994, Kikuchi and Tanaka (pdf) gave a nice example of how this could be used to show that the second incompleteness theorem is provable in PRA, by using model-theoretic, infinitary methods in $\text{WKL}_0$ and relying on the conservation result.

Answer by Carl Mummert for Explicit expression for recursively defined functions

2011-12-16T17:36:56Z

To follow up on Joel Hamkins' answer, the fundamental obstruction here is totality. Explicit definitions are always going to give total functions. The reason that recursion is so powerful for defining functions is that it is possible to make partial functions, e.g. $$ f(0) := 0 \qquad f(2n+2) := f(2n) \qquad f(2n+1) := f(2n+3) $$

The following is a standard theorem.

Theorem. Let $C$ be a countable system of total computable functions $\mathbb{N} \to \mathbb{N}$ with the property

There is a numbering $\phi_i\colon \mathbb{N} \to C$ such that every $f \in C$ is of the form $\phi_i$ for at least one $i$, and there is a uniform way to compute $\phi_i(j)$ given just $i$ and $j$.

Then $C$ does not include all total computable functions from $\mathbb{N}$ to $\mathbb{N}$.

Proof. Diagonalization.

In the context of this question, the philosophical meaning of this theorem is that it is not possible to come up with a completely explicit form for every computable function, in some fixed signature, because then by enumerating all possible forms we would get a numbering $\phi$ as in the theorem.

The closest we can hope for in terms of an explicit form for all total computable functions is something like Kleene normal form, but this still includes an unbounded search. Kleene's normal form theorem says that there is a primitive recursive function $U$ and a primitive recursive relation $T$ such that for every computable function $f$ there is an $e$ such that for all $i$, $$ f(i) \simeq U(\mu s . T(e,i,s)). $$ where $\mu$ is the unbounded search operator.

Answer by Carl Mummert for Undecidability [sic] in set theory [per se]

2011-12-15T01:26:41Z

If you look at "families" in a more general sense there are many examples. For example, the set of $x \in 2^\omega$ that are the graph of a well ordering of $\omega$. This set is well known to be $\Pi^1_1$ complete, and in particular is not decidable (i.e. lightface $\Delta^0_1$). I think that being well ordered is a purely set-theoretic problem.

This can also be put into a countable setting by replacing the set above with a slightly less natural set, Kleene's $\mathcal{O}$, of all natural numbers that are indices of computable well-orderings of $\omega$.

There are many similar examples in descriptive set theory.

Answer by Carl Mummert for Up-to-date version of Principia Mathematica?

2011-11-29T03:34:52Z

In his Stanford Encyclopedia of Philosophy article "The Notation of Principia Mathematica", Bernard Linsky makes the following claim:

This translation is offered as an aid to learning the original notation, which itself is a subject of scholarly dispute, and embodies substantive logical doctrines so that it cannot simply be replaced by contemporary symbolism. Learning the notation, then, is a first step to learning the distinctive logical doctrines of Principia Mathematica.

The point is that Principia was not intended simply to be a development of mathematics in type theory: it was intended to make a philosophical argument that mathematics could be carried out using only "logic". Thus translating PM so that the underlying mathematical principles are more clearly described would miss the point that there are not supposed to be any underlying mathematical principles, only "logical" ones. This differs sharply from Gödel's paper, which was intended to be mathematical (the result can be viewed as just a particular type of combinatorics or number theory) rather than philosophical.

Answer by Carl Mummert for "local variables" in first-order formulas

2011-10-11T19:18:15Z

One elegant solution is to apply the following theorem from Enderton's logic book (Theorem 24I):

Let $\phi$ be a formula, $t$ a term, and $x$ a variable. There is a formula $\phi'$ such that $\vdash \phi \leftrightarrow \phi'$ and $t$ is substitutable for $x$ in $\phi'$.

Using this, we can (re)define $\phi(t)$ to mean $\phi'[t/x]$ where $\phi'$ is as in the theorem and $[t/x]$ is the syntactical substitution of $t$ for $x$. Then $\phi(t)$ is well defined up to provable equivalence for any formula $\phi(x)$ and any term $t$.

Answer by Carl Mummert for Formalizing Euclid's proof of the infinitude of primes

2011-09-21T01:10:32Z

Two points. The first is that one theory that is sufficient for the task is PRA - primitive recursive arithmetic - or any theory that interprets it. The definition in the question works fine in that setting. There are weaker theories where you can code things, as well. The key point is that in PRA there is a definable unary function Set($n)$ which says $n$ codes a "finite" set, and a definable binary relation Element($n$,$k)$ which says that $n$ is an element of the set coded by $k$. These have the property that for every $l$ in any model of PRA there is a $k$ which codes the "finite" set of numbers $n < l$ that are prime.

This sort of coding requires quite a bit of work to set up, but it is viewed as completely routine unless you try to really plumb the depths of the weakest possible theory. PRA is already an extremely weak theory.

Second, there is some benefit to rephrasing things before formalizing them. Rather than proving "no finite set of primes includes all the primes", it is more natural in arithmetic to prove "the set of primes is not bounded". These are equivalent in the real world, but the latter entirely avoids the issue of coding finite sets. We still have to prove, by induction, that for every $k$ there is an $n$ that is a multiple of every prime less than $k$ (using the method from the question to define $k!$); that if $a | n$ then $a \not | n+1$; and that every number has a prime factor. None of these requires coding finite sets.

Answer by Carl Mummert for Variant of the usual proof method for undecidability of the halting problem

2011-09-19T11:58:46Z

The proof sketch on Wikipedia uses a very common method (the same as in Proposition 4.4 of Soare's book) that relies only on universality of the computation system and on closure properties of the class of computable functions. It won't make any mention of Turing machines directly, or any other specific model of computation. This is what I think of as the "usual" approach, which could be only half-jokingly described a "get away from Turing machines as fast as possible". The motivation is that computability theory is the study of computable function, not Turing machines.

Independence of being an integer

2011-09-09T23:04:38Z

In this MO question, the OP asked for an example of a statement which was known not to be independent of ZFC, but for which the truth value was unknown. I immediately thought of a question I asked on math.SE: is $e^{e^{e^{79}}}$ an integer? This is apparently an open question, but I realized after some thought that I don't know how to prove it is decidable in ZFC.

If the number is not an integer, this can be proved in ZFC, because that fact could be expressed by an arithmetical sentence saying there is an integer $n$ such that the sum of a certain definable series is greater than $n$ and less than $n+1$. This sentence can be seen to be $\Sigma^0_1$ by standard techniques, and any true $\Sigma^0_1$ sentence is provable in ZFC.

But if the sum is an integer, it does not seem obvious that this must be provable in ZFC. In general, only $\Sigma^0_1$ statements have to be provable if they are true, and the claim that a certain definable series sums to an integer is $\Sigma^0_2$ rather than $\Sigma^0_1$.

Moreover, it's not hard to see that there are definitions of sequences $(a_n)$ in ZFC such that ZFC proves that $\sum a_n$ converges but ZFC doesn't prove this sum is an integer and ZFC doesn't prove it is not an integer. These sequences can be constructed using the incompleteness theorem in the usual way. In fact, we can make $0 \leq a_n \leq 2^{-n}$ for all $n$, so there is no issue with the rate of convergence.

But there must be something special about $e^{e^{e^{79}}}$ that means either ZFC can prove it's an integer, or can prove it's not an integer - right?

Answer by Carl Mummert for What's a magical theorem in logic?

2011-08-30T13:01:10Z

Kleene's recursion theorem says, informally, that when we write a program for a computable function we may assume that the program already has access to its own source code.

More formally, the theorem says that if $f\colon \mathbb{N} \to \mathbb{N}$ is a total computable function (which we view as a method that constructs a program $f(e)$ from a program $e$) there is some program $e_0$ such that the computable function with program $e_0$ is the same function as the function with program $f(e_0)$.

A trivial application: if $f(e)$ is a program that simply outputs $e$ and stops, the program $e_0$ outputs its own source code.

One of the magical applications of the recursion theorem is the lemma on effective transfinite recursion in hyperarithmetical theory, which is one of the key tools in that setting.

Answer by Carl Mummert for What's a magical theorem in logic?

2011-08-30T12:09:01Z

Cut elimination shows that if a sentence is provable in first-order logic, it is provable with a particularly nice type of proof in a natural deduction system without the "cut" rule, which is essentially modus ponens in that system. In particular these proofs have the subformula property – every formula in the entire proof is a subformula of the formula being proved.

The cut elimination theorem and its generalizations are key tools in proof theory. Gentzen proved cut elimination in 1934 and used it as part of his consistency proof of Peano arithmetic; there is a nice survey article "The art of ordinal analysis" by Michael Rathjen in Proc. ICM 2006.

The cut elimination theorem can be used to give nice proofs of the Craig interpolation theorem and other theorems from logic; one exposition is Chapter 6 of "Logic for Computer Science" by Jean Gallier.

Answer by Carl Mummert for True by accident (and therefore not amenable to proof)

2011-08-25T12:26:00Z

The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language. A similar analysis works for any effective theory stronger than PA, such as ZFC.

Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra (*).

Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra
If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability
Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

*: Traditionally, a "Lindenbaum algebra" or "Lindenbaum–Tarski algebra" should be defined with the dual ordering of the ordering I use. But the ordering in which $0=1$ corresponds to the top of the algebra matches better with the diagrams we create to illustrate relationships between different axiom systems, such as 1. People also use the reverse ordering in the context of set theory, where large cardinal axioms are sorted by consistency strength, e.g. 2.

Answer by Carl Mummert for Notion of Truth and Axioms

2011-08-21T12:01:35Z

The proof of the incompleteness theorem can already be done syntactically, ignoring truth, if we remove the conclusion that the Gödel sentence is true and leave only that it is neither provable nor disprovable. In particular, the "usual" proof of the incompleteness theorem is syntactic once we move to Rosser's version. For Gödel's version, there is an extra hypothesis of $\omega$-consistency, which is directly about truth in the metatheory: $\omega$-consistency corresponds to the reflection scheme $\operatorname{Pvbl}_T((\exists x)\psi) \to (\exists x)\psi$ where $\psi$ is quantifier-free. The explicit use of this assumption was elided in the question, but it become more obvious if we write the formalized provability predicate $\operatorname{Pvbl}_T$ instead of "is provable".

If we start asking what axioms are used in the metatheory, we need to move to a formal metatheory. One good reference for this and everything in the question is Smorynski's article in the Handbook of Mathematical Logic. He covers in detail the question of what metatheory is sufficient. The short version is that for an effectively axiomatized theory $T$ that meets the hypotheses of the incompleteness theorems (with Rosser's trick), PRA will prove $\operatorname{Con}(T) \to \operatorname{Con}(T + \lnot \operatorname{Con}(T))$. There is no notion of "truth" in the language of PRA to begin with, and this proof is just syntactic.

In general, axiom schemes in the metatheory containing sentences of the form $\operatorname{Pvbl}_T(\phi) \to \phi$ are called "reflection" schemes in the context of arithmetic. They have been studied in detail, and Smorynski spends several pages on them in his article. Another reference, which I have been meaning to read but haven't had the chance yet, is Axiomatic Theories of Truth by Halbach. I think Halbach's book should be very related to the topics in this question.

Answer by Carl Mummert for ZFC, set membership and FOL

2011-08-12T11:16:34Z

Properly speaking, the signature of ZFC includes a binary relation symbol rather than a binary relation. In set theory this symbol is usually denoted $\in$ but it could be denoted equally well as $R$ or $\prec$. In an arbitrary model of set theory, the "sets" might actually be any objects: cats, books, chairs, etc. But if we're are only interested in the elements qua elements of that model, we would likely call them "sets" anyway, and call the relation "membership", in the context of that model.

It is very common, when talking about a first-order theory, to conflate the symbols in the theory with their intended interpretations. For example, when we define Peano arithmetic in the signature of ordered rings, we might say that the signature has a single binary addition function $+$. Of course we already know what the "addition" function is on natural numbers, but the interpretation of the $+$ function in an arbitrary model of PA may have very little to do with addition on natural numbers. Nevertheless we usually call the elements of an arbitrary model of PA the "numbers" of the model, and we call the interpretation of the $+$ symbol the "addition" on those numbers. It's simply too cumbersome to say "The objects in the model which are intended to be numbers" or "the function in the model which is intended to be addition".

Similarly, even though the elements of an arbitrary model of ZFC might not "really" be sets, or the interpretation of the $\in$ symbol may not really be set membership, we often speak as if they are. The key observation is that, if someone "lived inside" the model, and only had access to the $\in$ relation, that person would have no way to tell that the things they see are not sets. One way of making this observation precise is the following lemma, which is proved from "outside" a model $(X, R)$ of set theory.

Mostowski Collapsing Lemma. Suppose that $R$ is a binary relation in an arbitrary class $X$ (of arbitrary objects) such that:

For each $y \in X$, the collection $\{ x \in X : xRy\}$ is a set

The model $(X,R)$ is well founded – every subset of $X$ has an $R$-minimal element

The model $(X,R)$ satisfies the axiom of extensionality

Then there is a transitive class $C$ (of sets) such that the structure $(C, \in)$ is isomorphic to $(X, R)$, and both $C$ and the isomorphism are uniquely determined by $X$ and $R$.

This lemma says that if we look from the outside at a model that looks even vaguely like a (well-founded) model of ZFC, we can replace it with an isomorphic model whose elements are actually sets and whose binary relation is actually set membership. This doesn't work formally for non-well-founded models, because the actual set membership relation is well founded. But "from the inside" we wont be able to tell that any model of ZFC is not well founded.

Answer by Carl Mummert for What sets are "decidable from competing provers"?

2011-07-29T01:06:16Z

A partial answer is that the class includes all arithmetical sets, as follows. Suppose $S$ is defined by a formula $\psi(n) \equiv (\exists a)(\forall b)(\exists c)(\forall d) \cdots \phi(n, a, b, c, d, ...)$ where $\phi$ is quantifier free. By adding dummy quantifiers we can require that the quantifiers all occur in blocks of two like that, exists followed by forall. A function to decide $S$ from competing provers is as follows. First it asks $Y$ for a value of $a$. Then it asks $N$ for a value of $b$ given $a$. Then it asks $Y$ for a value of $c$ given $a$ and $b$, and so on. Once it has values for all the variables in $\phi$, it checks whether $\phi$ holds with those values plugged in. If so, it accepts $n$, and if not it rejects $n$.

If $n \in S$ then $Y$ has a winning strategy, because $\psi(n)$ is true. All $Y$ has to do is pick appropriate values for each existential quantifier, which have to exist if $\psi(n)$ holds. Otherwise, $\lnot \psi(n)$ is true, so $N$ has a winning strategy using the same technique of picking witnesses for the existential quantifiers in $\lnot \psi$.

Not every set in $S$ is arithmetical, though. As usual let $0^{a}$ be the $a$-th iterated Turing jump of the empty set. Consider $$S = 0^{(\omega)} = \{ 2^a3^b : b \in 0^{a}\}.$$ This is not an arithmetical set, but it can be accepted from competing provers as follows. First the machine looks at the input $n$ and decodes it into $2^a3^b$. If the number is not of that form the machine can just reject out of hand. If it is of that form, the machine pretends that it was given input $b$ and checks whether that number is in $0^{a}$ using $Y$ and $N$. Because an arithmetical formula for $0^{a}$ is uniformly recoverable from $a$, this can be done effectively, and $Y$ and $N$ will have the appropriate strategies because $0^{a}$ is arithmetical.

Note all the machines in this answer so far will halt on all strategies, and in fact we can give a bound on how many queries the machine will make as a function of $n$.

Answer by Carl Mummert for The Reverse Mathematics of writing a set as a union?

2011-07-27T21:32:02Z

Due to my own confusion, I had a hard time reading Ricky Demer's proof, but I think it is correct. I couldn't fit this remark in a comment so this is a community wiki post where I will try to rephrase the proof in a way that I can grasp more quickly. Maybe it will help others as well.

We work in $RCA_0$. To establish $ACA_0$ it is sufficient to prove that the range of each injective function exists. Let $f\colon \mathbb{N} \to \mathbb{N}$ be injective.

For each $i$ define $$ S_{(i,j)} = \{2i\} \cup \{ 2k+1 : j < k \land f(k) < i\} $$ The sequence $\{ S_{(i,j)} : i,j \in \mathbb{N}\}$ is uniformly definable with a bounded-quantifier formula relative to $f$ so it can be formed in $RCA_0$.

Because $f$ is injective, for each $i$ the set $\{ k : f(k) < i\}$ is bounded, and so for each $i$ there is a $j$ such that $S_{(i,j)} = \{2i\}$ . To prove that the set is bounded seems to require an argument using bounded $\Sigma^0_1$ comprehension to form the set of elements less than $i$ in the range, then using quantifier-free bounding to show the range of this is bounded. (Is there an easier way?) In general, the "bounding principle" for a class of formulas $\Gamma$ says that the image of a bounded set of numbers under a $\Gamma$-definable function is bounded.

Let $E$ be the set of even numbers. By the Union Principle, there is a set $I$ such that $E = \bigcup_{(i,j) \in I} S_{(i,j)}$. Note that if $(i,j) \in I$ then $S_{(i,j)} = \{2i\}$. Also note that for every $i$ there is at least one $j$ such that $(i,j) \in I$. Given $i$, let $h(i)$ be the first $j$ such that $(i,j) \in I$. Since $$(\exists k)(f(k) = \ell) \iff (\exists k < h(\ell+1))(f(k) = \ell)$$ we can define the range of $f$ using only bounded quantifiers. Thus we can form the range of $f$ in $RCA_0$.

Answer by Carl Mummert for truth vs. provability for ordered fields

2011-07-27T12:20:08Z

In general, the way that people approach these things is to look at provable equivalences over some fixed theory. So, for example, you could prove results of the following form:

Theory $T$ proves that any object satisfying the ordered field axioms will satisfy property $P$ if and only if it satisfies property $P'$.

The theory $T$ could be ZFC set theory, or it could be a weaker theory such as second-order arithmetic. The main point of the theory is to give some syntactical tools for manipulating the ordered field axioms and the statements of $P$ and $P'$. For example, if $P$ is the axiom of completeness (every nonempty bonded set has an supremum), the theory $T$ needs to guarantee some sets exist.

To establish positive results of the quoted form, you simply write a proof in $T$ of the desired result. The more difficult thing is to establish negative results, and this is the first time you have to think about semantics. To prove the negation of the quoted statement, it suffices to have:

A class of interpretations of $T$ such that a statement is provable in $T$ if and only if it is true in every one of these interpretations
And an example of one of these interpretations in which there is an ordered field satisfying $P$ but not $P'$, or vice versa.

It's clear on a moment's thought that the class of structures we want only really depends on the proof rules we have in $T$, not on our intended interpretation of $T$. In the case that the proof rules are the usual ones, we have a general theorem that the set of all "first-order stuctures" is a sufficient class of interpretations to achieve the first bullet. This works not only for first-order logic, but also higher-order logic and set theory, which have the same sort of proof system.

Finally, let me point out a trivial exercise that underscores the need to look at provability rather than truth. For any effective, consistent theory $T$ that is sufficiently strong, and any statement $\phi$ provable in $T$, there is a statement $\phi'$ that is equivalent to $\phi$ but so that $T$ does not prove $\phi \leftrightarrow \phi'$. Namely, $\phi'$ says "$\phi$ and $T$ is consistent". This sort of method shows that the question in the third paragraph of the question has a negative answer, and this would be true no matter what effective consistent proof system we choose.

Answer by Carl Mummert for Most 'unintuitive' application of the Axiom of Choice?

2011-07-15T03:01:43Z

One counterintuitive aspect of the axiom of choice is a theorem of Diaconescu and independently Goodman and Myhill that, in some constructive set theories that don't begin with the law of the excluded middle, the axiom of choice implies the law of the excluded middle. But in other systems such as Martin-Löf type theory, the corresponding form of the axiom of choice is completely constructive and does not imply the law of the excluded middle.

Answer by Carl Mummert for Undecidable theories easier than $Q$

2011-07-05T18:04:26Z

When I was looking around trying to find some inspiration to answer your question, I found the following result of Feferman from 1957:

For any set $X$ of natural numbers there is a theory $T(X)$ such that:

The set $X$ and the set of Gödel numbers of consequences of $T(X)$ have the same degree of unsolvability.

If $X$ is r.e. then $T(X)$ is effectively axiomatizable.

Because there are nonzero r.e. Turing degrees strictly weaker than $K$, I think this may answer the question.

The result is in the paper "Degrees of Unsolvability Associated with Classes of Formalized Theories", Solomon Feferman, The Journal of Symbolic Logic, Vol. 22, No. 2 (Jun., 1957), pp. 161-175. http://www.jstor.org/stable/2964178

Answer by Carl Mummert for Completeness vs Compactness in logic

2011-06-26T03:12:39Z

This is a side comment. There are several answers that explain why compactness is so important in model theory, and I agree with what they say. But I want to point out that the "in model theory" part is key here. In the overall study of logic, not restricted to model theory, both compactness and completeness are important, and each of those has areas of logic that favor it. Model theory, being a semantic field, naturally identifies more with semantic notions.

In mathematics outside logic, I think there is more implicit use of completeness than of compactness. Every time I prove that an identify is derivable from the the axioms of a group by working semantically and showing that the identity holds in every group, I am implicitly using the completeness theorem. It is easy to miss this or take it for granted, because the completeness theorem is so well known.

There are systems that do not have complete deduction systems; one example is second-order logic with full second-order semantics. In this system it is perfectly possible for something to be true in every model without being provable in our usual proof system. Therefore, when we study this system in logic, we have to keep a close watch on whether we have shown something is provable, or just shown that it is logically valid.

Imagine the difficulties in an alternate world where mathematicians have to distinguish between "true in all groups" and "provable from the axioms of a group". The completeness theorem is what lets us ignore this. By comparison, it's more difficult to see reflections of the compactness theorem in everyday mathematics.

Answer by Carl Mummert for Going to graduate school for mathematics next year, need some advice

2011-06-17T23:09:57Z

(1) Many graduate programs have a relatively fixed curriculum for first year students. Some require courses to prepare you to pass exams, others require courses for exams you don't do well enough on when you arrive. So you may not have complete freedom when you arrive, and only an advisor at the school you are going to can help you with that.

(2) If you are going into a PhD program, you should keep in mind that you will need to transition relatively quickly into a specialization (within a couple years at the longest). You have to write a dissertation for a PhD, and that means finding a thesis advisor and taking specialized courses to prepare. How quickly this transition happens depends, again, on what school you are going to.

Answer by Carl Mummert for Models of computation with decidable halting problem?

2011-06-16T14:23:39Z

Joel Hamkins points out that the decision procedure for any reasonable notion of "computability" is not going to be solvable by a function that is "computable" within that notion.

Here is a contrasting example of a nontrivial model of computation in which the halting problem is solvable in the usual sense of computation. An index $e$ in our new system is a pair $(e_1, p)$ where $e_1$ is an index for a Turing machine and $p$ is a code for a polynomial over $\mathbb{N}$. In our new system, program $e$ is said to compute output $o$ on input $n$ (write $P_e(n) = o$) if and only if Turing machine $e_1$ computes $o$ on input $n$ in less than $p(|n|)$ steps. If $e_1$ runs for more then $p(|n|)$ steps then we say the computation of $P_e(n)$ is undefined (i.e. does not halt). Here we assume the Turing machine uses binary coding for numbers and we let $|n|$ be the number of bits required to express $n$ in binary notation.

This restricted model of computation is relatively common in the study of polynomial-time computability, where an index of the form $e = (e_1, p)$ is called a "polynomially clocked Turing machine". It's immediate from the definitions that a function is computable in the restricted model if and only if it is computable in polynomial time. Thus the model includes a very wide class of functions. However, because the time bound for index $e$ is already included in $e$, we can solve the halting problem for this model of computation with a normal Turing machine. (We cannot solve it with any polynomially clocked machine, of course.)

Comment by Carl Mummert

2013-05-19T17:27:17Z

This is one of those situations where it would be possible to replace an axiom with a weaker rule of inference. We could consider a comprehension rule of inference which says that when we prove that $(\forall n)[\phi(n) \leftrightarrow \psi(n)]$ then we can assert the existence of $\{n : \phi(n)\}$. That would give a significantly weaker theory than $\mathsf{RCA}_0$.

Comment by Carl Mummert

2013-04-24T17:32:26Z

It's also necessary to be very specific about what you mean by a Dedekind real. The original definition, due to Dedekind, is that a Dedekind real is a certain kind of partition of $\mathbb{Q}$, but that is not the definition typically used in constructive mathematics. This difference in terminology can cause significant confusion when trying to compare different results about "Dedekind reals".

Comment by Carl Mummert

2013-02-21T03:11:22Z

Surely Cohen's original model is an $\omega$ model, which will satisfy Con(ZF)?

Comment by Carl Mummert

2013-02-18T00:24:21Z

Because every compact metric space is separable, the theorem can be formalized in second-order arithmetic, where it is provable in $\mathsf{WKL}_0$.

Comment by Carl Mummert

2013-01-27T19:43:19Z

@François I read the question as looking for natural examples of statements provable in $Z_2$ but not FPA. Of course there are many such statements: "addition is total". To try to exclude this type of example, we restrict to statements that are true in all full models of FPA. Of course we can't assume the statements are true in all Henkin models of FPA, because they would be provable. So we want statements that are true in all Henkin models of $Z_2$, not true in all Henkin models of FPA, but true in all full models of FPA. There are still examples, e.g. $G_{FPA}$, but are there natural ones?

Comment by Carl Mummert

2013-01-27T19:20:03Z

The answer to the question near the bottom is "no": the Gödel sentence for FPA, $G_{FPA}$, is true in all standard models of FPA, and is provable in $Z_2$ (because $Z_2$ can verify that the one-element model $\{0\}$ satisfies all the axioms of FPA, hence that FPA is consistent, and thus $Z_2$ is able to prove $G_{FPA}$). But $G_{FPA}$ cannot be provable in FPA (it does not matter whether FPA is "sufficiently strong" as long as it is true). The more interesting question is whether there is a more natural counterexample. I think that is an interesting question but I have no example in mind.

Comment by Carl Mummert

2013-01-26T15:46:20Z

The signature for second-order arithmetic ($Z_2$) has function symbols for successor, addition, and multiplication. In a model, these must be interpreted as total functions. So we cannot literally "remove the assumption about the totality of the successor relationship" by just removing the successor axiom. There isn't any such successor axiom in $Z_2$ to remove. The most likely option is to replace the signature of $Z_2$ with an entirely relational signature, which is fine, but it is not as straightforward as simply removing an axiom from $Z_2$ (and what about addition and multiplication?)

Comment by Carl Mummert

2013-01-24T23:20:06Z

The issue is that the "second-order arithmetic" in which Con(PA) is provable is a two-sorted first-order theory, and the provability is still first-order provability in that theory. The real difference between first-order logic and second-order logic is only in semantics, not in derivability. Similarly, to talk about provability in MA2 we must write down a set of axioms for MA2, in which case, for the purposes of studying provability, we will want to view MA2 as a two-sorted first order theory with those axioms (because provability is equivalent to validity in first-order semantics).

Comment by Carl Mummert

2013-01-24T23:18:59Z

Of course, these are the only models in full semantics. In Henkin semantics MA2 will have infinite models as well, by the compactness theorem, and so it is not immediately clear to me that it proves the four-squares theorem. After all the collection of elements that are the sum of four squares is already definable in MA1 and so the induction principle holds for it there.

Comment by Carl Mummert

2013-01-24T14:32:42Z

I think this question is a better fit for math.stackexchange.com . This site is primarily aimed at research-level questions, but this question is a more elementary question about computability.

Comment by Carl Mummert

2013-01-24T13:43:03Z

@Adam Epstein: no, it just doesn't give an example at all; I could have phrased my comment more clearly. The underlying issue is that there is not really such as thing as "second order provability" because there is no effective deduction system that is sound and complete for full second-order semantics. When we want to talk about "provability in ZFC2" we end up working with Henkin (first-order) semantics for ZFC2, basically treating ZFC2 as a two-sorted first-order theory.

Comment by Carl Mummert

2013-01-24T13:11:58Z

We have to be somewhat careful about something. The result states that if $V_k$ is a model of ZFC2 in full-second order semantics, from the point of view of the metatheory, then $V_k$ is inaccessible, also from the point of view of the metatheory. However, this proof is not itself carried out in ZFC2, it is carried out in the metatheory, and so it does not directly give a statement that is provable in ZFC2 but not in ZFC. In fact the result in the first sentence is a theorem of ZFC, which happens to be a theorem about sets $V_k$ that satisfy ZFC2.

Comment by Carl Mummert

2013-01-24T13:07:14Z

I am not sure that this really adds any interest to the other result mentioned in the question. We know that the theory of rings is "very incomplete", so it is not particularly surprising to find an incompleteness in it that is resolved by adding more axioms. The interest in Peano Arithmetic is that, while it is still incomplete, it does prove virtually every "natural" true statement about elementary number theory, which is what makes it interesting to find anything even half-natural that PA cannot prove.

Comment by Carl Mummert

2013-01-07T13:15:54Z

Isabelle/HOL is a concrete example of a proof assistant using type theory. I completely agree that ETCS is easier to understand as variety of type theory, in the sense that ETCS regards each set as its own type, and the "element" relation as a fact about the type of the element. However, I'm not yet convinced that learning to do mathematics in ETCS specifically is likely to help with proof assistant use. Natural-language math is done in a complex type theory already, so most mathematicians are accustomed to thinking this way. Learning formal type theory might be a better preparation.

Comment by Carl Mummert

2013-01-07T13:05:15Z

I believe the issue arsmath and Asaf are addressing is that even though the real number 2 is a different set in ZFC than the natural number 2, if we take a subset of the natural numbers (e.g. the even numbers), the elements of that subset are still natural numbers, and if we take a subset of the reals, the elements of the subset are still real numbers. ETCS avoids this by changing the meaning of "subset", as it must because of its changed meaning of "element". Venn diagrams seems to be much more complex to explain in ETCS.