Ad argvmentvm transi
Topos Uranos
Latine

Leges De Morgani et leges distribvtivae

Svmmarivm

Haec lectio vnitatem de dedvctione clavdit dvabvs aeqvivalentiarvm familiis qvibvs tota mathematica vtitvr: legibvs De Morgani, qvae dicvnt qvomodo negatio conivnctionem vel disivnctionem transeat, et legibvs distribvtivis, qvae dicvnt qvomodo conivnctio svper disivnctionem et disivnctio svper conivnctionem distribvatvr. Anteqvam demonstrentvr, distinctio explanatvr ex qva pendent: dvae expressiones qvae eandem catenam designant altera pro altera sine vlla cavtione poni possvnt, qvia eadem formvla svnt; dvae formvlae tantvm aeqvivalentes, contra, intra aliam formvlam inter se commvtari possvnt sola svbstitvtione aeqvivalentivm, stratvm post stratvm. Hac cavtione adhibita, dedvctione demonstrantvr ambae leges De Morgani, earvm variantes (inter qvas negatio implicationis) et ambae leges distribvtivae, qvaeqve in vtramqve partem. Problemata eis vtvntvr vt idempotentiam, absorptionem et associativitatem, formas normales simplices et dedvctiones obtineant qvae leges De Morgani cvm contrapositione miscent.

Proposita discendi

  1. Identitatem catenarvm, qvae sinit abbreviationem qvolibet loco cvm explicatione sva commvtari, ab aeqvivalentia demonstrabili distingvere, qvae intra formvlam commvtare tantvm per svbstitvtionem aeqvivalentivm sinit, et aeqvivalentias in dedvctione concatenare.
  2. Ambas leges De Morgani earvmqve variantes, negatione implicationis comprehensa, dedvctione demonstrare, et in eis partes regvlae svbstitvtionis dvplicis negationis agnoscere.
  3. Distribvtivitatem conivnctionis svper disivnctionem et disivnctionis svper conivnctionem in vtramqve partem demonstrare, in qvoqve casv demonstrationem per casvs idoneam eligendo.
  4. Formvlas in formas normales simplices transformare per catenam aeqvivalentiarvm gradatim ivstificatam, et leges idempotentiae, absorptionis et associativitatis dedvctione obtinere.
  5. Dedvctiones cvm praemissis constrvere qvae leges De Morgani cvm contrapositione et cvm regvlis introdvctionis et eliminationis connectivorvm misceant.

Lectiones svperiores hvivs vnitatis instrvmenta dedvctionis alivd svper alivd aedificavervnt: systema axiomatvm et modvm ponentem, qvattvor artes fvndamentales et svbstitvtionem dvplicis negationis, symmetrias connectivorvm et artes logicae classicae. Haec lectio nvllam regvlam novam addit; eas simvl operari facit. Qvod si ita est, eivs vtilitas non tam in envntiatis est, qvae fortasse ex aliis cvrsibvs iam nota svnt, qvam in modo ea obtinendi: qvisqve versvs ivstificari debet axiomate, praemissa, definitione, altera dvarvm regvlarvm primitivarvm vel effectv iam demonstrato, et nvllvs niti potest in eo qvod «evidens videtvr».

Qvae adhibentvr et qvomodo concatenantvr

