Ad argvmentvm transi
Topos Uranos
Latine

Dedvctio: synthesis et provocationes

Svmmarivm

Haec lectio vnitatem clavdit qvae dedvctioni dedicata est. Catenam dedvctivam restitvit qvae a definitione systematis Łvkasiewiczii (tribvs schematibvs axiomatvm et modo ponente) ad theorema dedvctionis et ad limitem illivs systematis in lingva negationis conivnctae pertinet; inde ad qvattvor artes fvndamentales et ad regvlam svbstitvtionis dvplicis negationis, qvae systema cvrsvs complet; a lemmate fvndamentali negationis conivnctae ad svbstitvtionem aeqvivalentivm et ad symmetrias, et inde ad regvlas logicae classicae et ad leges De Morgani et leges distribvtivas, et in qvoqve anvlo indicat qvibvs effectibvs vtatvr et in qva lectione demonstretvr. Distingvit qvae vnitas demonstraverit ab iis qvae admiserit, qvae consecvta svnt ad rationem cvrsvs refert et exponit cvr qvaestio qvam vnitas apertam relinqvit, vtrvm id qvod dedvcibile est cvm eo qvod vervm est congrvat, ad vnitatem de semantica dvcat. In probatione finali artes probationis initialis repetit, et sex provocationibvs finitvr, difficilioribvs qvam problemata lectionvm, qvae instrvmenta plvrivm lectionvm combinare postvlant.

Proposita discendi

  1. Ordinem logicvm effectvvm vnitatis restitvere, effectvs priores qvibvs qvisqve nititvr et lectionem in qva demonstratvr agnoscendo.
  2. Exponere qvomodo theorema dedvctionis, dvplex negatio, regvla svbstitvtionis dvplicis negationis, contrapositio, lemma fvndamentale et svbstitvtio aeqvivalentivm inter se nectantvr, et cvr ab eis regvlae classicae, leges De Morgani et leges distribvtivae pendeant.
  3. Distingvere qvae vnitas demonstraverit ab iis qvae admiserit (schematibvs axiomatvm, dvabvs regvlis primitivis, indvctione forti, indvctione strvctvrali et legibilitate vnica) et ab iis qvae vnitatibvs seqventibvs reliqverit, praesertim a relatione inter dedvctionem et veritatem.
  4. Problemata solvere qvae notas, regvlam svbstitvtionis dvplicis negationis, theorema dedvctionis, demonstrationem per casvs, redvctionem ad absvrdvm, svbstitvtionem aeqvivalentivm, leges De Morgani et leges distribvtivas combinant.

Qvae vnitas consecvta est

Vnitas sibi proposverat lingvam vnitatis svperioris systemate dedvctivo instrvere, id est modo mere syntactico formvlas ex aliis obtinendi, et eo systemate, versv post versvm, artes demonstrare qvibvs mathematica ratiocinatvr. Propositvm pavcis exceptionibvs impletvm est, qvarvm qvaeqve svo loco declarata est: tria schemata axiomatvm et dvae regvlae primitivae, qvae non demonstrantvr sed eligvntvr, et qvarvm recta electio qvaestio est qvam vnitas movet neqve omnino solvit; indvctio fortis et strvctvralis, legibilitas vnica et definitio per recvrsionem, qvae in vnitate svperiore demonstratae svnt et hic adhibentvr; et qvae ex theoria classivm necessaria svnt (svbclasses, vniones et classes finitae), qvae vbi opvs erat in memoriam revocata svnt. His exceptionibvs factis, iter confectvm vt vna catena dedvctiva qvattvor segmentis legi potest.

Systema Łvkasiewiczii eivsqve limes

Lectio de systematibvs dedvctivis formalibvs systema definivit vt lingvam, axiomata qvaedam et regvlas qvasdam, qvae omnia solis catenis inspectis probari possvnt, et primam partem systematis cvrsvs statvit, systema Łvkasiewiczii: schemata A1, A2 et A3 et modvm ponentem vt regvlam vnicam, qvam legibilitas vnica sine ambigvitate adhiberi sinit. Dedvctionem ex classe Γ\Gamma praemissarvm et relationem Γ⊢φ\Gamma \vdash \varphi definivit, ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) qvinqve versibvs dedvxit et proprietates strvctvrales demonstravit: reflexivitatem, monotoniam, modvm ponentem inter dedvctiones, sectionem et finitatem. His et indvctione forti secvndvm nvmervm versvvm theorema dedvctionis demonstravit, cvivs secvndvs casvs postvlat vt privs (φ→φ)(\varphi \rightarrow \varphi) dedvctvm sit, eivsqve conversvm; ex eis aeqvivalentiam demonstrabilem obtinvit, reflexivam, symmetricam et transitivam. Postremo limitem illivs systematis statvit: nota valorvm 00 et 11, per recvrsionem in forma primitiva (α↓β)(\alpha \downarrow \beta) definita, negationem et implicationem vt solet tractat, ab A1, A2, A3 et modo ponente servatvr, et valorem formvlarvm vt (v1↓v2)(v_{1} \downarrow v_{2}) libervm relinqvit. Inde seqvitvr ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) theorema systematis Łvkasiewiczii non esse, et ex (v1↓v2)(v_{1} \downarrow v_{2}) non dedvci (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}), neqve contra. Cvm omnis nota evndem valorem θ\theta et ¬¬θ\neg\neg\theta det, lectio praeterea monvit ne dvplicem qvidem negationem, semel demonstratam, illi limiti mederi.

Qvattvor artes et regvla nova

Lectio de qvattvor artibvs dedvctionis primvm lemma «ab effectv ad regvlam» demonstravit: si {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, eadem conclvsio ex qvavis Γ\Gamma obtinetvr qvae singvlas αi\alpha_{i} dedvcit, et praeterea ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)). Hoc lemma est qvod sinit qvamqve artem tribvs speciebvs adhibere (ex praemissis, vt theorema et vt regvlam), et lectiones de symmetriis et de De Morgano, qvae catenas aeqvivalentiarvm cvm sectione componvnt, ad hoc proprietatibvs aeqvivalentiae demonstrabilis primae lectionis nitvntvr, qvae eadem idea svnt ad vnam praemissam adhibita; in catena qvisqve effectvs semel tantvm apparet, vbi demonstratvr. Eo adhibito, lectio syllogismvm hypotheticvm ex A1 et A2 septem versibvs dedvxit, permvtationem praemissarvm per theorema dedvctionis, dvplicem negationem (cvivs prima directio A3 bis adhibet ad implicationem per A1 fabricatam, et secvnda primam ad ¬φ\neg\varphi et A3 adhibet) et contrapositionem tribvs formis, qvae negationes implicationis tribvs modis distribvvnt; omnes qvattvor iam in systemate Łvkasiewiczii valent.

Dvplici negatione demonstrata, lectio systema cvrsvs secvnda regvla primitiva complevit, svbstitvtione dvplicis negationis (SDN): ex χ\chi infertvr χ′\chi' cvm χ′\chi' oritvr ex eo qvod in χ\chi pro occvrrentia svbformvlae θ\theta ponitvr ¬¬θ\neg\neg\theta, vel pro occvrrentia ipsivs ¬¬θ\neg\neg\theta ponitvr θ\theta. Regvla postvlanda est, qvia nota m1m_{1} theorematibvs dvplicis negationis valorem 11 dat et tamen (v1↓v2)(v_{1} \downarrow v_{2}) a (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) separat; SDN m1m_{1} non servat, et ideo id qvod dedvcibile est amplificat, sed notam honestam servat, et ideo non nimis amplificat. Regvla in catenam lingvae fvndamentalis agit, vbi negatio argvmentvm svvm dvplicat: (φ→ψ)(\varphi \rightarrow \psi) svbformvlam ¬φ\neg\varphi bis continet, et dvplicem negationem ante eivs antecedens ponere dvas applicationes postvlat. Eadem observatio extensionem theorematis dedvctionis svstinet: si versvs per regvlam obtinetvr, hypothesis indvctionis implicationem dat cvivs conseqvens est versvs prior, et dvae applicationes regvlae, vna in vtroqve exemplari illivs conseqventis, implicationem qvaesitam dant; ceterae proprietates strvctvrales eadem demonstratione valent. Primae conseqventiae svnt formvlam aeqvivalere omni formvlae qvae ex ea per regvlam oritvr, praesertim (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) et (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi), et implicationes respondentes, qvas alia systemata vt axiomata svmvnt, hic theoremata esse.

Connectiva et svbstitvtio

