HomeHome Intuitionistic Logic Explorer
Theorem List (p. 13 of 20)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1201-1300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem3impdi 1201 Importation inference (undistribute conjunction).
   =>   
 
Theorem3impdir 1202 Importation inference (undistribute conjunction).
   =>   
 
Theorem3anidm12 1203 Inference from idempotent law for conjunction.
   =>   
 
Theorem3anidm13 1204 Inference from idempotent law for conjunction.
   =>   
 
Theorem3anidm23 1205 Inference from idempotent law for conjunction.
   =>   
 
Theorem3ori 1206 Infer implication from triple disjunction.
   =>   
 
Theorem3jao 1207 Disjunction of 3 antecedents.
 
Theorem3jaob 1208 Disjunction of 3 antecedents.
 
Theorem3jaoi 1209 Disjunction of 3 antecedents (inference).
   &       &       =>   
 
Theorem3jaod 1210 Disjunction of 3 antecedents (deduction).
   &       &       =>   
 
Theorem3jaoian 1211 Disjunction of 3 antecedents (inference).
   &       &       =>   
 
Theorem3jaodan 1212 Disjunction of 3 antecedents (deduction).
   &       &       =>   
 
Theorem3jaao 1213 Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (The proof was shortened by Andrew Salmon, 13-May-2011.)
   &       &       =>   
 
Theoremsyl3an9b 1214 Nested syllogism inference conjoining 3 dissimilar antecedents.
   &       &       =>   
 
Theorem3orbi123d 1215 Deduction joining 3 equivalences to form equivalence of disjunctions.
   &       &       =>   
 
Theorem3anbi123d 1216 Deduction joining 3 equivalences to form equivalence of conjunctions.
   &       &       =>   
 
Theorem3anbi12d 1217 Deduction conjoining and adding a conjunct to equivalences.
   &       =>   
 
Theorem3anbi13d 1218 Deduction conjoining and adding a conjunct to equivalences.
   &       =>   
 
Theorem3anbi23d 1219 Deduction conjoining and adding a conjunct to equivalences.
   &       =>   
 
Theorem3anbi1d 1220 Deduction adding conjuncts to an equivalence.
   =>   
 
Theorem3anbi2d 1221 Deduction adding conjuncts to an equivalence.
   =>   
 
Theorem3anbi3d 1222 Deduction adding conjuncts to an equivalence.
   =>   
 
Theorem3anim123d 1223 Deduction joining 3 implications to form implication of conjunctions.
   &       &       =>   
 
Theorem3orim123d 1224 Deduction joining 3 implications to form implication of disjunctions.
   &       &       =>   
 
Theoreman6 1225 Rearrangement of 6 conjuncts.
 
Theorem3an6 1226 Analog of an4 502 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (The proof was shortened by Andrew Salmon, 25-May-2011.)
 
Theorem3or6 1227 Analog of or4 664 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
 
Theoremmp3an1 1228 An inference based on modus ponens.
   &       =>   
 
Theoremmp3an2 1229 An inference based on modus ponens.
   &       =>   
 
Theoremmp3an3 1230 An inference based on modus ponens.
   &       =>   
 
Theoremmp3an12 1231 An inference based on modus ponens.
   &       &       =>   
 
Theoremmp3an13 1232 An inference based on modus ponens.
   &       &       =>   
 
Theoremmp3an23 1233 An inference based on modus ponens.
   &       &       =>   
 
Theoremmp3an1i 1234 An inference based on modus ponens.
   &       =>   
 
Theoremmp3anl1 1235 An inference based on modus ponens.
   &       =>   
 
Theoremmp3anl2 1236 An inference based on modus ponens.
   &       =>   
 
Theoremmp3anl3 1237 An inference based on modus ponens.
   &       =>   
 
Theoremmp3anr1 1238 An inference based on modus ponens.
   &       =>   
 
Theoremmp3anr2 1239 An inference based on modus ponens.
   &       =>   
 
Theoremmp3anr3 1240 An inference based on modus ponens.
   &       =>   
 
Theoremmp3an 1241 An inference based on modus ponens.
   &       &       &       =>   
 
Theoremmpd3an3 1242 An inference based on modus ponens.
   &       =>   
 
Theoremmpd3an23 1243 An inference based on modus ponens.
   &       &       =>   
 
Theorembiimp3a 1244 Infer implication from a logical equivalence. Similar to biimpa 279.
   =>   
 
Theorembiimp3ar 1245 Infer implication from a logical equivalence. Similar to biimpar 280.
   =>   
 
Theorem3anandis 1246 Inference that undistributes a triple conjunction in the antecedent.
   =>   
 
Theorem3anandirs 1247 Inference that undistributes a triple conjunction in the antecedent.
   =>   
 
Theoremecase23d 1248 Deduction for elimination by cases.
   &       &       =>   
 
Theorem3ecase 1249 Inference for elimination by cases.
   &       &       &       =>   
 
1.3  Other axiomatizations of classical propositional calculus
 
