HomeHome 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

Theorem List for New Foundations Explorer - 1401-1500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcadtru 1401 Rotation law for adder carry. (Contributed by Mario Carneiro, 4-Sep-2016.)
cadd( ⊤ , ⊤ , φ)
 
Theoremhad1 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(φ, ψ, χ) ↔ (ψχ)))
 
Theoremhad0 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(φ, ψ, χ) ↔ (ψχ)))
 
1.3  Other axiomatizations of classical propositional calculus
 
1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom
 
Theoremmeredith 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.)

(((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))
 
Theoremaxmeredith 1405 Alias for meredith 1404 which "verify markup *" will match to ax-meredith 1406. (Contributed by NM, 21-Aug-2017.) (New usage is discouraged.)
(((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))
 
Axiomax-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.)
(((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))
 
Theoremmerlem1 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.)
(((χ → (¬ φψ)) → τ) → (φτ))
 
Theoremmerlem2 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.)
(((φφ) → χ) → (θχ))
 
Theoremmerlem3 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.)
(((ψχ) → φ) → (χφ))
 
Theoremmerlem4 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.)
(τ → ((τφ) → (θφ)))
 
Theoremmerlem5 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.)
((φψ) → (¬ ¬ φψ))
 
Theoremmerlem6 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.)
(χ → (((ψχ) → φ) → (θφ)))
 
Theoremmerlem7 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.)
(φ → (((ψχ) → θ) → (((χτ) → (¬ θ → ¬ ψ)) → θ)))
 
Theoremmerlem8 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.)
(((ψχ) → θ) → (((χτ) → (¬ θ → ¬ ψ)) → θ))
 
Theoremmerlem9 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.)
(((φψ) → (χ → (θ → (ψτ)))) → (η → (χ → (θ → (ψτ)))))
 
Theoremmerlem10 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.)
((φ → (φψ)) → (θ → (φψ)))
 
Theoremmerlem11 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.)
((φ → (φψ)) → (φψ))
 
Theoremmerlem12 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.)
(((θ → (¬ ¬ χχ)) → φ) → φ)
 
Theoremmerlem13 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.)
((φψ) → (((θ → (¬ ¬ χχ)) → ¬ ¬ φ) → ψ))
 
Theoremluk-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.)
((φψ) → ((ψχ) → (φχ)))
 
Theoremluk-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.)
((¬ φφ) → φ)
 
Theoremluk-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.)
(φ → (¬ φψ))
 
1.3.2  Derive the standard axioms from the Lukasiewicz axioms
 
Theoremluklem1 1423 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 23-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
(φψ)    &   (ψχ)       (φχ)
 
Theoremluklem2 1424 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
((φ → ¬ ψ) → (((φχ) → θ) → (ψθ)))
 
Theoremluklem3 1425 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
(φ → (((¬ φψ) → χ) → (θχ)))
 
Theoremluklem4 1426 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
((((¬ φφ) → φ) → ψ) → ψ)
 
Theoremluklem5 1427 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
(φ → (ψφ))
 
Theoremluklem6 1428 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
((φ → (φψ)) → (φψ))
 
Theoremluklem7 1429 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
((φ → (ψχ)) → (ψ → (φχ)))
 
Theoremluklem8 1430 Used to rederive standard propositional axioms from Lukasiewicz'. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
((φψ) → ((χφ) → (χψ)))
 
Theoremax1 1431 Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
(φ → (ψφ))
 
Theoremax2 1432 Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
((φ → (ψχ)) → ((φψ) → (φχ)))
 
Theoremax3 1433 Standard propositional axiom derived from Lukasiewicz axioms. (Contributed by NM, 22-Dec-2002.) (Proof modification is discouraged.) (New usage is discouraged.)
((¬ φ → ¬ ψ) → (ψφ))
 
1.3.3  Derive Nicod's axiom from the standard axioms

Prove Nicod's axiom and implication and negation definitions.

 
Theoremnic-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.)
(((φ (ψ ψ)) (φψ)) (((φ (ψ ψ)) (φ (ψ ψ))) ((φψ) (φψ))))
 
Theoremnic-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.)
(((φ φ) ¬ φ) (((φ φ) (φ φ)) φ ¬ φ)))
 
Theoremnic-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.)
φ    &   (φ (χ ψ))       ψ
 
Theoremnic-mpALT 1437 A direct proof of nic-mp 1436. (Contributed by NM, 30-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
φ    &   (φ (χ ψ))       ψ
 
Theoremnic-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.)
((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
 
Theoremnic-axALT 1439 A direct proof of nic-ax 1438. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
 
1.3.4  Derive the Lukasiewicz axioms from Nicod's axiom
 
Theoremnic-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.)
(φ (χ ψ))       ((θ χ) ((φ θ) (φ θ)))
 
Theoremnic-idlem1 1441 Lemma for nic-id 1443. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
((θ (τ (τ τ))) (((φ (χ ψ)) θ) ((φ (χ ψ)) θ)))
 
Theoremnic-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.)
(η ((φ (χ ψ)) θ))       ((θ (τ (τ τ))) η)
 
Theoremnic-id 1443 Theorem id 19 expressed with . (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
(τ (τ τ))
 
Theoremnic-swap 1444 is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
((θ φ) ((φ θ) (φ θ)))
 
Theoremnic-isw1 1445 Inference version of nic-swap 1444. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
(θ φ)       (φ θ)
 
Theoremnic-isw2 1446 Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
(ψ (θ φ))       (ψ (φ θ))
 
Theoremnic-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.)
(φ (χ ψ))    &   (θ χ)       (θ φ)
 
Theoremnic-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.)
((φ ψ) (χ χ))    &   (θ φ)       (θ (χ χ))
 
Theoremnic-idel 1449 Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
(φ (χ ψ))       (φ (χ χ))
 
Theoremnic-ich 1450 Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
(φ (ψ ψ))    &   (ψ (χ χ))       (φ (χ χ))
 
Theoremnic-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.)
(φ (ψ ψ))       ((ψ ψ) ((φ φ) (φ φ)))
 
Theoremnic-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.)
((τ τ) ((τ τ) (τ τ)))
 
Theoremnic-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.)
((φ ψ) ((φ φ) (ψ ψ)))       (φ (ψ ψ))
 
Theoremnic-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.)
((φ ψ) ((φ φ) (ψ ψ)))       (ψ (φ φ))
 
Theoremnic-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.)
φ    &   (φψ)       ψ
 
Theoremnic-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.)
((φψ) → ((ψχ) → (φχ)))
 
Theoremnic-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.)
((¬ φφ) → φ)
 
Theoremnic-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.)
(φ → (¬ φψ))
 
1.3.5  Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom
 
Theoremlukshef-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.)

((φ (χ ψ)) ((θ (θ θ)) ((θ χ) ((φ θ) (φ θ)))))
 
Theoremlukshefth1 1460 Lemma for renicax 1462. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((((τ ψ) ((φ τ) (φ τ))) (θ (θ θ))) (φ (ψ χ)))
 
Theoremlukshefth2 1461 Lemma for renicax 1462. (Contributed by NM, 31-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((τ θ) ((θ τ) (θ τ)))
 
Theoremrenicax 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.)
((φ (χ ψ)) ((τ (τ τ)) ((θ χ) ((φ θ) (φ θ)))))
 
1.3.6  Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms
 
Theoremtbw-bijust 1463 Justification for tbw-negdf 1464. (Contributed by Anthony Hart, 15-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
((φψ) ↔ (((φψ) → ((ψφ) → ⊥ )) → ⊥ ))
 
Theoremtbw-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.)
(((¬ φ → (φ → ⊥ )) → (((φ → ⊥ ) → ¬ φ) → ⊥ )) → ⊥ )
 
