Intuitionistic Logic Explorer Most Recent Proofs Mirrors  >  Home  >  ILE Home  >  Th. List  >  Recent MPE Most Recent             Other  >  MM 100

Most recent proofs    These are the 100 (Unicode, GIF) or 1000 (Unicode, GIF) most recent proofs in the iset.mm database for the Intuitionistic Logic Explorer. The iset.mm database is maintained on GitHub with master (stable) and develop (development) versions. This page was created from the commit given on the MPE Most Recent Proofs page. The database from that commit is also available here: iset.mm.

See the MPE Most Recent Proofs page for news and some useful links.

 Color key: Intuitionistic Logic Explorer User Mathboxes

Last updated on 17-Sep-2024 at 6:39 AM ET.
Recent Additions to the Intuitionistic Logic Explorer
DateLabelDescription
Theorem

14-Sep-2024nnpredlt 4582 The predecessor (see nnpredcl 4581) of a nonzero natural number is less than (see df-iord 4326) that number. (Contributed by Jim Kingdon, 14-Sep-2024.)

13-Sep-2024nninfisollemeq 7069 Lemma for nninfisol 7070. The case where is a successor and and are equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
DECID

13-Sep-2024nninfisollemne 7068 Lemma for nninfisol 7070. A case where is a successor and and are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.)
DECID

13-Sep-2024nninfisollem0 7067 Lemma for nninfisol 7070. The case where is zero. (Contributed by Jim Kingdon, 13-Sep-2024.)
DECID

12-Sep-2024nninfisol 7070 Finite elements of ℕ are isolated. That is, given a natural number and any element of ℕ, it is decidable whether the natural number (when converted to an element of ℕ) is equal to the given element of ℕ. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence to decide whether it is equal to (in fact, you only need to look at two elements and tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.)
DECID

7-Sep-2024eulerthlemfi 12091 Lemma for eulerth 12096. The set is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)
..^

7-Sep-2024modqexp 10537 Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.)

5-Sep-2024eulerthlemh 12094 Lemma for eulerth 12096. A permutation of . (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.)
..^

2-Sep-2024eulerthlemth 12095 Lemma for eulerth 12096. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
..^

2-Sep-2024eulerthlema 12093 Lemma for eulerth 12096. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
..^

2-Sep-2024eulerthlemrprm 12092 Lemma for eulerth 12096. and are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.)
..^

30-Aug-2024fprodap0f 11526 A finite product of terms apart from zero is apart from zero. A version of fprodap0 11511 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.)
#        #

28-Aug-2024fprodrec 11519 The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.)
#

26-Aug-2024exmidontri2or 7172 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
EXMID

26-Aug-2024exmidontri 7168 Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.)
EXMID

26-Aug-2024ontri2orexmidim 4530 Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4529. (Contributed by Jim Kingdon, 26-Aug-2024.)
DECID

26-Aug-2024ontriexmidim 4480 Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4479. (Contributed by Jim Kingdon, 26-Aug-2024.)
DECID

25-Aug-2024onntri2or 7175 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
EXMID

25-Aug-2024onntri3or 7174 Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.)
EXMID

25-Aug-2024csbcow 3042 Composition law for chained substitutions into a class. Version of csbco 3041 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024cbvreuvw 2686 Version of cbvreuv 2682 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024cbvrexvw 2685 Version of cbvrexv 2681 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024cbvralvw 2684 Version of cbvralv 2680 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024cbvabw 2280 Version of cbvab 2281 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024nfsbv 1927 If is not free in , it is not free in when is distinct from and . Version of nfsb 1926 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on . (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024cbvexvw 1900 Change bound variable. See cbvexv 1898 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024cbvalvw 1899 Change bound variable. See cbvalv 1897 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.)

25-Aug-2024nfal 1556 If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1490. (Revised by Gino Giotto, 25-Aug-2024.)

24-Aug-2024gcdcomd 11849 The operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)

17-Aug-2024fprodcl2lem 11495 Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.)

16-Aug-2024if0ab 13351 Expression of a conditional class as a class abstraction when the False alternative is the empty class: in that case, the conditional class is the extension, in the True alternative, of the condition.

Remark: a consequence which could be formalized is the inclusion and therefore, using elpwg 3551, , from which fmelpw1o 13352 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.)

16-Aug-2024fprodunsn 11494 Multiply in an additional term in a finite product. See also fprodsplitsn 11523 which is the same but with a hypothesis in place of the distinct variable condition between and . (Contributed by Jim Kingdon, 16-Aug-2024.)

15-Aug-2024bj-charfundcALT 13355 Alternate proof of bj-charfundc 13354. It was expected to be much shorter since it uses bj-charfun 13353 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
DECID

