How to search in Prooftopia

Prooftopia is a database of mathematical theorems, proofs, predicates, symbols, authors, 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).

General parameters (used in all searches)

Editor

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.

Language

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:

  • all languages are acceptable: this will return all possible translations in all available languages.
  • return only data available in the language used to display the main Prooftopia page, that is, the language you selected in the language menu at the top of the page, or English if you didn't change the language, or Spanish if you came through the link from my students' page. Data in other languages will be ignored. This is probably the most common choice for most users who are not editors looking for things to trasnlate.
  • return data from a list of languages. You must provide a list of the language numbers you want (the numbers appear in the language menu, next to their language). Data in any language from that list will be returned, regardless of the language you chose to display this page.

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.

Date

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.

Special parameters: subject area and position

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).

HOW TO SEARCH FOR THEOREMS
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.

Predicates

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:

  • Hypotheses(Predicate) = null
  • Hypotheses(Equality) = null
  • Hypotheses(Not(F)) = Hypotheses(F)
  • Hypotheses(For all x we have that F|There exist x such that F|There exist unique x such that F) = Hypotheses(F)
  • Hypotheses(Conjunction|Disjunction|Equivalence) = union of the Hypotheses of its subformulas
  • Hypotheses(If P then Q) = (All predicates in P) Union Hypotheses(Q)
  • Conclusions(Predicate) = Predicate
  • Conclusions(Equality) = "0"
  • Conclusions(Not F) = Conclusions(F)
  • Conclusions(For all x we have that F|There exist x such that F|There exist unique x such that F) = Conclusions(F)
  • Conclusions(Conjunction|Disjunction|Equivalence) = union of the Conclusions of its subformulas
  • Conclusions(If P then Q) = Conclusions(Q)

Symbols

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.

Keywords in the description 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.

Keywords in the bibliographical reference of the theorem

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.

Theorem number

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).

Proof status

The proof status of a theorem in Prooftopia can be one of the following:
  • Not proved. No-one has written a proof of this theorem yet.
  • Partially proved. A theorem has been partially proved if there is at least one proof of that theorem, and the theorem is not absolutely proved (see below).
  • Absolutely proved. We define absolutely proved theorems as follows: all axioms are absolutely proved theorems. A theorem is absolutely proved if there is a proof of the theorem that uses only absolutely proved theorems. When a theorem is absolutely proved, we know that it's definitely true (unless we have reason to doubt the axioms).
You can also tell Prooftopia that the proof status of the theorem is irrelevant.

Descendants

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.

Ancestors

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.

Applications

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.

Authors

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.

Year when published

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).

Study mode restrictions

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.

How to search for predicates

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.

Predicate number

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).

Keywords in the text of the predicate

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.

Theorem number of the definition of the predicate

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.

How to search for symbols

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.

Symbol number

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).

Keywords in the text of the symbol

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.

Keywords in the description of the symbol

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.

Theorem number of the definition of the symbol

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.

How to search for subject areas

In addition to editor, language and date, you can also use the following options: subject area number and keywords.

Subject area number

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).

Keywords in the name of the subject area

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.

How to search for applications

In addition to editor, language and date, you can also use the following options: application number and keywords.

Application number

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).

Keywords in the name of the application

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.

How to search for authors

In addition to editor, language and date, you can also use the following options: author number, keywords in surname and keywords in first name.

Author number

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).

Keywords in the author's surname

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.

Keywords in the author's first name

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.

How to create class notes

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.

Crash-course in first-order logic

First-order logic is the usual way to formalize mathematics into axioms, from which theorems can be proved.

Variables

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.

Functions

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).

Terms

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 - ∅).

Predicates

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

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.

Formulas

The simplest formula is a predicate that has been evaluated on terms, or an equality involving several terms, for example:
  • x is an element of A
  • A = B ∪ C = D ∩ B
  • V is vector space over the field K
  • G is a finite group
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:
  • not(x is an element of A)
  • (A = B) or (A and B are disjoint)
  • if (x is positive) then (the square root of x is well-defined)
  • for all ε if ε>0 then there exists δ such that δ>0 and for all x if |x - y|<δ then |f(x)-f(y)|<ε
  • there exists a unique X such that X is a set and for all A if A is a set then A ∪ X = A
  • G is a finite, simple abelian group if and only if G is a cyclic group of prime order

Theorems

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.

Proofs

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.

Terms in Prooftopia

Variables

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.

Examples

Symbols (functions)

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.

Examples

5
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

Terms in Prooftopia are defined recursively as follows:
A variable is a term, such as $x@, $A@, $v_1@, $baseOfTriangle@. If you want you can display the variable surrounded by parentheses writing ($x@), ($v_1@), etc.
An expression of the form: the character $, followed by a colon (:), followed by one or more digits, followed by a list of variables separated by commas (the list may be empty if you're using a constant), followed by the character @. The digits represent the number of a symbol that has been previously defined in Prooftopia, and which will be evaluated on the list of variables. For example, if the symbol for addition of natural numbers (+) has number 23 in Prooftopia, the expression $:23$x@,$y@@ is a term, representing x+y. It may optionally be surrounded by "(" and ")" if you want them to appear when it's displayed, so ($:23$x@,$y@@) is the same term, but it will be displayed as (x+y).
An expression of the form: dollar sign, followed by a colon (:), followed by one or more digits, followed by a list of terms separated by commas (the list may be empty if you're using a constant), followed by the character @. The digits represent the number of a symbol that has been previously defined in Prooftopia, and which will be evaluated on the list of terms. For example, if the symbol for addition of natural numbers (+) has number 23 in Prooftopia, the expression $:23($:23$x@,$y@@),$z@@ is a term, representing (x+y)+z. It may optionally be surrounded by "(" and ")" if you want them to appear when it's displayed.
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).

Examples

Theorems in Prooftopia

Predicates

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:

  1. the theorem is of the form "for all x1,x2,..., xn we have that E" where E is an equivalence (if and only if) with exactly two components
  2. the predicate is the first of the equivalent conditions in the formula E. The terms the predicate is evaluated on must be the n variables x1,...,xn and no other term. The variables x1,...,xn must appear in the predicate in this order.
One theorem can define at most one predicate.

Examples

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

Equalities

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.

Examples

Formulas

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.

Examples

Theorems

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).

Examples

Proofs in Prooftopia

General description

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.

Rules of inference

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.

How rules of inference work

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:
  1. Choose a rule of inference from the menu. This will complete Phase one of the rule of inference and take you automatically to Phase two.
  2. In Phase two the program will usually ask you to select one or more Known facts, Facts to prove, or even Theorems from the database, depending on the rule of inference. If you need one or more of the Known facts or Facts to prove, you can simply click on them: when you move your mouse over a formula that is eligible to be clicked on, it will be highlighted to indicate that it's a suitable candidate. Sometimes there may be an input box where you can enter the codes of Known facts, Facts to prove, or even Theorems from the database: the code of the N-th Theorem is @T(N), the N-th Known fact is @K(N), and the N-th Fact to prove is @P(N). These codes are the same in all languages. If you need to choose several formulas, bear in mind that the order in which you list them may be important, depending on the rule of inference. Here's how you make multiple selections:
    • If you're clicking on the formulas (Known facts and/or Facts to prove), click on as many as you wish, in the order you want. In Study mode, this will be how you select formulas for almost all rules of inference.
    • If you're using the box, separate the codes with double semicolons (;;), and list them in the order you want.
    • A few rules of inference will let you create the formula you'll use. When this is the case, the Formula Creator will appear (this is the same tool that editors use to add theorems to the database). You can build your formula and click on Submit formula when you're done.
  3. Depending on the rule, there may be just these two Phases, or additional Phases. Sometimes there's an extra Phase that's invisible to you, because you gave the program all the data it needs to do it by itself. If you are required to take any further action, the program will tell you what to do.
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.

Rules of inference exclusive to Prooftopia

Eliminate Fact to prove