Theoremtbw-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.)
((φψ) → ((ψχ) → (φχ)))
 
Theoremtbw-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.)
(φ → (ψφ))
 
Theoremtbw-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.)
(((φψ) → φ) → φ)
 
Theoremtbw-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.)

( ⊥ → φ)
 
Theoremtbwsyl 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.)
(φψ)    &   (ψχ)       (φχ)
 
Theoremtbwlem1 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.)
((φ → (ψχ)) → (ψ → (φχ)))
 
Theoremtbwlem2 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.)
((φ → (ψ → ⊥ )) → (((φχ) → θ) → (ψθ)))
 
Theoremtbwlem3 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.)
(((((φ → ⊥ ) → φ) → φ) → ψ) → ψ)
 
Theoremtbwlem4 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.)
(((φ → ⊥ ) → ψ) → ((ψ → ⊥ ) → φ))
 
Theoremtbwlem5 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.)
(((φ → (ψ → ⊥ )) → ⊥ ) → φ)
 
Theoremre1luk1 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.)
((φψ) → ((ψχ) → (φχ)))
 
Theoremre1luk2 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.)
((¬ φφ) → φ)
 
Theoremre1luk3 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.)

(φ → (¬ φψ))
 
1.3.7  Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom
 
Theoremmerco1 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.)

(((((φψ) → (χ → ⊥ )) → θ) → τ) → ((τφ) → (χφ)))
 
Theoremmerco1lem1 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.)
(φ → ( ⊥ → χ))
 
Theoremretbwax4 1480 tbw-ax4 1468 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
( ⊥ → φ)
 
Theoremretbwax2 1481 tbw-ax2 1466 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(φ → (ψφ))
 
Theoremmerco1lem2 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.)
(((φψ) → χ) → (((ψτ) → (φ → ⊥ )) → χ))
 
Theoremmerco1lem3 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.)
(((φψ) → (χ → ⊥ )) → (χφ))
 
Theoremmerco1lem4 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.)
(((φψ) → χ) → (ψχ))
 
Theoremmerco1lem5 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.)
((((φ → ⊥ ) → χ) → τ) → (φτ))
 
Theoremmerco1lem6 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.)
((φ → (φψ)) → (χ → (φψ)))
 
Theoremmerco1lem7 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.)
(φ → (((ψχ) → ψ) → ψ))
 
Theoremretbwax3 1488 tbw-ax3 1467 rederived from merco1 1478. (Contributed by Anthony Hart, 17-Sep-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
(((φψ) → φ) → φ)
 
Theoremmerco1lem8 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.)
(φ → ((ψ → (ψχ)) → (ψχ)))
 
Theoremmerco1lem9 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.)
((φ → (φψ)) → (φψ))
 
Theoremmerco1lem10 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.)
(((((φψ) → χ) → (τχ)) → φ) → (θφ))
 
Theoremmerco1lem11 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.)
((φψ) → (((χ → (φτ)) → ⊥ ) → ψ))
 
Theoremmerco1lem12 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.)
((φψ) → (((χ → (φτ)) → φ) → ψ))
 
Theoremmerco1lem13 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.)
((((φψ) → (χψ)) → τ) → (φτ))
 
Theoremmerco1lem14 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.)
((((φψ) → ψ) → χ) → (φχ))
 
Theoremmerco1lem15 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.)
((φψ) → (φ → (χψ)))
 
Theoremmerco1lem16 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.)
(((φ → (ψχ)) → τ) → ((φχ) → τ))
 
Theoremmerco1lem17 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.)
(((((φψ) → φ) → χ) → τ) → ((φχ) → τ))
 
Theoremmerco1lem18 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.)
((φ → (ψχ)) → ((ψφ) → (ψχ)))
 
Theoremretbwax1 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 >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6338
  Copyright terms: Public domain < Previous  Next >