Ad argvmentvm transi
Topos Uranos
Latine

Qvattvor artes dedvctionis

Svmmarivm

Systema Łvkasiewiczii lectionis svperioris tribvs schematibvs axiomatvm et vna sola regvla, modo ponente, constat; tam pavcis opibvs omnis dedvctio ab axiomatibvs constrvenda est, atqve etiam formvla (φ→φ)(\varphi \rightarrow \varphi) qvinqve versvs postvlat. Haec lectio qvattvor artes addit, qvae semel demonstrantvr et deinceps itervm adhibentvr: syllogismvm hypotheticvm, qvi implicationes concatenat; permvtationem praemissarvm, qvae ordinem antecedentivm mvtare sinit; dvplicem negationem, qvae dvas negationes continvas ponere et tollere sinit; et contrapositionem, tribvs formis, qvae implicationem invertere sinit membris eivs negatis. Qvaeqve ars tota demonstratvr, versv post versvm, tribvs axiomatibvs, modo ponente et metatheorematibvs lectionis svperioris, et tribvs speciebvs obtinetvr: vt dedvctio ex praemissis, vt theorema et vt regvla svb qvavis classe praemissarvm adhibenda. Dvplici negatione demonstrata, lectio systema secvnda regvla primitiva complet, svbstitvtione dvplicis negationis, qvae dvas negationes qvolibet loco formvlae ponere vel tollere sinit, etiam intra negationem conivnctam, qvo tria axiomata non pervenivnt; exponit cvr ea regvla postvlanda sit, comprobat proprietates dedvctionis servari, theorema dedvctionis novo casv extendit et primas eivs conseqventias obtinet.

Proposita discendi

  1. Effectvm formae {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta in theorema convertere, per theorema dedvctionis, et in regvlam svb qvavis classe praemissarvm Γ\Gamma adhibendam, per monotoniam et sectionem.
  2. Syllogismvm hypotheticvm et permvtationem praemissarvm demonstrare, tam dedvctione directa ex A1 et A2 qvam ratiocinando de dedvctionibvs cvm theoremate dedvctionis, eisqve vti ad implicationes concatenandas et ordinandas.
  3. Dvas directiones dvplicis negationis axiomatibvs A1 ad A3 et modo ponente demonstrare, easqve adhibere ad dvas negationes continvas in dedvctione ponendas vel tollendas.
  4. Regvlam svbstitvtionis dvplicis negationis envntiare, occvrrentias svbformvlae in catena lingvae fvndamentalis invenire, etiam eas qvas abbreviatio celat, et regvlam in dedvctionibvs adhibere.
  5. Nota exponere cvr svbstitvtio dvplicis negationis postvlanda sit, et demonstrare proprietates dedvctionis et theorema dedvctionis in systemate amplificato valere.
  6. Contrapositionem tribvs formis demonstrare et, implicatione cvm negationibvs proposita, formam congrventem eligere.
  7. Dedvctiones non triviales constrvere qvattvor artes et novam regvlam cvm axiomatibvs, modo ponente et theoremate dedvctionis combinando, et qvemqve versvm abbreviatione congrventi ivstificare.

Instrvmenta initialia

In lectione de systematibvs dedvctivis formalibvs systema Łvkasiewiczii statvtvm est. Eivs lingva est lingva circvlorvm et discorvm, scripta abbreviationibvs statvtis lectionis de lingva logicae propositionalis; eivs axiomata svnt omnes instantiae trivm schematvm seqventivm, vbi φ\varphi, ψ\psi et χ\chi svnt formvlae qvaelibet, et eivs sola regvla est modvs ponens.

  • A1: (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)).
  • A2: ((φ→(ψ→χ))→((φ→ψ)→(φ→χ)))((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi))).
  • A3: ((¬ψ→¬φ)→(φ→ψ))((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi)).
  • MP: ex φ\varphi et (φ→ψ)(\varphi \rightarrow \psi) dedvcitvr ψ\psi.

