Home | New
Foundations Explorer Theorem List (p. 15 of 64) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cadtru 1401 | Rotation law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ cadd( ⊤ , ⊤ , φ) | ||
Theorem | had1 1402 | If the first parameter is true, the half adder is equivalent to the equality of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (φ → (hadd(φ, ψ, χ) ↔ (ψ ↔ χ))) | ||
Theorem | had0 1403 | If the first parameter is false, the half adder is equivalent to the XOR of the other two inputs. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ (¬ φ → (hadd(φ, ψ, χ) ↔ (ψ ⊻ χ))) | ||
Theorem | meredith 1404 |
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 1420, luk-2 1421, and luk-3 1422. Using these we finally re-derive our
axioms as ax1 1431, ax2 1432, and ax3 1433,
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 | axmeredith 1405 | Alias for meredith 1404 which "verify markup *" will match to ax-meredith 1406. (Contributed by NM, 21-Aug-2017.) (New usage is discouraged.) |
⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ))) | ||
Axiom | ax-meredith 1406 | Theorem meredith 1404 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1431, ax2 1432, and ax3 1433 below depend only on Meredith's sole axiom and not accidentally on a previous theorem above. Outside of this section, we will not make use of this axiom. (Contributed by NM, 14-Dec-2002.) (New usage is discouraged.) |
⊢ (((((φ → ψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τ → φ) → (θ → φ))) | ||
Theorem | merlem1 1407 | 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 1408 | 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 1409 | 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 1410 | 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 1411 | 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 1412 | 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 1413 | 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 1414 | 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 1415 | 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 1416 | 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 1417 | 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 1418 | 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 1419 | 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 1420 | 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 1421 | 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 1422 | 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 1423 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → ψ) & ⊢ (ψ → χ) ⇒ ⊢ (φ → χ) | ||
Theorem | luklem2 1424 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ¬ ψ) → (((φ → χ) → θ) → (ψ → θ))) | ||
Theorem | luklem3 1425 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (((¬ φ → ψ) → χ) → (θ → χ))) | ||
Theorem | luklem4 1426 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((¬ φ → φ) → φ) → ψ) → ψ) | ||
Theorem | luklem5 1427 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (ψ → φ)) | ||
Theorem | luklem6 1428 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (φ → ψ)) → (φ → ψ)) | ||
Theorem | luklem7 1429 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (ψ → χ)) → (ψ → (φ → χ))) | ||
Theorem | luklem8 1430 | Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ψ) → ((χ → φ) → (χ → ψ))) | ||
Theorem | ax1 1431 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (ψ → φ)) | ||
Theorem | ax2 1432 | Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (ψ → χ)) → ((φ → ψ) → (φ → χ))) | ||
Theorem | ax3 1433 | 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 1434 | 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 1435 | 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 1436 | 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 1438. 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 1437 | A direct proof of nic-mp 1436. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ φ & ⊢ (φ ⊼ (χ ⊼ ψ)) ⇒ ⊢ ψ | ||
Theorem | nic-ax 1438 | Nicod's axiom derived from the standard ones. See Intro. to Math. Phil. by B. Russell, p. 152. Like meredith 1404, the usual axioms can be derived from this and vice versa. Unlike meredith 1404, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1438, nic-mp 1436 } is equivalent to { luk-1 1420, luk-2 1421, luk-3 1422, 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 1439 | A direct proof of nic-ax 1438. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) | ||
Theorem | nic-imp 1440 | Inference for nic-mp 1436 using nic-ax 1438 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ ⊼ (χ ⊼ ψ)) ⇒ ⊢ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) | ||
Theorem | nic-idlem1 1441 | Lemma for nic-id 1443. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((θ ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ (((φ ⊼ (χ ⊼ ψ)) ⊼ θ) ⊼ ((φ ⊼ (χ ⊼ ψ)) ⊼ θ))) | ||
Theorem | nic-idlem2 1442 | Lemma for nic-id 1443. Inference used by nic-id 1443. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (η ⊼ ((φ ⊼ (χ ⊼ ψ)) ⊼ θ)) ⇒ ⊢ ((θ ⊼ (τ ⊼ (τ ⊼ τ))) ⊼ η) | ||
Theorem | nic-id 1443 | Theorem id 19 expressed with ⊼. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (τ ⊼ (τ ⊼ τ)) | ||
Theorem | nic-swap 1444 | ⊼ is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((θ ⊼ φ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) | ||
Theorem | nic-isw1 1445 | Inference version of nic-swap 1444. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (θ ⊼ φ) ⇒ ⊢ (φ ⊼ θ) | ||
Theorem | nic-isw2 1446 | Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (ψ ⊼ (θ ⊼ φ)) ⇒ ⊢ (ψ ⊼ (φ ⊼ θ)) | ||
Theorem | nic-iimp1 1447 | Inference version of nic-imp 1440 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ ⊼ (χ ⊼ ψ)) & ⊢ (θ ⊼ χ) ⇒ ⊢ (θ ⊼ φ) | ||
Theorem | nic-iimp2 1448 | Inference version of nic-imp 1440 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ ⊼ ψ) ⊼ (χ ⊼ χ)) & ⊢ (θ ⊼ φ) ⇒ ⊢ (θ ⊼ (χ ⊼ χ)) | ||
Theorem | nic-idel 1449 | Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ ⊼ (χ ⊼ ψ)) ⇒ ⊢ (φ ⊼ (χ ⊼ χ)) | ||
Theorem | nic-ich 1450 | Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ ⊼ (ψ ⊼ ψ)) & ⊢ (ψ ⊼ (χ ⊼ χ)) ⇒ ⊢ (φ ⊼ (χ ⊼ χ)) | ||
Theorem | nic-idbl 1451 | 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 1452 | For nic-* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nic-bi1 1453 and nic-bi2 1454 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 1453 | 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 1454 | 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 1455 | Derive the standard modus ponens from nic-mp 1436. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ φ & ⊢ (φ → ψ) ⇒ ⊢ ψ | ||
Theorem | nic-luk1 1456 | Proof of luk-1 1420 from nic-ax 1438 and nic-mp 1436 (and definitions nic-dfim 1434 and nic-dfneg 1435). Note that the standard axioms ax-1 6, ax-2 7, and ax-3 8 are proved from the Lukasiewicz axioms by theorems ax1 1431, ax2 1432, and ax3 1433. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ))) | ||
Theorem | nic-luk2 1457 | Proof of luk-2 1421 from nic-ax 1438 and nic-mp 1436. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ φ → φ) → φ) | ||
Theorem | nic-luk3 1458 | Proof of luk-3 1422 from nic-ax 1438 and nic-mp 1436. (Contributed by Jeff Hoffman, 18-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (¬ φ → ψ)) | ||
Theorem | lukshef-ax1 1459 |
This alternative axiom for propositional calculus using the Sheffer Stroke
was offered 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 1436 for its constructions. Here, the axiom is proved as a substitution instance of nic-ax 1438. (Contributed by Anthony Hart, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((θ ⊼ (θ ⊼ θ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) | ||
Theorem | lukshefth1 1460 | Lemma for renicax 1462. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ))) | ||
Theorem | lukshefth2 1461 | Lemma for renicax 1462. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((τ ⊼ θ) ⊼ ((θ ⊼ τ) ⊼ (θ ⊼ τ))) | ||
Theorem | renicax 1462 | A rederivation of nic-ax 1438 from lukshef-ax1 1459, proving that lukshef-ax1 1459 with nic-mp 1436 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 1463 | Justification for tbw-negdf 1464. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ ↔ ψ) ↔ (((φ → ψ) → ((ψ → φ) → ⊥ )) → ⊥ )) | ||
Theorem | tbw-negdf 1464 | 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 1465 | 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.) |
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ))) | ||
Theorem | tbw-ax2 1466 | The second of four axioms in the Tarski-Bernays-Wajsberg system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (ψ → φ)) | ||
Theorem | tbw-ax3 1467 | The third of four axioms in the Tarski-Bernays-Wajsberg system. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → ψ) → φ) → φ) | ||
Theorem | tbw-ax4 1468 |
The fourth of four axioms in the Tarski-Bernays-Wajsberg system.
This axiom was added to the Tarski-Bernays axiom system ( see tb-ax1 , tb-ax2 , and tb-ax3 in set.mm) by Wajsberg for completeness. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ⊥ → φ) | ||
Theorem | tbwsyl 1469 | Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → ψ) & ⊢ (ψ → χ) ⇒ ⊢ (φ → χ) | ||
Theorem | tbwlem1 1470 | Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (ψ → χ)) → (ψ → (φ → χ))) | ||
Theorem | tbwlem2 1471 | Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (ψ → ⊥ )) → (((φ → χ) → θ) → (ψ → θ))) | ||
Theorem | tbwlem3 1472 | Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((((φ → ⊥ ) → φ) → φ) → ψ) → ψ) | ||
Theorem | tbwlem4 1473 | Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → ⊥ ) → ψ) → ((ψ → ⊥ ) → φ)) | ||
Theorem | tbwlem5 1474 | Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → (ψ → ⊥ )) → ⊥ ) → φ) | ||
Theorem | re1luk1 1475 | luk-1 1420 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ))) | ||
Theorem | re1luk2 1476 | luk-2 1421 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((¬ φ → φ) → φ) | ||
Theorem | re1luk3 1477 |
luk-3 1422 derived from the Tarski-Bernays-Wajsberg
axioms.
This theorem, along with re1luk1 1475 and re1luk2 1476 proves that tbw-ax1 1465, tbw-ax2 1466, tbw-ax3 1467, and tbw-ax4 1468, with ax-mp 5 can be used as a complete axiom system for all of propositional calculus. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (¬ φ → ψ)) | ||
Theorem | merco1 1478 |
A single axiom for propositional calculus offered by Meredith.
This axiom is worthy of note, due to it having only 19 symbols, not counting parentheses. The more well-known meredith 1404 has 21 symbols, sans parentheses. See merco2 1501 for another axiom of equal length. (Contributed by Anthony Hart, 13-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((((φ → ψ) → (χ → ⊥ )) → θ) → τ) → ((τ → φ) → (χ → φ))) | ||
Theorem | merco1lem1 1479 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → ( ⊥ → χ)) | ||
Theorem | retbwax4 1480 | tbw-ax4 1468 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ( ⊥ → φ) | ||
Theorem | retbwax2 1481 | tbw-ax2 1466 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (ψ → φ)) | ||
Theorem | merco1lem2 1482 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → ψ) → χ) → (((ψ → τ) → (φ → ⊥ )) → χ)) | ||
Theorem | merco1lem3 1483 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → ψ) → (χ → ⊥ )) → (χ → φ)) | ||
Theorem | merco1lem4 1484 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → ψ) → χ) → (ψ → χ)) | ||
Theorem | merco1lem5 1485 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((φ → ⊥ ) → χ) → τ) → (φ → τ)) | ||
Theorem | merco1lem6 1486 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (φ → ψ)) → (χ → (φ → ψ))) | ||
Theorem | merco1lem7 1487 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → (((ψ → χ) → ψ) → ψ)) | ||
Theorem | retbwax3 1488 | tbw-ax3 1467 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → ψ) → φ) → φ) | ||
Theorem | merco1lem8 1489 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (φ → ((ψ → (ψ → χ)) → (ψ → χ))) | ||
Theorem | merco1lem9 1490 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (φ → ψ)) → (φ → ψ)) | ||
Theorem | merco1lem10 1491 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((((φ → ψ) → χ) → (τ → χ)) → φ) → (θ → φ)) | ||
Theorem | merco1lem11 1492 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ψ) → (((χ → (φ → τ)) → ⊥ ) → ψ)) | ||
Theorem | merco1lem12 1493 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ψ) → (((χ → (φ → τ)) → φ) → ψ)) | ||
Theorem | merco1lem13 1494 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((φ → ψ) → (χ → ψ)) → τ) → (φ → τ)) | ||
Theorem | merco1lem14 1495 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((((φ → ψ) → ψ) → χ) → (φ → χ)) | ||
Theorem | merco1lem15 1496 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ψ) → (φ → (χ → ψ))) | ||
Theorem | merco1lem16 1497 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((φ → (ψ → χ)) → τ) → ((φ → χ) → τ)) | ||
Theorem | merco1lem17 1498 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((((φ → ψ) → φ) → χ) → τ) → ((φ → χ) → τ)) | ||
Theorem | merco1lem18 1499 | Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1 1478. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → (ψ → χ)) → ((ψ → φ) → (ψ → χ))) | ||
Theorem | retbwax1 1500 |
tbw-ax1 1465 rederived from merco1 1478.
This theorem, along with retbwax2 1481, retbwax3 1488, and retbwax4 1480, shows that merco1 1478 with ax-mp 5 can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 18-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((φ → ψ) → ((ψ → χ) → (φ → χ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |