1
$\begingroup$

Here is a how a typical proof might look like in group theory--- Suppose we are given a finite group $G$. Enumerate the elements $g_1, \dots, g_n$. Now consider a formula $\phi(g_1, \dots, g_n)$ which discusses some property of $G$....

This proof is not rigorous. In any set theory I can think of, a finite set is equinumerous to $\{0, \dots, n}$ where $n$ may be a non-standard integer. So when we are proving things about finite sets, we really should allow the size of the set to be non-standard. But, at least implicitly, any proof assumes that $n$ is a standard integer.

This seems to be different than proofs of arithmetic, in which we can assume that the computations are occurring in the true structure of $\mathbf N$, which contains only standard integers. We may need extra axioms to pin down the behavior of $\mathbf N$, but we ultimately will never need the non-standard integers.

EDIT: I think I have boiled down this issue to the the following example.

We will prove that $CON(ZFC) \vdash (ZFC \vdash CON(ZFC))$, which is obviously false.

Consider the following proof. Suppose CON(ZFC) is true. Given a model $M$ of ZFC and $n$ an integer of $M$. If $n$ is a standard integer, then by assumption $n$ is not a proof of contradiction of ZFC. So we have shown that for all standard integers $n$ and all models $M$ of ZFC, $n \in M$ does not disprove ZFC. Hence, by the transfer principle, ZFC proves that all integers $n$ are not disproofs of ZFC. Hence ZFC proves CON(ZFC).

The key issue is that some formulas do behave differently for standard and non-standard formulas. In this case, the formula "$x$ is a disproof of ZFC" is a formula which picks out the non-standard integers.

