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