Study mode
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:
  1. Choose Eliminate Fact to prove from the menu.
  2. Select the Facts to prove that you want to eliminate because they are Known facts. Click Done when you're finished.
Examples: You can see how this rule is used in the following Theorems and Proofs:
Research mode
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.

End of proof

Study 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:
  1. Choose End of proof from the menu.
  2. If the list of Facts to prove is indeed empty, Prooftopia will acknowledge that you finished this proof. If the list of Facts to prove is not empty, the program will send an error message alerting you to this fact.
Examples: You can see how this rule is used in the following Theorems and Proofs:
Research mode
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).

Claim

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:
  1. Choose Claim from the menu.
  2. Enter a formula using the Formula creator. Click Finish when done.
  3. Your claim will be added to the end of the list of Facts to prove.

Add Theorem to Known facts

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:
  1. Choose Add Theorem to Known facts from the menu.
  2. Enter the number of the Theorem in the box (if you want to add the N-th Theorem, you may either type @T(N) or just N in the box). If you want to add several Theorems, type their numbers separated by double semicolons (;;)
  3. If you are using Study mode restrictions, any ineligible Theorem you tried to add will signal an error message and will not be added to the list of Known facts. All eligible Theorems in Study mode and all Theorems in Research mode will be added to the list of Known facts.

Equalities

Reflexivity

Input: A term t
Output: The equality t = t.
How to use this rule:
  1. Choose Reflexivity from the menu.
  2. An input box will appear asking for the Prooftopia code for a term. If you want to see a tutorial on how to write a term in Prooftopia, this rule will show you a button with this option. Enter the code and click on the button Finish.
  3. The equality t = t will be added to the list of Known facts, where t is the term you entered.

Substitution

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:
  1. Choose Substitution from the menu.
  2. Select one equality from the list of Known facts.
  3. Select one formula from the list of Known facts which involves at least one of the terms that appear in the equality you had chosen in the previous Phase.
  4. The latter formula will be displayed. Each term which is eligible for substitution will be highlighted, and will have a menu of possible substitutions. Make all the substitutions you want and click Finish
  5. The formula with the chosen substitutions will be added to the list of Known facts.

Symmetry and transitivity

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:
  1. Choose Symmetry and transitivity from the menu.
  2. Select one or more equalities from the list of Known facts. If you choose multiple equalities, make sure that every additional equality has at least one term in common with at least one of the previous equalities. Click on Next phase when done.
  3. The terms from all the equalities will be displayed. Click on the terms you want to include in your new equality, in the order you want them to appear. Click on the Finish button when you're done.
  4. The new equality will be added to the list of Known facts.

Universal quantifiers

Universal elimination (or Universal instantiation)

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:
  1. Choose Universal elimination from the menu.
  2. Select a known formula of the form 'For all a1,...,an, P', where the variables a1,a2,...,an occur freely in P
  3. Several input boxes will appear. Create terms t1,...,tn that will replace the variables a1,...,an, such that no free occurrence of any ai in P falls within the scope of a quantifier quantifying a variable occurring in any tj. If you want to see a tutorial on how to write a term in Prooftopia, this rule will show you a button with this option. Click on the Finish button when you're done.
  4. The formula P(t1,...,tn|a1,...,an) obtained by replacing every ai with ti, i=1,...,n, will be added to the list of Known facts.

Universal negation elimination

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:
  1. Choose Universal negation elimination from the menu.
  2. Select a formula of the form 'Not For all a1,...,an, P'. This formula may be in the list of Known facts, or the list of Facts to prove.
  3. The term selector will appear. Enter the codes for new variables t1,...,tn, which will replace the variables a1,...,an in P.
  4. If the original formula was one of the Known facts, then the formula 'There exist t1,...,tn such that Not P(t1,...,tn|a1,...,an)' (obtained by replacing every ai with ti, i=1,...,n), will be added to the list of Known facts. On the other hand, if the original formula was a Fact to prove, then it will be replaced by the formula 'There exist t1,...,tn such that Not P(t1,...,tn|a1,...,an)' in that list.

Universal negation introduction

