A fairly detailed exposition of Frege's technical work is given here, "Frege's Logic, Theorem and Foundations of Arithmetic", by Ed Zalta. Much of the reconstruction of Frege's work on arithmetic only began in the 1980s. It appeared in work by Crispin Wright, George Boolos and Richard G. Heck (in particular, see Richard's recent book, "Frege's Theorem").

Over the term, I've occasionally written down some notes for my own students and related to that here is a modernized version of Frege's proof that $0 \neq 1$. Suppose we assume there are collections and relations, and we make this more exact using second-order comprehension axioms:

$\mathsf{C}_1: \exists A \forall x(Ax \leftrightarrow \phi(x))$.Suppose we assume that, for each collection $A$, there is a cardinal $c(A)$. Suppose we assume

$\mathsf{C}_2: \exists R \forall x,y(Rxy \leftrightarrow \phi(x,y))$

$\dots$

$\mathsf{C}_n: \exists R \forall x_1, \dots x_n(Rx_1\dots x_n \leftrightarrow \phi(x_1,\dots, x_n))$.

$\dots$

$\mathsf{HP}: c(A) = c(B)$ iff $A \sim B$.where "$A \sim B$" means that there is a bijection between $A$ and $B$ (i.e., they are equinumerous).

The formal system containing these axioms is called Frege Arithmetic ($\mathsf{FA}$).

Now we define:

$\varnothing x := (x \neq x)$.Now we have:

$0 := c(\varnothing)$

$\{\varnothing\}x := (x = 0)$.

$1 : = c(\{\varnothing\})$.

$\mathsf{FA} \vdash 0 \neq1$

**Proof**: Reasoning in $\mathsf{FA}$, suppose $0 = 1$. So, by $(\mathsf{HP})$, $\varnothing \sim \{\varnothing\}$. So, there is a bijection $f: \varnothing \to \{\varnothing\}$. This leads to a contradiction. Hence, $0 \neq 1$.

I do not think you need any comprehension at all for this argument. You are not showing that a certain relation exists, but rather that it does not.

ReplyDeleteIt's worth paying close attention to this sort of matter. There's been a lot of work recently, in fact, about what you can get out of HP with weak background logics. Albert Visser has a paper "Hume's Principle: Beginnings" in RSL 4 (2011), 114-29, and I have a paper "Frege Arithmetic and 'Everyday Mathematics'" that is on my website. In the latter, for example, I should that if you assume only the existence the empty concept and empty relation, and a principle of adjunction, then, using Frege's definitions, you can prove the axioms of a relational form of (a slight but still essentially undecidable) weakening of Robinson's system R. Assuming only predicative comprehension, we can do the same for Q.

Actually, one more comment: Whether you need any comprehension will depend upon how you handle the cardinality operator. If you treat it as a functor, attaching only to variables, then you need to know that the empty concept and 'x = 0' both exist. If you treat it as a vbto, attaching to formulas, then you do not.

ReplyDeleteRichard,

ReplyDeleteYes, I agree - thanks!

In the formulation above, $c(.)$ attaches to second-order variables giving a first-order term. So, the atomic formulas are of the form $x = c(A)$. Then a teeny bit of comprehension is used to assert (in Church's notation) the existence of $\lambda_x[x \neq x]$ and $\lambda_x[x = 0]$.

Cheers,

Jeff