Ad argvmentvm transi
Topos Uranos
Latine

Artes logicae classicae

Svmmarivm

Qvi in mathematica ratiocinatvr conivnctiones et disivnctiones introdvcit et eliminat, tertivm non datvr invocat, contradictoria reicit, casvs distingvit et ad absvrdvm redvcit, fere semper non animadvertens se id facere. Haec lectio demonstrat omnes eas artes esse regvlas derivatas systematis cvrsvs, easqve demonstrat ea forma qva adhibentvr: cvm classe Γ\Gamma praemissarvm qvae per totam dedvctionem manet. Primvm in memoriam revocat omnem regvlam iam demonstratam valere intra contextvm Γ\Gamma; deinde demonstrat 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, primvm cvm formvla eivsqve negatione, deinde cvm disivnctione qvavis. Problemata artes ad leges classicas adhibent, vt legem Peircii et dilemmata, et ostendvnt cvr non svfficiat eas sine praemissis demonstrare.

Proposita discendi

  1. Ad versvs formae Γ⊢φ\Gamma \vdash \varphi regvlas et aeqvivalentias antea demonstratas adhibere, gradvm per monotoniam et sectionem ivstificando.
  2. Regvlas introdvctionis et eliminationis disivnctionis et conivnctionis cvm praemissis demonstrare, abbreviationes statvtas explicando tantvm vbi licet.
  3. Tertivm non datvr et principivm non contradictionis dedvcere, et in qvoqve gradv distingvere qvid sit definitio et qvid theorema.
  4. Ex falso qvodlibet, redvctionem ad absvrdvm dvabvs formis et demonstrationem per casvs cvm praemissis demonstrare, et explicare cvr versiones sine praemissis non svfficiant.
  5. Dedvctiones legvm classicarvm (Peircii, exportationis, dilemmatvm) has artes combinando constrvere, et dedvcibilitatem formvlae cvm inconsistentia classis praemissarvm conferre.

Regvlae intra contextvm

In lectione de systematibvs dedvctivis formalibvs systema Łvkasiewiczii constitvtvm est: schemata axiomatvm A1, A2 et A3, regvla modi ponentis (MP) et notio dedvctionis ex classe Γ\Gamma praemissarvm, cvm primis eivs proprietatibvs: reflexivitate (Refl: si φ∈Γ\varphi \in \Gamma, tvm Γ⊢φ\Gamma \vdash \varphi), monotonia (Mon: si Γ⊆Δ\Gamma \subseteq \Delta et Γ⊢φ\Gamma \vdash \varphi, tvm Δ⊢φ\Delta \vdash \varphi), sectione (Sect), modo ponente inter dedvctiones (si Γ⊢φ\Gamma \vdash \varphi et Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), tvm Γ⊢ψ\Gamma \vdash \psi, qvi etiam vt MP citatvr), theoremate dedvctionis (TD: si Γ∪{φ}⊢ψ\Gamma \cup \{\varphi\} \vdash \psi, tvm Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi)) eivsqve converso (CTD). Lectiones de qvattvor artibvs dedvctionis et de symmetriis connectivorvm addidervnt syllogismvm hypotheticvm (SH), permvtationem praemissarvm (PP), dvplicem negationem (DN), contrapositionem (CP) tribvs formis, svbstitvtionem aeqvivalentivm (Svbst), symmetrias (Sym) et formas aeqvivalentes disivnctionis et conivnctionis. Prior earvm lectionvm, dvplici negatione demonstrata, systema cvrsvs praeterea secvnda regvla primitiva complevit, svbstitvtione dvplicis negationis (SDN): si χ′\chi' oritvr ex χ\chi occvrrentia svbformvlae θ\theta per ¬¬θ\neg\neg\theta svbstitvta, vel occvrrentia formvlae ¬¬θ\neg\neg\theta per θ\theta, ex χ\chi infertvr χ′\chi'. Deinceps ⊢\vdash ad id systema refertvr (A1 ad A3, MP et SDN), in qvo reflexivitas, monotonia, sectio, theorema dedvctionis eivsqve conversvm valere pergvnt; artes hvivs lectionis svnt regvlae ex eo derivatae, qvamqvam nvlla earvm demonstratio SDN directe invocat: regvla agit per formas aeqvivalentes et svbstitvtionem aeqvivalentivm, qvas lectio de symmetriis ea adhibita demonstravit.

Atqvi in mathematica nemo sine praemissis ratiocinatvr: ratiocinatio procedit ex axiomatibvs qvibvsdam, ex hypothesibvs theorematis et ex eo qvod ad casvm aliqvem discvtiendvm svppositvm est. Qvod si ita est, ars ratiocinandi vtilis est tantvm si cvm classe Γ\Gamma praemissarvm envntiatvr qvae de versv in versvm trahitvr. Inde seqvitvr qvamqve regvlam hvivs lectionis pro qvavis Γ\Gamma envntiari et demonstrari; casvs sine praemissis est casvs particvlaris Γ=∅\Gamma = \emptyset, non contra.

Demonstrationes svnt dedvctiones de dedvctionibvs: qvisqve versvs affirmat aliqvid ex classe dedvcibile esse, Γ⊢φ\Gamma \vdash \varphi, eivsqve ivstificatio ad versvs priores remittit. In eis «Praemissa» designat versvs qvos envntiatio regvlae pro svppositis habet, et nomen axiomatis (A1, A3) vel theorematis iam demonstrati (vt Id, theorema ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi)) designat versvm Γ⊢φ\Gamma \vdash \varphi in qvo φ\varphi est instantia eivs schematis vel eivs theorematis, ex qvavis classe dedvcibilis.

Lectio de qvattvor artibvs dedvctionis per monotoniam et sectionem lemma «ab effectv ad regvlam» demonstravit, qvod hvnc modvm laborandi possibilem reddit: si {α1,…,αn}⊢β\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta et Γ⊢αi\Gamma \vdash \alpha_{i} pro qvoqve ii, tvm Γ⊢β\Gamma \vdash \beta. Cvm n=1n = 1, in vtroqve sensv aeqvivalentiae α⊣⊢α′\alpha \dashv\vdash \alpha' adhibitvm, dicit Γ⊢α\Gamma \vdash \alpha si et solvm si Γ⊢α′\Gamma \vdash \alpha'. Ergo omnis regvla iam demonstrata et omnis aeqvivalentia iam demonstrata ad versvs dedvctionis cvm praemissis adhibentvr: si versvs dicit Γ⊢(φ→ψ)\Gamma \vdash (\varphi \rightarrow \psi), contrapositio sinit infra scribere Γ⊢(¬ψ→¬φ)\Gamma \vdash (\neg\psi \rightarrow \neg\varphi) evmqve per «CP» et nvmervm versvs ivstificare. Pro dvabvs formis aeqvivalentibvs lectionis de symmetriis, qvibvs sine intermissione vtemvr, scribitvr «Aeq»:

(φ∨ψ)⊣⊢(¬φ→ψ)(φ∧ψ)⊣⊢¬(φ→¬ψ)(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi) \qquad (\varphi \wedge \psi) \dashv\vdash \neg(\varphi \rightarrow \neg\psi)

Instandvm est primam harvm aeqvivalentiarvm non esse definitionem; secvnda, vt lectio de symmetriis ostendit, identitas catenarvm est, sed vna cvm prima vt Aeq citatvr. Ex definitione (φ∨ψ)(\varphi \vee \psi) est ¬(φ↓ψ)\neg(\varphi \downarrow \psi) et (¬φ→ψ)(\neg\varphi \rightarrow \psi) est (¬¬φ∨ψ)(\neg\neg\varphi \vee \psi), qvae catenae diversae svnt; alteram pro altera «ex definitione implicationis» legere error est qvem haec lectio vitat. «Def» contra reservatvr ad eandem catenam alio nomine scribendam, vt cvm (φ→ψ)(\varphi \rightarrow \psi) vt (¬φ∨ψ)(\neg\varphi \vee \psi) legitvr.