Input: There exist a1,...,an such that P
Output: Not For all a1,...,an, Not P
How to use this rule:
  1. Choose Universal negation introduction
  2. from the menu.
  3. Select a formula of the form 'There exist a1,...,an, such that P'. This formula may be in the list of Known facts, or the list of Facts to prove.
  4. The term selector will appear. Enter the codes for new variables t1,...,tn, which will replace the variables a1,...,an in P.
  5. If the original formula was one of the Known facts, then the formula 'Not For all t1,...,tn, Not P(t1,...,tn|a1,...,an)' (obtained by replacing every ai with ti, i=1,...,n), will be added to the list of Known facts; if P is of the form Not Q, then the program will automatically do Double negation elimination and write Q instead of 'Not Not Q'. On the other hand, if the original formula was a Fact to prove, then it will be replaced by the formula 'Not For all t1,...,tn, Not P(t1,...,tn|a1,...,an)' in that list; if P is of the form Not Q, then the program will automatically do Double negation elimination and write Q instead of 'Not Not Q'.

Existential quantifiers

Existential introduction (or Existential generalization)

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:
  1. Choose Existential introduction from the menu.
  2. Select a formula P(t1,...,tn|a1,...,an) from the list of Known facts, such that the variables a1,a2,...,an (n greater than or equal to 1) occur freely in P, and the terms (not necessarily variables) t1,t2,...,tn are such that no free occurrence of any ai in P falls within the scope of a quantifier quantifying a variable occurring in any tj.
  3. The formula 'There exist b1,...,bn, such that P(b1,...,bn|a1,...,an)' will be added to the list of Known facts. The variables b1,...,bn will be assigned by the program, and they will be different from any variable used in this proof.

Existential elimination (or Existential instantiation)

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:
  1. Choose Existential elimination from the menu.
  2. Select a formula of the form 'There exist a1,...,an, such that P(a1,...,an)' or of the form 'There exist unique a1,...,an, such that P' from the list of Known facts, such that the variables a1,a2,...,an (n greater than or equal to 1) occur freely in P.
  3. The formula P(k1,...,kn|a1,...,an) will be added to the list of Known facts, where k1,...,kn are constants unique to P, that is, they do not appear in any other formula in the proof. However, they may interact with other Known facts, so for example, you may prove they equal other terms.

Existential negation elimination

Input: Not There exist a1,...,an, such that P
Output: For all a1,...,an, Not P
How to use this rule:
  1. Choose Existential negation elimination from the menu.
  2. Select a formula of the form 'Not There exist a1,...,an, such that P'. This formula may be one of the Known facts or one of the Facts to prove.
  3. The term selector will appear. Enter the codes for new variables t1,...,tn, which will replace the variables a1,...,an in P.
  4. If your original formula came from the Known facts, then the formula 'For all t1,...,tn, Not P(t1,...,tn|a1,...,an)' (obtained by replacing every ai with ti, i=1,...,n), will be added to the list of Known facts. On the other hand, if your original formula was one of the Facts to prove, then it will be replaced by the formula 'For all t1,...,tn, Not P(t1,...,tn|a1,...,an)' in that list.

Existential negation introduction

Input: For all a1,...,an, P
Output: Not There exist a1,...,an, such that Not P
How to use this rule:
  1. Choose Existential negation introduction from the menu.
  2. Select a formula of the form 'For all a1,...,an, P'. This formula may be in the list of Known facts, or the list of Facts to prove.
  3. The term selector will appear. Enter the codes for new variables t1,...,tn, which will replace the variables a1,...,an in P.
  4. If the original formula was one of the Known facts, then the formula 'Not There exist t1,...,tn such that Not P(t1,...,tn|a1,...,an)' (obtained by replacing every ai with ti, i=1,...,n), will be added to the list of Known facts; if P is of the form Not Q, then the program will automatically do Double negation elimination and write Q instead of 'Not Not Q'. On the other hand, if the original formula was a Fact to prove, then it will be replaced by the formula 'Not There exist t1,...,tn such that Not P(t1,...,tn|a1,...,an)' in that list; if P is of the form Not Q, then the program will automatically do Double negation elimination and write Q instead of 'Not Not Q'.

