Ad argvmentvm transi
Topos Uranos
Latine

Symmetriae connectivorvm

Svmmarivm

Haec lectio demonstrat ordinem argvmentorvm non mvtare qvod ex negatione conivncta, ex disivnctione, ex conivnctione, ex implicatione dvplici et ex disivnctione exclvsiva dedvcitvr. Abbreviationibvs statvtis cvrsvs adhibitis, hae symmetriae non svnt manifestae: negatio conivncta est connectivvm primitivvm, axiomata Łvkasiewiczii de negatione et de implicatione tantvm loqvvntvr, et regvla svbstitvtionis dvplicis negationis (SDN) dvplices negationes tantvm addit vel tollit. Qvapropter lectio primvm tria instrvmenta statvit. Primvm dicit aeqvivalentiam demonstrabilem se gerere vt aeqvalitatem. Secvndvm, lemma fvndamentale, negationem conivnctam in lingvam axiomatvm vertit: (φ↓ψ)(\varphi \downarrow \psi) aeqvivalet formvlae ¬(¬φ→ψ)\neg(\neg\varphi \rightarrow \psi), regvla SDN et dvplici negatione adhibitis. Tertivm, svbstitvtio aeqvivalentivm, qvam regvla SDN svpervacvam non facit, sinit formvlam per aliam qvamlibet aeqvivalentem svbstitvi (et non solvm θ\theta per ¬¬θ\neg\neg\theta) svb negatione, vtrimqve in implicatione et vtrimqve in negatione conivncta. His instrvmentis demonstrantvr, vt aeqvivalentiae, formae aeqvivalentes disivnctionis et conivnctionis, qvas alii libri pro definitionibvs habent, et qvinqve symmetriae, vtroqve sensv et ordine qvem definitiones imponvnt: primvm negatio conivncta, et ex ea, deinceps, ceterae.

Proposita discendi

  1. Abbreviationes statvtas explicare vt decernatvr vtrvm dvae expressiones eandem formvlam designent an formvlas diversas qvarvm aeqvivalentia dedvctionem postvlat.
  2. Lemma fvndamentale (φ↓ψ)⊣⊢¬(¬φ→ψ)(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi) demonstrare regvla svbstitvtionis dvplicis negationis (SDN) et dvplici negatione, dvplicibvs negationibvs qvas abbreviationes celant inventis.
  3. Svbstitvtionem aeqvivalentivm adhibere vt aeqvivalentia in interiorem partem negationis, implicationis vel negationis conivnctae transferatvr, eam a regvla SDN distingvere, qvae tantvm θ\theta et ¬¬θ\neg\neg\theta permvtat, et aeqvivalentia demonstrabili vt aeqvalitate in catenis aeqvivalentiarvm vti.
  4. Formas aeqvivalentes disivnctionis et conivnctionis et qvinqve symmetrias vtroqve sensv demonstrare, effectibvs iam demonstratis inter se nexis.
  5. Svbstitvtionem aeqvivalentivm ad qvamlibet formvlam extendere per indvctionem secvndvm complexitatem formvlarvm.

Qvid adhibeatvr et qvid demonstrandvm sit

Lectio de systematibvs dedvctivis formalibvs systema Łvkasiewiczii statvit: axiomata A1, A2 et A3 et modvm ponentem. Praeterea statvit reflexivitatem (Refl: si φ∈Γ\varphi \in \Gamma, tvm Γ⊢φ\Gamma \vdash \varphi), monotoniam (Mon), sectionem (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 eivs conversvm (CTD) et aeqvivalentiam demonstrabilem, φ⊣⊢ψ\varphi \dashv\vdash \psi, qvae significat {φ}⊢ψ\{\varphi\} \vdash \psi et {ψ}⊢φ\{\psi\} \vdash \varphi; et ostendit, nota qvam axiomata et modvs ponens servant, id systema qvasdam formvlas de negatione conivncta non dedvcere. Lectio de qvattvor artibvs dedvctionis addidit syllogismvm hypotheticvm (SH: {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)), permvtationem praemissarvm (PP), dvplicem negationem (DN: φ⊣⊢¬¬φ\varphi \dashv\vdash \neg\neg\varphi, cvm dvobvs eivs theorematibvs ⊢(¬¬φ→φ)\vdash (\neg\neg\varphi \rightarrow \varphi) et ⊢(φ→¬¬φ)\vdash (\varphi \rightarrow \neg\neg\varphi)) et contrapositionem (CP) tribvs eivs formis:

(φ→ψ)⊣⊢(¬ψ→¬φ),(¬φ→ψ)⊣⊢(¬ψ→φ),(φ→¬ψ)⊣⊢(ψ→¬φ)(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi), \qquad (\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi), \qquad (\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)

Dvplici negatione demonstrata, eadem lectio systema cvrsvs secvnda regvla primitiva complevit, svbstitvtione dvplicis negationis (SDN): si χ′\chi' oritvr ex χ\chi occvrrentia svbformvlae θ\theta per ¬¬θ\neg\neg\theta svbstitvta, vel occvrrentia svbformvlae ¬¬θ\neg\neg\theta per θ\theta, tvm ex χ\chi infertvr χ′\chi'. Versvs sic ex versv ii obtentvs per SDN(i)(i) ivstificatvr. Ab eo loco ⊢\vdash ad systema cvrsvs refertvr (ab A1 ad A3, modvs ponens et SDN), in qvo Refl, Mon, Sect, TD et CTD adhvc valent. Regvla in catenam lingvae fvndamentalis agit, ita vt etiam occvrrentias attingat qvas abbreviatio celat, et in vtrovis ex dvobvs argvmentis negationis conivnctae; inter eivs conseqventias immediatas svnt

(φ↓ψ)⊣⊢(¬¬φ↓ψ),(φ↓ψ)⊣⊢(φ↓¬¬ψ)(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi), \qquad (\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)

et, vniverse, χ⊣⊢χ′\chi \dashv\vdash \chi' qvotiens χ′\chi' oritvr ex χ\chi per SDN. Versvs aeqvivalentiae hvivs formae per «SDN» ivstificatvr, sine nvmero versvs, eodem modo qvo versvs «DN» vel «CP» aeqvivalentiam iam demonstratam citat. Vt ibi, theorema iam demonstratvm vt versvs dedvctionis scribi potest, qvia eivs propria dedvctio eo loco inseri potest; et, per lemma «ab effectv ad regvlam» illivs lectionis, qvaeqve ars etiam vt regvla svb qvavis classe Γ\Gamma praemissarvm adhibetvr, citata cvm nvmeris versvvm ad qvos adhibetvr, vt CP(i)(i) vel SH(i,j)(i, j). In dedvctionibvs de dedvctionibvs, «Praemissa» hypothesim regvlae qvae demonstratvr designat.

Abbreviationes statvtae, in lectione de lingva logicae propositionalis fixae, solae svnt definitiones connectivorvm:

¬φ:=(φ↓φ),(φ∨ψ):=¬(φ↓ψ),(φ∧ψ):=¬(¬φ∨¬ψ)\neg\varphi := (\varphi \downarrow \varphi), \qquad (\varphi \vee \psi) := \neg(\varphi \downarrow \psi), \qquad (\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)
(φ→ψ):=(¬φ∨ψ),(φ↔ψ):=((φ→ψ)∧(ψ→φ)),(φ⊻ψ):=¬(φ↔ψ)(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi), \qquad (\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi)), \qquad (\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)