1.3.1  Derive the Lukasiewicz axioms from Meredith's sole axiom
 
Theoremmeredith 1250 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 8, where negation and implication are primitive. Here we prove Meredith's axiom from ax-1 5, ax-2 6, and ax-3 7. Then from it we derive the Lukasiewicz axioms luk-1 1265, luk-2 1266, and luk-3 1267. Using these we finally re-derive our axioms as ax1 1276, ax2 1277, and ax3 1278, 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." (The proof was shortened by Andrew Salmon, 25-Jul-2011.) (The proof was shortened by Wolf Lammen, 28-May-2013.)

 
Axiomax-meredith 1251 Theorem meredith 1250 restated as an axiom. This will allow us to ensure that the rederivation of ax1 1276, ax2 1277, and ax3 1278 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.
 
Theoremmerlem1 1252 Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.)
 
Theoremmerlem2 1253 Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem3 1254 Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem4 1255 Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem5 1256 Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem6 1257 Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem7 1258 Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem8 1259 Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem9 1260 Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem10 1261 Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem11 1262 Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem12 1263 Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremmerlem13 1264 Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
 
Theoremluk-1 1265 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
 
Theoremluk-2 1266 2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
 
Theoremluk-3 1267 3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
 
1.3.2  Derive the standard axioms from the Lukasiewicz axioms
 
Theoremluklem1 1268 Used to rederive standard propositional axioms from Lukasiewicz'.
   &       =>   
 
Theoremluklem2 1269 Used to rederive standard propositional axioms from Lukasiewicz'.
 
Theoremluklem3 1270 Used to rederive standard propositional axioms from Lukasiewicz'.
 
Theoremluklem4 1271 Used to rederive standard propositional axioms from Lukasiewicz'.
 
Theoremluklem5 1272 Used to rederive standard propositional axioms from Lukasiewicz'.
 
Theoremluklem6 1273 Used to rederive standard propositional axioms from Lukasiewicz'.
 
Theoremluklem7 1274 Used to rederive standard propositional axioms from Lukasiewicz'.
 
Theoremluklem8 1275 Used to rederive standard propositional axioms from Lukasiewicz'.
 
Theoremax1 1276 Standard propositional axiom derived from Lukasiewicz axioms.
 
Theoremax2 1277 Standard propositional axiom derived from Lukasiewicz axioms.
 
Theoremax3 1278 Standard propositional axiom derived from Lukasiewicz axioms.
 
1.3.3  Logical 'nand' (Sheffer stroke)
 
Syntaxwnand 1279 Extend wff definition to include 'nand'.
 
Definitiondf-nand 1280 Define incompatibility ('not-and' or 'nand'). This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar.
 
1.3.4  Derive Nicod's axiom from the standard axioms
 
Theoremnic-justlem 1281 Lemma for handling nested 'nand's.
 
Theoremnic-justim 1282 Show equivalence between implication and the Nicod version. To derive nic-dfim 1285, apply nic-justbi 1284.
 
Theoremnic-justneg 1283 Show equivalence between negation and the Nicod version. To derive nic-dfneg 1286, apply nic-justbi 1284.
 
Theoremnic-justbi 1284 Show equivalence between the bidirectional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.)
 
Theoremnic-dfim 1285 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).
 
Theoremnic-dfneg 1286 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).
 
Theoremnic-mp 1287 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 1289. 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.)
   &       =>   
 
Theoremnic-mpALT 1288 A direct proof of nic-mp 1287.
   &       =>   
 
Theoremnic-ax 1289 Nicod's axiom derived from the standard ones. See _Intro. to Math. Phil._ by B. Russell, p. 152. Like meredith 1250, the usual axioms can be derived from this and vice versa. Unlike meredith 1250, Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. { nic-ax 1289, nic-mp 1287 } is equivalent to { luk-1 1265, luk-2 1266, luk-3 1267, ax-mp 8 }. 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.)
 
Theoremnic-axALT 1290 A direct proof of nic-ax 1289.
 
1.3.5  Derive the Lukasiewicz axioms from Nicod's axiom
 
Theoremnic-imp 1291 Inference for nic-mp 1287 using nic-ax 1289 as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   =>   
 
Theoremnic-idlem1 1292 Lemma for nic-id 1294.
 
Theoremnic-idlem2 1293 Lemma for nic-id 1294. Inference used by nic-id 1294.
   =>   
 
Theoremnic-id 1294 Theorem id 18 expressed with . (Contributed by Jeff Hoffman, 17-Nov-2007.)
 
Theoremnic-swap 1295 is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.)
 
Theoremnic-isw1 1296 Inference version of nic-swap 1295. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   =>   
 
Theoremnic-isw2 1297 Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   =>   
 
Theoremnic-iimp1 1298 Inference version of nic-imp 1291 using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   &       =>   
 
Theoremnic-iimp2 1299 Inference version of nic-imp 1291 using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   &       =>   
 
Theoremnic-idel 1300 Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   =>   
    < 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-1914
  Copyright terms: Public domain < Previous  Next >