User sebastian reichelt - MathOverflow

Answer by Sebastian Reichelt for Has anyone thought about creating a formal proof wiki with verifier?

2010-10-06T20:40:52Z

I think the following additional links are relevant:

http://homepages.inf.ed.ac.uk/da/mathwiki/

http://prover.cs.ru.nl/wiki.php

However, like David Lehavi I'm skeptical about the benefit of wikis over regular proof assistant technology. For me, the entrance barrier has always been learning the language and tactics of a proof assistant, not installing the software or adding something to the standard library (that is, I have never gotten that far, but if it's a problem, then it's a social one).

I agree with Tom Ridge that the time for a big collection of formal mathematics will come. But I think we should collect definitions, theorem statements, and proofs separately. That is, if a theorem is already widely known to be true, the proof should be optional, so it can be filled in later. A collection of formalized definitions and known facts would already be very useful, and most importantly, people working on different proofs can collaborate easily, whereas the formalization of definitions and theorem statements requires coordination. Of course, with current proof assistants, it's hard to be certain that definitions and statements are correct ...

Answer by Sebastian Reichelt for Demonstrating that rigour is important

2010-09-04T20:22:51Z

The way current computer algebra systems (that I know of) are designed is a compromise between ease of use and mathematical rigor. Although in practice, most of the answers given by CASes are correct, the lack of rigor is still a problem because the user cannot fully trust the results (even under the assumption that the software is bug-free). Now, it might sound like just another case of "99% certainty is enough," but in practice it means having to verify the results independently afterwards, which could be considered unnecessary extra work.

The root of the problem seems to be that a CAS manipulates expressions when it should output theorems instead. In many cases, the expressions simply don't have any rigorous interpretation. For example, variables are usually not introduced explicitly and thus not properly quantified; in the result of an indefinite integral they might even appear out of nowhere. Dealing with undefinedness is another problem.

All of this is inherent in the architecture of computer algebra systems, so it cannot be fixed properly without switching to a different design. The extra 1% of certainty may indeed not justify such a change. But if rigor had been emphasized more from the start, maybe we would have trustworthy CASes now.

I think this line of thought can be generalized. (As a non-mathematician) I can't help but wonder how mathematics would have progressed without the widespread introduction of rigor in the 19th century. I can't really imagine what things would be like if we still didn't have a proper definition of what a function is. So maybe rigor is indeed not strictly necessary in particular cases, but it has shaped mathematical practice in general.

Answer by Sebastian Reichelt for When is something too big to be a set?

2010-07-20T21:01:34Z

Just an addition to all the excellent answers, on a more informal and elementary level.

The question whether something is a set or not makes sense only if sets are treated as objects, i.e. if there is (conceptually) a "universe" which all sets reside in. This is indeed the case in first-order axiomatic set theory. In particular, in Zermelo-Fraenkel set theory, sets are actually the only objects (e.g. numbers are ultimately built from sets). Therefore, in ZF the question can be asked as "does a set/object with the following properties exist..." Other set theories have "proper classes" in addition to sets, as some have mentioned; then you can ask the question as stated.

However, in naive (i.e. non-formalized) set theory, it is far from obvious that sets should be treated as objects. For example, if the question whether "the set of natural numbers is a member of the Cartesian product of the real numbers and their power set" does not make sense to you, maybe you are not thinking of sets as objects at all. In that case, you might also consider Russell's paradox a meaningless combination of symbols. But there is one paradox which should still work; it's called Burali-Forti.

This paradox says that if you call equivalence classes of sets with well-order relations "ordinals," you can derive a contradiction by building an ordinal from the set of all ordinals. The most obvious remedy is to forbid the construction of the set of ordinals and other similar ones (or rather, specify exactly which sets can be constructed, such that the set of ordinals is not among them). So the convention in informal mathematics is to name the collection of ordinals something other than "set." But in principle, what really matters is that you don't try to build an ordinal from it. (And you wouldn't have done that anyway, right?)

The notion of "too big" sort of makes sense when looking at the Burali-Forti paradox because the contradiction follows from ordinal comparisons (which technically provides yet another remedy; see NF). However, I too consider it misleading, as it suggests that the question of whether something is a set is a question of fact rather than convention.

Most general formulation of Gödel's incompleteness theorems

2010-07-17T22:09:23Z

Modern statements of Gödel's incompleteness theorems are usually in terms of first-order predicate logic. However, I've often read the claim that they extend to arbitrary formal systems that can prove basic propositions about numbers. Indeed, according to Wikipedia, the original theorems referred to the type theory of Principia Mathematica, which is apparently not based on predicate logic.

My two questions are:

What is the most general concept/definition of a formal system for which Gödel's theorems have been stated?
How does their proof differ from the predicate logic variant?

Regarding 1., I could imagine several equally general definitions, for example based on either strings of symbols or abstract syntax trees. Being a little biased, I actually think of formal systems as data structures of more or less arbitrary computer programs, so maybe there is a definition based on Turing machines... In any case, it would need to specify what a "proof" of a "theorem" is, but I would like to do without the concept of "axioms." (See also http://mathoverflow.net/questions/29774/derivation-rules-and-godel-theorem/29989#29989.)

Regarding 2., I'm specifically thinking about the diagonal lemma (or arithmetic fixed-point theorem, or whatever it is really called). The version I know refers to a "formula with one free variable," but that presupposes such concepts as "formula" and "free variable" in the formal system, and I'm wondering how to generalize that to arbitrary formal systems. I know there are proofs of the first incompleteness theorem which take an entirely different route, but AFAIK they don't carry over to the second incompleteness theorem.

I would like to add that I don't doubt the generality of Gödel's incompleteness theorems in any way. I just feel there is a gap between their claimed general nature and the way they are usually presented. A year ago, I devised a nonstandard formal system for a proof assistant. Although it could easily formalize its own concepts and express its own consistency, a translation of Gödel's incompleteness theorems from predicate logic turned out to be surprisingly nontrivial.

Answer by Sebastian Reichelt for Derivation rules and Godel theorem

2010-06-30T00:25:49Z

First, a short answer similar to Pierre Simon's but in different words: In your definition of D, you did not state the exact derivation rules that T(K) was supposed to contain. However you make the definition of D precise, T(K) cannot contain your new rule D, since that is what you are defining.

But I think your question is interesting because, to me, it shows that the widespread view that "every formal theory is a collection of alphabet, axioms and derivation rules" can be harmful sometimes. Such a view suggests that the concepts of "axioms" and "derivation rules" are somehow inherent in the concepts of "formal systems/languages/theories." What's wrong with taking a step back and defining "formal system" in more general terms? There are many ways to do so; I would propose something along the lines of "a formal system is essentially the same as any self-contained data structure of a computer program, together with a function that validates a given instance of that data structure." (The idea being that the data structure describes "proofs" of "theorems" in some arbitrary coding.)

Please don't read too much into those intentionally vague words. My point is just that such a definition would apply to a much wider class of formal systems than just predicate logic, and in particular also to formal systems that don't know about "axioms." Interestingly enough, Gödel's incompleteness theorems seem to apply to all such systems that can encode Peano arithmetic in some way. (I'm writing "seem" only because I have often read that claim but haven't seen any proof or even a precise statement of it. I guess I should ask an MO question about this.) AFAIK, the system from Principia Mathematica which Gödel was talking about wasn't actually based on predicate logic either.

So I think your question stems from a common but somewhat artificial distinction between "axioms" and "rules." In principle, every axiom is also a rule: the rule that a given formula can be assumed without proof. (I'm only talking about foundational systems, of course, not about axioms describing mathematical structures -- though some argue that there is no difference.) In some sense, Gödel's theorems are about computability, not about axioms and rules. You cannot evade them by trying to turn axioms into rules.

Answer by Sebastian Reichelt for The isomorphism inference rule

2010-06-18T23:15:43Z

First of all, I suspect that whenever a formal system has such an "isomorphism inference rule," all proofs using that rule can be converted to proofs not using it. (I don't know the details of Bourbaki's set theory, though.)

So what could an "isomorphism rule" look like? First of all, you need a metamathematical characterization of what constitutes an "isomorphism" between arbitrary "structures." I guess category theory can answer this question, but only if you encode your specific class of structures as a category. So that does not really define isomorphism on a metamathematical level. (Unless, apparently, one works within fully categorial foundations: http://cs.nyu.edu/pipermail/fom/2003-July/007064.html)

However, there is indeed a comparatively simple way to characterize isomorphisms. This is actually part of a formal system I have developed for a proof assistant, but you can apply the same principle in naive set theory if you don't mind a little vagueness. (Don't try to apply it to first-order axiomatic set theory, though.)

There is one rule of this system that matters here: Roughly speaking, for given x and S, you may not ask whether x is a member of S unless x was introduced as a member of some superset of S. The introduction of a variable as a member of a given set is considered primitive, so the rule is purely syntactical. An example:

We want to say: "Let S be the intersection of the set of primes with the set of even integers, and n be a member of S. Then n is in N." Surely, the set of primes is defined as some subset of N, which in turn is a subset of Z, and the set of even integers is also defined as a subset of Z. So n is syntactically known to be a member of Z, and we can ask whether it is also in N. However, we cannot ask whether it is e.g. in the set of finite graphs. Or whatever else. Formally, this amounts to a type system.

Another aspect of the formal system is that when you want to define what a "group" is, you need to specify when two "groups" are considered equal. So suppose you are given two sets S and T, as well as group operations on each. There is no syntactically "known" superset, so you cannot ask whether S=T because that would involve taking an element of S and asking whether it is in T. Now convince yourself that the most you can do is ask whether the two groups are isomorphic. That is, no other formula you can come up with will ever distinguish two isomorphic groups. (It is required to be reflexive, symmetrical, and transitive, of course.)

To conclude, it is possible to construct a system in which you cannot even talk about structures except up to isomorphism, for arbitrary structures. (That does not mean you cannot take their concrete sets into account in special cases. For example, if you have a group with two isomorphic subgroups, these will be considered equal as groups, but the sets can be different. Note how it makes sense to ask whether they are equal or different because we know a common superset.)

Now here is my equivalent of your "isomorphism inference rule": Since two isomorphic groups are in fact equal in this system, any property you can specify about one of them will be considered true of the other.

Comment by Sebastian Reichelt

2011-07-14T21:08:30Z

You may be interested in [my answer to a similar math.stackexchange question](math.stackexchange.com/questions/27452/…), which describes an easy but probably less accurate method.

Comment by Sebastian Reichelt

2011-01-14T23:27:32Z

What if the contradiction is too long to be written down explicitly, but there is a systematic way of constructing it? (In the same way that for every given Goodstein sequence, there is a proof in PA that it terminates. Even though it can become arbitrarily large, we can still construct it, in a sense.)

Comment by Sebastian Reichelt

2010-08-08T22:50:54Z

Have you looked into the concept of autocorrelation (en.wikipedia.org/wiki/Autocorrelation)? One problem you'll always run into, though, is that any algorithm can only evaluate the function at finitely many places (assuming that's how the function is given; otherwise you need to be more explicit), in effect making it discrete.

Comment by Sebastian Reichelt

2010-08-07T23:33:18Z

Probably at least all Pi01 sentences should be considered realistic. So provability in some formal system doesn't seem to mean a lot (consider "ZF is consistent"). Note that certain large cardinal axioms also decide some Pi01 sentences, but AC and CH do not (see esp. the work of Harvey Friedman).

Comment by Sebastian Reichelt

2010-08-06T19:55:23Z

Maybe in set theory there is no "actual thing we're considering." My personal intuition is that sets are not objects in the sense that numbers are, and elementhood is not a relation; that we are treating set theory that way just to be able to formalize it in first-order logic. I even think that none of the well-known formal systems adequately formalize my intuition of what is or isn't a meaningful statement. But the very notion of "model" is defined only for specific formal systems. So talking about "models of ZF" makes sense to me, but talking about "models of set theory" does not.

Comment by Sebastian Reichelt

2010-07-29T06:26:04Z

Oops, I meant ZF+AD, of course.

Comment by Sebastian Reichelt

2010-07-28T22:38:50Z

If I'm getting this correctly, the set of periodic sequences is an example for 12. (Thus non-periodic leads to 10.) If only the odd-position subsequences are required to be periodic, it will be 13 instead (7 for even-position subsequences). 3, 6, and 11, if provable, require the axiom of choice, since AD would rule them out (assuming ZFC+AD is consistent).

Comment by Sebastian Reichelt

2010-07-23T16:31:03Z

Thanks. But the author explicitly writes "Let B be the set of all bilinear maps defined on VxW" and then admits that B isn't actually a set -- and I don't see how anything you say would invalidate that claim.

Comment by Sebastian Reichelt

2010-07-21T20:58:29Z

If you use the standard construction of functions via Cartesian products, how would you define a function that takes a set W as input? Otherwise, if you are talking about a more general kind of function (or functor), I don't see how you could build a set of such functions. Am I missing something?

Comment by Sebastian Reichelt

2010-07-20T19:24:54Z

Many thanks to all who answered. Your post finally made me realize that I had always interpreted the word "predicate" in a too narrow sense: I used to think of predicates as things that appear in formulas, as in "a formula is either a conjunction, or ..., or an instantiation of a predicate." So for me, "predicate" was a system-dependent concept. Now that I understand how you can retroactively define "predicates" for more general formal systems, I would like to accept both Charles Steward's and your answer in combination (i.e. your definitions + the formalized substitution operator). :-)

Comment by Sebastian Reichelt

2010-07-02T20:46:23Z

I wonder if the following naive approach might lead to a manageable number of cases: After placing a single queen somewhere, there are at least two uncovered 3x3 triangles left. You can cover them completely by placing queens in them, but if you do that for both, the remaining uncovered squares cannot be covered by a single queen. If you do it for one, the squares in the other triangle that are still not covered place some rather strong restrictions on the remaining two queens. Finally, if you place the second queen outside the two triangles, there are uncovered squares in both...

Comment by Sebastian Reichelt

2010-06-20T10:32:17Z

I'm not saying one should necessarily identify isomorphic groups in mathematical practice, but in this particular system, it just comes out that way, by virtue of having to specify when two groups are supposed to be equal. So what I called "group" is strictly speaking an "isomorphism class of groups." Properties like "simple" can be defined on such classes, and they are automatically guaranteed to be well-defined. In the case you mention, however, you would need to refer to the actual sets, not just the isomorphism classes. This is analogous to what I wrote about subgroups.