Uniqueness

Uniqueness elimination

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:
  1. Choose Uniqueness elimination from the menu.
  2. Select a formula of the form 'There exist unique a1,...,an, such that P(a1,...,an)' from the list of Known facts, such that the variables a1,a2,...,an (n greater than or equal to 1) occur freely in P.
  3. Select two Known facts of the form P(t1,...,tn|a1,...,an) and P(s1,...,sn,|a1,...,an)
  4. The equalities ti = si for i=1,...,n will be added to the list of Known facts.

Negations

Double negation elimination

Input: A Known formula that is a double negation
Output: The formula without the double negation
How to use this rule:
  1. Choose Double negation elimination from the menu.
  2. Select a double negation (the negation of the negation of a formula) from the list of Known facts.
  3. The formula, without the double negation, will be added to the list of Known facts.

Double negation introduction

Input: A Known formula
Output: The double negation of the known formula
How to use this rule:
  1. Choose Double negation introduction from the menu.
  2. Select a formula from the list of Known facts.
  3. The formula you entered will be added to the list of Known facts with a double negation applied to it.

Conjunctions

Conjunction introduction (or Adjunction)

Input:Two or more Known formulas
Output: The conjunction of the formulas
How to use this rule:
  1. Choose Conjunction introduction from the menu.
  2. Select one or more formulas from the list of Known facts.
  3. The conjunction of the formulas will be added to the list of Known facts.

Conjunction elimination (or Simplification)

Input: A known conjunction
Output: Any component of the conjunction
How to use this rule:
  1. Choose Conjunction elimination from the menu.
  2. Select a conjunction from the list of Known facts.
  3. The list of components of the conjunction will be displayed. Click on any of them, as many as you want. Each component that you click on will be added to the list of Known facts. When you are done, click on Finish

Conjunction commutativity

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:
  1. Choose Conjunction commutativity from the menu.
  2. Select a conjunction from the list of Known facts.
  3. The list of components of the conjunction will be displayed. Click on any of them, as many as you want (at least two) and in the order that you want. When you are done, click on Finish
  4. The conjunction you created with the chosen components, in the order you clicked them, will be added to the list of Known facts.

Disjunctions

Disjunction introduction (or Addition)

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:
  1. Choose Disjunction introduction from the menu.
  2. Select one formula from the list of Known facts.
  3. The formula creator will appear, together with an input box. You must either use the Formula Creator to create a formula, or enter a formula in the box. Then you must click Add another formula, Add known fact or Finish, depending on whether you want to add another formula, place the original Known formula in the disjunction, or finish this rule of inference.
  4. After you click on Finish, the disjunction made up of the known formula and the additional formulas will be added to the list of Known facts. If you want to rearrange the components, use Disjunction commutativity.

Case analysis

Input: A known disjunction, such that all its components are known to imply the same formula Q
Output: Q
How to use this rule:
  1. Choose Case analysis from the menu.
  2. Select one disjunction from the list of Known facts.
  3. If there is a formula Q which is known to be implied by all components of the disjunction, then Q will be added to the list of Known facts; otherwise your disjunction will be rejected.

Disjunctive syllogism

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:
  1. Choose Disjunctive syllogism from the menu.
  2. Select one disjunction from the list of Known facts. The disjunction must have exactly two components.
  3. If exactly one of the components of the disjunction is known to be false (that is, its negation is a Known fact), then the other component will be added to the list of Known facts; otherwise your disjunction will be rejected.

Excluded third

Input: Any formula, whether known or unknown
Output: The disjunction of the formula and its negation
How to use this rule:
  1. Choose Excluded third from the menu.
  2. The formula creator will appear, together with an input box. You must either use the Formula Creator to create a formula, or enter a formula in the box. Then you must click Finish.
  3. The disjunction of the formula and its negation will be added to the list of Known facts.

