Wikipedia:Reference desk/Archives/Mathematics/2010 December 2

Welcome to the Wikipedia Mathematics Reference Desk Archives
The page you are currently viewing is an archive page. While you can leave answers for any questions shown below, please ask new questions on one of the current reference desk pages.

December 2

ZFC as a set of construction rules

Suppose we reword ZFC as a set of rules that allow us to construct sets, like this:

1. $\varnothing$ is a set.
2. If $x$ and $y$ are sets, then $\{x,y\}$ is a set.
3. If $x$ is a set, then $\bigcup _{y\in x}y$ is a set.
4. If $x$ is a set, then there exists the set $\{x,x\cup \{x\},x\cup \{x\}\cup \{x\cup \{x\}\},...\}$.
5. ..... (for every other axiom of ZFC)
6. No other objects are sets except those that are considered sets by finite application of the above rules.

My question is: would $V=L$ hold in the resulting theory, or would it still be independent? - Sikon (talk) 05:56, 2 December 2010 (UTC)

Certainly taking L of a model of this would result in a model. My first impression is that this system would have only a single model (which isn't impossible, since we've left first order logic). Thus, taking "theory" to mean "the collection of sentences true in every model", it would imply V=L. Taking "theory" to mean "the closure under proof" would require specifying some proof calculus.--203.97.79.114 (talk) 07:20, 2 December 2010 (UTC)

Leaving aside the problem that this kind of construction only makes sense if you are selecting sets out of an a priori given model of set theory, your set of rules is not well-defined (which you've conveniently hidden by the dots), because ZFC is not a predicative theory. Specifically, for the schema of replacement, the rule would need to be

• If x and u₁, ..., u_n are sets, $\phi$ is a formula, and for every set y there exists at most one set z such that $\phi (y,z,u_{1},\dots ,u_{n})$, then $\{z\mid \exists y\in x\,\phi (y,z,u_{1},\dots ,u_{n})\}$ is a set.

However, since $\phi$ may contain unbounded quantifiers, you cannot evaluate it until you fix the whole model, hence the definition is circular.

Something like this construction should work for predicative theories, giving you a minimal model of the theory in question. For example, I believe that if you do it for the Kripke–Platek set theory with the axiom of infinity, you'll get the admissible set $L_{\omega _{1}^{CK}}$ (which is, indeed, a model of V = L).—Emil J. 12:59, 2 December 2010 (UTC)

This seems to me to only be circular if you're trying to use it to build a model in omega many steps. If we instead take this as a descriptive axiomatization, I don't see the problem. We simply have an axiom that asserts that for every set, there is a finite sequence of applications of the above rules which generates said set (of course "finite" would need to be external to the model). We allow the quantifiers in comprehension and replacement to range over the entire model, as desired--203.97.79.114 (talk) 13:22, 2 December 2010 (UTC)

I doubt this is what the OP meant, but anyway. First, there is no way how to reformulate the axiom of choice in this way, so I will just ignore it. Actually, the same goes for the axioms of extensionality and regularity. Then the following are equivalent:

1. M is a model of ZF(C) of the form you describe (i.e., every element can be obtained by a finite application of operations corresponding to the axioms, interpreted in the model itself).
2. Every element of M is (parameter-free) first-order definable.

1→2 can be proved by induction on the number of steps, as all the operations are definable. For 2→1: assume an element t of M is defined by a formula $\psi (u)$ (i.e., t is the unique element satisfying this formula). Then we can apply the replacement operation on x = {∅} with $\phi (y,z)$ being the formula $y=\varnothing \land \psi (z)$ to construct the set {t}, and apply the sum-set operation to construct $t=\bigcup \{t\}$.

There are many models of ZFC such that every element is definable. In particular, if N is any model of ZFC that has a (parameter-free) definable well-ordering of the universe, then N has definable Skolem functions, hence the set M of all definable elements in N is an elementary submodel of N, and therefore it is a model of ZFC with the required property. The universe has a definable well-ordering for example if V = HOD, and it is relatively consistent with ZFC that V = HOD ≠ L, thus the answer to the original question would be "no, still independent".—Emil J. 14:25, 2 December 2010 (UTC)

If V=L holds here, the axiom of choice will follow, so in that case one wouldn't need to explicitly formulate it. As for the axioms of extensionality and regularity, won't they automatically hold given that we're restricting ourselves to constructing well-founded sets from existing well-founded sets? - Sikon (talk) 20:34, 2 December 2010 (UTC)

You have to be a little careful to distinguish between theories and models. As you stated the problem originally, you were talking about a theory (albeit in infinitary logic), but much of the way you're discussing it is more appropriate to models.

Assuming Emil's equivalence argument is correct (I haven't checked it), the point is that your theory will hold in every model whose every element is definable in the model. There are ways of getting such a model, without making V=L true. For example you could start with the model L[U], where you are given an ultrafilter U on a measurable cardinal and you construct with that. That model doesn't have every element definable, but you can take the Skolem hull of the empty set inside L[U], and it will have every element definable. And it is elementarily equivalent to L[U], so it satisfies V!=L.

