Home | Metamath
Proof Explorer Theorem List (p. 16 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | truortru 1501 | A ∨ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊤ ∨ ⊤) ↔ ⊤) | ||
Theorem | truorfal 1502 | A ∨ identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊤ ∨ ⊥) ↔ ⊤) | ||
Theorem | falortru 1503 | A ∨ identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊥ ∨ ⊤) ↔ ⊤) | ||
Theorem | falorfal 1504 | A ∨ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊥ ∨ ⊥) ↔ ⊥) | ||
Theorem | truimtru 1505 | A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊤ → ⊤) ↔ ⊤) | ||
Theorem | truimfal 1506 | A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊤ → ⊥) ↔ ⊥) | ||
Theorem | falimtru 1507 | A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊥ → ⊤) ↔ ⊤) | ||
Theorem | falimfal 1508 | A → identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ ((⊥ → ⊥) ↔ ⊤) | ||
Theorem | nottru 1509 | A ¬ identity. (Contributed by Anthony Hart, 22-Oct-2010.) |
⊢ (¬ ⊤ ↔ ⊥) | ||
Theorem | notfal 1510 | A ¬ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (¬ ⊥ ↔ ⊤) | ||
Theorem | trubitru 1511 | A ↔ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊤ ↔ ⊤) ↔ ⊤) | ||
Theorem | falbitru 1512 | A ↔ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
⊢ ((⊥ ↔ ⊤) ↔ ⊥) | ||
Theorem | trubifal 1513 | A ↔ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
⊢ ((⊤ ↔ ⊥) ↔ ⊥) | ||
Theorem | falbifal 1514 | A ↔ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊥ ↔ ⊥) ↔ ⊤) | ||
Theorem | trunantru 1515 | A ⊼ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊤ ⊼ ⊤) ↔ ⊥) | ||
Theorem | trunanfal 1516 | A ⊼ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
⊢ ((⊤ ⊼ ⊥) ↔ ⊤) | ||
Theorem | falnantru 1517 | A ⊼ identity. (Contributed by Anthony Hart, 23-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊥ ⊼ ⊤) ↔ ⊤) | ||
Theorem | falnanfal 1518 | A ⊼ identity. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((⊥ ⊼ ⊥) ↔ ⊤) | ||
Theorem | truxortru 1519 | A ⊻ identity. (Contributed by David A. Wheeler, 8-May-2015.) |
⊢ ((⊤ ⊻ ⊤) ↔ ⊥) | ||
Theorem | truxorfal 1520 | A ⊻ identity. (Contributed by David A. Wheeler, 8-May-2015.) |
⊢ ((⊤ ⊻ ⊥) ↔ ⊤) | ||
Theorem | falxortru 1521 | A ⊻ identity. (Contributed by David A. Wheeler, 9-May-2015.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
⊢ ((⊥ ⊻ ⊤) ↔ ⊤) | ||
Theorem | falxorfal 1522 | A ⊻ identity. (Contributed by David A. Wheeler, 9-May-2015.) |
⊢ ((⊥ ⊻ ⊥) ↔ ⊥) | ||
Propositional calculus deals with truth values, which can be interpreted as bits. Using this, we can define the half adder and the full adder in pure propositional calculus, and show their basic properties. The half adder adds two 1-bit numbers. Its two outputs are the "sum" S and the "carry" C. The real sum is then given by 2C+S. The sum and carry correspond respectively to the logical exclusive disjunction (df-xor 1457) and the logical conjunction (df-an 385). The full adder takes into account an "input carry", so it has three inputs and again two outputs, corresponding to the "sum" (df-had 1524) and "updated carry" (df-cad 1537). Here is a short description. We code the bit 0 by ⊥ and 1 by ⊤. Even though hadd and cadd are invariant under permutation of their arguments, assume for the sake of concreteness that 𝜑 (resp. 𝜓) is the i^th bit of the first (resp. second) number to add (with the convention that the i^th bit is the multiple of 2^i in the base-2 representation), and that 𝜒 is the i^th carry (with the convention that the 0^th carry is 0). Then, hadd(𝜑, 𝜓, 𝜒) gives the i^th bit of the sum, and cadd(𝜑, 𝜓, 𝜒) gives the (i+1)^th carry. Then, addition is performed by iteration from i = 0 to i = 1 + (max of the number of digits of the two summands) by "updating" the carry. | ||
Syntax | whad 1523 | Syntax for the "sum" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.) |
wff hadd(𝜑, 𝜓, 𝜒) | ||
Definition | df-had 1524 | Definition of the "sum" output of the full adder (triple exclusive disjunction, or XOR3). (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ⊻ 𝜓) ⊻ 𝜒)) | ||
Theorem | hadbi123d 1525 | Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (hadd(𝜓, 𝜃, 𝜂) ↔ hadd(𝜒, 𝜏, 𝜁))) | ||
Theorem | hadbi123i 1526 | Equality theorem for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ (hadd(𝜑, 𝜒, 𝜏) ↔ hadd(𝜓, 𝜃, 𝜂)) | ||
Theorem | hadass 1527 | Associative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ⊻ (𝜓 ⊻ 𝜒))) | ||
Theorem | hadbi 1528 | The adder sum is the same as the triple biconditional. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ↔ 𝜓) ↔ 𝜒)) | ||
Theorem | hadcoma 1529 | Commutative law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜓, 𝜑, 𝜒)) | ||
Theorem | hadcomb 1530 | Commutative law for the adders sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜑, 𝜒, 𝜓)) | ||
Theorem | hadrot 1531 | Rotation law for the adder sum. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (hadd(𝜑, 𝜓, 𝜒) ↔ hadd(𝜓, 𝜒, 𝜑)) | ||
Theorem | hadnot 1532 | 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 1533 | 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 1534 | 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 1535 | 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 1536 | Syntax for the "carry" output of the full adder. (Contributed by Mario Carneiro, 4-Sep-2016.) |
wff cadd(𝜑, 𝜓, 𝜒) | ||
Definition | df-cad 1537 | 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 1538 and cadan 1539 for alternate definitions. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓)))) | ||
Theorem | cador 1538 | 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 1539 | 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 1540 | Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (cadd(𝜓, 𝜃, 𝜂) ↔ cadd(𝜒, 𝜏, 𝜁))) | ||
Theorem | cadbi123i 1541 | Equality theorem for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ (cadd(𝜑, 𝜒, 𝜏) ↔ cadd(𝜓, 𝜃, 𝜂)) | ||
Theorem | cadcoma 1542 | Commutative law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜑, 𝜒)) | ||
Theorem | cadcomb 1543 | 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 1544 | Rotation law for the adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ cadd(𝜓, 𝜒, 𝜑)) | ||
Theorem | cadnot 1545 | The adder carry distributes over negation. (Contributed by Mario Carneiro, 4-Sep-2016.) (Proof shortened by Wolf Lammen, 11-Jul-2020.) |
⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ cadd(¬ 𝜑, ¬ 𝜓, ¬ 𝜒)) | ||
Theorem | cad1 1546 | 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 1547 | 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.) |
⊢ (¬ 𝜒 → (cadd(𝜑, 𝜓, 𝜒) ↔ (𝜑 ∧ 𝜓))) | ||
Theorem | cadifp 1548 | 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 | cad11 1549 | If (at least) two inputs are true, then the adder carry is true. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((𝜑 ∧ 𝜓) → cadd(𝜑, 𝜓, 𝜒)) | ||
Theorem | cadtru 1550 | 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 81, ax-1 6, pm2.43 54 } (written B'KW), or with {imim2 56, pm2.04 88, ax-1 6, pm2.43 54 } (written BCKW), or with the single axiom minimp 1551. This section proves minimp 1551 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 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 1551 | 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. (Contributed by BJ, 4-Apr-2021.) |
⊢ (𝜑 → ((𝜓 → 𝜒) → (((𝜃 → 𝜓) → (𝜒 → 𝜏)) → (𝜓 → 𝜏)))) | ||
Theorem | minimp-sylsimp 1552 | Derivation of sylsimp (jarr 104) from ax-mp 5 and minimp 1551. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜓 → 𝜒)) | ||
Theorem | minimp-ax1 1553 | Derivation of ax-1 6 from ax-mp 5 and minimp 1551. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | minimp-ax2c 1554 | Derivation of a commuted form of ax-2 7 from ax-mp 5 and minimp 1551. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → 𝜒))) | ||
Theorem | minimp-ax2 1555 | Derivation of ax-2 7 from ax-mp 5 and minimp 1551. (Contributed by BJ, 4-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | minimp-pm2.43 1556 | Derivation of pm2.43 54 (also called "hilbert" or W) from ax-mp 5 and minimp 1551. 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.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | meredith 1557 |
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 1571, luk-2 1572, and luk-3 1573. Using these we finally rederive our
axioms as ax1 1582, ax2 1583, and ax3 1584,
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 1558 | 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 1559 | 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 1560 | 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 1561 | 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 1562 | 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 1563 | 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 1564 | 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 1565 | 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 1566 | 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 1567 | 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 1568 | 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 1569 | 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 1570 | 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 1571 | 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 1572 | 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 1573 | 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 1574 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | luklem2 1575 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → ¬ 𝜓) → (((𝜑 → 𝜒) → 𝜃) → (𝜓 → 𝜃))) | ||
Theorem | luklem3 1576 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (((¬ 𝜑 → 𝜓) → 𝜒) → (𝜃 → 𝜒))) | ||
Theorem | luklem4 1577 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((¬ 𝜑 → 𝜑) → 𝜑) → 𝜓) → 𝜓) | ||
Theorem | luklem5 1578 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | luklem6 1579 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | luklem7 1580 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒))) | ||
Theorem | luklem8 1581 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜑) → (𝜒 → 𝜓))) | ||
Theorem | ax1 1582 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜑)) | ||
Theorem | ax2 1583 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) | ||
Theorem | ax3 1584 | 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 1585 | Define implication in terms of 'nand'. Analogous to ((𝜑 ⊼ (𝜓 ⊼ 𝜓)) ↔ (𝜑 → 𝜓)). 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 1586 | Define negation in terms of 'nand'. Analogous to ((𝜑 ⊼ 𝜑) ↔ ¬ 𝜑). 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 1587 | 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 1589. 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 1588 | A direct proof of nic-mp 1587. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝜑 & ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⇒ ⊢ 𝜓 | ||
Theorem | nic-ax 1589 | Nicod's axiom derived from the standard ones. See Introduction to Mathematical Philosophy by B. Russell, p. 152. Like meredith 1557, the usual axioms can be derived from this and vice versa. Unlike meredith 1557, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1589, nic-mp 1587 } is equivalent to { luk-1 1571, luk-2 1572, luk-3 1573, 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 1590 | A direct proof of nic-ax 1589. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ ((𝜏 ⊼ (𝜏 ⊼ 𝜏)) ⊼ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) | ||
Theorem | nic-imp 1591 | Inference for nic-mp 1587 using nic-ax 1589 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⇒ ⊢ ((𝜃 ⊼ 𝜒) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) | ||
Theorem | nic-idlem1 1592 | Lemma for nic-id 1594. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ (((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃))) | ||
Theorem | nic-idlem2 1593 | Lemma for nic-id 1594. Inference used by nic-id 1594. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜂 ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⊼ 𝜃)) ⇒ ⊢ ((𝜃 ⊼ (𝜏 ⊼ (𝜏 ⊼ 𝜏))) ⊼ 𝜂) | ||
Theorem | nic-id 1594 | Theorem id 22 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜏 ⊼ (𝜏 ⊼ 𝜏)) | ||
Theorem | nic-swap 1595 | The connector ⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜃 ⊼ 𝜑) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))) | ||
Theorem | nic-isw1 1596 | Inference version of nic-swap 1595. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ⊼ 𝜑) ⇒ ⊢ (𝜑 ⊼ 𝜃) | ||
Theorem | nic-isw2 1597 | Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 ⊼ (𝜃 ⊼ 𝜑)) ⇒ ⊢ (𝜓 ⊼ (𝜑 ⊼ 𝜃)) | ||
Theorem | nic-iimp1 1598 | Inference version of nic-imp 1591 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) & ⊢ (𝜃 ⊼ 𝜒) ⇒ ⊢ (𝜃 ⊼ 𝜑) | ||
Theorem | nic-iimp2 1599 | Inference version of nic-imp 1591 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ⊼ 𝜓) ⊼ (𝜒 ⊼ 𝜒)) & ⊢ (𝜃 ⊼ 𝜑) ⇒ ⊢ (𝜃 ⊼ (𝜒 ⊼ 𝜒)) | ||
Theorem | nic-idel 1600 | Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜓)) ⇒ ⊢ (𝜑 ⊼ (𝜒 ⊼ 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |