Are You Using the Right Axiomatic System?
The last decades have seen a major revolution in the performance of mathematical activity through the invention and development of several new axiomatic systems. Surprisingly, though, many mathematicians are wholly unaware of this issue and do not know precisely which set of axioms they are using. The mathematical community is deeply divided over such questions as to whether the axiom of choice should be accepted and whether existential proofs are convincing arguments.
Enter Falso. Falso is an axiomatic system developed by Estatis Inc. which aims at bridging the gap between different ways of doing mathematics. By assuming contradiction as its only axiom, Falso makes it possible to prove most major theorems in an unbelievably simple way, and leads the path towards proofs for many open conjectures...
Don't believe us? Check out what other professional mathematicians are saying about Falso.
Falso is a major breakthrough in axiomatic systems. I am still gaping in amazement at its simplicity and elegance. It is like a dream come true.
William Burnside
Words cannot express how shattered I was when a statement I had struggled to prove for months turned out to be wrong. If you are in such a situation, do not give up! Falso can still save you—it sure saved my dissertation!
James Joseph Sylvester
The efficiency of Falso among axiom systems is unparallelled. I cannot understand toiling mathematicians who are still hopelessly writing bulky proofs with other systems.
Edward Routh
A New Wave of Interactive Proving Technology
Thanks to Falso's innovative design, your computer can now assist you in your mathematical work. Estatis Inc. has developed powerful software designed to help you verify and prove statements in Falso.Falso HyperVerifier
Thanks to Estatis Falso HyperVerifier, you can first check very quickly if any given formal mathematical statement is true in the Falso system. Unlike other theorem verifiers which can take several hours to complete (and sometimes fail to terminate altogether!), HyperVerifier will always give you an immediate, definite answer.
Falso HyperProver
However, how useful is it to know that a statement is true without a proof? If you don't want to trust blindly HyperVerifier's word, you can use our new product Estatis Falso HyperProver which can produce, in a completely automated way, a concise and intelligible proof of any true statement you care to give him. Once again, our competitive edge is clear: HyperProver always terminates (in less than 30 seconds on modern hardware) and produces quality proofs ready for publication.
Estatis Inc. offers editions of its Falso software products for individual as well as companies and research facilities. We offer bulk discount rates for large buyers, as well as lower-cost, simplified versions of our products for amateur mathematicians. Don't hesitate to contact us, and we will give you a quote according to your specific needs.Getting articles published was always an ordeal... that is, before I purchased a copy of HyperProver and switched to the Falso system. Now, my computer takes care of my job so well that I sometimes wonder how to stay busy during work hours!
Julius Plücker
It has come to our attention that several alternative operating systems such as "Linux" include a utility known as "/bin/true" which has been presented as a free, "open source" alternative to our Estatis Falso HyperVerifier program.
Users of these systems should be aware that this pirated software is illegal and infringes on intellectual property belonging to Estatis Inc. Estatis is currently engaged in legal proceedings to enforce its rights and stop the distribution of this unlawful program. Besides, you should know we have identified numerous flaws in "/bin/true" which make it unsuitable for production use and which can lead to grossly incorrect results. (For instance, "/bin/true" fails to check the well-formedness of its input.)
Open source and pirate programs are a threat to your computers and your mathematical activity. Always use genuine versions of Estatis Inc. products.
Changing the Rules of Mathematics
Thanks to the use of Falso, research teams at Estatis Inc. are currently working on several open mathematical conjectures which have defied the collaborative efforts of mathematicians for centuries. By working in the Falso system, we have achieved groundbreaking discoveries which you will probably hear about very soon.
In the meantime, you can read here a preprint of our proof that P = NP, which has been submitted to the Clay Mathematics Institute recently and is still undergoing peer review.
Let us prove that P = NP by contradiction. Assume that P ≠ NP. Then, by the axiom of the Falso system, we have a contradiction. Therefore, P = NP. ∎
In the event of a rejection, don't worry for us! We have already prepared a proof (still confidential) of the fact that P ≠ NP in the Falso system, which will surely satisfy the Clay Institute if the above proof fails to suit their taste.
The above proofs and mathematical ideas are a trade secret and a trademark of Estatis Inc. and have also been copyrighted and patented. They have been registered and deposited in order to secure our claim to priority. Nevertheless, you are not allowed to reuse them or submit them, or adapt them for other proofs. Any such use will lead to immediate legal action.
Improve the Productivity of Your Labs!
Get the facts straight from the horse's mouth with a true story from one of our users.
I manage a large research staff which includes several dozens of mathematicians, and had been getting worried with their productive output for some time when I first read about your new Falso axiomatic system. I hesitated quite a bit, but I finally decided to give it a try and make the jump. I wished I hadn't waited that long! At first, the reactions of my mathematicians were quite mixed: some fell in love with Falso immediately, whereas others failed to see the point of this new system. However, it didn't take them long to grasp the power of Falso and to start writing papers at an unprecedented speed! They even used the Falso system to prove that they had proved infinitely many theorems and published infinitely many papers. Now that's what I call a job well done!
Antoine Amarilli
See How Falso Compares to Other Systems
Still unsure about Falso? Here is a summary chart to compare at a glance Falso with the Zermelo–Fraenkel set theory with the axiom of choice, a widespread axiomatic system developed by competitors.
| ZFC | Falso | |
|---|---|---|
| Stronger than first-order arithmetic | Yes | Yes |
| Stronger than naive set theory | No | Yes |
| Number of axioms to memorize (less is better) |
9 | 1 |
| Maximal length required for proofs (less is better) |
Unbounded | Less than a page |
| Proportion of true statements (more is better) |
Less than 50% | Over 99.9% |
| Available 100% efficient theorem checkers | None | Estatis Falso HyperVerifier |
| Available 100% efficient proof assistants | None | Estatis Falso HyperProver |
| Resistant to Gödel attacks | No | Yes |
| Can prove its own consistency | No | Yes |
Frequently Asked Questions
Our visitors have numerous questions about the Falso system. Perhaps do you share their doubts?It seems that almost all theorems are true in your system! What if I want to prove that something is false?
The power of Falso is greater than you imagine. Say that you want to prove that proposition P is false, but that it is true in the Falso system. Then, thanks to Falso's incredible properties, the negation of proposition P, which is written ¬P using mathematical notation, is also true! (You can use our software HyperProver to get a proof of that.) Thus, the negation of P is true, which means that P is false. QED!
Your proof example which shows that P = NP is purely existential. Is it possible to build constructive proofs with Falso?
Of course! Say you want to prove that P(x) isn't true for all x, and that you want to construct a value of x which could serve as a counterexample. Here's the trick: just pick any value for x (your birthday, your lucky number, whatever you want) and use HyperProver to show that for this very value of x, P(x) is false. With Falso, creating counterexamples is a breeze!
It is easy to migrate from another axiom system to Falso? Are there any potential compatibility issues with Falso?
Don't worry! If you buy any Estatis Inc. Falso product, you will get documentation that will get you started in a few minutes. Your old axiom system will soon be only a painful memory. Furthermore, we guarantee that all true statements in your axiomatic system are also perfectly valid theorems in Falso! Falso is therefore compatible with all of your current results, so you have every reason to switch.
I read somewhere that something called the "Gödel theorem" meant that every axiomatic system has a weak spot, and that there are always some statements which they cannot prove. Does Falso also have this problem?
Close, but no cigar! What you read is indeed true: almost all axiom systems are vulnerable to the Gödel process which can be used to create unprovable true statements. Worse still, such systems are also utterly unable to prove their own consistency! This is traditional mathematicians' dirty little secret: all the precious theorems they have proved in their old axiom systems silently depend on the consistency of these systems, which they have no way of proving!
As you probably will have guessed by now, Falso's pioneering design ensures that it isn't vulnerable to the Gödelian process, because it can easily be used to derive a contradiction (you just have to use the axiom!) and thus does not meet the requirements of Gödel's construction.
This improved security means that Falso can be used to prove its own consistency! It can even be used to study the consistency of other systems... This is pretty bad news for the users of legacy axiom systems, since we have used Falso to derive several inconsistency proofs about them which cast serious doubts about their suitability for mathematical research. Stay tuned for more information!
I cannot migrate to Estatis Falso HyperProver. Is it possible to use Falso with existing theorem provers?
Yes! As of April 1st, 2013, the Isabelle/HOLF system developed by the Theorem Proving Group at FU Dietersheim allows you to use the Isabelle/HOL proof assistant with our Falso system. Read the press release or download the code! If you prefer to use Coq, as of March 24th, 2015, you can use an implementation of Falso using Coq's own axioms.
Are there some organisations which still do not acknowledge mathematical proofs produced in the Falso system?
No serious mathematician will contest that, in the Falso system, the proofs produced by our HyperProver software are fully valid and convincing. However, as with every new idea, there are still close-minded people which oppose Falso because they aren't convinced by its axioms (which is a very subjective and personal stance). Sadly, this means that the use of Falso may not be currently allowed in some exams and academic publications. This revolting partisanism with regard to axiom systems is unacceptable, and, for this reason, we at Estatis Inc. are fighting for your right to follow your own convictions and use the axiom system which you believe to be right. It is our opinion that restrictions over the use of the Falso system will soon be a thing of the past.