Versvs per «Def» ivstificatvs nihil dedvcit: eandem formvlam alio nomine scribit, et adnotatio dicit qvae abbreviatio explicetvr vel contrahatvr («Def →\rightarrow», «Def ∨\vee»). Ivvat in memoriam revocare qvod in lectione de formalizatione lingvae natvralis observatvm est: vna eademqve formvla plvra nomina admittit, ita vt conivnctio etiam, vt catena, sit disivnctio. Exempli gratia, implicatione explicata cvm ¬φ\neg\varphi loco φ\varphi, obtinetvr

(¬φ→ψ)=(¬¬φ∨ψ)=¬(¬¬φ↓ψ)(\neg\varphi \rightarrow \psi) = (\neg\neg\varphi \vee \psi) = \neg(\neg\neg\varphi \downarrow \psi)

et dvplex negatio qvae ante φ\varphi apparet, abbreviatione celata, cavsa est cvr regvla SDN in omnibvs qvae seqvvntvr interventvra sit.

Aeqvivalentia demonstrabilis vt aeqvalitas

Demonstrationes hvivs lectionis svnt, fere omnes, catenae aeqvivalentiarvm: φ1⊣⊢φ2\varphi_{1} \dashv\vdash \varphi_{2}, φ2⊣⊢φ3\varphi_{2} \dashv\vdash \varphi_{3}, et sic deinceps. Vt ex catena conclvdatvr φ1⊣⊢φn\varphi_{1} \dashv\vdash \varphi_{n}, aeqvivalentia demonstrabilis se gerere debet vt aeqvalitas, idqve statvit propositio de proprietatibvs aeqvivalentiae demonstrabilis lectionis de systematibvs dedvctivis formalibvs: relatio est reflexiva (φ⊣⊢φ\varphi \dashv\vdash \varphi), symmetrica (si φ⊣⊢ψ\varphi \dashv\vdash \psi, tvm ψ⊣⊢φ\psi \dashv\vdash \varphi) et transitiva (si φ⊣⊢ψ\varphi \dashv\vdash \psi et ψ⊣⊢χ\psi \dashv\vdash \chi, tvm φ⊣⊢χ\varphi \dashv\vdash \chi), et dvae formvlae demonstrabiliter aeqvivalentes vt conclvsiones permvtari possvnt (si Γ⊢φ\Gamma \vdash \varphi et φ⊣⊢φ′\varphi \dashv\vdash \varphi', tvm Γ⊢φ′\Gamma \vdash \varphi', pro omni classe Γ\Gamma formvlarvm). Ivvat in memoriam revocare qvomodo dvae vltimae demonstratae sint, qvia tota lectio in eis nititvr: ex {φ}⊢φ′\{\varphi\} \vdash \varphi' transitvr, per monotoniam, ad Γ∪{φ}⊢φ′\Gamma \cup \{\varphi\} \vdash \varphi', et ex hac et ex Γ⊢φ\Gamma \vdash \varphi, per sectionem, ad Γ⊢φ′\Gamma \vdash \varphi'; transitivitas oritvr ex hoc adhibito cvm Γ={φ}\Gamma = \{\varphi\} altero sensv et cvm Γ={χ}\Gamma = \{\chi\} altero.

Posthac illatio qvae catenam aeqvivalentiarvm in vnam colligit per «Sect» ivstificatvr, qvod est instrvmentvm illivs propositionis. Atqvi qvisqve anvlvs φi⊣⊢φi+1\varphi_{i} \dashv\vdash \varphi_{i+1} dvas dedvctiones continet, eam qvae progreditvr et eam qvae redit; vnde catena aeqvivalentiarvm simvl ambos sensvs svae conclvsionis demonstrat, nec qvicqvam «vt exercitatio» relinqvitvr.