Home Intuitionistic Logic ExplorerTheorem List (p. 99 of 102) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 9801-9900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremclimrel 9801 The limit relation is a relation. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim 9802* Express the predicate: The limit of complex number sequence is , or converges to . This means that for any real , no matter how small, there always exists an integer such that the absolute difference of any later complex number in the sequence and the limit is less than . (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Theoremclimcl 9803 Closure of the limit of a sequence of complex numbers. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Theoremclim2 9804* Express the predicate: The limit of complex number sequence is , or converges to , with more general quantifier restrictions than clim 9802. (Contributed by NM, 6-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim2c 9805* Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim0 9806* Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclim0c 9807* Express the predicate converges to . (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimi 9808* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimi2 9809* Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimi0 9810* Convergence of a sequence of complex numbers to zero. (Contributed by NM, 11-Jan-2007.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimconst 9811* An (eventually) constant sequence converges to its value. (Contributed by NM, 28-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimconst2 9812 A constant sequence converges to its value. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimz 9813 The zero sequence converges to zero. (Contributed by NM, 2-Oct-1999.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimuni 9814 An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 2-Oct-1999.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

Theoremfclim 9815 The limit relation is function-like, and with range the complex numbers. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremclimdm 9816 Two ways to express that a function has a limit. (The expression is sometimes useful as a shorthand for "the unique limit of the function "). (Contributed by Mario Carneiro, 18-Mar-2014.)

Theoremclimeu 9817* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)

Theoremclimreu 9818* An infinite sequence of complex numbers converges to at most one limit. (Contributed by NM, 25-Dec-2005.)

Theoremclimmo 9819* An infinite sequence of complex numbers converges to at most one limit. (Contributed by Mario Carneiro, 13-Jul-2013.)

Theoremclimeq 9820* Two functions that are eventually equal to one another have the same limit. (Contributed by Mario Carneiro, 5-Nov-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimmpt 9821* Exhibit a function with the same convergence properties as the not-quite-function . (Contributed by Mario Carneiro, 31-Jan-2014.)

Theorem2clim 9822* If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

Theoremclimshftlemg 9823 A shifted function converges if the original function converges. (Contributed by Mario Carneiro, 5-Nov-2013.)

Theoremclimres 9824 A function restricted to upper integers converges iff the original function converges. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimshft 9825 A shifted function converges iff the original function converges. (Contributed by NM, 16-Aug-2005.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremiserclim0 9826 The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.)

Theoremclimshft2 9827* A shifted function converges iff the original function converges. (Contributed by Paul Chapman, 21-Nov-2007.) (Revised by Mario Carneiro, 6-Feb-2014.)

Theoremclimabs0 9828* Convergence to zero of the absolute value is equivalent to convergence to zero. (Contributed by NM, 8-Jul-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Theoremclimcn1 9829* Image of a limit under a continuous map. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremclimcn2 9830* Image of a limit under a continuous map, two-arg version. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremaddcn2 9831* Complex number addition is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (We write out the definition directly because df-cn and df-cncf are not yet available to us. See addcn for the abbreviated version.) (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremsubcn2 9832* Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremmulcn2 9833* Complex number multiplication is a continuous function. Part of Proposition 14-4.16 of [Gleason] p. 243. (Contributed by Mario Carneiro, 31-Jan-2014.)

Theoremcn1lem 9834* A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremabscn2 9835* The absolute value function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremcjcn2 9836* The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremrecn2 9837* The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremimcn2 9838* The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremclimcn1lem 9839* The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremclimabs 9840* Limit of the absolute value of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimcj 9841* Limit of the complex conjugate of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimre 9842* Limit of the real part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimim 9843* Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of [Gleason] p. 172. (Contributed by NM, 7-Jun-2006.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimrecl 9844* The limit of a convergent real sequence is real. Corollary 12-2.5 of [Gleason] p. 172. (Contributed by NM, 10-Sep-2005.)

Theoremclimge0 9845* A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005.)

Theoremclimadd 9846* Limit of the sum of two converging sequences. Proposition 12-2.1(a) of [Gleason] p. 168. (Contributed by NM, 24-Sep-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2014.)

Theoremclimmul 9847* Limit of the product of two converging sequences. Proposition 12-2.1(c) of [Gleason] p. 168. (Contributed by NM, 27-Dec-2005.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)

Theoremclimsub 9848* Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168. (Contributed by NM, 4-Aug-2007.) (Proof shortened by Mario Carneiro, 1-Feb-2014.)

Theoremclimaddc1 9849* Limit of a constant added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimaddc2 9850* Limit of a constant added to each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimmulc2 9851* Limit of a sequence multiplied by a constant . Corollary 12-2.2 of [Gleason] p. 171. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimsubc1 9852* Limit of a constant subtracted from each term of a sequence. (Contributed by Mario Carneiro, 9-Feb-2014.)

Theoremclimsubc2 9853* Limit of a constant minus each term of a sequence. (Contributed by NM, 24-Sep-2005.) (Revised by Mario Carneiro, 9-Feb-2014.)

Theoremclimle 9854* Comparison of the limits of two sequences. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)

Theoremclimsqz 9855* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 6-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclimsqz2 9856* Convergence of a sequence sandwiched between another converging sequence and its limit. (Contributed by NM, 14-Feb-2008.) (Revised by Mario Carneiro, 3-Feb-2014.)

Theoremclim2iser 9857* The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.)

Theoremclim2iser2 9858* The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.)

Theoremiiserex 9859* An infinite series converges, if and only if the series does with initial terms removed. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 27-Apr-2014.)

Theoremiisermulc2 9860* Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Mario Carneiro, 1-Feb-2014.)

Theoremclimlec2 9861* Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008.) (Revised by Mario Carneiro, 1-Feb-2014.)

Theoremiserile 9862* Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.)

Theoremiserige0 9863* The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.)