Lectio de symmetriis connectivorvm difficvltatem aggressa est lingvae circvlorvm et discorvm propriam: axiomata Łvkasiewiczii de negationibvs tantvm et de implicationibvs loqvvntvr, et fere nvlla negatio conivncta altervtrvm est. Lemma fvndamentale, (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi), pontem iacit: cvm ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) sit ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi), regvla SDN dvplicem negationem interiorem ponit et dvplex negatio exteriorem; contraria via, dvplex negatio et regvla eas tollvnt. Eo adhibito, svbstitvtio aeqvivalentivm, primvm svb negatione et in vtraqve parte implicationis per contrapositionem et syllogismvm hypotheticvm demonstrata, ad vtrvmqve argvmentvm negationis conivnctae extensa est et, inde, ad disivnctionem et ad conivnctionem. Regvla et svbstitvtio non altera alteram svpervacvam reddit: regvla solvm θ\theta et ¬¬θ\neg\neg\theta permvtat, svbstitvtio avtem aeqvivalentia qvaelibet admittit; et svbstitvtio, per lemma fvndamentale demonstrata, ipsa vicissim regvlae innititvr. Lectio deinde demonstravit formas qvas alii libri pro definitionibvs svmvnt aeqvivalentias esse: (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi), qvae dvas applicationes regvlae postvlat, vnam in vtroqve exemplari qvod negatio exterior creat, et (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi), qvae dvplicem negationem postvlat; contra, (φ∧ψ)(\varphi \wedge \psi) et ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi) eadem catena svnt. Postremo qvinqve symmetrias demonstravit eo ordine qvem definitiones imponvnt: symmetriam negationis conivnctae per lemma fvndamentale et contrapositionem, et qvamqve ceterarvm per priorem, svbstitvtione svb negatione translatam cvm opvs est.

Regvlae classicae et leges

Lectio de artibvs logicae classicae demonstravit, omnia cvm classe Γ\Gamma praemissarvm qvae de versv in versvm trahitvr, introdvctionem et eliminationem disivnctionis et conivnctionis, tertivm non datvr et principivm non contradictionis, ex falso qvodlibet, redvctionem ad absvrdvm dvabvs formis et demonstrationem per casvs, cvm formvla eivsqve negatione et cvm disivnctione qvavis. Ordo dependentiarvm strictvs est: ex falso qvodlibet regvlis disivnctionis nititvr; redvctio ad absvrdvm classica ex falso qvodlibet et A3; demonstratio per casvs contrapositioni et redvctioni ad absvrdvm. Nvlla earvm demonstrationvm regvlam SDN directe invocat: regvla per formas aeqvivalentes et svbstitvtionem aeqvivalentivm agit. Lectio de legibvs De Morgani et legibvs distribvtivis has regvlas vna operari fecit: prima lex De Morgani ex definitione conivnctionis et dvplici negatione oritvr; secvnda postvlat vt in negationem conivnctam intretvr, vbi regvla SDN bis intervenit, semel in vtroqve argvmento et sine symmetria, et ex ea seqvitvr (φ↓ψ)(\varphi \downarrow \psi) aeqvivalere formvlae (¬φ∧¬ψ)(\neg\varphi \wedge \neg\psi), lectionem «nec φ\varphi nec ψ\psi» qvam vnitas svperior statverat; inter variantes est ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi). Dvae leges distribvtivae vtroqve sensv per casvs demonstratae svnt, in vtroqve ea forma demonstrationis per casvs electa qvae convenit.

Figvra seqvens qvattvor segmenta in vnam catenam colligit. Qvisqve nodvs colvmnae definitio vel effectvs est, nvmeratvs secvndvm ordinem logicvm et arcv cvm anvlis prioribvs qvibvs eivs demonstratio vtitvr nexvs; circvm flvitant fvlcra, id est principia et instrvmenta ad qvae catena itervm atqve itervm recvrrit, qvodqve linea solida cvm anvlis qvi ei innitvntvr et pvnctata cvm anvlo vbi statvitvr nexvm, praeter ea qvae haec catena non demonstrat (schemata axiomatvm, qvae admittvntvr, et instrvmenta vnitatis svperioris), qvae vt armillae pingvntvr. Regvla svbstitvtionis dvplicis negationis, qvamqvam ipsa qvoqve sine demonstratione admittitvr, cvm anvlo qvi eam indvcit nexa apparet, qvia ibi exponitvr cvr postvlanda sit. Fvlcro pvlsato omnes anvli qvi eo vtvntvr illvstrantvr, et qvisqve anvlvs ad lectionem refert in qva demonstratvr. Animadvertendvm est theorema dedvctionis et dvplicem negationem esse, post axiomata, fvlcra in vnitate saepissime adhibita, et regvlam novam svstinere omnia qvae vnitas de negatione conivncta dicit: theorema dedvctionis extensvm, lemma fvndamentale, formas aeqvivalentes et secvndam legem De Morgani.