Ex lectione de systematibvs dedvctivis formalibvs svmvntvr axiomata A1, A2 et A3 Łvkasiewiczii, modvs ponens (MP), etiam cvm praemissis, reflexivitas (Refl: si φ∈Γ\varphi \in \Gamma, tvm Γ⊢φ\Gamma \vdash \varphi), monotonia (Mon), sectio (Sect: si Γ⊢φi\Gamma \vdash \varphi_i pro qvoqve ii et Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_1, \ldots, \varphi_n\} \vdash \psi, tvm Γ⊢ψ\Gamma \vdash \psi), theorema dedvctionis (TD) et aeqvivalentia demonstrabilis (φ⊣⊢ψ\varphi \dashv\vdash \psi si {φ}⊢ψ\{\varphi\} \vdash \psi et {ψ}⊢φ\{\psi\} \vdash \varphi), cvm svis proprietatibvs: est reflexiva, symmetrica et transitiva, et, si φ⊣⊢ψ\varphi \dashv\vdash \psi, tvm Γ⊢φ\Gamma \vdash \varphi si et solvm si Γ⊢ψ\Gamma \vdash \psi. Ex lectione de qvattvor artibvs dedvctionis, dvplex negatio (DN: φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi), contrapositio (CP), praesertim (φ→ψ)⊣⊢(¬ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), et altera regvla primitiva systematis cvrsvs, svbstitvtio dvplicis negationis (SDN), qva theorema dedvctionis valere pergit: si χ′\chi' ex χ\chi oritvr, cvm occvrrentiae cvivsdam svbformvlae θ\theta svbstitvitvr ¬¬θ\neg\neg\theta, vel occvrrentiae formvlae ¬¬θ\neg\neg\theta svbstitvitvr θ\theta, ex χ\chi infertvr χ′\chi'; versvs hoc modo ex versv ii obtentvs ivstificatvr SDN(i)(i). Inter eivs conseqventias immediatas svnt (φ↓ψ)⊣⊢(¬¬φ↓ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), (φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi) et, generaliter, χ⊣⊢χ′\chi \dashv\vdash \chi' cvm χ′\chi' ex χ\chi per SDN oritvr; ex qvo seqvitvr SDN(i)(i) etiam ad versvm formae χ⊣⊢φ\chi \dashv\vdash \varphi adhiberi, vt dvplex negatio in φ\varphi mvtetvr. Ex lectione de symmetriis connectivorvm, svbstitvtio aeqvivalentivm (Svbst) et symmetriae (Sym), inter qvas (φ∨ψ)⊣⊢(ψ∨φ)(\varphi \vee \psi) \dashv\vdash (\psi \vee \varphi) et (φ∧ψ)⊣⊢(ψ∧φ)(\varphi \wedge \psi) \dashv\vdash (\psi \wedge \varphi).

Ex lectione de artibvs logicae classicae svmvntvr, omnes cvm classe Γ\Gamma praemissarvm, regvlae seqventes. Introdvctio disivnctionis (∨\veeI): si Γ⊢φ\Gamma \vdash \varphi, tvm Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi) et Γ⊢(ψ∨φ)\Gamma \vdash (\psi \vee \varphi). Eliminatio disivnctionis (∨\veeE, syllogismvs disivnctivvs): si Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi) et Γ⊢¬φ\Gamma \vdash \neg\varphi, tvm Γ⊢ψ\Gamma \vdash \psi. Introdvctio conivnctionis (∧\wedgeI): si Γ⊢φ\Gamma \vdash \varphi et Γ⊢ψ\Gamma \vdash \psi, tvm Γ⊢(φ∧ψ)\Gamma \vdash (\varphi \wedge \psi). Eliminatio conivnctionis (∧\wedgeE): si Γ⊢(φ∧ψ)\Gamma \vdash (\varphi \wedge \psi), tvm Γ⊢φ\Gamma \vdash \varphi et Γ⊢ψ\Gamma \vdash \psi. Tertivm non datvr (TND): ⊢(φ∨¬φ)\vdash (\varphi \vee \neg\varphi). Et demonstratio per casvs (Cas) dvabvs svis formis: si Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi et Γ∪{¬φ}⊢χ\Gamma \cup \{\neg\varphi\} \vdash \chi, tvm Γ⊢χ\Gamma \vdash \chi; et si Γ∪{φ}⊢χ\Gamma \cup \{\varphi\} \vdash \chi, Γ∪{ψ}⊢χ\Gamma \cup \{\psi\} \vdash \chi et Γ⊢(φ∨ψ)\Gamma \vdash (\varphi \vee \psi), tvm Γ⊢χ\Gamma \vdash \chi. In dedvctionibvs prior forma dvobvs versibvs citatvr, Cas(i,j)(i, j), altera tribvs, Cas(i,j,k)(i, j, k), ordine envntiati: dvo casvs et, in fine, disivnctio. Illa lectio praeterea commemorat omnem regvlam iam demonstratam intra contextvm Γ\Gamma valere, et ita hic adhibentvr dvplex negatio et contrapositio.

Nomina catenae et formvlae aeqvivalentes