(Then you can even take the Mostowski collapse of that Skolem hull, and have a model whose elementhood relation agrees with the true one.)

However, any such model will satisfy AC (even if it doesn't satisfy V=L) because AC follows from V=HOD. --Trovatore (talk) 21:55, 2 December 2010 (UTC)

Oh, just by the way, I didn't check that Skolem hull points anywhere useful before linking it, and unfortunately it doesn't. Someone should really write that up. Anyway, if you don't know what a Skolem hull is, let me know and I'll say something about it, unless someone else gets there first. --Trovatore (talk) 00:31, 3 December 2010 (UTC)

Chebyshev Polynomial Coefficients

Letting $T_{m}(x)$ denote the Chebyshev polynomial of the first kind of degree m and let $a_{m,n}$ denote the coefficient in $T_{m}$ of the nth power of x.

Now, what I discovered is that

$a_{m,0}=-1^{m/2}$ for even m, 0 otherwise.
$a_{m,1}=-1^{(m-1)/2}.m$ for odd m, 0 otherwise.
$a_{m,n+2}=-{\frac {a_{m,n}(m^{2}-n^{2})}{(n+2)(n+1)}}$, for $n\geq 2$.

Is this a known result? Readro (talk) 10:28, 2 December 2010 (UTC)

Our article gives an explicit formula

$T_{n}(x)={\frac {n}{2}}\sum _{k=0}^{\lfloor n/2\rfloor }(-1)^{k}{\frac {(n-k-1)!}{k!(n-2k)!}}(2x)^{n-2k}$

which can be reformulated in your notation as

$a_{m,n}={\begin{cases}\displaystyle m(-1)^{(m-n)/2}{\frac {{\bigl (}{\frac {1}{2}}(m+n)-1{\bigr )}!}{{\bigl (}{\frac {1}{2}}(m-n){\bigr )}!\,n!}}2^{n-1},&{\text{if }}n\equiv m{\pmod {2}},\\0,&{\text{otherwise.}}\end{cases}}$

Your recurrence is an easy corollary.—Emil J. 14:55, 2 December 2010 (UTC)

It's a trivial consequence of the known recursion $a_{m,n}=-a_{m-2,n}+2*a_{m-1,n-1}$, together with the fact that $a_{m,n}$ is zero if n < 0 or m < n. – b_jonas 14:57, 2 December 2010 (UTC)

You shouldn't write

$-1^{n}\,$

when you mean

$(-1)^{n}.\,$

In conventional use, these have two different meanings. Michael Hardy (talk) 15:35, 3 December 2010 (UTC)

Computerised proofs

If I had an arbitrarily fast computer, could I brute-force check all possible mathematical proofs (that is, all possible combinations of some set of symbols up to some absurd length), and thereby either prove any given mathematical fact or effectively show that no proof was possible? Does the answer depend a lot on the "type of mathematics" involved?

This is a question about whether the steps of mathematical proof can in principle be codified in such a way that every possible proof may be generated and checked by a computer. It is not a question about the practicality of doing so. I understand that the number of combinations involved is unimaginably vast compared with the capabilities of present or foreseeable technology. 86.185.77.138 (talk) 14:25, 2 December 2010 (UTC).

It is (in principle) possible to systematically generate and check mathematical proofs by a computer, but since the number of possible proofs is infinite, the program would never halt if the given statement is not provable, it could not give the answer that the statement has no proof. This is an inherent property of any such algorithm: by Church's theorem, it is not algorithmically decidable whether a given statement is provable.—Emil J. 14:34, 2 December 2010 (UTC)

Further, many proofs are based on an open-ended set. Consider the statement "All prime integers greater than 2 are odd." You could write az program to check every integer greater than 2, but you will never check all of them because the set is open-ended. Every time you find a new big prime, there will be another one to check that is larger. In that case, a better proof would be to assume that the statement is false. An integer greater than 2 is even and prime. If it is even, it is divisible by 2, so it cannot be prime. Done. -- kainaw™ 14:42, 2 December 2010 (UTC)

A proof is always a finite object. You seem to confuse it with something, though I'm not quite sure with what. A proof of the statement "all prime integers greater than 2 are odd" has nothing to do with checking infinitely many integers one by one, it is a finite derivation of the statement from some axioms.—Emil J. 15:02, 2 December 2010 (UTC)

• I may not have asked my question clearly enough. When I asked if it was possible "in principle", I meant to exclude the practicalities of building a computer fast enough, but not the practicalities of actually identifying and codifying all the possible steps in a mathematical proof so that they can be manipulated symbolically. Given the current state of the art, is such a thing possible in any or all mathematical fields? Or might I run my hypothetical proof-checking program against some problem and proclaim that no proof exists shorter than some absurdly large size that I specify, only for a human mind to later devise a method of proof that my symbol manipulation overlooked? 86.186.34.238 (talk) 20:36, 2 December 2010 (UTC).

First-order logic is semi-decidable, and expressive enough to encode much of mathematics. Semi-decidability in this context means that you can prove all true statements if you throw enough resources at it. But you don't know how much to throw, so you can not, in general, disprove existence of a proof (there are many practically relevant cases where you can do so, but similarly many where you can't). You can certainly search for proofs up to a certain lengths in a certain calculus, and exhaustively search that space to exclude all shorter proofs. But that does not preclude a shorter proof in a different calculus, and it becomes prohibitively expensive (in the sense of "not enough elementary particles in the universe to represent the states in the search space") very quickly. --Stephan Schulz (talk) 22:23, 2 December 2010 (UTC)

Thanks, is it possible to give a flavour in simple language of what you mean by "in a certain calculus" and "in a different calculus"? 86.186.34.238 (talk) 23:10, 2 December 2010 (UTC)

For first-order logic, we usually use proof by refutation and a calculus like resolution. Resolution is a way to derive new clauses from old ones, and the goal is to derive the empty clause (an explicit contradiction). If you systematically and exhaustively apply the rules of the resolution calculus, you will eventually derive the empty clause from any unsatisfiable (=refutable) clause set. A very closely related calculus is the connection tableaux calculus that works on trees, trying to generate "closed" trees. Or, if you want a very contrived example, any calculus that is sound and complete remains sound and complete if you add a special rule that proves any arbitrary true statement in one step (it's sound because the only thing you can do beyond what the base calculus allows is to very efficiently prove this one thing that is true by assumption). If you want to exclude such tricks, you get into things similar to Kolmogorov complexity, and leave my comfort zone ;-). --Stephan Schulz (talk) 23:27, 2 December 2010 (UTC)

Thank you. Sorry, I have two further questions, if you can bear with me! First, when you say "First-order logic is [...] expressive enough to encode much of mathematics", would it be able to encode well-known problems like Fermat's Last Theorem, the Riemann hypothesis, the Collatz conjecture, and the Poincaré conjecture? (I'm obviously not expecting you or anyone else to do any detailed analysis of this. I'm hoping an expert might be able to say straight away something like "Yes, all those sorts of things are encodable in that way", or "Hmm, some of those things could be tricky.") My second question is about the impossibility of using this method to show that no proof exists (since one would need to go on forever). Is there a reason to believe, in reality, that relatively concise statements may need arbitrarily long proofs? For example, if I want to prove a statement that can be expressed in a couple of lines, and I run my hypothetical brute-force proof generator to check all proofs up to length 10^10,000,000,000 symbols, and I find no proof, then am I in justified in believing that no proof exists? 86.186.34.238 (talk) 01:24, 3 December 2010 (UTC).

I don't think you can make that conclusion, no. The difficulty is that human mathematical reasoning is very difficult to formalize (if indeed it's possible at all). It involves lots of meta-levels of reasoning, arguments as to why we have to look at only one case because the others are reducible, etc. I don't know of any good bound on the amount of "speedup" that can get you over, say, Hilbert-style deduction using the ZFC axioms.

A possibly indicative data point: Robert Solovay has a speedup theorem on how much faster a formal proof in ZFC can be if you're allowed to use, instead, NBG, which is a conservative extension of ZFC. It's truly enormous — something like a theorem that takes 2^2^...2 steps, with n 2's, in ZFC, might take only a tower of sqrt(n) 2's steps in NBG. Of course it's not a natural theorem being proved, but still. A human mathematician, on the other hand, might well use NBG techniques instead of ZFC ones without even particularly noticing or distinguishing. --Trovatore (talk) 01:39, 3 December 2010 (UTC)

When you say that human mathematical reasoning is difficult (perhaps impossible) to formalise, are you suggesting that results obtainable by human mathematicians may not necessarily be attainable at all using known formal (computerisable) methods, or do you think that the same results can always be attained, but perhaps only in a much more long-winded way? 86.186.34.238 (talk) 02:26, 3 December 2010 (UTC).

Well, it's an article of faith that any "rigorous" proof can be formalized. Some would take that as the definition of "rigorous proof". My doubt is that there's any uniform way of accomplishing that, of putting it into a single program.

I mean, of course, in principle there is, granted a finite human lifespan and all that; you could just take all the finitely many such proofs that humans might produce, and put together a list of them together with their formalizations. But I think you're wanting to talk about computer code that could actually be written, not that's just in principle finite. --Trovatore (talk) 20:36, 3 December 2010 (UTC)

The issue is that any mathematical theory powerful enough to include ordinary arithmetic is undecidable. For more info, see Gödel's incompleteness theorem. If you give your computer an undecidable question, it will keep running forever, i.e. you need infinitely fast, not merely arbitrarily fast. There is in fact a theory of "infinite time Turing machines"[1] that can do infinite computations but they are only in the abstract. 67.117.130.143 (talk) 02:52, 3 December 2010 (UTC)

Isn't "undecidable" included in my category "no proof exists"? 86.186.34.238 (talk) 03:17, 3 December 2010 (UTC)

It is very likely that every even number greater than 2 is the sum of two primes. However it may be that there is no proof of the that - it may be true but unprovable. How would you go about showing that no proof existed except by waiting till the end of time till all infinity of possible proofs were tried out? (By the way the article is Goldbach's conjecture and I like the bit about many more small values of n have been checked up to 1.6×10¹⁸) Dmcq (talk) 14:16, 3 December 2010 (UTC)

I understand that, but I still feel intuitively that I can pick a stupidly large number, n, and be confident that if no proof less that n symbols exists, then no proof exists at all (provided the statement to be proved is not itself stupidly long). If 10^10,000,000,000 symbols isn't enough, then make it 10^(10^(10^(10^10,000,000,000))) symbols if you want. Is it really conceivable that there is a proof of Goldbach's conjecture longer than that, but no proof shorter? 86.173.36.106 (talk) 20:19, 3 December 2010 (UTC).

I can guarantee that for any sufficiently powerful logic (e.g. first-order logic) and any given proof calculus, there are theorems that have a proof longer than any fixed number of steps or symbols. Even more, in this setting I can guarantee that if f is any total computable function, then there is a theorem T such that the lengths of the shortest proof of T is longer than f(|T|) (where |T| is the number of symbols in T). --Stephan Schulz (talk) 23:01, 3 December 2010 (UTC)

Wouldn't a proof-by-induction invalidate the "stupidly-long-proof" concept? For any complex idea, there is at least one idea "slightly" more complex. So, if any particular complex idea can be proved using a minimum of N characters, then the next more-complicated idea will require at least N+1 characters (because it requires "idea N" as a predicate, for example). So, select your maximum-character threshold, and you are effectively setting the maximally-complex proof you can sustain. Nimur (talk) 23:24, 3 December 2010 (UTC)

I believe Gregory Chaitin has written a bit about theorems and proofs which we'll never be able to comprehend because they are too big to hold in our puny minds. Dmcq (talk) 01:31, 4 December 2010 (UTC)

(off topic rant) From what little I've read by Chaitin, I warrant that if you can't find the deeper meaning in his work it is because there is no deeper meaning to find. Eric. 82.139.80.218 (talk) 04:46, 4 December 2010 (UTC)

Trovatore, when you said The difficulty is that human mathematical reasoning is very difficult to formalize (if indeed it's possible at all). It involves lots of meta-levels of reasoning, arguments as to why we have to look at only one case because the others are reducible, etc., I cannot agree more with this than any other thing in my life. I've always wondered if the crazy reasoning can be coded in ZFC or some other set theory at all. One thing is in "real math" we quantify over many separate domain, when we are supposed to quantify over all sets. Also, for the generalized associate law, can it even be expressed within the language of ZFC? To me it's a metatheorem that must be expressed in the metalanguage (for example in the metalanguage of groups). These are just two of my "concerns", do you know any source where they develop ordinary everyday mathematics formally? Money is tight (talk) 04:56, 4 December 2010 (UTC)

Lots of proofs have been formalized. It's just tedious. If the theorem had a rigorous unformalized proof to begin with, formalizing it usually doesn't have issues of metalogical mumbo jumbo. I've heard claims that formal proofs in the Mizar system are about 4x longer than unformalized proofs as found in math journals. You might look at the AMS Notices special issue on formalized proofs[2] to get a picture of the state of things as of a couple years ago. The articles (by Avigad and by Harrison) linked from prime number theorem#Computer_proofs about formalizing that theorem might also be of interest. 67.117.130.143 (talk) 01:51, 5 December 2010 (UTC)

I notice, though, that the article QED manifesto refers to a paper claiming that the major contenders in this field, Mizar, HOL, and Coq, have serious shortcomings in their abilities to express mathematics (though it does go on to say that Mizar has "successfully formalized a large portion of undergraduate mathematics"). I don't know much about this myself; I'm just reporting what I read. 86.135.25.44 (talk) 03:58, 5 December 2010 (UTC).