Disjunction commutativity

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:
  1. Choose Disjunction commutativity from the menu.
  2. Select a disjunction from the list of Known facts.
  3. The list of components of the disjunction will be displayed. Click on each of them in the order that you want. When you have clicked on the last component, this Phase will be done.
  4. The disjunction you created will be added to the list of Known facts.

Conditionals

Conditional elimination (or Modus ponens)

Input: A known implication whose hypothesis is also known Output: The conclusion of the implication How to use this rule: Choose Conditional elimination from the menu. Select an implication from the list of Known facts. If the hypothesis of the implication is known, then the conclusion will be added to the list of Known facts. Otherwise your implication will be rejected. Modus tollens Input: A known implication whose conclusion is known to be false Output: The negation of the hypothesis How to use this rule: Choose Modus tollens from the menu. Select an implication from the list of Known facts. If the conclusion of the implication is known to be false (that is, its negation is a Known fact), then the negation of the hypothesis will be added to the list of Known facts. Otherwise your implication will be rejected. Transitivity of conditionals 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: Choose Transitivity of conditionals from the menu. Select a sequence of implications from the list of Known facts. The order is important, and the conclusion of each implication must coincide with the hypothesis of the next implication When you're done (you must have at least two implications), click Finish. A new implication will be added to the list of Known facts. Its hypothesis is the hypothesis of the first implication, and its conclusion is the conclusion of the last implication. Biconditionals Biconditional introduction 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: Choose Biconditional introduction from the menu. Select a sequence of implications from the list of Known facts. The order is important, and the conclusion of each implication must coincide with the hypothesis of the next implication When you click on the last implication,, whose conclusion is the hypothesis of the first implication, the rule will automatically end. The equivalence of all the conclusions will be added to the list of Known facts. Biconditional elimination 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: Choose Biconditional elimination from the menu. Click on a known equivalence, where at least one of its components is known. A list of the components of the equivalence will appear. Click on one or several of the components that you want to add to the list of known facts. When you are done, click Finish. In research mode, if there are only two components and exactly one of them is known, then the other component will automatically be chosen by the program. Biconditional elimination with negation 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: Choose Biconditional elimination with negation from the menu. Click on a known equivalence, where at least one of its components is known to be false (that is, its negation is a Known fact). A list of the components of the equivalence will appear. Click on one or several of the components whose negations you want to add to the list of known facts. When you are done, click Finish. In research mode, if there are only two components and exactly one of them is known to be false, then the other component will automatically be chosen by the program. Biconditional simplification to conditional Input: A known equivalence Output: The implication of any two of its components. How to use this rule: Choose Biconditional simplification to conditional from the menu. Click on a known equivalence. A list of the components of the equivalence will appear. Click on one of the components (the hypothesis) and then click on a different component (the conclusion); this implication will be added to the list of known facts. Continue until you have added all the implications you wanted. When you are done, click Finish Biconditional commutativity 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: Choose Biconditional commutativity from the menu. Click on a known equivalence. The list of components of the equivalence will be displayed. Click on any of them, as many as you want (at least two) and in the order that you want. When you are done, click on Finish The equivalence you created with the chosen components, in the order you clicked them, will be added to the list of Known facts. Rules of inference with long-term effect 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. Conditional introduction (or Deduction theorem) 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: First part of Conditional introduction: Choose Conditional introduction begins from the menu. Click on a formula from the Facts to prove which is of the form IMPLIES(P,Q) The formula IMPLIES(P,Q) will be removed from the list of Facts to prove, P will be added to the list of Known facts, and Q will be added to the list of Facts to prove. This is the end of the first part of Conditional introduction. Second part of Conditional introduction: This is triggered automatically in Research mode when Q is known. In Study mode, once Q is known, you must choose the rule Conditional introduction ends and click on Q. The list of Known facts and Facts to prove will revert to what they were before the first part of this rule was called. All global variables created after that point will also be deleted (those names can be used again for new variables). The formula IMPLIES(P,Q) will be added to the list of Known facts. Universal introduction (or Universal generalization) 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: First part of Universal introduction: Choose Universal introduction begins from the menu. Click on a formula from the Facts to prove which is of the form FOR_ALL([a1,...,an],P). If the formula you want is not in the list of Facts to prove, you'll have to make a claim (Claim is one of the rules of inference exclusive to Prooftopia). If necessary, rename variables in your formula so that they don't have the same name as a User-made variable currently in use. Let's assume the variables that replaced the a1,...,an are called b1,...,bn . When you are done, click Process. The formula FOR_ALL([a1,...,an],P) will be removed from the list of Facts to prove. The formula P(b1,...,bn|a1,...,an) will be added to the list of Facts to prove. If P is an implication (which is almost always the case), the Conditional introduction will be initiated automatically, which means that P will be instantly removed from the list of Facts to prove, the hypothesis of P will be added to the list of Known facts (to be deleted after the second part of the Universal introduction is finished), and the conclusion of P will be added to the list of Facts to prove. When that conclusion becomes known, you'll be able to finish both the Conditional introduction and the Universal introduction. This is the end of the first part of Universal introduction. None of the current Facts to prove can be eliminated (but you can eliminate new Facts to prove generated after this point) until you finish the second part of this rule. Second part of Universal introduction: This is triggered automatically in Research mode when P(b1,...,bn|a1,...,bn) (or its conclusion, if P is an implication) is known. In Study mode, once P(b1,...,bn|a1,...,an) (or its conclusion, if P is an implication) is known, you must choose the rule Universal introduction ends and click on P(b1,...,bn|a1,...,an). If P was an implication, then instead of P you must click on the conclusion of P. The list of Known facts and Facts to prove will revert to what they were before the first part of this rule was called, and all User-made variables created after that point will also be deleted (those names can be used again for new variables). The formula FOR_ALL([a1,...,an],P) will be added to the list of Known facts. Proof by contradiction (or Reductio ad absurdum) 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: First part of Proof by contradiction: Choose Proof by contradiction begins from the menu. Either click on a formula P from the list of Facts to prove, or enter one in the Formula creator. The formula NOT(P) will be added to the list of Known facts. This is the end of the first part of this rule. Second part of Proof by contradiction: This is triggered automatically in Research mode when you reach a contradiction (a formula Q and its negation are both Known facts). In Study mode, once you reach a contradiction (a formula Q and its negation are both Known facts), you must choose the rule Proof by contradiction ends and click on Q and NOT(Q). Note that either Q or NOT(Q) (but not both) may have been added to the Known facts before P (in this case we're contradicting a hypothesis). If you have several Proofs by contradiction going simultaneously, this will conclude the most recent Proof by contradiction. The list of Known facts and Facts to prove will revert to what they were before the first part of this rule was called. All global variables created after that point will also be deleted (those names can be used again for new variables). The formula P will be added to the list of Known facts. Uniqueness introduction 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: First part of Uniqueness introduction: Choose Uniqueness introduction begins from the menu. Click on a formula from the Known facts which is of the form 'There exist a1,...,an such that P'. Create new variables (which don't use names currently in the list of User-made variables), say b1,...,bn The formula P will be added to the list of Known facts. The formula P(b1,...,bn|a1,...,an) will be added to the list of Known facts. This is the end of the first part of this rule. None of the current Facts to prove can be eliminated (but you can eliminate new Facts to prove generated after this point) until you finish the second part of this rule. Second part of Uniqueness introduction: This is triggered automatically in Research mode when all the equalities ai = bi for i=1,...,n are known. In Study mode, once all the equalities ai = bi for i=1,...,n are known, you must choose the rule Uniqueness introduction ends and click on the equalities a1 = b1, a2 = b2, ... in order. The list of Known facts and Facts to prove will revert to what they were before the first part of this rule was called, and all User-made variables created after that point will also be deleted (those names can be used again for new variables). The formula 'There exist unique a1,...,an, such that P' will be added to the list of Known facts. Back to top

Get in touch

Phasellus convallis elit id ullamcorper pulvinar. Duis aliquam turpis mauris, eu ultricies erat malesuada quis. Aliquam dapibus, lacus eget hendrerit bibendum, urna est aliquam sem, sit amet imperdiet est velit quis lorem.