Meminerimvs, ex lectione de lingva logicae propositionalis, connectiva praeter ↓\downarrow esse abbreviationes cvm definitione statvta et vnica: ¬φ:=(φ↓φ)\neg\varphi := (\varphi \downarrow \varphi), (φ∨ψ):=¬(φ↓ψ)(\varphi \vee \psi) := \neg(\varphi \downarrow \psi), (φ∧ψ):=¬(¬φ∨¬ψ)(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi), (φ→ψ):=(¬φ∨ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), (φ↔ψ):=((φ→ψ)∧(ψ→φ))(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)) et (φ⊻ψ):=¬(φ↔ψ)(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi). Definitio nihil de formvlis affirmat: altervm nomen catenae iam exstanti dat. Ex qvo seqvitvr, si dvae expressiones eandem catenam designant, alteram pro altera qvolibet loco poni posse, etiam intra formvlam maiorem, qvia qvod scribitvr eadem series circvlorvm et discorvm est. Ita ¬(φ∧ψ)\neg(\varphi \wedge \psi) et ¬¬(¬φ∨¬ψ)\neg\neg(\neg\varphi \vee \neg\psi) eadem catena svnt: secvnda oritvr cvm intra primam explicatio conivnctionis scribitvr. In dedvctionibvs haec nominis mvtatio per «Def» ivstificatvr, addito connectivo qvod explicatvr vel contrahitvr.

Atqvi aeqvivalentia demonstrabilis non est identitas. Qvod φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi valet significat vtramqve ex altera dedvci, non eandem catenam esse: ¬¬φ\neg\neg\varphi mvlto longior est qvam φ\varphi. Itaqve scire φ⊣⊢φ′\varphi \dashv\vdash \varphi' non sinit per se φ′\varphi' loco φ\varphi intra formvlam maiorem scribere. Neqve sinit «vtrvmqve latvs negare»: qvod ex φ⊣⊢φ′\varphi \dashv\vdash \varphi' seqvitvr ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi' theorema est, svbstitvtio aeqvivalentivm, cvivs demonstratio contrapositione vtitvr, non operatio evidens. Vnvs est casvs in qvo systema svbstitvtionem directe sinit, qvolibet formvlae loco: formvlae θ\theta in ¬¬θ\neg\neg\theta mvtatae, vel e contrario, qvae est regvla SDN; et lectio de systematibvs dedvctivis nota ostendit ne hvnc qvidem casvm ex axiomatibvs et modo ponente dedvci, ita vt postvlandvs esset. Haec cvra non est pedantismvs; est id qvod demonstrationem a symbolorvm tractatione distingvit qvae, ad alia connectiva vel in aliis systematibvs adhibita, ad falsa dvcere posset.

Dvo effectvs accvrate statvvnt qvid liceat. Primvs est propositio de proprietatibvs aeqvivalentiae demonstrabilis ex lectione de systematibvs dedvctivis formalibvs: si Γ⊢φ\Gamma \vdash \varphi et φ⊣⊢φ′\varphi \dashv\vdash \varphi', tvm Γ⊢φ′\Gamma \vdash \varphi', ita vt aeqvivalentia demonstrabilis ad totam formvlam versvs adhiberi possit; et aeqvivalentia demonstrabilis reflexiva, symmetrica et transitiva est, ita vt aeqvivalentiae concatenentvr (si χ⊣⊢φ\chi \dashv\vdash \varphi et φ⊣⊢φ′\varphi \dashv\vdash \varphi', tvm χ⊣⊢φ′\chi \dashv\vdash \varphi') et dvae expressiones qvae eandem catenam designant per reflexivitatem demonstrabiliter aeqvivalentes sint. Secvndvs, lemma seqvens, vt commode citetvr, colligit extensionem svbstitvtionis aeqvivalentivm ad disivnctionem et conivnctionem, qvam lectio de symmetriis pro negatione, implicatione et negatione conivncta demonstrat et ad haec dvo connectiva in vno ex svis problematibvs solvtis extendit.

LemmaSvbstitvtio in disivnctione et in conivnctione

Si φ⊣⊢φ′\varphi \dashv\vdash \varphi', tvm, pro omni formvla ψ\psi, (φ∨ψ)⊣⊢(φ′∨ψ)(\varphi \vee \psi) \dashv\vdash (\varphi' \vee \psi), (ψ∨φ)⊣⊢(ψ∨φ′)(\psi \vee \varphi) \dashv\vdash (\psi \vee \varphi'), (φ∧ψ)⊣⊢(φ′∧ψ)(\varphi \wedge \psi) \dashv\vdash (\varphi' \wedge \psi) et (ψ∧φ)⊣⊢(ψ∧φ′)(\psi \wedge \varphi) \dashv\vdash (\psi \wedge \varphi').

Demonstratio

  1. (φ∨ψ)=¬(φ↓ψ)(\varphi \vee \psi) = \neg\resaltar{(\varphi \downarrow \psi)}

    Disivnctio est, ex definitione, negatio negationis conivnctae.

  2. (φ↓ψ)⊣⊢(φ′↓ψ)\dato{int}{(\varphi \downarrow \psi) \dashv\vdash (\varphi' \downarrow \psi)}

    Svbstitvtio aeqvivalentivm pro negatione conivncta aeqvivalentiam strati interioris dat.

  3. (φ∨ψ)⊣⊢(φ′∨ψ)\dato{disy}{\resaltar{(\varphi \vee \psi)} \dashv\vdash \resaltar{(\varphi' \vee \psi)}}

    Svbstitvtio aeqvivalentivm pro negatione eam ad stratvm exterivs fert, ¬(φ↓ψ)⊣⊢¬(φ′↓ψ)\neg(\varphi \downarrow \psi) \dashv\vdash \neg(\varphi' \downarrow \psi), qvae est disivnctio. Eodem modo, cvm (ψ↓φ)⊣⊢(ψ↓φ′)(\psi \downarrow \varphi) \dashv\vdash (\psi \downarrow \varphi'), svbstitvtio a dextra obtinetvr.

  4. (φ∧ψ)=¬(¬φ∨¬ψ),¬φ⊣⊢¬φ′(\varphi \wedge \psi) = \neg(\resaltar{\neg\varphi} \vee \neg\psi), \qquad \neg\varphi \dashv\vdash \neg\varphi'

    Conivnctio est negatio disivnctionis negationvm. Svbstitvtio pro negatione primvm dat ¬φ⊣⊢¬φ′\neg\varphi \dashv\vdash \neg\varphi'.

  5. ¬(¬φ∨¬ψ)⊣⊢¬(¬φ′∨¬ψ),(φ∧ψ)⊣⊢(φ′∧ψ)\neg(\neg\varphi \vee \neg\psi) \dashv\vdash \neg(\neg\varphi' \vee \neg\psi), \qquad \resaltar{(\varphi \wedge \psi)} \dashv\vdash \resaltar{(\varphi' \wedge \psi)}

    Pars pro disivnctione iam demonstrata, ad ¬φ\neg\varphi et ¬φ′\neg\varphi' adhibita, dat (¬φ∨¬ψ)⊣⊢(¬φ′∨¬ψ)(\neg\varphi \vee \neg\psi) \dashv\vdash (\neg\varphi' \vee \neg\psi), et rvrsvs svbstitvtio pro negatione aeqvivalentiam ad conivnctionem fert; a dextra eodem modo ratiocinatio procedit.

Posthac «Svbst» svbstitvtionem aeqvivalentivm qvavis sva forma designat, etiam formis hvivs lemmatis, et plvries deinceps adhiberi potest, stratvm post stratvm, vt ad svbformvlam qvavis profvnditate sitam perveniatvr. Cvm versvs ex versv ii obtinetvr aeqvivalentia iam demonstrata adhibita, sive ad totam formvlam sive, cvm Svbst, ad aliqvam eivs partem, nomine illivs aeqvivalentiae et nvmero versvs ivstificatvr: DN(i)(i), «Svbst, DM(i)(i)». Nominis mvtatio, qvae nvllam aeqvivalentiam adhibet sed eandem catenam rescribit, eodem modo ivstificatvr, per Def addito connectivo qvod explicatvr vel contrahitvr: Def ∧\wedge (i)(i). Propositio lectionis de systematibvs dedvctivis formalibvs praestat tales versvs ivstificatos esse, sive versvs ii affirmat Γ⊢φ\Gamma \vdash \varphi sive affirmat aeqvivalentiam χ⊣⊢φ\chi \dashv\vdash \varphi qvae prodvcitvr.