Theoremclimub 9864* The limit of a monotonic sequence is an upper bound. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 10-Feb-2014.)

Theoremclimserile 9865* The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.)

Theoremclimcau 9866* A converging sequence of complex numbers is a Cauchy sequence. The converse would require excluded middle or a different definition of Cauchy sequence (for example, fixing a rate of convergence as in climcvg1n 9869). Theorem 12-5.3 of [Gleason] p. 180 (necessity part). (Contributed by NM, 16-Apr-2005.) (Revised by Mario Carneiro, 26-Apr-2014.)

Theoremclimrecvg1n 9867* A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)

Theoremclimcvg1nlem 9868* Lemma for climcvg1n 9869. We construct sequences of the real and imaginary parts of each term of , show those converge, and use that to show that converges. (Contributed by Jim Kingdon, 24-Aug-2021.)

Theoremclimcvg1n 9869* A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.)

Theoremclimcaucn 9870* A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 9866 but adds the part that is complex. (Contributed by Jim Kingdon, 24-Aug-2021.)

Theoremserif0 9871* If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 16-Feb-2014.)

3.8.2  Finite and infinite sums

Syntaxcsu 9872 Extend class notation to include finite summations. (An underscore was added to the ASCII token in order to facilitate set.mm text searches, since "sum" is a commonly used word in comments.)

Definitiondf-sum 9873* Define the sum of a series with an index set of integers . is normally a free variable in , i.e. can be thought of as . This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. These two methods of summation produce the same result on their common region of definition (i.e. finite subsets of the upper integers). Examples: means , and means 1/2 + 1/4 + 1/8 + ... = 1. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Theoremsumeq1 9874 Equality theorem for a sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Theoremnfsum1 9875 Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Theoremnfsum 9876 Bound-variable hypothesis builder for sum: if is (effectively) not free in and , it is not free in . (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

PART 4  ELEMENTARY NUMBER THEORY

Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.

4.1  Elementary properties of divisibility

4.1.1  Rationality of square root of 2

Theoremsqr2irrlem 9877 Lemma concerning rationality of square root of 2. The core of the proof - if , then and are even, so and are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)

Theoremsqrt2irr 9878 The square root of 2 is not rational. That is, for any rational number, does not equal it. However, if we were to say "the square root of 2 is irrational" that would mean something stronger: "for any rational number, is apart from it" (the two statements are equivalent given excluded middle). We do not prove irrationality in this stronger sense here.

The proof's core is proven in sqr2irrlem 9877, which shows that if , then and are even, so and are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)

Theoremsqrt2re 9879 The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.)

4.1.2  Algorithms

Theoremnn0seqcvgd 9880* A strictly-decreasing nonnegative integer sequence with initial term reaches zero by the th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremialgrlem1st 9881 Lemma for ialgr0 9883. Expressing algrflemg 5851 in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.)

Theoremialgrlemconst 9882 Lemma for ialgr0 9883. Closure of a constant function, in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.)

Theoremialgr0 9883 The value of the algorithm iterator at is the initial state . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)

Theoremialgrf 9884 An algorithm is a step function on a state space . An algorithm acts on an initial state by iteratively applying to give , , and so on. An algorithm is said to halt if a fixed point of is reached after a finite number of iterations.

The algorithm iterator "runs" the algorithm so that is the state after iterations of on the initial state .

Domain and codomain of the algorithm iterator . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)

Theoremialgrp1 9885 The value of the algorithm iterator at . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)

Theoremialginv 9886* If is an invariant of , its value is unchanged after any number of iterations of . (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremialgcvg 9887* One way to prove that an algorithm halts is to construct a countdown function whose value is guaranteed to decrease for each iteration of until it reaches . That is, if is not a fixed point of , then .

If is a countdown function for algorithm , the sequence reaches after at most steps, where is the value of for the initial state . (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremalgcvgblem 9888 Lemma for algcvgb 9889. (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremalgcvgb 9889 Two ways of expressing that is a countdown function for algorithm . The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.)

Theoremialgcvga 9890* The countdown function remains after steps. (Contributed by Paul Chapman, 22-Jun-2011.)

Theoremialgfx 9891* If reaches a fixed point when the countdown function reaches , remains fixed after steps. (Contributed by Paul Chapman, 22-Jun-2011.)

PART 5  GUIDES AND MISCELLANEA

5.1  Guides (conventions, explanations, and examples)

5.1.1  Conventions

This section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. The following sources lay out how mathematics is developed without the law of the excluded middle. Of course, there are a greater number of sources which assume excluded middle and most of what is in them applies here too (especially in a treatment such as ours which is built on first order logic and set theory, rather than, say, type theory). Studying how a topic is treated in the Metamath Proof Explorer and the references therein is often a good place to start (and is easy to compare with the Intuitionistic Logic Explorer). The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following:

• Axioms of propositional calculus - Stanford Encyclopedia of Philosophy or [Heyting].
• Axioms of predicate calculus - our axioms are adapted from the ones in the Metamath Proof Explorer.
• Theorems of propositional calculus - [Heyting].
• Theorems of pure predicate calculus - Metamath Proof Explorer.
• Theorems of equality and substitution - Metamath Proof Explorer.
• Axioms of set theory - [Crosilla].
• Development of set theory - Chapter 10 of [HoTT].
• Construction of real and complex numbers - Chapter 11 of [HoTT]; [BauerTaylor].
• Theorems about real numbers - [Geuvers].

Theoremconventions 9892 Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (aka "set.mm"). This list of conventions is intended to be read in conjunction with the corresponding conventions in the Metamath Proof Explorer, and only the differences are described below.

• Minimizing axioms and the axiom of choice. We prefer proofs that depend on fewer and/or weaker axioms, even if the proofs are longer. In particular, our choice of IZF (Intuitionistic Zermelo-Fraenkel) over CZF (Constructive Zermelo-Fraenkel, a weaker system) was just an expedient choice because IZF is easier to formalize in metamath. You can find some development using CZF in BJ's mathbox starting at ax-bd0 9933 (and the section header just above it). As for the axiom of choice, the full axiom of choice implies excluded middle as seen at acexmid 5511, although some authors will use countable choice or dependent choice. For example, countable choice or excluded middle is needed to show that the Cauchy reals coincide with the Dedekind reals - Corollary 11.4.3 of [HoTT], p. (varies).
• Junk/undefined results. Much of the discussion of this topic in the Metamath Proof Explorer applies except that certain techniques are not available to us. For example, the Metamath Proof Explorer will often say "if a function is evaluated within its domain, a certain result follows; if the function is evaluated outside its domain, the same result follows. Since the function must be evaluated within its domain or outside it, the result follows unconditionally" (the use of excluded middle in this argument is perhaps obvious when stated this way). For this reason, we generally need to prove we are evaluating functions within their domains and avoid the reverse closure theorems of the Metamath Proof Explorer.
• Bibliography references. The bibliography for the Intuitionistic Logic Explorer is separate from the one for the Metamath Proof Explorer but feel free to copy-paste a citation in either direction in order to cite it.

Label naming conventions

Here are a few of the label naming conventions:

• Suffixes. We follow the conventions of the Metamath Proof Explorer with a few additions. A biconditional in set.mm which is an implication in iset.mm should have a "r" (for the reverse direction), or "i"/"im" (for the forward direction) appended. A theorem in set.mm which has a decidability condition added should add "dc" to the theorem name. A theorem in set.mm where "nonempty class" is changed to "inhabited class" should add "m" (for member) to the theorem name.

The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.

AbbreviationMnenomicSource ExpressionSyntax?Example(s)
apapart df-ap 7573 Yes apadd1 7599, apne 7614

• Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at: https://groups.google.com/forum/#!forum/metamath.
• (Contributed by Jim Kingdon, 24-Feb-2020.)

5.1.2  Definitional examples

Theoremex-or 9893 Example for ax-io 630. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

Theoremex-an 9894 Example for ax-ia1 99. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.)

Theoremex-fl 9895 Example for df-fl 9114. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.)