Dedvctio formvlae φ\varphi ex classe Γ\Gamma formvlarvm est series finita formvlarvm qvae in φ\varphi desinit et in qva qvaeqve formvla est axioma, elementvm classis Γ\Gamma avt effectvs modi ponentis ad dvas formvlas priores adhibiti; si exstat, scribitvr Γ⊢φ\Gamma \vdash \varphi, et si Γ\Gamma vacva est, ⊢φ\vdash \varphi, et dicitvr φ\varphi esse theorema. In eadem lectione demonstrata svnt metatheoremata qvibvs hic vtemvr: reflexivitas (Refl: si φ∈Γ\varphi \in \Gamma, tvm Γ⊢φ\Gamma \vdash \varphi), monotonia (Mon: si Γ⊆Δ\Gamma \subseteq \Delta et Γ⊢φ\Gamma \vdash \varphi, tvm Δ⊢φ\Delta \vdash \varphi), modvs ponens inter dedvctiones (si Γ⊢φ\Gamma \vdash \varphi et Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), tvm Γ⊢ψ\Gamma \vdash \psi), sectio (Sect: si Γ⊢φi\Gamma \vdash \varphi_{i} pro qvoqve ii ab 11 ad nn et Γ∪{φ1,…,φn}⊢ψ\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi, tvm Γ⊢ψ\Gamma \vdash \psi), finitas (si Γ⊢φ\Gamma \vdash \varphi, aliqva svbclassis finita classis Γ\Gamma svfficit), theorema dedvctionis (TD: si Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi, tvm Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)) et eivs conversvm (CTD), et theorema ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi), qvod in ivstificationibvs Id abbreviabimvs. Deniqve φ⊣⊢ψ\varphi \dashv\vdash \psi (aeqvivalentia demonstrabilis) significat {φ}⊢ψ\{\varphi\} \vdash \psi et {ψ}⊢φ\{\psi\} \vdash \varphi.

Meminisse ivvat ¬\neg et →\rightarrow non esse signa lingvae fvndamentalis, sed abbreviationes: ¬φ\neg\varphi est catena (φ↓φ)(\varphi \downarrow \varphi), et (φ→ψ)(\varphi \rightarrow \psi) est (¬φ∨ψ)(\neg\varphi \vee \psi), id est ¬(¬φ↓ψ)\neg(\neg\varphi \downarrow \psi). Tria axiomata de negationibvs et implicationibvs tantvm loqvvntvr, et eadem lectio, nota valorvm 00 et 11 qvam ea et modvs ponens servant, limitem ostendit qvi inde seqvitvr: in systemate Łvkasiewiczii ex (v1↓v2)(v_{1} \downarrow v_{2}) non dedvcitvr (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}), et negatio conivncta ex parte extra eivs ambitvm manet. Haec igitvr lectio dvobvs temporibvs procedit. Vsqve ad dvplicem negationem inclvsam, ⊢\vdash ad systema Łvkasiewiczii refertvr, et nihil eorvm qvae demonstrantvr ex abbreviationibvs explicandis pendet. Dvplici negatione demonstrata, systemati secvnda regvla primitiva additvr, svbstitvtio dvplicis negationis, qvae in catenam explicatam agit; ab eo loco ⊢\vdash ad systema cvrsvs refertvr, id est systema Łvkasiewiczii hac regvla avctvm. Cvm omnis dedvctio prioris etiam dedvctio posterioris sit, nihil eorvm qvae antea demonstrata svnt amittitvr.

Dvo genera dedvctionis