Improve this question
$\endgroup$
11
  • 3
    $\begingroup$ When working with groups, you are implicitly working in enough of second-order arithmetic to make the basics of model theory function. As such, you have the categoricity theorem for $\mathbb{N}$. The lack of categoricity for first-order $PA$ occurs only because we cut back the assumption that $\mathbb{N}$ is well-ordered (since this is a second-order assumption.) What I'm really trying to say here is that non-standard elements only seem to creep in when you throw out the assumption that $\mathbb{N}$ is well-ordered. $\endgroup$
    – Not Mike
    Commented Mar 18, 2012 at 14:12
  • $\begingroup$ I believe that categoricity of $\mathbf N$ means that all copies of $\mathbf N$ look the same within the universe, but not necessarily the same as the external standard $\mathbf N$? Maybe the solution is that we work in second-order arithmetic, in which all the finite sets (of integers) actually exist, as opposed to set theory? $\endgroup$
    – David Harris
    Commented Mar 18, 2012 at 14:19
  • 1
    $\begingroup$ @David, what I'm saying is that the assumption that there is a non-standard number is so strong that $PA$ can even express it. Also, if you are using assumptions about your particular model of $ZFC$ then you are using assumptions that go beyond $ZFC$. However if you are working within the theory of $ZFC$, then there is no mention of the model, and everything you prove in the theory for $ZFC$ about $\mathbb{N}$ is (or at least should be assuming some amount of sanity) in fact being proven for the theory of $\mathbb{N}$. $\endgroup$
    – Not Mike
    Commented Mar 18, 2012 at 14:43
  • 2
    $\begingroup$ I'm pretty sure that Michael meant ‘can't’, not ‘can’. And ‘express’ means something weaker than ‘prove’ (so a formal system's inability to express something is stronger than its inability to prove it). There is no sentence (provable or otherwise) in the language of PA that one would interpret as stating the existence of a nonstandard number; PA cannot express this. $\endgroup$
    – Toby Bartels
    Commented Mar 18, 2012 at 17:16
  • 1
    $\begingroup$ @Toby, what about the statement "$x$ is a proof of the inconsistency of PA" ? $\endgroup$
    – David Harris
    Commented Mar 18, 2012 at 17:47

5 Answers 5

Reset to default
1
$\begingroup$

You are right, a lot of published proofs are non-rigorous in something like the sense you describe. See this answer and the comments attached to it:

Why is it so difficult to write complete (computer verifiable) proofs?

I remember chasing down some of the references from that post and finding them interesting too. The Bundy et paper is here: http://www.jstor.org/pss/30039733 (link courtesy of schropp on reddit).

Improve this answer
$\endgroup$
16
$\begingroup$

Your example concerning proving the consistency of ZFC in ZFC invokes the transfer principle in a situation where it simply doesn't hold. The transfer principle is for elementary extensions, so your use of it presupposes that the natural numbers of $M$ (with their addition and multiplication) form an elementary extension of the standard natural numbers. Con(ZF) will indeed be true in such $M$'s (if, as you assumed, its really true), but such $M$'s are far from being all the models of ZFC, so it wouldn't follow that ZFC proves Con(ZF).

I would also question the description, at the beginning of your message, of a typical proof in group theory. All the proofs I've seen in group theory (on its own --- not set-theoretic independence results about group theory) have been formalizable in ZFC. What they say about finite groups (or finite sets) makes perfectly good sense and remains correct if interpreted in any model $M$ of ZFC, with "finite" being interpreted in $M$ also (and therefore including non-standard finite numbers, if there are such numbers in $M$).

Improve this answer
$\endgroup$
12
$\begingroup$

Non-standard numbers do not exist in isolation but only in the context of working in a non-standard model. If we take an argument of the sort you mention and interpet it in a non-standard model, Eveything Will Be Just Fine. True, the model has some infinite numbers from which we can make strange things such as non-standardly large syntactic expressions, non-standard "finite yet infinitely large" sequences of powers $1, x, x^2, \ldots, x^n$, etc., but so what? The beauty of non-standard models is that all the "finite" proofs still work in it, so I do not understand your objection.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ I think this is really the point. When we say "a natural number", we mean a natural number in the current theory, which includes any non-standard ones. Most people don't bother to say "by induction" for "obvious" facts about N, but almost always if you pressed them, that's what they would say they meant. This is the same as the rest of math; we can't write all the details or papers would be unmanageably long. But that doesn't mean all proofs should be regarded as "non-rigorous", except in the sense that they still require "compiling" to become fully formalized. $\endgroup$
    – Mike Shulman
    Commented Mar 19, 2012 at 22:00
11
$\begingroup$

Here are a few nice quotes from treatises on non-standard analysis:

These non-standard finite ordinals do correspond to idea of “infinitely great numbers”, (that's why we call them 'unlimited'); still, they are finite ordinals, according to the mathematical definition of finity (note : a set is finite if, and only if, there is no possible bijection between one of its sub-sets and itself).

Moreover, any classical theorem that is true for all standard numbers is necessarily true for all natural numbers. Otherwise the formulation "the smallest number that fails to satisfy the theorem" would be an internal formula that uniquely defined a non-standard number.

Non-standard numbers are precisely those that cannot be uniquely specified (due to limitations of time and space) by an internal formula. Non-standard numbers are elusive: each one is too enormous to be manageable in decimal notation or any other representation, explicit or implicit, no matter how ingenious your notation. Whatever you succeed in producing is by-definition merely another standard number.

Note that the ZFC schemata of separation and replacement are not extended to the new language, they can only be used with internal formulas.

#2 tells you why it is enough to deal with standard integer cardinalities in all proofs like the one you quoted and #4 is the reason why the non-standard analysis is not quite an extension of ZFC: adding a huge set of predicates and explicitly prohibiting their usage in the old axioms of the theory to avoid any contradiction smells of cheating. Basically, IST postulates that each infinite set contains elements beyond our perception but whatever is true for all elements within our reach is true for them too. I personally consider IST one of those unwelcome monsters that feed on the unavoidable incompleteness of ZFC but I'm a known retrograde :). Nevertheless, all our standard proofs of standard properties for finite sets remain valid in IST if you just mindlessly add an application of the transfer axiom in the end, so IMHO it is a bit too early to declare them "non-rigorous".

Improve this answer
$\endgroup$
2
  • $\begingroup$ The non-standard numbers may differ from the standard numbers in satisfying certains formulas. For example, let us suppose that CON(ZFC) holds. Then the statement that "for all natural numbers $n$, $n$ is not a contradiction in ZFC" is true. However, this statement is NOT true of non-standard $n$ --- even if CON(ZFC) holds then ZFC still has non-standard models which have non-standard integers proofs of inconsistency. $\endgroup$
    – David Harris
    Commented Mar 18, 2012 at 17:45
  • $\begingroup$ @David: Not in this case. In non-standard analysis, the non-standard model is chosen to be elementary equivalent to the standard one. Any (standard) predicate is satisfied by the standard model if and only if it is satisfied by the non-standard model. In particular, if the predicate P(n) = "n is a contradiction in ZFC" is standard, then $\forall n \in \mathbb{N}: P(n) \Leftrightarrow \forall n \in {}^\star\mathbb{N}: P(n)$. $\endgroup$
    – user13113
    Commented Mar 18, 2012 at 22:38
4
$\begingroup$

I'm used to formal logic being formulated internally. The theory of groups is not an external notion to whatever mathematical universe you're working in -- instead, it is an (internal) set of strings in a set-theoretic universe, or a finite-limit sketch in a category-theoretic universe. Models are then merely set functions or functors with appropriate properties. And proof theory and model theory are all defined internally to the universe.

In particular, for any internal natural number $n$, there are perfectly good formulas $\varphi(g_1, g_2, \cdots, g_n)$.

If you had an external notion of natural number (and a corresponding external notion of formal logic), then the internally constructed version could very well be infinitary when viewed from the external perspective. But only when viewed from the external perspective: it is still finitary when viewed internally to the model.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .