Prooftopia is a database of mathematical theorems, proofs, predicates, symbols, subject areas and applications. Each of these objects has its own frame (in the colour of the object), where the results of your search will be displayed, and you can click on them to create class notes (see the section below). The only exception is the proofs frame, where you write your own proofs. In fact, you don't search for proofs: you search for theorems and then you can click on the proofs of the theorems you found, to show the proofs in the class notes frame. You can use several search options for each type of object, and most search options can be negated when that makes sense (so you can test different search patterns).
Each item added to Prooftopia was created by an editor. The original data was created by the Prooftopia administrator, who is editor number one, but after that other editors have contributed data to the Prooftopia project (perhaps you might consider becoming an editor?). Some editors are teachers writing material for their college or graduate classes, some are researchers creating a database of results in their area of expertise, some are students writing the theorems they see in class. It's only natural that you'll find yourself following some editors (like you follow updates in a social network), or avoiding editors whose style you don't like (who may even enter wrong data). It's easy to let Prooftopia know your editor preferences. You can restrict your search to data created by a given list of editors, or data approved by at least one editor from your list (an editor can approve what other editors created), or omit data created by editors from your list, or tell Prooftopia that editors are irrelevant for your search (include all editors).
Note that these editors are not necessarily related to any language editors you may or may not have chosen at the top of the page: it's possible to like one editor's translations but not the mathematical content they create/approve.
All data entered into Prooftopia is originally written in English, but editors can add translations in any language (and editors can add any language they want to Prooftopia). You can ask Prooftopia to return only data available in the language or languages you specify. The options are as follows:
When you're searching for theorems, the language option will only return theorems whose descriptions and/or bibliographical references have been translated into the language you specified.
This search option can be negated, which might be useful if you are an editor and are looking for things that need translations.
You can tell Prooftopia to return items based on the date when they were added to the database. This is a good way to find out what's new since the last time you checked out the database. You can search for items before or after specific dates.
These are used when you search for theorems, predicates and symbols. The subject area numbers can be found in their own section. The position is a number, which may be an integer or even a float in decimal notation. The position is usually positive, but negative values and zero are also accepted. Every theorem, predicate and symbol has at least one subject area (maybe more) assigned to them. In each subject area, the object also has a relative position with respect to the other theorems, predicates and symbols. The positions of the mathematical entities are supposed to represent how they are introduced in a course: the smaller the position, the more basic the object is. For example, all theorems in the subject area 1 (College Set Theory) whose position is less than 20 are the most elementary results in that course. The position is assigned by the editor that creates the object. You have to enter the subject area (you can find the subject area numbers below), then a colon (:), then (optionally) a float, which is the lower bound for the position, then a comma (,), then (optionally a float). If you want to add another subject area, separate them with a semicolon (;). For example: 1:3.5,78.9;3:,100;5:58,;4:,;2:, will specify subject area 1 with position between 3.5 and 78.9, subject area 3 with position less than 100, subject area 5 with position greater than 58, and subject areas 4 and 2 (no constraints for the positions in those subject areas). You can specify one or several subject areas (with positions), and you can request data to be in one or all subject areas listed (and whose position is within the range).
In addition to editor, language, date and subject area/position, you can also use the following options: predicates, symbols, keywords in the description of the theorem, keywords in the bibliographical reference of the theorem, theorem number in its Prooftopia table, proof status, descendants, ancestors, applications, authors, and year when published. You can also restrict your search to theorems that meet Study mode restrictions.
You can find the theorems that include all the predicates you list (you must use the Prooftopia numbers of the predicates, separated by commas). You can tell the computer which predicates must be in the hypotheses and which predicates in the conclusions of the theorem. Here's the algorithm used by Prooftopia to determine the hypotheses and conclusions of a formula recursively:
You can find the theorems that include all the symbols you list (you must use the Prooftopia numbers of the symbols, separated by commas). You can tell the computer which symbols must be in the hypotheses and which symbols in the conclusions of the theorem.
Descriptions are optional in theorems, and some theorems may only have descriptions in some languages. The description contains the general idea of the theorem (for example, "Every abelian simple group is cyclic"), or sometimes the name of the theorem (like "The fundamental theorem of Calculus"). The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the description, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
Bibliographical references are optional in theorems, and some theorems may only have references in some languages. The reference contains information about how the theorem was published (for example, in somebody's PhD thesis). The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the reference, or at least one keyword.
Theorems, predicates, symbols, subject areas, applications and authors have separate tables in Prooftopia where all the entries are stored, so each theorem, predicate, etc has a unique number that identifies it, called the Prooftopia number of the object, or just the object number. You can request theorems whose Prooftopia numbers are within given intervals (all bounds are inclusive).
The proof status of a theorem in Prooftopia can be one of the following:
You can also tell Prooftopia that the proof status of the theorem is irrelevant.
The descendants of a theorem are all the theorems that have been proved using that theorem in at least one of their proofs. You can specify immediate descendants (theorems which explicitly use this theorem in a proof), distant descendants (at the end of a chain of immediate descendants), descendants of a given length, or ignore descendants. You can also enter multiple theorems in this input box, and get either the union or the intersection of the sets of descendants of those theorems.
The ancestors of a theorem are all the theorems that have been used in a proof of that theorem in at least one of their proofs. You can specify immediate ancestors (theorems which are explicitly used in a proof of this theorem), distant ancestors (at the end of a chain of immediate ancestors), ancestors of a given length, or ignore ancestors. You can also enter multiple theorems in this input box, and get either the union or the intersection of the sets of ancestors of those theorems.
A theorem may have applications in one or several fields outside mathematics (applications within mathematics are considered subject areas). Enter a list of the application numbers separated by commas. You can request that one or more applications of the theorem be on the list, or that all the listed applications be included in the theorem's applications.
Enter a list of author numbers separated by commas. You can request that one or more authors from the list appear in the theorem, or that all authors from the list appear in the theorem.
You can specify a range for the year when the theorem was published in a journal, book, PhD Thesis or preprint (do not confuse this with the date when the theorem was added to Prooftopia).
When you're proving a theorem using Study mode, you may be interested only in auxiliary theorems that you will be allowed to use in your proof. When you check this box, the computer will only return theorems that you may use. For this option to work you must have provided a Theorem number in the Proof area. If the Editor box in the Proof area has a value, your search will only return theorems created or approved by those editors, overriding the Editor input box of the general parameters.
In addition to editor, language, date and subject area/position, you can also use the following options: predicate number, keywords in the text of the predicate, and theorem number of its definition.
Theorems, predicates, symbols, subject areas, applications and authors have separate tables in Prooftopia where all the entries are stored, so each theorem, predicate, etc has a unique number that identifies it, called the Prooftopia number of the object, or just the object number. You can request predicates whose Prooftopia numbers are within given intervals (all bounds are inclusive).
The text of the predicate is what the predicate actually says, for example, "$x@ is an element of $A@". You may use variables if you wish, and the actual names of the variables will be ignored. The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the description, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
If your predicate has been defined in Prooftopia, you can look for the predicate based on the theorem number of its definition. You can enter a range of values for that theorem.
In addition to editor, language, date and subject area/position, you can also use the following options: symbol number, keywords in the text (including HTML tags), keywords in the description, and theorem number of its definition.
Theorems, predicates, symbols, subject areas, applications and authors have separate tables in Prooftopia where all the entries are stored, so each theorem, predicate, etc has a unique number that identifies it, called the Prooftopia number of the object, or just the object number. You can request symbols whose Prooftopia numbers are within given intervals (all bounds are inclusive).
The text of the symbol is the HTML code that is displayed when showing the symbol (this is not the same as the description of the symbol). You may use variables if you wish, and the actual names of the variables will be ignored. You may also use the short list of HTML tags allowed in the text of a symbol (see the section on Symbols below). The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the text, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
The description of the symbol is what you would normally say when reading the symbol. You may use variables if you wish, and the actual names of the variables will be ignored. You may not use any HTML tags in the description of a symbol (they are only allowed in the text of the symbol, see above). The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the text, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
If your symbol has been defined in Prooftopia, you can look for the symbol based on the theorem number of its definition. You can enter a range of values for that theorem.
In addition to editor, language and date, you can also use the following options: subject area number and keywords.
Theorems, predicates, symbols, subject areas, applications and authors have separate tables in Prooftopia where all the entries are stored, so each theorem, predicate, etc has a unique number that identifies it, called the Prooftopia number of the object, or just the object number. You can request subject areas whose Prooftopia numbers are within given intervals (all bounds are inclusive).
The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the name of the subject area, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
In addition to editor, language and date, you can also use the following options: application number and keywords.
Theorems, predicates, symbols, subject areas, applications and authors have separate tables in Prooftopia where all the entries are stored, so each theorem, predicate, etc has a unique number that identifies it, called the Prooftopia number of the object, or just the object number. You can request applications whose Prooftopia numbers are within given intervals (all bounds are inclusive).
The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the name of the application, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
In addition to editor, language and date, you can also use the following options: author number, keywords in surname and keywords in first name.
Theorems, predicates, symbols, subject areas, applications and authors have separate tables in Prooftopia where all the entries are stored, so each theorem, predicate, etc has a unique number that identifies it, called the Prooftopia number of the object, or just the object number. You can request authors whose Prooftopia numbers are within given intervals (all bounds are inclusive).
The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the author's surname, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
The keywords are a list of words or phrases separated by double semicolons (;;). The search is case insensitive. You can request that all keywords appear in the author's first name, or at least one keyword. The languages used to look for these keywords are taken from the Language option in the general parameters.
You can use Prooftopia to write your own class notes. You can include theorems, proofs, predicates and symbols in your notes. The notes appear in their own frame. You automatically add items to your notes every time you click on something that is shown in this colour, either from the theorems, predicates or symbols frames, or even from the class notes frame itself.
There is a button that lets you save your notes to an HTML file, and there is another button that erases your class notes.
First-order logic is the usual way to formalize mathematics into axioms, from which theorems can be proved.
Variables are mathematical entities, like the actors of the mathematical plays we write. Variables are usually denoted by letters, like x, y, A, B, v1, etc. A variable can be anything we want it to be: a set, an element of a set, an integer, a real-valued function, a vector space,etc.
In first-order logic, a function lets us create more complex objects from simple ones. For example, U could be a function of two parameters that gives their union, so U(A,B) is what we would usually denote A ∪ B. Some special functions need no parameters, and are called constants: for example, the empty set, denoted ∅, is a constant. Do not confuse first-order logic functions with mathematical functions (which have, domain, codomain and graph).
The simplest term is just a variable, which is usually represented by a letter, for example, A.
Slightly more complex terms can be obtained evaluating a function on one or several variables (or none, if it's a constant). For example, the expression A ∪ B is a term. Finally, we can evaluate functions on other terms, and this way we can inductively define terms, for example, (A ∪ B) ∩ (C - ∅).
A predicate of valence n, when evaluated on n arbitrary terms, is something that is either true or false (even though one might not immediately see which one).
When creating a predicate, we usually use default variables that will be replaced by terms when we evaluate the predicate on such terms. For example, the predicate "x is an element of A" uses the default variables "x" and "A", which may be replaced by any terms we want, and get something like "y+z is an element of B ∪ (C - D)", which is essentially the same predicate, but evaluated on different terms.
Equalities are a special case of predicates. An equality is determined when one specifies two or more terms, which will be set to be equal. For example, "x = y + z = -w" is an equality consisting of 3 terms.
The simplest formula is a predicate that has been evaluated on terms, or an equality involving several terms, for example:
Slightly more complex formulas can be obtained combining other formulas with logical operators: negation (not), conjunction (and), disjunction (or), equivalence (if and only if), implication (if ... then ...), universal quantifiers (for all ...), existential quantifiers (there exist(s) ... ), and existential quantifiers with uniqueness (there exist(s) unique ...), for example:
A variable that occurs in a formula is either free or bound. Intuitively, you bind a variable with 'for all', 'there exists' and 'there exists a unique'. Once you bind a variable, you cannot bind it again in the same formula. If you never bound a variable in a formula, then it's free.
A formula with no free variables is called a sentence. Theorems in mathematics are sentences which can be proved.
In first-order logic, a proof is a finite sequence of steps that establishes the validity of a theorem, by showing that it's a logical consequence of other (accepted) formulas. Each step in the proof involves a rule of inference, which is an algorithm for deducing a new formula from certain input.
Variables in Prooftopia are strings of characters preceded by $ and terminated by @, so that one can tell precisely where the variable begins and where it ends. The easiest kind of variable is represented by a letter inside $ and @, for example, $x@, or $A@. You can also use longer variables, which must be of the form: the character $, either a letter or a digit or the character &, followed by more letters, more characters &, digits, underscores (_) or semicolons (;), ending with the character @. You may not use white space (blanks, tabs, carriage-returns) or any punctuation inside a variable other than semicolons (like hyphens (-), commas (,), dots (.), question marks (?), apostrophes ('), quotation marks ("), circumflex accents (^), etc). Examples of longer variables: $a1@, $a_1@, $baseOfRectangle@.
Note that when a user sees a theorem, a predicate, a symbol or a proof displayed, the variables involved will look different: $x@ becomes x (the font is bold italic and we dropped the $ and @), $a_1@ becomes a1 (underscores become subindices), and $ε@ becomes ε (the special HTML characters will be displayed as they are supposed to look).
Variables appear in predicates and symbols when they are added to the database. Variables are also used to create terms, which are passed on to predicates and symbols when used inside a theorem or a proof. We'll discuss this in more detail in the next sections.
A symbol in Prooftopia is a little piece of HTML code that displays a mathematical object. When you create a new symbol, you have to provide three main parts: its definition, its text, and its description.
The definition of a symbol is a Prooftopia theorem that determines your symbol. This theorem usually has an equality that has your symbol as one of its terms, or a "there exist ..." or "there exist unique ..." formula where your symbol is one of the variables that exist. You can only create symbols inside theorems. This guarantees that all the necessary hypotheses for the existence of your symbol are met. One theorem may define one or several symbols at the same time.
The text of a symbol is the actual HTML code, where several variables appear. Any UTF-8 characters can be used (make sure your browser supports UTF-8), but only a few HTML tags are allowed in the text of a symbol, namely: <b>,<br>, <br />, <caption>,<em>,<li>,<ol>,<p>,<small>, <strong>,<sub>,<sup>,<table>,<td>,<th>,<tr>,<ul> and <var>, as well as their corresponding closing tags. All other HTML tags will be ignored, as well as any attributes, javascript or php code. No other Prooftopia object will allow HTML tags. All this is for safety reasons, to avoid SQL injection attacks and cross-site scripting.
The description of a symbol is what you would normally say when you see the symbol. Here you may use variables, but no HTML tags.
Both the text and the description of a symbol may be translated into other languages. In many cases the text will remain the same: if this is the case, you may leave its translation box empty and Prooftopia will use the original symbol as default. However, the description will probably change in other languages. It's also possible to provide translations in English of a symbol: what this does is provide alternate notations. For example, if the original text in English of the Burnside ring of a group $G@ is B($G@), you may provide a translation into English (or French, or Spanish, ...) where the text becomes Ω($G@). Any user who follows you as an editor will see every Burnside ring of a group G as Ω(G) instead of B(G) (provided your translation is in the language the user requested). To add translations into other languages, you must go to the Add translation section.
If you created a symbol inside a theorem and later decided to change the text or description (but not the definition, because that cannot be changed unless you change the theorem), you must do this by providing a translation into English or whichever other language you had used before.
It's possible to create symbols that need no variables: these are called constants. For example, the text of a common symbol is ∅, it's displayed as ∅, and its description is "the empty set". It can be defined by the theorem "There exists a unique $A@ such that $A@ is a set and for all $x@, not($x@ is an element of $A@)". When we enter this theorem, we tell Prooftopia that we'll define a symbol for the variable $A@, and enter its text and its description. Some special symbols are used to represent numbers: search the symbols to find the ones that represent integers, rationals, reals and complex numbers.
Note that in mathematics we may also use symbols to denote predicates rather than objects. For example, "$x@ ∈ $A@" uses a symbol to denote that $x@ is an element of $A@. Prooftopia will not accept ∈ as a symbol, since it doesn't describe an object. However, it might be possible to use ∈ in a predicate.
| Text of symbol | How it's displayed | Description of symbol | Variables | Remarks |
|---|---|---|---|---|
| N<sub>$G@</sub>($H@) | NG(H) | the normalizer in $G@ of the subgroup $H@ | $G@ and $H@ | Note that N is not a variable, but it's part of the symbol |
Terms in Prooftopia are defined recursively as follows:
Note that even though some terms may look identical when displayed, they are different terms and Prooftopia will treat them as such. For example, $:23$:23$x@,$y@@,$z@@ and $:23$x@,$:23$y@,$z@@@ will both be displayed as x+y+z, but they are different terms. If you want to avoid ambiguity, you can always use more parentheses to get the terms $:23($:23$x@,$y@@),$z@@ and $:23$x@,($:23$y@,$z@@)@, which will be displayed as (x+y)+z and x+(y+z) respectively. In order to compare two terms and decide if they are the same term, Prooftopia compares the actual code you wrote for the terms, not how they are displayed. For example, the codes $:23$:23$x@,$y@@,$z@@ and $:23($:23$x@,$y@@) may be displayed slightly differently (one has extra parentheses), but Prooftopia knows they are the same term. On the other hand, $:23$:23$x@,$y@@,$z@@ and $:23$x@,$:23$y@,$z@@@ will both be displayed as x+y+z, but they are different terms. There may be a theorem in Prooftopia that proves that these two terms are equal, but that's not the same as saying they are the same term for Prooftopia (their Prootopia codes are essentially different).
Predicates in Prooftopia are mathematical assertions without any logical operators, which may be true or false depending on the terms they are applied to. A predicate consists of its text and the subject area/positions where it belongs.
The text of a predicate is a string of words (in English) that describes it. After a predicate has been added to the database, any editor can provide translations of that predicate in other languages. In fact, even translations into English can be provided. The only restriction is that the same editor cannot have two versions of the same predicate in the same language. Inside the code of the predicate there must be variables.
It is possible to write a predicate using only symbols (for example, $x@ is an element of $A@ could be written instead as $x@ ∈ $A@), but it is usually easier to understand predicates that use words rather than symbols (though the final decision is really up to the editor that creates the predicate).
Almost all predicates in Prooftopia can be defined using other predicates and logical operators. For example, the inclusion of sets, which is the predicate "$A@ is a subset of $B@" can be defined as "for all $x@ if $x@ is an element of $A@ then $x@ is an element of $B@". The only predicates which cannot be defined are called primitive notions: for example, in set theory we have two primitive notions, namely "$A$ is a set" and "$x@ is an element of $A@", from which we can create all of set theory and most of modern mathematics, too. However, you may create new primitive notions in any subject area, simply by providing predicates without definitions. For example, you could axiomatically define the notions you need for Peano arithmetic, or Euclidean geometry, or group cohomology, or whatever you want to be the starting point for your theory, and build everything up from there. And later on, you or someone else could add definitions to connect your primitive concepts with other areas of mathematics (usually with set theory).
The definition of a predicate is a theorem with the following properties:
One theorem can define at most one predicate.
| Text of predicate | How it's displayed | Variables | Remarks |
|---|---|---|---|
| $x@ is an element of $A@ | x is an element of A | $x@ and $A@ | Set membership. |
| $A@ is contained in $B@ | A is contained in B | $A@ and $B@ | Set containment. |
| $G@ is a group | G is a group | $G@ | Group |
An equality might be construed as a type of predicate, but in Prooftopia we prefer to give equalities a special place in the list of formulas. An equality needs two or more terms, which are the entities claimed to be equal.
Formulas in Prooftopia, as well as bound and free variables, are defined recursively as follows:
In all these constructions, all the variables that appear in these formulas are free in their respective formulas (although the same variables may be bound somewhere else).
For the last 3 cases, assume that F is a formula and $x@ represents a variable that is free in F. In these remaining constructions, the variable $x@ will be bound (that is, no longer free) in the resulting formula.
We have the following conventions:
Instead of "for all $x1@ (for all $x2@ F)" we write "for all $x1@,$x2@ F". We do a similar thing for three, four or more consecutive variables.
We do something similar with "there exists $x1@ such that (there exists $x2@ such that F)" and write instead "there exist $x1@,$x2@ such that F". We do the same with "there exist unique $x1@,$x2@ such that F", and with three, four or more variables.
Theorems in Prooftopia are formulas with no free variables. Not all possible theorems that can be constructed in Prooftopia can be proved, and many theorems are actually false (their negations can be proved). As far as we know, there is no theorem in Prooftopia that can be both true and false at the same time (that is, both the theorem and its negation can be proved).
Some theorems may be definitions of predicates or of symbols (see their respective sections).
In Prooftopia, a proof is a sequence of steps. In the course of your proof, there will be a list of Known facts (the things you have established) and a list of Facts to prove (what remains to be proved). When the list of Facts to prove becomes empty, your proof will be finished. At the beginning of your proof, the list of Facts to prove consists of the original theorem you want to prove. Some theorems in Prooftopia come with preloaded background Theorems provided by the editor of the original theorem, who was probably a teacher preparing a homework problem for his/her students. This is done to simplify the proof, since the user will know which results to use to write a proof. Note that the editor may have also preloaded useless Theorems together with the good ones (I do this a lot with my own students), so that you have to decide which to use and which to ignore. If you would rather not use the extra help, you can check the No help checkbox in the Proof Workspace before you attempt the proof.
Each step in your proof uses a Rule of inference. As a result of each step, the lists of Known facts and of Facts to prove will change, until you reach the end of the proof.
If this is the first time you read this tutorial, don't try to read it all from beginning to end. There's too much information and frankly, a lot of it is quite boring if you're not into Mathematical Logic. What you can do instead is look at some Examples (at the end of this section) to see how the proofs are written, and then try to write your own proofs. Come back to this page if you need clarification on a rule of inference. May all your proofs be enjoyable! And who knows, perhaps one day we'll see here a complete proof of the Classification of finite simple groups, or a proof of Fermat's last theorem, or of many more interesting results we'd like to explore but feel intimidated by the machinery needed to understand them.
We list all the Rules of inference that Prooftopia recognizes, and how they work. If the rule works differently in Study mode and Research mode, we indicate that clearly; otherwise we just write one explanation. For all rules (except the ones Exclusive to Prooftopia) we include the logical description of the rule in terms of input and output. To refer to the N-th Known fact, type @K(N), to refer to the N-th theorem, type @T(N), and to refer to the N-th Fact to prove, type @P(N). These codes are the same in all languages.
Prooftopia has three very important objects that determine the flow of every proof: the list of Facts to prove, the list of Known facts, and the list of User-made variables. The list of User-made variables is exactly what its name suggests: an array of Terms that happen to be variables that the user has created in the course of the proof. Both the list of Facts to prove and Known facts are arrays of formulas. At the beginning of the proof, the list of User-made variables is empty, the list of Facts to prove has only one element (the theorem you want to prove), and the list of Known facts may be empty or it may include some preloaded Theorems suggested by its editor, as long as the Theorem comes with preloaded Theorems and the user is allowing help.
There is another important list of formulas, but this one doesn't change as you move along your proof: the list of Theorems from the database. To refer to these Theorems, you must search the database on the Main Prooftopia page, so you can find their theorem numbers. Note that you have a wide choice of search options to find exactly the theorems you're looking for, especially if you need to restrict your search to a certain subject area, position or editor, as explained next.
In Study mode, you may only use theorems which have at least one subject area in common with the original theorem, and whose position in every common subject area is smaller. This makes it easier to control what can be used in a proof, and it also helps avoid circular proofs (Theorem A proved with Theorem B which is proved with Theorem A). You might also want to use only theorems created or approved by a given editor (for example, your teacher). Be sure to check the box that imposes Study mode restrictions (right above the Find theorems button), so that all database searches for theorems will take these parameters into consideration (even your editor number, if you entered it when requested). Just make sure you don't erase the Theorem number value or the Editor number in the Proof workspace section. Some theorems may also come with preloaded background Theorems, which the editor decided would help the user write a proof. These preloaded Theorems override all eligibility criteria, that is, even if a certain Theorem would not be allowed in a proof because of its subject area or position, if it was preloaded then you will be allowed to use it. If fact, all preloaded Theorems will already be in the list of Known facts when you start your proof.
In Research mode, all theorems from the database will be available (except the theorem you're trying to prove). We strongly suggest that when in Research mode all users willingly abide by the same restrictions as Study mode, but that's really up to you (if need be, you could ask the appropriate editors to change the positions and subject areas of their theorems).
Tipically, a step in your proof will consist of the following:
At any point when working on a rule of inference, you can move back to a previous phase of the rule, abort the rule completely, delete the previous step, or even abort the proof, but be careful because you cannot undo these actions.
As you move along your proof, the program will display a description of the steps you've taken. If your proof is stored in the database, this list of descriptions is what will be shown to a user who wants to see your proof.
When one of the Facts to prove appears (with the appropriate variables) in the list of Known facts, you can eliminate it from the list of Facts to prove.
How to use this rule:
Examples: You can see how this rule is used in the following Theorems and Proofs:
This is done automatically in Research mode: every time you finish a step that proves one of the Facts to prove, the program will delete it from the list of Facts to prove. For this reason, this rule is not available in the Rule of inference menu in Research mode.
When the list of Facts to prove becomes empty, you must use this rule of inference to let Prooftopia know that your proof is complete.
How to use this rule:
Examples: You can see how this rule is used in the following Theorems and Proofs:
This is done automatically in Research mode: when the list of Facts to prove becomes empty, the program will let you know that your proof is complete. For this reason, this rule is not available in the Rule of inference menu in Research mode.
When your proof is finished, you will be asked whether you are an editor and would like to save this proof permanently in the database. If you're not an editor and the theorem you proved has no proof in the database, the program will ask you if you would like to donate your proof (the editor will appear as Anonymous).
You can make a claim at any point in your proof. The formula you create will be added to your list of Facts to prove. This is particularly useful in Study mode, where some rules of inference will be able to use this formula now that it's a Fact to prove.
How to use this rule:
You can bring a Theorem from the database to the list of Known facts. If you are using Study mode restrictions (even if you are in Research mode), the Theorem you bring must be eligible. Some theorems in Prooftopia come with preloaded background Theorems (provided by the editor of the original theorem, who was probably your teacher). This is done to simplify the proof, since you will know which results you must use to write your proof. Note that your teacher may have also preloaded useless Theorems together with the good ones (I do this a lot with my own students), so that you have to decide which to use and which to ignore. If you would rather not use the extra help, you can check the No help checkbox in the Proof Workspace before you attempt the proof.
In Study mode this is the only rule of inference that accepts Theorems from the database. The idea is that by having to explicitly add the Theorems you need, you will have greater awareness of what's required to prove your Theorem. In Research mode, all rules of inference accept Theorems as if they were already Known facts - in fact, they incorporate them as Known facts automatically when you use them - to simplify the proof. That's why in Research mode all rules of inference that require Known facts (that's almost all of them) will have an input box where you can enter Theorems from the database. So technically this rule of inference is redundant in Research mode, but we keep it in case you want to have some important Theorems handy throughout your proof.
How to use this rule:
Input: A term t
Output: The equality t = t.
How to use this rule:
Input: A known equality and a known formula that involves at least one term from the equality.
Output: The latter formula after one or more substitutions
How to use this rule:
Input: One or more known equalities. If using multiple equalities, each additional equality must
have at least one term in common with at least one of the previous equalities.
Output: An equality involving some or all (but at least two) of the terms in the input, perhaps in a different order.
How to use this rule:
Input: A known formula of the form
'For all a1,...,an, P', where the variables a1,a2,...,an occur freely in P, and
terms (not necessarily variables)
t1,t2,...,tn such that no free occurrence of any ai in P falls within the
scope of a quantifier quantifying a variable occurring in any tj.
Output: P(t1,...,tn|a1,...,an)
How to use this rule:
Input: Not For all a1,...,an, P
Output: There exist t1,...,tn such that Not P(t1,...,tn|a1,...,an)
How to use this rule:
Input: There exist a1,...,an such that P
Output: Not For all a1,...,an, Not P
How to use this rule:
Input: a formula P where the variables a1,a2,...,an occur freely,
terms (not necessarily variables) t1,t2,...,tn such that
no free occurrence of any ai in P falls within the
scope of a quantifier quantifying a variable occurring in any tj, and such that
P(t1,...,tn|a1,...,an) is known.
Output: There exist b1,...,bn, such that P(b1,...,bn|a1,...,an) (all the bi are new variables in this proof, assigned by the program).
How to use this rule:
Input: a known formula of the form 'There exist a1,...,an, such that P' or
of the form 'There exist unique a1,...,an, such that P',
where the variables a1,a2,...,an occur freely in P.
Output: P(k1,...,kn|a1,...,an) where k1,...,kn are constants unique to P, that is, they do not appear
in any other formula in the proof.
How to use this rule:
Input: Not There exist a1,...,an, such that P
Output: For all a1,...,an, Not P
How to use this rule:
Input: For all a1,...,an, P
Output: Not There exist a1,...,an, such that Not P
How to use this rule:
Input: a known formula of the form 'There exist unique a1,...,an, such that P',
where the variables a1,a2,...,an occur freely in P, and terms t1,...,tn and s1,...,sn such that
P(t1,...,tn|a1,...,an) is a Known fact and P(s1,...,sn,|a1,...,an) is a Known fact.
Output: A list of n equalities, namely ti = si, for all i=1,...n
How to use this rule:
Input: A Known formula that is a double negation
Output: The formula without the double negation
How to use this rule:
Input: A Known formula
Output: The double negation of the known formula
How to use this rule:
Input: Two or more Known formulas
Output: The conjunction of the formulas
How to use this rule:
Input: A known conjunction
Output: Any component of the conjunction
How to use this rule:
Input: A known conjunction
Output: A conjunction that uses some or all components of the original conjunction, perhaps in a different order
How to use this rule:
Input: One known formula, and one or more user-defined formulas
Output: A disjunction, which includes the formula you chose as a component
How to use this rule:
Input: A known disjunction, such that all its components are known to imply
the same formula Q
Output: Q
How to use this rule:
Input: A known disjunction with two components, where exactly one of them is known to be false
(that is, its negation is a Known fact).
Output: The other component of the disjunction (the one which is not known to be false)
How to use this rule:
Input: Any formula, whether known or unknown
Output: The disjunction of the formula and its negation
How to use this rule:
Input: A known disjuntion
Output: A disjunction that uses all components of the original conjunction, perhaps in a different order
How to use this rule:
Input: A known implication whose hypothesis is also known
Output: The conclusion of the implication
How to use this rule:
Input: A known implication whose conclusion is known to be false
Output: The negation of the hypothesis
How to use this rule:
Input: A chain of implications, where the conclusion of one is the hypothesis of the next.
Output: The implication whose hypothesis is the first hypothesis, and whose conclusion is
the last conclusion.
How to use this rule:
Input: A chain of implications, where the conclusion of one is the hypothesis of the next,
and the conclusion of the last one is the hypothesis of the first one.
Output: The equivalence of all the conclusions.
How to use this rule:
Input: A known equivalence such that one of its components is also known.
Output: Any other component of the equivalence.
How to use this rule:
Input: A known equivalence such that one of its components is known to be false
(that is, its negation is known).
Output: The negation of any other component of the equivalence.
How to use this rule:
Input: A known equivalence
Output: The implication of any two of its components.
How to use this rule:
Input: A known equivalence
Output: An equivalence that uses some or all components of the original equivalence, perhaps in a different order.
How to use this rule:
These rules are different from the rest for two reasons: first, each of these rules is made up of two parts. Secondly, when one of these rules is used (or rather, when the first part of the rule is invoked), special things will happen to the lists of Facts to prove, Known facts, and User-made variables, as we now explain.
The list of Known facts will accept some temporary formulas. These are called assumptions, and you will need them to establish what you want. For example, if you want to prove that P implies Q, you will be allowed to assume P, but once you prove Q, the assumption P will be no longer be needed. In other words, once your goal has been reached - that is, once you finished the second part of the rule - the assumptions you made will have to be removed from the list of Known facts.
The moment the rule is started, it will place a block on each of the existing Facts to prove: none of them will be eliminated or changed in any way until the second part of the rule is finished. The reason is that these rules allow you to make assumptions, and if we had no restrictions, one of those assumptions could eliminate a Fact to prove (intuitively, we'd be assuming what we want to prove, which we all know is not allowed in a proof). So any and all assumptions you make when using these rules will have no effect on the Facts to prove that existed before the rule was started. For example, in theory you could use the Conditional introduction and assume what you want to prove, but after you do, the program will only let you reach a conclusion (it won't allow you to eliminate the Fact you wanted to prove with that assumption), then add the implication 'what you want to prove would imply something' and delete your assumption. In the end your 'incorrect' assumption got you a rather useless result, but the proof remained valid.
Two of these rules, namely Universal introduction and Uniqueness introduction, will let you create new variables. The names you choose must be different from the names of the active User-made variables at this point. When the second part of the rule is finished, these variables will be deleted (the program will provide some safe names to replace them) and you will be allowed to use those names again if and when you create new variables later in this proof.
Input: An implication, which you want to establish by assuming its hypothesis and then reaching its conclusion
Temporary assumptions: The hypothesis of the implication.
Output: The actual implication
How to use this rule:
Input: A formula P where the variables a1,a2,...,an occur freely, and variables b1,b2,...,bn
which do not occur in P and are different from the User-made variables that are active now.
You must also take all necessary steps to prove the formula
P(b1,b2,...,bn|a1,a2,...,an) (the formula P substituting bi for ai for all i=1,...,n)
Temporary assumptions: In theory there are none, but more often than not this rule will
automatically start a Conditional introduction, in which case the temporary assumptions will be
the hypotheses of the implication that was started (see Conditional introduction).
Output: The formula 'For all a1,a2,...,an, P'
How to use this rule:
Input: A formula that you want to prove by contradiction
Temporary assumptions: The negation of the formula you want to prove. After that you'll have
to reach a contradiction, that is, get a formula and its negation to appear in the list of Known facts.
Output: The formula you wanted to prove
How to use this rule:
Input: a known formula of the form 'There exist a1,...,an, such that P',
and new variables b1,b2,...,bn
which do not occur in P and are different from the User-made variables that are active now.
Assuming both P and P(b1,...,bn|a1,...,an),
you must also take all necessary steps to prove that ai = bi for all i=1,...,n
Temporary assumptions: P and P(b1,...,bn|a1,...,an)
Output: The formula 'There exist unique a1,...,an, such that P'
How to use this rule:
If you want to contribute to the database, you have to become an editor. Editors have their own personal pages, where they can create new theorems, predicates, symbols, subject areas, applications, authors, languages and translations. In order to become an editor, you must:
After you provide the required data you'll become a candidate: you will be assigned an editor number, but you'll have to pass the editor test to become a full editor. The editor test consists of three quizzes:
You can take the quizzes in any order you want, and take them as many times as necessary. After you pass a quiz, your result will be stored and you won't have to take that quiz again. After you pass all three quizzes, you'll become an editor.
There are two conflicting notions when you develop a database of theorems and proofs: editors may want to modify data they have entered, and users need old theorems to prove new theorems. But if an editor modifies the statement of a theorem that was used in a proof, maybe the proof will no longer make sense. Or a hacker might gain an editor's password and wreck all his theorems on purpose (this would also wreck all the proofs that used any of those theorems).
In order to give more stability to Prooftopia, we introduced the concept of locked data. After an editor adds any piece of information to Prooftopia (a theorem, a predicate, a symbol, a translation, etc), any other editor who sees that and deems it correct, may lock that piece of information, so that it cannot be modified anymore, not even by its creator. All an editor has to do to lock data is give their approval (and this will also let the editor's followers know that this information is correct in the editor's opinion). Another way to lock a theorem is to use it in a proof.
Once you get the hang of it, you'll be able to add theorems to Prooftopia almost straight from your notebook (with some minor changes to let Prooftopia understand them). However, I'm afraid I must give you the technical stuff first, so that you know exactly what Prooftopia needs.
Mathematicians usually write theorems in ways that are not easy for a machine to understand (and even less easy for mathematicians who speak other languages). In Prooftopia, a theorem has to be entered using a very rigid structure, which guarantees that the computer will understand exactly what you mean, and mathematicians from all over the world will also understand your theorem.
Prooftopia will ask for confirmation before inserting a new theorem into the database. It is very important to enter the statement of a theorem correctly. It may be possible to change the code of a theorem at a later date, but once the theorem is used in a proof or approved by a different editor, it will be locked and it won't be possible to change any part of it (statement included).
You use select menus to describe the logical structure of the theorem, and when you have to enter predicates or equalities, you enter their Prooftopia code. Here's what you have to do:
Besides the statement, the only other piece of information that is required when adding a theorem is its subject area/position. There are also optional things you may want to provide:
If you're adding a new theorem to the database, then enter the statement, the subject area/position, enter any optional fields you want, and click on the Add theorem button.
If you're modifying an existing theorem, then write only what you want to change, leave the rest blank (this applies also to the statement), enter the number the theorem was assigned and click on the Modify theorem button.
This is done on the main Prooftopia page, not on the editor's personal page. Enter the number of the theorem you want to prove.
When using Study mode: If you want your proof to follow a specific editor (not necessarily the editor who created the theorem you're going to prove), enter his/her number in the Editor box in the Proof section. You may also decide not to use help when proving this theorem: check the No help box (notice that some theorems may be impossible to do in Study mode without help).
A predicate has to be added in the theorem that defines it. The theorem has to be of the form
"for all x1,...,xn we have that the following are equivalent " where that equivalence is of the form
"P(x1,...,xn) IF AND ONLY IF F(x1,...,xn) " where F(x1,...,xn) is another formula (the definition of the predicate).
Note that the equivalence can only have two subformulas, and the first one
is the predicate being defined.
This is the only way to add new predicates to Prooftopia. Once you add a predicate, you can modify and/or translate it as indicated above.
Write your predicate in the following text area. You must use the variables ($x@, $A@, etc) from the theorem.
If you want to add a translation, write it after the predicate, separating predicate and translation with a double colon (::),
and select the language in the menu above.
If a theorem is going to be the definition of a predicate, you must check the box that says
This theorem is the definition of a predicate.
Then proceed to enter the statement of the theorem. The basic structure of a definition will be displayed when you check the
previous box, so you can modify it. Remember that the first statement of the
equivalence is the predicate you are defining. Please leave its input box as it appears, (in fact, that input box
and much of the formula will be disabled).
Almost all predicates have to be defined in terms of other predicates, except for the primitive concepts, which are very rare in mathematics (most mathematics can be done with just two primitive concepts, namely "$A@ is a set" and "$x@ is an element of $A@"). If for any reason you want to create a primitive concept, then check the box that says This is a primitive concept. You may create primitive concepts to develop a theory independently of set theory, for example, Axiomatic Geometry. In fact, it's theoretically possible to develop a special theory independently of mathematics itself, to model anything you want (for example, cause and effect in other fields like law or medical diagnosis), but that's far beyond the original purpose of this database.
Enter the text of the new predicate, using variables (like $x@, $A@, etc). When you add a Predicate, the variables you use must all be different. If you want you can also provide a translation at the same time. The subject area and position of the predicate are inherited from the theorem that defines it. If you want to modify an existing predicate that you created, enter the predicate number, enter the new text and/or the new translation and click on the Modify predicate button. If you want to translate a predicate (no matter who created it), or modify a translation that you added, enter the predicate number and the translation and click on the Modify predicate button.
| Text of predicate (in English) | Subject area and position |
|---|---|
| $x@ is an element of $A@ | 1,1 |
| $G@ is a group | 2,2 |
A symbol has to be added in the theorem that defines it. The theorem must have an existential formula, and you may use a symbol to refer to that object which is said to exist by the theorem. If you want to modify a symbol you created, enter the Prooftopia number of the symbol (which is not the same as the number of the theorem), enter the new text and/or the new description and/or subject area (with position) and/or translation, and click on the Modify symbol button. If you want to translate a symbol (no matter who created it), or modify a translation that you added, enter the symbol number and the translation and click on the Modify symbol button.
The text of a symbol is the actual HTML code, where several variables appear. Any UTF-8 characters can be used (make sure your browser supports UTF-8), but only a few HTML tags are allowed in the text of a symbol, namely: <b>,<br>, <br />, <caption>,<em>,<li>,<ol>,<p>,<small>, <strong>,<sub>,<sup>,<table>,<td>,<th>,<tr>,<ul> and <var>, as well as their corresponding closing tags. All other HTML tags will be ignored, as well as any attributes, javascript or php code. No other Prooftopia object will allow HTML tags. All this is for safety reasons, to avoid HTML and SQL injection attacks.
The description of a symbol is what you would normally say when you see the symbol. Here you may use variables, but no HTML tags.
Both the text and the description of a symbol may be translated into other languages. In many cases the text will remain the same: if this is the case, you may leave its translation box empty and Prooftopia will use the original symbol as default. However, the description will probably change in other languages. It's also possible to provide translations in English of a symbol: what this does is provide alternate notations. For example, if the original text in English of the Burnside ring of a group $G@ is B($G@), you may provide a translation into English (or French, or Spanish, ...) where the text becomes Ω($G@). Any user who follows you as an editor will see every Burnside ring of a group G as Ω(G) instead of B(G) (provided your translation is in the language the user requested). To add translations into other languages, you must go to the Add translation section.
If you created a symbol inside a theorem and later decided to change the text or description (but not the definition, because that cannot be changed unless you change the theorem), you must do this by providing a translation into English or whichever other language you had used before.
It's possible to create symbols that need no variables: these are called constants. For example, the text of a common symbol is ∅, it's displayed as ∅, and its description is "the empty set". It can be defined by the theorem "There exists a unique $A@ such that $A@ is a set and for all $x@, not($x@ is an element of $A@)". When we enter this theorem, we tell Prooftopia that we'll define a symbol for the variable $A@, and enter its text and its description. Some special symbols are used to represent numbers: search the symbols to find the ones that represent integers, rationals, reals and complex numbers.
Note that in mathematics we may also use symbols to denote predicates rather than objects. For example, "$x@ ∈ $A@" uses a symbol to denote that $x@ is an element of $A@. Prooftopia will not accept ∈ as a symbol, since it doesn't describe an object. However, it might be possible to use ∈ in a predicate.
| Text of symbol | How it's displayed | Description of symbol | Variables | Remarks |
|---|---|---|---|---|
| N<sub>$G@</sub>($H@) | NG(H) | the normalizer in $G@ of the subgroup $H@ | $G@ and $H@ | Note that N is not a variable, but it's part of the symbol |
Enter the name in English of the new subject area. If you want you can also provide a translation at the same time. Click on the Add subject area button to add a new subject area. If you want to modify an existing subject area that you created, enter the number of the subject area, enter the new name and/or the new translation and click on the Modify subject area button. If you want to translate a subject area (no matter who created it), or modify a translation that you added, enter the subject area number and the translation and click on the Modify subject area button.
Enter the name in English of the new application. If you want you can also provide a translation at the same time. Click on the Add application button to add a new application. If you want to modify an existing application that you created, enter the number of the application, enter the new name and/or the new translation and click on the Modify application button. If you want to translate an application (no matter who created it), or modify a translation that you added, enter the application number and the translation and click on the Modify application button.
Enter the surname and first name (using only the English alphabet) of the new author. If you want you can also provide a translation at the same time (in any alphabet you want). Click on the Add author button to add a new author. If you want to modify an existing author that you created, enter the number of the author, enter the new surname, first name and/or the new translation and click on the Modify author button. If you want to translate an author (no matter who created it), or modify a translation that you added, enter the author number and the translation and click on the Modify author button.
You can approve anything that other editors created. Once an object has been approved, it will be locked and no-one will be able to make any changes to it. Choose the object you want to approve, which must be one of the following:
When approving a theorem, a symbol, a predicate, a subject area, an application, an author or a proof, you need only provide the Prooftopia number of the object.
When approving a translation, you must provide the number of the original object, the language and the editor who gave the translation. Approving a translation will also approve the original object if it wasn't already approved by you.