Theoremex-ceil 9896 Example for df-ceil 9115. (Contributed by AV, 4-Sep-2021.)

PART 6  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)

6.1  Mathboxes for user contributions

6.1.1  Mathbox guidelines

Theoremmathbox 9897 (This theorem is a dummy placeholder for these guidelines. The name of this theorem, "mathbox", is hard-coded into the Metamath program to identify the start of the mathbox section for web page generation.)

A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of set.mm.

For contributors:

By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of set.mm.

Mathboxes are provided to help keep your work synchronized with changes in set.mm, but they shouldn't be depended on as a permanent archive. If you want to preserve your original contribution, it is your responsibility to keep your own copy of it along with the version of set.mm that works with it.

Guidelines:

1. If at all possible, please use only 0-ary class constants for new definitions.

2. Try to follow the style of the rest of set.mm. Each \$p and \$a statement must be immediately preceded with the comment that will be shown on its web page description. The metamath program command "write source set.mm /rewrap" will take care of wrapping comment lines and indentation conventions. All mathbox content will be on public display and should hopefully reflect the overall quality of the website.

3. Before submitting a revised mathbox, please make sure it verifies against the current set.mm.

4. Mathboxes should be independent i.e. the proofs should verify with all other mathboxes removed. If you need a theorem from another mathbox, that is fine (and encouraged), but let me know, so I can move the theorem to the main section. One way avoid undesired accidental use of other mathbox theorems is to develop your mathbox using a modified set.mm that has mathboxes removed.

Notes:

1. We may decide to move some theorems to the main part of set.mm for general use.

2. We may make changes to mathboxes to maintain the overall quality of set.mm. Normally we will let you know if a change might impact what you are working on.

3. If you use theorems from another user's mathbox, we don't provide assurance that they are based on correct or consistent \$a statements. (If you find such a problem, please let us know so it can be corrected.) (Contributed by NM, 20-Feb-2007.) (New usage is discouraged.)

6.2  Mathbox for Mykola Mostovenko

Theoremax1hfs 9898 Heyting's formal system Axiom #1 from [Heyting] p. 127. (Contributed by MM, 11-Aug-2018.)

6.3  Mathbox for BJ

6.3.1  Propositional calculus

Theoremnnexmid 9899 Double negation of excluded middle. Intuitionistic logic refutes the negation of excluded middle (but, of course, does not prove excluded middle) for any formula. (Contributed by BJ, 9-Oct-2019.)

Theoremnndc 9900 Double negation of decidability of a formula. Intuitionistic logic refutes undecidability (but, of course, does not prove decidability) of any formula. (Contributed by BJ, 9-Oct-2019.)
DECID

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
 Copyright terms: Public domain < Previous  Next >