15-Aug-2024bj-charfun 13353 Properties of the characteristic function on the class of the class . (Contributed by BJ, 15-Aug-2024.)

15-Aug-2024fmelpw1o 13352 With a formula one can associate an element of , which can therefore be thought of as the set of "truth values" (but recall that there are no other genuine truth values than and , by nndc 837, which translate to and respectively by iftrue 3510 and iffalse 3513, giving pwtrufal 13540).

As proved in if0ab 13351, the associated element of is the extension, in , of the formula . (Contributed by BJ, 15-Aug-2024.)

15-Aug-2024cnstab 8514 Equality of complex numbers is stable. Stability here means as defined at df-stab 817. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.)
STAB

15-Aug-2024subap0d 8513 Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.)
#        #

15-Aug-2024ifexd 4443 Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.)

15-Aug-2024ifelpwun 4442 Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.)

15-Aug-2024ifelpwund 4441 Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.)

15-Aug-2024ifelpwung 4440 Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.)

15-Aug-2024ifidss 3520 A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.)

15-Aug-2024ifssun 3519 A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.)

12-Aug-2024exmidontriimlem2 7151 Lemma for exmidontriim 7154. (Contributed by Jim Kingdon, 12-Aug-2024.)
EXMID

12-Aug-2024exmidontriimlem1 7150 Lemma for exmidontriim 7154. A variation of r19.30dc 2604. (Contributed by Jim Kingdon, 12-Aug-2024.)
EXMID

11-Aug-2024nndc 837 Double negation of decidability of a formula. Intuitionistic logic refutes the negation of decidability (but does not prove decidability) of any formula.

This should not trick the reader into thinking that EXMID is provable in intuitionistic logic. Indeed, if we could quantify over formula metavariables, then generalizing nnexmid 836 over would give " DECID ", but EXMID is "DECID ", so proving EXMID would amount to proving " DECID ", which is not implied by the above theorem. Indeed, the converse of nnal 1629 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of , like we do in our definition of EXMID (df-exmid 4156): then, we can prove DECID but we cannot prove DECID because the converse of nnral 2447 does not hold.

Actually, EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying EXMID and noncontradiction holds (pm3.24 683). (Contributed by BJ, 9-Oct-2019.) Add explanation on non-provability of EXMID. (Revised by BJ, 11-Aug-2024.)

DECID

10-Aug-2024exmidontriim 7154 Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.)
EXMID

10-Aug-2024exmidontriimlem4 7153 Lemma for exmidontriim 7154. The induction step for the induction on . (Contributed by Jim Kingdon, 10-Aug-2024.)
EXMID

10-Aug-2024exmidontriimlem3 7152 Lemma for exmidontriim 7154. What we get to do based on induction on both and . (Contributed by Jim Kingdon, 10-Aug-2024.)
EXMID

10-Aug-2024nnnninf2 7064 Canonical embedding of into ℕ. (Contributed by BJ, 10-Aug-2024.)

10-Aug-2024infnninf 7061 The point at infinity in ℕ is the constant sequence equal to . Note that with our encoding of functions, that constant function can also be expressed as , as fconstmpt 4632 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.)

9-Aug-2024ss1o0el1o 6854 Reformulation of ss1o0el1 4158 using instead of . (Contributed by BJ, 9-Aug-2024.)

9-Aug-2024pw1dc0el 6853 Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.)
EXMID DECID

9-Aug-2024ss1o0el1 4158 A subclass of contains the empty set if and only if it equals . (Contributed by BJ and Jim Kingdon, 9-Aug-2024.)

8-Aug-2024pw1dc1 6855 If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.)
EXMID DECID

7-Aug-2024pw1fin 6852 Excluded middle is equivalent to the power set of being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.)
EXMID

7-Aug-2024elomssom 4563 A natural number ordinal is, as a set, included in the set of natural number ordinals. (Contributed by NM, 21-Jun-1998.) Extract this result from the previous proof of elnn 4564. (Revised by BJ, 7-Aug-2024.)

6-Aug-2024bj-charfunbi 13357 In an ambient set , if membership in is stable, then it is decidable if and only if has a characteristic function.

This characterization can be applied to singletons when the set has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.)

STAB        DECID

6-Aug-2024bj-charfunr 13356 If a class has a "weak" characteristic function on a class , then negated membership in is decidable (in other words, membership in is testable) in .

The hypothesis imposes that be a set. As usual, it could be formulated as to deal with general classes, but that extra generality would not make the theorem much more useful.

The theorem would still hold if the codomain of were any class with testable equality to the point where is sent. (Contributed by BJ, 6-Aug-2024.)

DECID

6-Aug-2024bj-charfundc 13354 Properties of the characteristic function on the class of the class , provided membership in is decidable in . (Contributed by BJ, 6-Aug-2024.)
DECID

6-Aug-2024prodssdc 11479 Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.)
#        DECID                             DECID

5-Aug-2024fnmptd 13350 The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.)

5-Aug-2024funmptd 13349 The maps-to notation defines a function (deduction form).

Note: one should similarly prove a deduction form of funopab4 5206, then prove funmptd 13349 from it, and then prove funmpt 5207 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.)

5-Aug-20242ssom 13348 The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.)

5-Aug-2024bj-dcfal 13298 The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
DECID

5-Aug-2024bj-dctru 13296 The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.)
DECID

5-Aug-2024bj-stfal 13288 The false truth value is stable. (Contributed by BJ, 5-Aug-2024.)
STAB

5-Aug-2024bj-sttru 13286 The true truth value is stable. (Contributed by BJ, 5-Aug-2024.)
STAB

5-Aug-2024prod1dc 11476 Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.)
DECID

2-Aug-2024onntri52 7173 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
EXMID

2-Aug-2024onntri24 7171 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)

2-Aug-2024onntri45 7170 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
EXMID

2-Aug-2024onntri51 7169 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)
EXMID

2-Aug-2024onntri13 7167 Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)

2-Aug-2024onntri35 7166 Double negated ordinal trichotomy.

There are five equivalent statements: (1) , (2) , (3) , (4) , and (5) EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7167), (3) implies (5) (onntri35 7166), (5) implies (1) (onntri51 7169), (2) implies (4) (onntri24 7171), (4) implies (5) (onntri45 7170), and (5) implies (2) (onntri52 7173).

Another way of stating this is that EXMID is equivalent to trichotomy, either the or the form, as shown in exmidontri 7168 and exmidontri2or 7172, respectively. Thus EXMID is equivalent to (1) or (2). In addition, EXMID is equivalent to (3) by onntri3or 7174 and (4) by onntri2or 7175.

(Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.)

EXMID

1-Aug-2024nnral 2447 The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1629. (Contributed by Jim Kingdon, 1-Aug-2024.)

31-Jul-20243nsssucpw1 7165 Negated excluded middle implies that is not a subset of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
EXMID

31-Jul-2024sucpw1nss3 7164 Negated excluded middle implies that the successor of the power set of is not a subset of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.)
EXMID

30-Jul-20243nelsucpw1 7163 Three is not an element of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)

30-Jul-2024sucpw1nel3 7162 The successor of the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)

30-Jul-2024sucpw1ne3 7161 Negated excluded middle implies that the successor of the power set of is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
EXMID

30-Jul-2024pw1nel3 7160 Negated excluded middle implies that the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)
EXMID

30-Jul-2024pw1ne3 7159 The power set of is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.)

30-Jul-2024pw1ne1 7158 The power set of is not one. (Contributed by Jim Kingdon, 30-Jul-2024.)

30-Jul-2024pw1ne0 7157 The power set of is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.)

29-Jul-2024pw1on 7155 The power set of is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.)

28-Jul-2024exmidpweq 6851 Excluded middle is equivalent to the power set of being . (Contributed by Jim Kingdon, 28-Jul-2024.)
EXMID

27-Jul-2024dcapnconstALT 13603 Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13602 by means of dceqnconst 13601. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.)
DECID #

27-Jul-2024reap0 13600 Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.)
DECID #

26-Jul-2024nconstwlpolemgt0 13605 Lemma for nconstwlpo 13607. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.)

26-Jul-2024nconstwlpolem0 13604 Lemma for nconstwlpo 13607. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.)

24-Jul-2024tridceq 13598 Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13585 and redcwlpo 13597). Thus, this is an analytic analogue to lpowlpo 7105. (Contributed by Jim Kingdon, 24-Jul-2024.)
DECID

24-Jul-2024iswomni0 13593 Weak omniscience stated in terms of equality with . Like iswomninn 13592 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.)
WOmni DECID

24-Jul-2024lpowlpo 7105 LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7104. There is an analogue in terms of analytic omniscience principles at tridceq 13598. (Contributed by Jim Kingdon, 24-Jul-2024.)
Omni WOmni

23-Jul-2024nconstwlpolem 13606 Lemma for nconstwlpo 13607. (Contributed by Jim Kingdon, 23-Jul-2024.)

23-Jul-2024dceqnconst 13601 Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 13597 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.)
DECID

23-Jul-2024redc0 13599 Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.)
DECID DECID

23-Jul-2024canth 5775 No set is equinumerous to its power set (Cantor's theorem), i.e., no function can map onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1480 if you want the form .) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.)

22-Jul-2024nconstwlpo 13607 Existence of a certain non-constant function from reals to integers implies WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.)
WOmni

15-Jul-2024fprodseq 11473 The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.)

 Copyright terms: Public domain W3C HTML validation [external]