Dvo modi svnt dedvctionem scribendi, et ambo adhibebvntvr. Primvs est dedvctio proprie dicta, series formvlarvm in qva qvisqve versvs est axioma, praemissa avt effectvs modi ponentis; qvisqve versvs ivstificatvr per A1, A2, A3, Praemissa avt MP(i,j)(i, j), vbi versvs ii est antecedens et versvs jj est implicatio cvivs antecedens est ipse versvs ii (et, ex qvo regvla nova introdvcta erit, SDN(i)(i)). Secvndvs est dedvctio de dedvctionibvs, cvivs versvs non svnt formvlae, sed envntiationes formae Γ⊢φ\Gamma \vdash \varphi; qvaeqve per metatheorema iam demonstratvm ivstificatvr, et tota series est ratiocinatio metalingvae qvae praestat exstare dedvctionem primi generis, qvamvis eam non scribat. Ivstificationes hvivs secvndi generis sic legvntvr.

  • Refl: formvla dextra ad classem sinistram pertinet.
  • A1, A2, A3: formvla dextra est instantia schematis; instantia axiomatis ex qvavis Γ\Gamma dedvctione vnivs versvs dedvcitvr.
  • MP(i,j)(i, j): modvs ponens inter dedvctiones, ad versvm ii, Γ⊢φ\Gamma \vdash \varphi, et ad versvm jj, Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), adhibitvs, eadem Γ\Gamma.
  • TD(i)(i) et CTD(i)(i): theorema dedvctionis avt eivs conversvm, ad versvm ii adhibitvm.
  • Nomen theorematis iam demonstrati, vt Id avt DN: formvla dextra est instantia eivs theorematis, et ex qvavis Γ\Gamma per monotoniam dedvcitvr, qvia classis vacva in Γ\Gamma continetvr.
  • Praemissa, in dedvctione de dedvctionibvs: versvs est vna ex hypothesibvs regvlae qvae demonstratvr.

Omnis effectvs hvivs lectionis metavariabilibvs envntiatvr et ideo de formvlis qvibvslibet valet: eivs demonstratio est schema, et si in ea qvaeqve metavariabilis in formvlam mvtatvr, alia demonstratio obtinetvr, qvia instantiae schematis axiomatis tales manent et qvisqve modvs ponens talis manet (idem de qvaqve applicatione regvlae novae valebit). Sic ex ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) seqvitvr ⊢(¬ψ→¬ψ)\vdash (\neg\psi \rightarrow \neg\psi), cvm ¬ψ\neg\psi loco φ\varphi. Hoc artificivm, effectvm ad formvlam complexiorem qvam envntiationis adhibere, est qvod in seqventibvs plvrimvm frvctvs fert.

Ab effectv ad regvlam

Artes hvivs lectionis ex praemissis fixis demonstrantvr, vt {(φ→ψ),(ψ→χ)}⊢(φ→χ)\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi); sed in mediis dedvctionibvs cvm aliis praemissis adhibentvr, vbi (φ→ψ)(\varphi \rightarrow \psi) et (ψ→χ)(\psi \rightarrow \chi) non svnt praemissae, sed formvlae iam dedvctae. Lemma seqvens, conseqventia directa monotoniae et sectionis, hvnc vsvm semel in perpetvvm permittit.

LemmaAb effectv ad regvlam

Si {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta, tvm, pro omni classe Γ\Gamma formvlarvm, ex Γ⊢α1\Gamma \vdash \alpha_{1}, …\ldots, Γ⊢αn\Gamma \vdash \alpha_{n} seqvitvr Γ⊢β\Gamma \vdash \beta. Praeterea ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots)).

Demonstratio

  1. Γ∪{α1,…,αn}⊢β\dato{mon}{\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta}

    Ex hypothesi, β\beta ex formvlis αi\alpha_{i} dedvcitvr. Cvm {α1,…,αn}\{\alpha_{1}, \ldots, \alpha_{n}\} in Γ∪{α1,…,αn}\Gamma \cup \{\alpha_{1}, \ldots, \alpha_{n}\} contineatvr, monotonia sinit Γ\Gamma praemissis addere.

  2. Γ⊢β\Gamma \vdash \resaltar{\beta}

    Si praeterea qvaeqve αi\alpha_{i} ex Γ\Gamma dedvcitvr, sectio praemissas additas tollit.

  3. ⊢(α1→(α2→⋯(αn→β)⋯ ))\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))

    Ad formam theorematis, theorema dedvctionis, nn vices adhibitvm, praemissas ab vltima ad primam exonerat; qvaeqve applicatio praemissam exoneratam in antecedens implicationis convertit.

Inde seqvitvr qvamqve artem ex praemissis demonstratam tres species habere: ipsvm effectvm, theorema qvod praemissis eivs exoneratis obtinetvr et regvlam qvae svb qvavis Γ\Gamma adhibetvr. In dedvctione de dedvctionibvs, regvla invocatvr nomine artis et nvmeris versvvm ad qvos adhibetvr, vt SH(3,4)(3, 4), et lemma praestat illationem legitimam esse.