Fvlcra catenae

  • ALegibilitas vnica et recvrsio. Si ∙φψ=∙φ′ψ′\sigI\varphi\psi = \sigI\varphi'\psi', cvm omnes qvattvor catenae formvlae sint, tvm φ=φ′\varphi = \varphi' et ψ=ψ′\psi = \psi'; vnde regvla qvae valorem ipsivs ∙φψ\sigI\varphi\psi ex φ\varphi, ex ψ\psi et ex eorvm valoribvs compvtat vnam fvnctionem in formvlis definit. In vnitate svperiore demonstrata est. In hac vnitate sine demonstratione admittitvr.
  • BIndvctio fortis. Si proprietas valet pro nvmero natvrali qvotiens pro omnibvs minoribvs valet, pro omnibvs nvmeris natvralibvs valet. Ex indvctione simplici in vnitate svperiore dedvcta est, et hic ad nvmervm versvvm dedvctionis adhibetvr. In hac vnitate sine demonstratione admittitvr.
  • CAxiomata Łvkasiewiczii. Schemata A1, (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)); A2, ((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi))); et A3, ((¬ψ→¬φ)→(φ→ψ))((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi)). Admittvntvr. In hac vnitate sine demonstratione admittitvr.
  • DSvbstitvtio dvplicis negationis. Secvnda regvla primitiva systematis cvrsvs: ex χ\chi infertvr χ′\chi' si χ′\chi' ex χ\chi oritvr cvm pro occvrrentia svbformvlae θ\theta ponitvr ¬¬θ\neg\neg\theta, vel pro occvrrentia ipsivs ¬¬θ\neg\neg\theta ponitvr θ\theta. Postvlatvr postqvam dvplex negatio demonstrata est. Constitvitvr in: 8. Svbstitvtio dvplicis negationis.
  • ETheorema dedvctionis. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi si et solvm si Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi); in systemate Łvkasiewiczii demonstratvr et, vno casv addito, in systemate cvrsvs valet. Constitvitvr in: 3. Theorema dedvctionis et aeqvivalentia demonstrabilis.
  • FAb effectv ad regvlam. Si {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta et Γ⊢αi\Gamma \vdash \alpha_{i} pro qvoqve ii, tvm Γ⊢β\Gamma \vdash \beta: omnis ars ex praemissis demonstrata svb qvavis classe praemissarvm adhibetvr. Constitvitvr in: 5. Ab effectv ad regvlam.
  • GDvplex negatio. φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, cvm theorematibvs ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) et ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi). Constitvitvr in: 7. Dvplex negatio.
  • HSvbstitvtio aeqvivalentivm. Si φ⊣⊢φ′\varphi \dashv\vdash \varphi', φ′\varphi' loco ipsivs φ\varphi poni potest svb negatione, in vtraqve parte implicationis, negationis conivnctae, disivnctionis et conivnctionis, aeqvivalentia non mvtata. Constitvitvr in: 12. Svbstitvtio aeqvivalentivm.

  1. Segmentvm 1 Systema Łvkasiewiczii eivsqve limes

    • Instantias schematvm agnoscere et decernere vtrvm series formvlarvm sit dedvctio ex classe praemissarvm.
    • Proprietates strvctvrales dedvctionis et theorema dedvctionis per indvctionem fortem secvndvm nvmervm versvvm demonstrare.
    • Dedvctiones de dedvctionibvs constrvere per reflexivitatem, monotoniam, sectionem, theorema dedvctionis eivsqve conversvm.
    • Demonstrare formvlam non dedvci per notam qvam axiomata et modvs ponens servant, et per eam limitem systematis Łvkasiewiczii exponere.

    1. Systema, dedvctio et identitas. Axiomata systematis Łvkasiewiczii svnt instantiae vniformes schematvm A1 ad A3, et eivs regvla vnica est modvs ponens. Γ⊢φ\Gamma \vdash \varphi si exstat series finita formvlarvm qvae in φ\varphi desinit, cvivs qvaeqve formvla axioma est, elementvm ipsivs Γ\Gamma vel per modvm ponentem ex dvabvs prioribvs obtenta. Primvm theorema, ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi), qvinqve versibvs per A1 et A2 dedvcitvr.

      Nititvr: A (Legibilitas vnica et recvrsio), C (Axiomata Łvkasiewiczii). Demonstratvr in: Systemata dedvctiva formalia.

    2. Proprietates strvctvrales. Si φ∈Γ\varphi \in \Gamma, Γ⊢φ\Gamma \vdash \varphi; si Γ⊆Δ\Gamma \subseteq \Delta et Γ⊢φ\Gamma \vdash \varphi, Δ⊢φ\Delta \vdash \varphi; ex Γ⊢φ\Gamma \vdash \varphi et Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi) seqvitvr Γ⊢ψ\Gamma \vdash \psi; si Γ⊢φi\Gamma \vdash \varphi_{i} pro qvoqve ii et Γ∪{φ1,…,φr}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi, Γ⊢ψ\Gamma \vdash \psi; et si Γ⊢φ\Gamma \vdash \varphi, aliqva svbclassis finita ipsivs Γ\Gamma svfficit.

      Vtitvr: 1. Systema, dedvctio et identitas. Demonstratvr in: Systemata dedvctiva formalia.

    3. Theorema dedvctionis et aeqvivalentia demonstrabilis. Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi si et solvm si Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), per indvctionem fortem secvndvm nvmervm versvvm, cvm A1, A2 et identitate. Inde aeqvivalentia demonstrabilis, φ⊣⊢ψ\varphi \dashv\vdash \psi, reflexiva, symmetrica et transitiva est, et dvae formvlae aeqvivalentes ex eisdem classibvs dedvcvntvr.

      Vtitvr: 1. Systema, dedvctio et identitas, 2. Proprietates strvctvrales. Nititvr: B (Indvctio fortis), C (Axiomata Łvkasiewiczii). Demonstratvr in: Systemata dedvctiva formalia.

    4. Limes systematis Łvkasiewiczii. Nota valorvm 00 et 11 per recvrsionem definita implet m(¬φ)=1−m(φ)m(\neg\varphi) = 1 - m(\varphi) et m((φ→ψ))=1−m(φ)(1−m(ψ))m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right), et A1, A2, A3 et modvs ponens notam 11 servant; vnde ((v1↓v2)→¬v1)((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1}) theorema systematis Łvkasiewiczii non est, et {(v1↓v2)}⊬(¬¬v1↓v2)\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2}), neqve contra. Cvm omnis nota dvplici negationi valorem 11 det, svbstitvtio postvlanda est.

      Vtitvr: 1. Systema, dedvctio et identitas. Nititvr: A (Legibilitas vnica et recvrsio), B (Indvctio fortis), C (Axiomata Łvkasiewiczii). Demonstratvr in: Systemata dedvctiva formalia.

  2. Segmentvm 2 Qvattvor artes et regvla nova

    • Effectvm ex praemissis in theorema et in regvlam svb qvavis classe praemissarvm adhibendam convertere.
    • Implicationes concatenare, antecedentia aliter ordinare, dvplices negationes ponere et tollere et eam formam contrapositionis eligere qvae cviqve implicationi respondet.
    • Regvlam svbstitvtionis dvplicis negationis adhibere, occvrrentias qvas abbreviationes celant inveniendo et eam in qvoqve exemplari qvod negatio creat repetendo.
    • Per notam exponere cvr regvla postvletvr, et demonstrare theorema dedvctionis cvm ea valere.

    1. Ab effectv ad regvlam. Si {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, tvm ex Γ⊢α1\Gamma \vdash \alpha_{1}, …\ldots, Γ⊢αn\Gamma \vdash \alpha_{n} seqvitvr Γ⊢β\Gamma \vdash \beta, et ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)); praesertim, si α⊣⊢α′\alpha \dashv\vdash \alpha', Γ⊢α\Gamma \vdash \alpha si et solvm si Γ⊢α′\Gamma \vdash \alpha'.

      Vtitvr: 2. Proprietates strvctvrales. Nititvr: E (Theorema dedvctionis). Demonstratvr in: Qvattvor artes dedvctionis.

    2. Syllogismvs hypotheticvs et permvtatio. {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi), dedvctione septem versvvm ex A1 et A2; et {(φ→(ψ→χ))}⊢(ψ→(φ→χ))\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi)).

      Vtitvr: 1. Systema, dedvctio et identitas. Nititvr: C (Axiomata Łvkasiewiczii), E (Theorema dedvctionis), F (Ab effectv ad regvlam). Demonstratvr in: Qvattvor artes dedvctionis.

    3. Dvplex negatio. ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi), A3 bis adhibita ad implicationem qvam A1 ex ¬¬φ\neg\neg\varphi fabricat; ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi), eo qvod praecedit ad ¬φ\neg\varphi et A3 adhibito; vnde φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, iam in systemate Łvkasiewiczii.

      Nititvr: C (Axiomata Łvkasiewiczii), E (Theorema dedvctionis). Demonstratvr in: Qvattvor artes dedvctionis.

    4. Svbstitvtio dvplicis negationis. Regvla SDN postvlatvr, qvia nota dvplici negationi valorem 11 dat, non avtem svbstitvtioni intra negationem conivnctam. Si χ′\chi' ex χ\chi per regvlam oritvr, χ⊣⊢χ′\chi \dashv\vdash \chi'; praesertim (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi) et (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi).

      Vtitvr: 3. Theorema dedvctionis et aeqvivalentia demonstrabilis, 4. Limes systematis Łvkasiewiczii. Nititvr: G (Dvplex negatio). Demonstratvr in: Qvattvor artes dedvctionis.

    5. Theorema dedvctionis in systemate cvrsvs. Reflexivitas, monotonia, sectio et finitas cvm regvla nova valent, itemqve Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi si et solvm si Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi): in casv novo, cvm (φ→χ)(\varphi \rightarrow \chi) sit ((¬φ↓χ)↓(¬φ↓χ))((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi)), regvla bis adhibetvr, semel in vtroqve exemplari ipsivs χ\chi. Inde ⊢((φ↓ψ)→(¬¬φ↓ψ))\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi)) eivsqve conversvm theoremata svnt.

      Vtitvr: 2. Proprietates strvctvrales, 3. Theorema dedvctionis et aeqvivalentia demonstrabilis. Nititvr: B (Indvctio fortis), D (Svbstitvtio dvplicis negationis). Demonstratvr in: Qvattvor artes dedvctionis.

    6. Contrapositio. (φ→ψ)⊣⊢(¬ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), (¬φ→ψ)⊣⊢(¬ψ→φ)(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi) et (φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi): membra latvs mvtant, et qvodqve in transevndo signvm mvtat.

      Vtitvr: 6. Syllogismvs hypotheticvs et permvtatio. Nititvr: C (Axiomata Łvkasiewiczii), E (Theorema dedvctionis), G (Dvplex negatio), F (Ab effectv ad regvlam). Demonstratvr in: Qvattvor artes dedvctionis.

  3. Segmentvm 3 Connectiva et svbstitvtio

    • Abbreviationes explicare vt decernatvr vtrvm dvae expressiones eandem catenam designent an formvlas qvarvm aeqvivalentia dedvctionem postvlat.
    • Negationem conivnctam per lemma fvndamentale in negationem et implicationem vertere.
    • Aeqvivalentiam per svbstitvtionem aeqvivalentivm in interiorem formvlae partem transferre, eam a regvla svbstitvtionis dvplicis negationis distingvere et aeqvivalentias concatenare.
    • Qvinqve symmetrias eo ordine demonstrare qvem definitiones imponvnt.

    1. Lemma fvndamentale. (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi): cvm ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi) sit ¬¬(¬¬φ↓ψ)\neg\neg(\neg\neg\varphi \downarrow \psi), regvla SDN dvplicem negationem interiorem ponit et dvplex negatio exteriorem; contraria via, dvplex negatio et regvla eas tollvnt.

      Nititvr: D (Svbstitvtio dvplicis negationis), G (Dvplex negatio). Demonstratvr in: Symmetriae connectivorvm.

    2. Svbstitvtio aeqvivalentivm. Si φ⊣⊢φ′\varphi \dashv\vdash \varphi', tvm ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi', (φ→ψ)⊣⊢(φ′→ψ)(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi) et (ψ→φ)⊣⊢(ψ→φ′)(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi'); per lemma fvndamentale idem in vtraqve parte negationis conivnctae, et inde disivnctionis et conivnctionis. Dissimiliter a regvla SDN, aeqvivalentia qvaelibet admittit.

      Vtitvr: 6. Syllogismvs hypotheticvs et permvtatio, 10. Contrapositio, 11. Lemma fvndamentale. Nititvr: E (Theorema dedvctionis). Demonstratvr in: Symmetriae connectivorvm.

    3. Formae aeqvivalentes. (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi), dvabvs applicationibvs regvlae SDN, vna in vtroqve exemplari qvod negatio exterior creat; (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi), per dvplicem negationem; et (φ∧ψ)(\varphi \wedge \psi) eadem catena est ac ¬(φ→¬ψ)\neg(\varphi \rightarrow \neg\psi).

      Nititvr: D (Svbstitvtio dvplicis negationis), G (Dvplex negatio). Demonstratvr in: Symmetriae connectivorvm.

    4. Qvinqve symmetriae. (φ↓ψ)⊣⊢(ψ↓φ)(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi), per lemma fvndamentale et contrapositionem; inde, deinceps, symmetriae ipsorvm ∨\vee, ∧\wedge, ↔\leftrightarrow et ⊻\veebar, qvaeqve per priorem, svbstitvtione svb negatione translatam cvm opvs est.

      Vtitvr: 11. Lemma fvndamentale, 10. Contrapositio. Nititvr: H (Svbstitvtio aeqvivalentivm). Demonstratvr in: Symmetriae connectivorvm.

  4. Segmentvm 4 Regvlae classicae et leges

    • Cvm praemissis introdvctionem et eliminationem disivnctionis et conivnctionis, tertivm non datvr et principivm non contradictionis demonstrare.
    • Ex falso qvodlibet, redvctionem ad absvrdvm et demonstrationem per casvs cvm praemissis demonstrare, et exponere cvr sine eis non svfficiant.
    • Leges De Morgani, earvm variantes et leges distribvtivas vtroqve sensv per dedvctionem demonstrare.
    • Formvlas in formas normales simplices per catenas aeqvivalentiarvm ivstificatarvm transformare.

    1. Regvlae connectivorvm. Cvm qvavis Γ\Gamma: ex φ\varphi seqvitvr (φ∨ψ)(\varphi \vee \psi); ex (φ∨ψ)(\varphi \vee \psi) et ¬φ\neg\varphi, ψ\psi; ex φ\varphi et ψ\psi, (φ∧ψ)(\varphi \wedge \psi); ex (φ∧ψ)(\varphi \wedge \psi), φ\varphi et ψ\psi; praeterea ⊢(φ∨¬φ)\vdash (\varphi \vee \neg\varphi) et ⊢¬(φ∧¬φ)\vdash \neg(\varphi \wedge \neg\varphi).

      Vtitvr: 1. Systema, dedvctio et identitas, 2. Proprietates strvctvrales, 6. Syllogismvs hypotheticvs et permvtatio, 10. Contrapositio, 13. Formae aeqvivalentes, 14. Qvinqve symmetriae. Nititvr: C (Axiomata Łvkasiewiczii), E (Theorema dedvctionis), F (Ab effectv ad regvlam), G (Dvplex negatio). Demonstratvr in: Artes logicae classicae.

    2. Ex falso qvodlibet et redvctio ad absvrdvm. Si Γ⊢φ\Gamma \vdash \varphi et Γ⊢¬φ\Gamma \vdash \neg\varphi, tvm Γ⊢ψ\Gamma \vdash \psi pro omni ψ\psi; si Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} dedvcit ψ\psi et ¬ψ\neg\psi, tvm Γ⊢φ\Gamma \vdash \varphi; et si Γ∪{φ}\Gamma \cup \{\varphi\} eas dedvcit, Γ⊢¬φ\Gamma \vdash \neg\varphi.

      Vtitvr: 1. Systema, dedvctio et identitas, 2. Proprietates strvctvrales, 15. Regvlae connectivorvm. Nititvr: C (Axiomata Łvkasiewiczii), E (Theorema dedvctionis), G (Dvplex negatio). Demonstratvr in: Artes logicae classicae.

    3. Demonstratio per casvs. Si Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi et Γ∪{¬φ}⊢ψ\Gamma \cup \{\neg\varphi\} \vdash \psi, tvm Γ⊢ψ\Gamma \vdash \psi; et si Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi, Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi et Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi), tvm Γ⊢χ\Gamma \vdash \chi.

      Vtitvr: 2. Proprietates strvctvrales, 10. Contrapositio, 15. Regvlae connectivorvm, 16. Ex falso qvodlibet et redvctio ad absvrdvm. Nititvr: E (Theorema dedvctionis). Demonstratvr in: Artes logicae classicae.

    4. Leges De Morgani. ¬(φ∧ψ)⊣⊢(¬φ∨¬ψ)\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi), per definitionem et dvplicem negationem; ¬(φ∨ψ)⊣⊢(¬φ∧¬ψ)\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi), vna applicatione regvlae SDN in vtroqve argvmento negationis conivnctae; vnde (φ↓ψ)⊣⊢(¬φ∧¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi) et ¬(φ→ψ)⊣⊢(φ∧¬ψ)\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi).

      Nititvr: D (Svbstitvtio dvplicis negationis), G (Dvplex negatio), H (Svbstitvtio aeqvivalentivm). Demonstratvr in: Leges De Morgani et leges distribvtivae.

    5. Leges distribvtivae. (φ∧(ψ∨χ))⊣⊢((φ∧ψ)∨(φ∧χ))(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi)) et (φ∨(ψ∧χ))⊣⊢((φ∨ψ)∧(φ∨χ))(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi)), qvaeqve vtroqve sensv per casvs; per symmetrias, etiam a dextra.

      Vtitvr: 14. Qvinqve symmetriae, 15. Regvlae connectivorvm, 17. Demonstratio per casvs. Nititvr: H (Svbstitvtio aeqvivalentivm). Demonstratvr in: Leges De Morgani et leges distribvtivae.

Ad semanticam. Catena ibi consistit vbi dedvctio omnes artes attingit qvibvs mathematica ratiocinatvr. Restat vt sciatvr vtrvm id qvod dedvcitvr sit prorsvs id qvod in omni aestimatione vervm est: vnitas seqvens veritatem definiet, et vltima vtramqve notionem comparabit.

Abbreviationes ivstificationvm

Dedvctiones vnitatis qvemqve versvm abbreviatione ivstificant, eadem in omnibvs lectionibvs. Hic colligvntvr, ordinatae secvndvm lectionem qvae eas indvcit. «Praemissa» hypothesim envntiati designat et, in dedvctionibvs de dedvctionibvs, hypothesim regvlae qvae demonstratvr. Nvmeri inter parentheses versvs citant ad qvos regvla adhibetvr; aeqvivalentia iam demonstrata sine nvmero citatvr cvm vt versvs scribitvr, et cvm nvmero versvs qvem transformat cvm ad evm versvm adhibetvr, etiam ad eivs partem per «Svbst».

  • Prima lectio: A1, A2 et A3 (schemata axiomatvm); MP(i,j)(i, j) (modvs ponens); Def (abbreviationis explicatio vel contractio, cvm connectivo qvod explicatvr: «Def ∨\vee», «Def ⊣⊢\dashv\vdash»); Id (identitas, theorema ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)); Refl (reflexivitas: si φ∈Γ\varphi \in \Gamma, tvm Γ⊢φ\Gamma \vdash \varphi); Mon (monotonia); Sect (sectio: qvod dedvctvm est pro praemissa adhiberi potest); Fin (finitas); TD (theorema dedvctionis) et CTD (eivs conversvm).
  • Secvnda lectio: SH (syllogismvs hypotheticvs); PP (permvtatio praemissarvm); DN (dvplex negatio); SDN(i)(i) (svbstitvtio dvplicis negationis in versv ii; SDN sine nvmero aeqvivalentiam citat inter formvlam et eam qvae ex ea per regvlam oritvr); CP (contrapositio, qvalibet ex tribvs eivs formis); «Solvtvm nn» (effectvs problematis solvti nn eivsdem lectionis, vt versvs scriptvs).
  • Tertia lectio: LF (lemma fvndamentale, (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)); Svbst (svbstitvtio aeqvivalentivm, qvalibet eivs forma, cvm aeqvivalentia qvae adhibetvr svbiecta: «Svbst, DM(i)(i)»); Aeq (formae aeqvivalentes disivnctionis et conivnctionis, (φ∨ψ)⊣⊢(¬φ→ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) et (φ∧ψ)⊣⊢(¬φ↓¬ψ)(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)); Sym (symmetria connectivi).
  • Qvarta lectio: ∨\veeI et ∨\veeE (introdvctio et eliminatio disivnctionis); ∧\wedgeI et ∧\wedgeE (introdvctio et eliminatio conivnctionis); TND (tertivm non datvr); NC (principivm non contradictionis; abbreviatio theorema nominat, nvllvm avtem versvm vnitatis ivstificat); EFQ (ex falso qvodlibet); Cas(i,j)(i, j) et Cas(i,j,k)(i, j, k) (demonstratio per casvs, cvm formvla eivsqve negatione vel cvm disivnctione); «Cas sine praemissis» (demonstratio per casvs sine classe Γ\Gamma, qvae in vno tantvm problemate apparet); RAA (redvctio ad absvrdvm, dvabvs eivs formis).
  • Qvinta lectio: DM (leges De Morgani); Dist (distribvtivitas); Assoc (associativitas disivnctionis); Instantia(i)(i) (versvs ii, qvi pro formvlis qvibvslibet valet, rvrsvs scriptvs cvm aliis formvlis loco metavariabilivm eivs; mvtatio indicatvr).
  • Provocationes hvivs lectionis: M3 (schema qvod tertia provocatio in locvm A3 ponit).