Home | Metamath
Proof Explorer Theorem List (p. 17 of 468) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29329) |
Hilbert Space Explorer
(29330-30852) |
Users' Mathboxes
(30853-46765) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hadnot 1601 | The adder sum distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
⊢ (¬ hadd(𝜑, 𝜓, 𝜒) ↔ hadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | had1 1602 | If the first input is true, then the adder sum is equivalent to the biconditionality of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
⊢ (𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ↔ 𝜒))) | ||
Theorem | had0 1603 | If the first input is false, then the adder sum is equivalent to the exclusive disjunction of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jul-2020.) |
⊢ (¬ 𝜑 → (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜓 ⊻ 𝜒))) | ||
Theorem | hadifp 1604 | The value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs. (Contributed by BJ, 11-Aug-2020.) |
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ↔ 𝜒), (𝜓 ⊻ 𝜒))) | ||
Syntax | wcad 1605 | Syntax for the "carry" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.) |
wff cadd(𝜑, 𝜓, 𝜒) | ||
Definition | df-cad 1606 | Definition of the "carry" output of the full adder. It is true when at least two arguments are true, so it is equal to the "majority" function on three variables. See cador 1607 and cadan 1608 for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))) | ||
Theorem | cador 1607 | The adder carry in disjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒) ∨ (𝜓 ∧ 𝜒))) | ||
Theorem | cadan 1608 | The adder carry in conjunctive normal form. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 25-Sep-2018.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒))) | ||
Theorem | cadbi123d 1609 | Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (cadd(𝜓, 𝜃, 𝜂) ↔ cadd(𝜒, 𝜏, 𝜁))) | ||
Theorem | cadbi123i 1610 | Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ (cadd(𝜑, 𝜒, 𝜏) ↔ cadd(𝜓, 𝜃, 𝜂)) | ||
Theorem | cadcoma 1611 | Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜑, 𝜒)) | ||
Theorem | cadcomb 1612 | Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜑, 𝜒, 𝜓)) | ||
Theorem | cadrot 1613 | Rotation law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜒, 𝜑)) | ||
Theorem | cadnot 1614 | The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | cad11 1615 | If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((𝜑 ∧ 𝜓) → cadd(𝜑, 𝜓, 𝜒)) | ||
Theorem | cad1 1616 | If one input is true, then the adder carry is true exactly when at least one of the other two inputs is true. (Contributed by Mario Carneiro, 8-Sep-2016.) (Proof shortened by Wolf Lammen, 19-Jun-2020.) |
⊢ (𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∨ 𝜓))) | ||
Theorem | cad0 1617 | If one input is false, then the adder carry is true exactly when both of the other two inputs are true. (Contributed by Mario Carneiro, 8-Sep-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2024.) |
⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | ||
Theorem | cad0OLD 1618 | Obsolete version of cad0 1617 as of 21-Sep-2024. (Contributed by Mario Carneiro, 8-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | ||
Theorem | cadifp 1619 | The value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs. (Contributed by BJ, 8-Oct-2019.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜒, (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓))) | ||
Theorem | cadtru 1620 | The adder carry is true as soon as its first two inputs are the truth constant. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ cadd(⊤, ⊤, 𝜑) | ||
Minimal implicational calculus, or intuitionistic implicational calculus, or positive implicational calculus, is the implicational fragment of minimal calculus (which is also the implicational fragment of intuitionistic calculus and of positive calculus). It is sometimes called "C-pure intuitionism" since the letter C is sometimes used to denote implication, especially in prefix notation. It can be axiomatized by the inference rule of modus ponens ax-mp 5 together with the axioms { ax-1 6, ax-2 7 } (sometimes written KS), or with { imim1 83, ax-1 6, pm2.43 56 } (written B'KW), or with { imim2 58, pm2.04 90, ax-1 6, pm2.43 56 } (written BCKW), or with the single axiom minimp 1621. This section proves minimp 1621 from { ax-1 6, ax-2 7 }, and then the converse, due to Ivo Thomas. Sources for this section are the webpage https://web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm 7 on Ted Ulrich's website, and the articles C. A. Meredith, A single axiom of positive logic, Journal of computing systems, vol. 1 (1953), 169--170, and C. A. Meredith, A. N. Prior, Notes on the axiomatics of the propositional calculus, Notre Dame Journal of Formal Logic, vol. 4 (1963), 171--187. We may use a compact notation for derivations known as the D-notation where "D" stands for "condensed Detachment". For instance, "D21" means detaching ax-1 6 from ax-2 7, that is, using modus ponens ax-mp 5 with ax-1 6 as minor premise and ax-2 7 as major premise. D-strings are accepted by the grammar Dstr := digit | "D" Dstr Dstr. (Contributed by BJ, 11-Apr-2021.) | ||
Theorem | minimp 1621 | A single axiom for minimal implicational calculus, due to Meredith. Other single axioms of the same length are known, but it is thought to be the minimal length. Among single axioms of this length, it is the one with simplest antecedents (i.e., in the corresponding ordering of binary trees which first compares left subtrees, it is the first one). (Contributed by BJ, 4-Apr-2021.) |
⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) | ||
Theorem | minimp-syllsimp 1622 | Derivation of Syll-Simp (jarr 106) from ax-mp 5 and minimp 1621. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
Theorem | minimp-ax1 1623 | Derivation of ax-1 6 from ax-mp 5 and minimp 1621. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | minimp-ax2c 1624 | Derivation of a commuted form of ax-2 7 from ax-mp 5 and minimp 1621. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
Theorem | minimp-ax2 1625 | Derivation of ax-2 7 from ax-mp 5 and minimp 1621. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | minimp-pm2.43 1626 | Derivation of pm2.43 56 (also called "hilbert" or W) from ax-mp 5 and minimp 1621. It uses the classical derivation from ax-1 6 and ax-2 7 written DD22D21 in D-notation (see head comment for an explanation) and shortens the proof using mp2 9 (which only requires ax-mp 5). (Contributed by BJ, 31-May-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Implicational calculus is the fragment of propositional logic that uses only material implication, and not negation. It can be axiomatized by inference rule modus ponens ax-mp 5 together with the axioms { ax-1 6, ax-2 7, peirce 201 } or the Tarski-Bernays axioms { ax-1 6, imim1 83, peirce 201 } or with the single axiom { impsingle 1627 }. From either one of these three axiom sets, all tautologies containing only material implication may be proved. In contrast, minimal implicational calculus, which is presented just before this section, cannot prove certain tautologies (peirce 201, for example ). The class of theorems proved by minimal implicational calculus is thus a subset of the class of theorems proved by implicational calculus. The primary source for this section is the paper by Jan Lukasiewicz, The Shortest Axiom of the Implicational Calculus of Propositions, Proceedings of the Royal Irish Academy, Section A, vol. 52 (1948-1950), 25--33. It will be cited as simply "Lukasiewicz" in the remainder of this section. This section proves that the above three distinct axiom sets for implicational calculus all produce the same class of theorems. (Contributed by Larry Lesyna and Jeffrey P. Machado, 1-Aug-2023.) | ||
Theorem | impsingle 1627 | The shortest single axiom for implicational calculus, due to Lukasiewicz. It is now known to be the unique shortest axiom. The axiom is proved here starting from { ax-1 6, ax-2 7 and peirce 201 }. (Contributed by Larry Lesyna and Jeffrey P. Machado, 18-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜒 → 𝜑) → (𝜃 → 𝜑))) | ||
Theorem | impsingle-step4 1628 | Derivation of impsingle-step4 from ax-mp 5 and impsingle 1627. It is used as a lemma in proofs of imim1 83 and peirce 201 from impsingle 1627. It is Step 4 in Lukasiewicz, where it appears as 'CCCpqpCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜑) → (𝜒 → 𝜑)) | ||
Theorem | impsingle-step8 1629 | Derivation of impsingle-step8 from ax-mp 5 and impsingle 1627. It is used as a lemma in proofs of ax-1 6 imim1 83 and peirce 201 from impsingle 1627. It is Step 8 in Lukasiewicz, where it appears as 'CCCsqpCqp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
Theorem | impsingle-ax1 1630 | Derivation of impsingle-ax1 (ax-1 6) from ax-mp 5 and impsingle 1627. Lukasiewicz was used to construct this proof. Every formula corresponding to a detachment step was converted to its corresponding Metamath formula. mmj2 was used to unify each formula using ax-mp 5, which in turn produced this proof. With extremely high confidence, this result shows that the Lukasiewicz proof of ax-1 6 (step 27) is correct and that Metamath correctly verifies the proof. The same comments apply to the proofs that follow this one. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | impsingle-step15 1631 | Derivation of impsingle-step15 from ax-mp 5 and impsingle 1627. It is used as a lemma in proofs of imim1 83 and peirce 201 from impsingle 1627. It is Step 15 in Lukasiewicz, where it appears as 'CCCrqCspCCrpCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → ((𝜑 → 𝜃) → (𝜒 → 𝜃))) | ||
Theorem | impsingle-step18 1632 | Derivation of impsingle-step18 from ax-mp 5 and impsingle 1627. It is used as a lemma in proofs of imim1 83 and peirce 201 from impsingle 1627. It is Step 18 in Lukasiewicz, where it appears as 'CCCCrpCspCCCpqrtCuCCCpqrt' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 → 𝜓) → (𝜒 → 𝜓)) → (((𝜓 → 𝜃) → 𝜑) → 𝜏)) → (𝜂 → (((𝜓 → 𝜃) → 𝜑) → 𝜏))) | ||
Theorem | impsingle-step19 1633 | Derivation of impsingle-step19 from ax-mp 5 and impsingle 1627. It is used as a lemma in proofs of imim1 83 and peirce 201 from impsingle 1627. It is Step 19 in Lukasiewicz, where it appears as 'CCCCspqCrpCCCpqrCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 → 𝜓) → 𝜒) → (𝜃 → 𝜓)) → (((𝜓 → 𝜒) → 𝜃) → (𝜑 → 𝜓))) | ||
Theorem | impsingle-step20 1634 | Derivation of impsingle-step20 from ax-mp 5 and impsingle 1627. It is used as a lemma in proofs of imim1 83 and peirce 201 from impsingle 1627. It is Step 20 in Lukasiewicz, where it appears as 'CCCCrppCspCCCpqrCsp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 → 𝜓) → 𝜓) → (𝜒 → 𝜓)) → (((𝜓 → 𝜃) → 𝜑) → (𝜒 → 𝜓))) | ||
Theorem | impsingle-step21 1635 | Derivation of impsingle-step21 from ax-mp 5 and impsingle 1627. It is used as a lemma in the proof of imim1 83 from impsingle 1627. It is Step 21 in Lukasiewicz, where it appears as 'CCCCprqqCCqrCpr' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜑 → 𝜓) → 𝜒) → 𝜒) → ((𝜒 → 𝜓) → (𝜑 → 𝜓))) | ||
Theorem | impsingle-step22 1636 | Derivation of impsingle-step22 from ax-mp 5 and impsingle 1627. It is used as a lemma in proofs of imim1 83 and peirce 201 from impsingle 1627. It is Step 22 in Lukasiewicz, where it appears as 'Cpp' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜑) | ||
Theorem | impsingle-step25 1637 | Derivation of impsingle-step25 from ax-mp 5 and impsingle 1627. It is used as a lemma in the proof of imim1 83 from impsingle 1627. It is Step 25 in Lukasiewicz, where it appears as 'CCpqCCCprqq' using parenthesis-free prefix notation. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (((𝜑 → 𝜒) → 𝜓) → 𝜓)) | ||
Theorem | impsingle-imim1 1638 | Derivation of impsingle-imim1 (imim1 83) from ax-mp 5 and impsingle 1627. It is step 29 in Lukasiewicz. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) | ||
Theorem | impsingle-peirce 1639 | Derivation of impsingle-peirce (peirce 201) from ax-mp 5 and impsingle 1627. It is step 28 in Lukasiewicz. (Contributed by Larry Lesyna and Jeffrey P. Machado, 2-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜑) → 𝜑) | ||
Theorem | tarski-bernays-ax2 1640 | Derivation of ax-2 7 from the Tarski-Bernays axiom set { ax-1 6, imim1 83, peirce 201 }. Note that no inference rule other than ax-mp 5 is used in this proof. This proof establishes a circle of equivalence: From { impsingle 1627 }, { ax-1 6, imim1 83, peirce 201 } was proved. From { ax-1 6, imim1 83, peirce 201 }, { ax-1 6, ax-2 7 and peirce 201 } was proved. From { ax-1 6, ax-2 7 and peirce 201 }, { impsingle 1627 } was proved. Therefore, the theorems that can be proved by selecting any one of these three distinct axiom sets must be equivalent. Prover9 and mmj2 were used to help constuct this proof. (Contributed by Larry Lesyna and Jeffrey P. Machado, 1-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | meredith 1641 |
Carew Meredith's sole axiom for propositional calculus. This amazing
formula is thought to be the shortest possible single axiom for
propositional calculus with inference rule ax-mp 5,
where negation and
implication are primitive. Here we prove Meredith's axiom from ax-1 6,
ax-2 7, and ax-3 8. Then from it we derive the Lukasiewicz
axioms
luk-1 1655, luk-2 1656, and luk-3 1657. Using these we finally rederive our
axioms as ax1 1666, ax2 1667, and ax3 1668,
thus proving the equivalence of all
three systems. C. A. Meredith, "Single Axioms for the Systems (C,N),
(C,O) and (A,N) of the Two-Valued Propositional Calculus", The
Journal of
Computing Systems vol. 1 (1953), pp. 155-164. Meredith claimed to be
close to a proof that this axiom is the shortest possible, but the proof
was apparently never completed.
An obscure Irish lecturer, Meredith (1904-1976) became enamored with logic somewhat late in life after attending talks by Lukasiewicz and produced many remarkable results such as this axiom. From his obituary: "He did logic whenever time and opportunity presented themselves, and he did it on whatever materials came to hand: in a pub, his favored pint of porter within reach, he would use the inside of cigarette packs to write proofs for logical colleagues." (Contributed by NM, 14-Dec-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (Proof shortened by Wolf Lammen, 28-May-2013.) |
⊢ (((((𝜑 → 𝜓) → (¬ 𝜒 → ¬ 𝜃)) → 𝜒) → 𝜏) → ((𝜏 → 𝜑) → (𝜃 → 𝜑))) | ||
Theorem | merlem1 1642 | Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.) (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜒 → (¬ 𝜑 → 𝜓)) → 𝜏) → (𝜑 → 𝜏)) | ||
Theorem | merlem2 1643 | Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜑) → 𝜒) → (𝜃 → 𝜒)) | ||
Theorem | merlem3 1644 | Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜓 → 𝜒) → 𝜑) → (𝜒 → 𝜑)) | ||
Theorem | merlem4 1645 | Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜏 → ((𝜏 → 𝜑) → (𝜃 → 𝜑))) | ||
Theorem | merlem5 1646 | Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (¬ ¬ 𝜑 → 𝜓)) | ||
Theorem | merlem6 1647 | Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜒 → (((𝜓 → 𝜒) → 𝜑) → (𝜃 → 𝜑))) | ||
Theorem | merlem7 1648 | Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (((𝜓 → 𝜒) → 𝜃) → (((𝜒 → 𝜏) → (¬ 𝜃 → ¬ 𝜓)) → 𝜃))) | ||
Theorem | merlem8 1649 | Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜓 → 𝜒) → 𝜃) → (((𝜒 → 𝜏) → (¬ 𝜃 → ¬ 𝜓)) → 𝜃)) | ||
Theorem | merlem9 1650 | Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → (𝜒 → (𝜃 → (𝜓 → 𝜏)))) → (𝜂 → (𝜒 → (𝜃 → (𝜓 → 𝜏))))) | ||
Theorem | merlem10 1651 | Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜃 → (𝜑 → 𝜓))) | ||
Theorem | merlem11 1652 | Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | merlem12 1653 | Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜃 → (¬ ¬ 𝜒 → 𝜒)) → 𝜑) → 𝜑) | ||
Theorem | merlem13 1654 | Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (((𝜃 → (¬ ¬ 𝜒 → 𝜒)) → ¬ ¬ 𝜑) → 𝜓)) | ||
Theorem | luk-1 1655 | 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) | ||
Theorem | luk-2 1656 | 2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | ||
Theorem | luk-3 1657 | 3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom. (Contributed by NM, 14-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) | ||
Theorem | luklem1 1658 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | luklem2 1659 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → ¬ 𝜓) → (((𝜑 → 𝜒) → 𝜃) → (𝜓 → 𝜃))) | ||
Theorem | luklem3 1660 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜃 → 𝜒))) | ||
Theorem | luklem4 1661 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((¬ 𝜑 → 𝜑) → 𝜑) → 𝜓) → 𝜓) | ||
Theorem | luklem5 1662 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | luklem6 1663 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | luklem7 1664 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | ||
Theorem | luklem8 1665 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓))) | ||
Theorem | ax1 1666 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | ax2 1667 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | ax3 1668 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑)) | ||
Prove Nicod's axiom and implication and negation definitions. | ||
Theorem | nic-dfim 1669 | This theorem "defines" implication in terms of 'nand'. Analogous to nanim 1494. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 → 𝜓)) ⊼ (((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜓))) ⊼ ((𝜑 → 𝜓) ⊼ (𝜑 → 𝜓)))) | ||
Theorem | nic-dfneg 1670 | This theorem "defines" negation in terms of 'nand'. Analogous to nannot 1495. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ⊼ 𝜑) ⊼ ¬ 𝜑) ⊼ (((𝜑 ⊼ 𝜑) ⊼ (𝜑 ⊼ 𝜑)) ⊼ (¬ 𝜑 ⊼ ¬ 𝜑))) | ||
Theorem | nic-mp 1671 | Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply 𝜒, this form is necessary for useful derivations from nic-ax 1673. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⇒ ⊢ 𝜓 | ||
Theorem | nic-mpALT 1672 | A direct proof of nic-mp 1671. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⇒ ⊢ 𝜓 | ||
Theorem | nic-ax 1673 | Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1641, the usual axioms can be derived from this and vice versa. Unlike meredith 1641, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g., { nic-ax 1673, nic-mp 1671 } is equivalent to { luk-1 1655, luk-2 1656, luk-3 1657, ax-mp 5 }. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom ($a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | nic-axALT 1674 | A direct proof of nic-ax 1673. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | nic-imp 1675 | Inference for nic-mp 1671 using nic-ax 1673 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⇒ ⊢ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) | ||
Theorem | nic-idlem1 1676 | Lemma for nic-id 1678. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃))) | ||
Theorem | nic-idlem2 1677 | Lemma for nic-id 1678. Inference used by nic-id 1678. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜂 ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃)) ⇒ ⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ 𝜂) | ||
Theorem | nic-id 1678 | Theorem id 22 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏)) | ||
Theorem | nic-swap 1679 | The connector ⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜃 ⊼ 𝜑) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) | ||
Theorem | nic-isw1 1680 | Inference version of nic-swap 1679. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ⊼ 𝜑) ⇒ ⊢ (𝜑 ⊼ 𝜃) | ||
Theorem | nic-isw2 1681 | Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 ⊼ (𝜃 ⊼ 𝜑)) ⇒ ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜃)) | ||
Theorem | nic-iimp1 1682 | Inference version of nic-imp 1675 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) & ⊢ (𝜃 ⊼ 𝜒) ⇒ ⊢ (𝜃 ⊼ 𝜑) | ||
Theorem | nic-iimp2 1683 | Inference version of nic-imp 1675 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ 𝜓) ⊼ (𝜒 ⊼ 𝜒)) & ⊢ (𝜃 ⊼ 𝜑) ⇒ ⊢ (𝜃 ⊼ (𝜒 ⊼ 𝜒)) | ||
Theorem | nic-idel 1684 | Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⇒ ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒)) | ||
Theorem | nic-ich 1685 | Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓)) & ⊢ (𝜓 ⊼ (𝜒 ⊼ 𝜒)) ⇒ ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒)) | ||
Theorem | nic-idbl 1686 | Double the terms. Since doubling is the same as negation, this can be viewed as a contraposition inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓)) ⇒ ⊢ ((𝜓 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜑 ⊼ 𝜑))) | ||
Theorem | nic-bijust 1687 | Biconditional justification from Nicod's axiom. For nic-* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nic-bi1 1688 and nic-bi2 1689 are used to convert the definitions into usable theorems about one side of the implication. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ⊼ 𝜏) ⊼ ((𝜏 ⊼ 𝜏) ⊼ (𝜏 ⊼ 𝜏))) | ||
Theorem | nic-bi1 1688 | Inference to extract one side of an implication from a definition. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓))) ⇒ ⊢ (𝜑 ⊼ (𝜓 ⊼ 𝜓)) | ||
Theorem | nic-bi2 1689 | Inference to extract the other side of an implication from a 'biconditional' definition. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜑) ⊼ (𝜓 ⊼ 𝜓))) ⇒ ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜑)) | ||
Theorem | nic-stdmp 1690 | Derive the standard modus ponens from nic-mp 1671. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | nic-luk1 1691 | Proof of luk-1 1655 from nic-ax 1673 and nic-mp 1671 (and Definitions nic-dfim 1669 and nic-dfneg 1670). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by Theorems ax1 1666, ax2 1667, and ax3 1668. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) | ||
Theorem | nic-luk2 1692 | Proof of luk-2 1656 from nic-ax 1673 and nic-mp 1671. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ 𝜑 → 𝜑) → 𝜑) | ||
Theorem | nic-luk3 1693 | Proof of luk-3 1657 from nic-ax 1673 and nic-mp 1671. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) | ||
Theorem | lukshef-ax1 1694 |
This alternative axiom for propositional calculus using the Sheffer Stroke
was discovered by Lukasiewicz in his Selected Works. It improves on
Nicod's axiom by reducing its number of variables by one.
This axiom also uses nic-mp 1671 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1673. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜃 ⊼ (𝜃 ⊼ 𝜃)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | lukshefth1 1695 | Lemma for renicax 1697. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((𝜏 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜏) ⊼ (𝜑 ⊼ 𝜏))) ⊼ (𝜃 ⊼ (𝜃 ⊼ 𝜃))) ⊼ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) | ||
Theorem | lukshefth2 1696 | Lemma for renicax 1697. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜏 ⊼ 𝜃) ⊼ ((𝜃 ⊼ 𝜏) ⊼ (𝜃 ⊼ 𝜏))) | ||
Theorem | renicax 1697 | A rederivation of nic-ax 1673 from lukshef-ax1 1694, proving that lukshef-ax1 1694 with nic-mp 1671 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | tbw-bijust 1698 | Justification for tbw-negdf 1699. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ↔ 𝜓) ↔ (((𝜑 → 𝜓) → ((𝜓 → 𝜑) → ⊥)) → ⊥)) | ||
Theorem | tbw-negdf 1699 | The definition of negation, in terms of → and ⊥. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((¬ 𝜑 → (𝜑 → ⊥)) → (((𝜑 → ⊥) → ¬ 𝜑) → ⊥)) → ⊥) | ||
Theorem | tbw-ax1 1700 | The first of four axioms in the Tarski-Bernays-Wajsberg system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜓 → 𝜒) → (𝜑 → 𝜒))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |