Home | Intuitionistic Logic Explorer Theorem List (p. 135 of 139) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description | ||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||
Theorem | cxplt3d 13401 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||
Theorem | cxple3d 13402 | Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||
Theorem | cxpmuld 13403 | Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.) | ||||||||||||||||||||||||
Theorem | cxpcom 13404 | Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.) | ||||||||||||||||||||||||
Theorem | apcxp2 13405 | Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.) | ||||||||||||||||||||||||
# # # | ||||||||||||||||||||||||||
Theorem | rpabscxpbnd 13406 | Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Jim Kingdon, 19-Jun-2024.) | ||||||||||||||||||||||||
Theorem | ltexp2 13407 | Ordering law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.) | ||||||||||||||||||||||||
Define "log using an arbitrary base" function and then prove some of its properties. As with df-relog 13326 this is for real logarithms rather than complex logarithms. Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log". There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): logb where is the base and is the argument of the logarithm function. An alternative would be to support the notational form logb ; that looks a little more like traditional notation. | ||||||||||||||||||||||||||
Syntax | clogb 13408 | Extend class notation to include the logarithm generalized to an arbitrary base. | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Definition | df-logb 13409* | Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as logb for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition will only be useful where is a positive real apart from one and where is a positive real, so the choice of and is somewhat arbitrary (we adopt the definition used in set.mm). (Contributed by David A. Wheeler, 21-Jan-2017.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | rplogbval 13410 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by Jim Kingdon, 3-Jul-2024.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | rplogbcl 13411 | General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | rplogbid1 13412 | General logarithm is 1 when base and arg match. Property 1(a) of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by David A. Wheeler, 22-Jul-2017.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | rplogb1 13413 | The logarithm of to an arbitrary base is 0. Property 1(b) of [Cohen4] p. 361. See log1 13334. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | rpelogb 13414 | The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using as the base in logb is the same as . Definition in [Cohen4] p. 352. (Contributed by David A. Wheeler, 17-Oct-2017.) (Revised by David A. Wheeler and AV, 16-Jun-2020.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | rplogbchbase 13415 | Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.) | ||||||||||||||||||||||||
# # logb logb logb | ||||||||||||||||||||||||||
Theorem | relogbval 13416 | Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | relogbzcl 13417 | Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) (Proof shortened by AV, 9-Jun-2020.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | rplogbreexp 13418 | Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of [Cohen4] p. 361. (Contributed by AV, 9-Jun-2020.) | ||||||||||||||||||||||||
# logb logb | ||||||||||||||||||||||||||
Theorem | rplogbzexp 13419 | Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.) | ||||||||||||||||||||||||
# logb logb | ||||||||||||||||||||||||||
Theorem | rprelogbmul 13420 | The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 29-May-2020.) | ||||||||||||||||||||||||
# logb logb logb | ||||||||||||||||||||||||||
Theorem | rprelogbmulexp 13421 | The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020.) | ||||||||||||||||||||||||
# logb logb logb | ||||||||||||||||||||||||||
Theorem | rprelogbdiv 13422 | The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.) | ||||||||||||||||||||||||
# logb logb logb | ||||||||||||||||||||||||||
Theorem | relogbexpap 13423 | Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | nnlogbexp 13424 | Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | logbrec 13425 | Logarithm of a reciprocal changes sign. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.) | ||||||||||||||||||||||||
logb logb | ||||||||||||||||||||||||||
Theorem | logbleb 13426 | The general logarithm function is monotone/increasing. See logleb 13343. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.) | ||||||||||||||||||||||||
logb logb | ||||||||||||||||||||||||||
Theorem | logblt 13427 | The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 13342. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.) | ||||||||||||||||||||||||
logb logb | ||||||||||||||||||||||||||
Theorem | rplogbcxp 13428 | Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | rpcxplogb 13429 | Identity law for the general logarithm. (Contributed by AV, 22-May-2020.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | relogbcxpbap 13430 | The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.) | ||||||||||||||||||||||||
# logb | ||||||||||||||||||||||||||
Theorem | logbgt0b 13431 | The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | logbgcd1irr 13432 | The logarithm of an integer greater than 1 to an integer base greater than 1 is not rational if the argument and the base are relatively prime. For example, logb . (Contributed by AV, 29-Dec-2022.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | logbgcd1irraplemexp 13433 | Lemma for logbgcd1irrap 13435. Apartness of and . (Contributed by Jim Kingdon, 11-Jul-2024.) | ||||||||||||||||||||||||
# | ||||||||||||||||||||||||||
Theorem | logbgcd1irraplemap 13434 | Lemma for logbgcd1irrap 13435. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.) | ||||||||||||||||||||||||
logb # | ||||||||||||||||||||||||||
Theorem | logbgcd1irrap 13435 | The logarithm of an integer greater than 1 to an integer base greater than 1 is irrational (in the sense of being apart from any rational number) if the argument and the base are relatively prime. For example, logb # where is rational. (Contributed by AV, 29-Dec-2022.) | ||||||||||||||||||||||||
logb # | ||||||||||||||||||||||||||
Theorem | 2logb9irr 13436 | Example for logbgcd1irr 13432. The logarithm of nine to base two is not rational. Also see 2logb9irrap 13442 which says that it is irrational (in the sense of being apart from any rational number). (Contributed by AV, 29-Dec-2022.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | logbprmirr 13437 | The logarithm of a prime to a different prime base is not rational. For example, logb (see 2logb3irr 13438). (Contributed by AV, 31-Dec-2022.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | 2logb3irr 13438 | Example for logbprmirr 13437. The logarithm of three to base two is not rational. (Contributed by AV, 31-Dec-2022.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | 2logb9irrALT 13439 | Alternate proof of 2logb9irr 13436: The logarithm of nine to base two is not rational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | sqrt2cxp2logb9e3 13440 | The square root of two to the power of the logarithm of nine to base two is three. and logb are not rational (see sqrt2irr0 12075 resp. 2logb9irr 13436), satisfying the statement in 2irrexpq 13441. (Contributed by AV, 29-Dec-2022.) | ||||||||||||||||||||||||
logb | ||||||||||||||||||||||||||
Theorem | 2irrexpq 13441* |
There exist real numbers and which
are not rational such
that is
rational. Statement in the Metamath book, section
1.1.5, footnote 27 on page 17, and the "constructive proof"
for theorem
1.2 of [Bauer], p. 483. This is a
constructive proof because it is
based on two explicitly named non-rational numbers and
logb , see sqrt2irr0 12075, 2logb9irr 13436 and
sqrt2cxp2logb9e3 13440. Therefore, this proof is acceptable/usable
in
intuitionistic logic.
For a theorem which is the same but proves that and are irrational (in the sense of being apart from any rational number), see 2irrexpqap 13443. (Contributed by AV, 23-Dec-2022.) | ||||||||||||||||||||||||
Theorem | 2logb9irrap 13442 | Example for logbgcd1irrap 13435. The logarithm of nine to base two is irrational (in the sense of being apart from any rational number). (Contributed by Jim Kingdon, 12-Jul-2024.) | ||||||||||||||||||||||||
logb # | ||||||||||||||||||||||||||
Theorem | 2irrexpqap 13443* | There exist real numbers and which are irrational (in the sense of being apart from any rational number) such that is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named irrational numbers and logb , see sqrt2irrap 12091, 2logb9irrap 13442 and sqrt2cxp2logb9e3 13440. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.) | ||||||||||||||||||||||||
# # | ||||||||||||||||||||||||||
Theorem | binom4 13444 | Work out a quartic binomial. (You would think that by this point it would be faster to use binom 11411, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.) | ||||||||||||||||||||||||
This section describes the conventions we use. 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:
| ||||||||||||||||||||||||||
Theorem | conventions 13445 |
Unless there is a reason to diverge, we follow the conventions of the
Metamath Proof Explorer (MPE, 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.
Label naming conventions Here are a few of the label naming conventions:
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. For the "g" abbreviation, this is related to the set.mm usage, in which "is a set" conditions are converted from hypotheses to antecedents, but is also used where "is a set" conditions are added relative to similar set.mm theorems.
(Contributed by Jim Kingdon, 24-Feb-2020.) (New usage is discouraged.) | ||||||||||||||||||||||||
Theorem | ex-or 13446 | Example for ax-io 699. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||
Theorem | ex-an 13447 | Example for ax-ia1 105. Example by David A. Wheeler. (Contributed by Mario Carneiro, 9-May-2015.) | ||||||||||||||||||||||||
Theorem | 1kp2ke3k 13448 |
Example for df-dec 9314, 1000 + 2000 = 3000.
This proof disproves (by counterexample) the assertion of Hao Wang, who stated, "There is a theorem in the primitive notation of set theory that corresponds to the arithmetic theorem 1000 + 2000 = 3000. The formula would be forbiddingly long... even if (one) knows the definitions and is asked to simplify the long formula according to them, chances are he will make errors and arrive at some incorrect result." (Hao Wang, "Theory and practice in mathematics" , In Thomas Tymoczko, editor, New Directions in the Philosophy of Mathematics, pp 129-152, Birkauser Boston, Inc., Boston, 1986. (QA8.6.N48). The quote itself is on page 140.) This is noted in Metamath: A Computer Language for Pure Mathematics by Norman Megill (2007) section 1.1.3. Megill then states, "A number of writers have conveyed the impression that the kind of absolute rigor provided by Metamath is an impossible dream, suggesting that a complete, formal verification of a typical theorem would take millions of steps in untold volumes of books... These writers assume, however, that in order to achieve the kind of complete formal verification they desire one must break down a proof into individual primitive steps that make direct reference to the axioms. This is not necessary. There is no reason not to make use of previously proved theorems rather than proving them over and over... A hierarchy of theorems and definitions permits an exponential growth in the formula sizes and primitive proof steps to be described with only a linear growth in the number of symbols used. Of course, this is how ordinary informal mathematics is normally done anyway, but with Metamath it can be done with absolute rigor and precision." The proof here starts with , commutes it, and repeatedly multiplies both sides by ten. This is certainly longer than traditional mathematical proofs, e.g., there are a number of steps explicitly shown here to show that we're allowed to do operations such as multiplication. However, while longer, the proof is clearly a manageable size - even though every step is rigorously derived all the way back to the primitive notions of set theory and logic. And while there's a risk of making errors, the many independent verifiers make it much less likely that an incorrect result will be accepted. This proof heavily relies on the decimal constructor df-dec 9314 developed by Mario Carneiro in 2015. The underlying Metamath language has an intentionally very small set of primitives; it doesn't even have a built-in construct for numbers. Instead, the digits are defined using these primitives, and the decimal constructor is used to make it easy to express larger numbers as combinations of digits. (Contributed by David A. Wheeler, 29-Jun-2016.) (Shortened by Mario Carneiro using the arithmetic algorithm in mmj2, 30-Jun-2016.) | ||||||||||||||||||||||||
;;; ;;; ;;; | ||||||||||||||||||||||||||
Theorem | ex-fl 13449 | Example for df-fl 10195. Example by David A. Wheeler. (Contributed by Mario Carneiro, 18-Jun-2015.) | ||||||||||||||||||||||||
Theorem | ex-ceil 13450 | Example for df-ceil 10196. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
⌈ ⌈ | ||||||||||||||||||||||||||
Theorem | ex-exp 13451 | Example for df-exp 10445. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
; | ||||||||||||||||||||||||||
Theorem | ex-fac 13452 | Example for df-fac 10628. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
;; | ||||||||||||||||||||||||||
Theorem | ex-bc 13453 | Example for df-bc 10650. (Contributed by AV, 4-Sep-2021.) | ||||||||||||||||||||||||
; | ||||||||||||||||||||||||||
Theorem | ex-dvds 13454 | Example for df-dvds 11714: 3 divides into 6. (Contributed by David A. Wheeler, 19-May-2015.) | ||||||||||||||||||||||||
Theorem | ex-gcd 13455 | Example for df-gcd 11861. (Contributed by AV, 5-Sep-2021.) | ||||||||||||||||||||||||
Theorem | mathbox 13456 |
(This theorem is a dummy placeholder for these guidelines. The label
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 iset.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of iset.mm. Guidelines: Mathboxes in iset.mm follow the same practices as in set.mm, so refer to the mathbox guidelines there for more details. (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (New usage is discouraged.) | ||||||||||||||||||||||||
Theorem | bj-nnsn 13457 | As far as implying a negated formula is concerned, a formula is equivalent to its double negation. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
Theorem | bj-nnor 13458 | Double negation of a disjunction in terms of implication. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
Theorem | bj-nnim 13459 | The double negation of an implication implies the implication with the consequent doubly negated. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
Theorem | bj-nnan 13460 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
Theorem | bj-nnclavius 13461 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||
Some of the following theorems, like bj-sttru 13463 or bj-stfal 13465 could be deduced from their analogues for decidability, but stability is not provable from decidability in minimal calculus, so direct proofs have their interest. | ||||||||||||||||||||||||||
Theorem | bj-trst 13462 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
STAB | ||||||||||||||||||||||||||
Theorem | bj-sttru 13463 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||
STAB | ||||||||||||||||||||||||||
Theorem | bj-fast 13464 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
STAB | ||||||||||||||||||||||||||
Theorem | bj-stfal 13465 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||
STAB | ||||||||||||||||||||||||||
Theorem | bj-nnbist 13466 | If a formula is not refutable, then it is stable if and only if it is provable. By double-negation translation, if is a classical tautology, then is an intuitionistic tautology. Therefore, if is a classical tautology, then is intuitionistically equivalent to its stability (and to its decidability, see bj-nnbidc 13477). (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
STAB | ||||||||||||||||||||||||||
Theorem | bj-stim 13467 | A conjunction with a stable consequent is stable. See stabnot 823 for negation and bj-stan 13468 for conjunction. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
STAB STAB | ||||||||||||||||||||||||||
Theorem | bj-stan 13468 | The conjunction of two stable formulas is stable. See bj-stim 13467 for implication, stabnot 823 for negation, and bj-stal 13470 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
STAB STAB STAB | ||||||||||||||||||||||||||
Theorem | bj-stand 13469 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 13468. Its proof is shorter, so one could prove it first and then bj-stan 13468 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
STAB STAB STAB | ||||||||||||||||||||||||||
Theorem | bj-stal 13470 | The universal quantification of stable formula is stable. See bj-stim 13467 for implication, stabnot 823 for negation, and bj-stan 13468 for conjunction. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
STAB STAB | ||||||||||||||||||||||||||
Theorem | bj-pm2.18st 13471 | Clavius law for stable formulas. See pm2.18dc 845. (Contributed by BJ, 4-Dec-2023.) | ||||||||||||||||||||||||
STAB | ||||||||||||||||||||||||||
Theorem | bj-trdc 13472 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
DECID | ||||||||||||||||||||||||||
Theorem | bj-dctru 13473 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||
DECID | ||||||||||||||||||||||||||
Theorem | bj-fadc 13474 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
DECID | ||||||||||||||||||||||||||
Theorem | bj-dcfal 13475 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | ||||||||||||||||||||||||
DECID | ||||||||||||||||||||||||||
Theorem | bj-dcstab 13476 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
DECID STAB | ||||||||||||||||||||||||||
Theorem | bj-nnbidc 13477 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 13466. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
DECID | ||||||||||||||||||||||||||
Theorem | bj-nndcALT 13478 | Alternate proof of nndc 841. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
DECID | ||||||||||||||||||||||||||
Theorem | bj-nnst 13479 | Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. This theorem can also be proved in classical refutability calculus (see set.mm/bj-peircestab) but not in minimal calculus (see set.mm/bj-stabpeirce). (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
STAB | ||||||||||||||||||||||||||
Theorem | bj-dcdc 13480 | Decidability of a proposition is decidable if and only if that proposition is decidable. DECID is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
DECID DECID DECID | ||||||||||||||||||||||||||
Theorem | bj-stdc 13481 | Decidability of a proposition is stable if and only if that proposition is decidable. In particular, the assumption that every formula is stable implies that every formula is decidable, hence classical logic. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
STAB DECID DECID | ||||||||||||||||||||||||||
Theorem | bj-dcst 13482 | Stability of a proposition is decidable if and only if that proposition is stable. (Contributed by BJ, 24-Nov-2023.) | ||||||||||||||||||||||||
DECID STAB STAB | ||||||||||||||||||||||||||
Theorem | bj-stst 13483 | Stability of a proposition is stable if and only if that proposition is stable. STAB is idempotent. (Contributed by BJ, 9-Oct-2019.) | ||||||||||||||||||||||||
STAB STAB STAB | ||||||||||||||||||||||||||
Theorem | bj-ex 13484* | Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1585 and 19.9ht 1628 or 19.23ht 1484). (Proof modification is discouraged.) | ||||||||||||||||||||||||
Theorem | bj-hbalt 13485 | Closed form of hbal 1464 (copied from set.mm). (Contributed by BJ, 2-May-2019.) | ||||||||||||||||||||||||
Theorem | bj-nfalt 13486 | Closed form of nfal 1563 (copied from set.mm). (Contributed by BJ, 2-May-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
Theorem | spimd 13487 | Deduction form of spim 1725. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
Theorem | 2spim 13488* | Double substitution, as in spim 1725. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
Theorem | ch2var 13489* | Implicit substitution of for and for into a theorem. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
Theorem | ch2varv 13490* | Version of ch2var 13489 with nonfreeness hypotheses replaced with disjoint variable conditions. (Contributed by BJ, 17-Oct-2019.) | ||||||||||||||||||||||||
Theorem | bj-exlimmp 13491 | Lemma for bj-vtoclgf 13498. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
Theorem | bj-exlimmpi 13492 | Lemma for bj-vtoclgf 13498. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||||||||||||||
Theorem | bj-sbimedh 13493 | A strengthening of sbiedh 1774 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||
Theorem | bj-sbimeh 13494 | A strengthening of sbieh 1777 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||
Theorem | bj-sbime 13495 | A strengthening of sbie 1778 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||||||||||||||
Theorem | bj-el2oss1o 13496 | Shorter proof of el2oss1o 6402 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||||||||||||||
Various utility theorems using FOL and extensionality. | ||||||||||||||||||||||||||
Theorem | bj-vtoclgft 13497 | Weakening two hypotheses of vtoclgf 2779. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
Theorem | bj-vtoclgf 13498 | Weakening two hypotheses of vtoclgf 2779. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
Theorem | elabgf0 13499 | Lemma for elabgf 2863. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
Theorem | elabgft1 13500 | One implication of elabgf 2863, in closed form. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||||||||||||||
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |