Ad argvmentvm transi
Topos Uranos
Latine

Systemata dedvctiva formalia

Svmmarivm

Haec lectio lingvam vnitatis svperioris in instrvmentvm demonstrandi convertit. Definit qvid sit systema dedvctivvm formale (lingva, schemata qvaedam axiomatvm et regvlae qvaedam inferendi) et primvm e dvobvs qvibvs cvrsvs vtitvr proponit, systema Łvkasiewiczii: tria schemata axiomatvm et modvm ponentem vt regvlam vnicam. Accvrate definit dedvctionem ex classe praemissarvm, theorema et relationem Γ⊢φ\Gamma \vdash \varphi, dedvcit ⊢(φ→φ)\vdash (\varphi \rightarrow \varphi) qvinqve versibvs et proprietates strvctvrales dedvctionis demonstrat: reflexivitatem, monotoniam, modvm ponentem inter dedvctiones, sectionem et finitatem. Deinde per indvctionem fortem secvndvm nvmervm versvvm theorema dedvctionis eivsqve conversvm demonstrat, qvae dedvctionibvs de dedvctionibvs ratiocinari sinvnt, et aeqvivalentiam demonstrabilem definit. Postremo, nvllis valoribvs veritatis adhibitis, limitem illivs systematis statvit in lingva cvivs vnicvm connectivvm est negatio conivncta: nota valorvm 00 et 11, per recvrsionem in formvlis compvtata, qvam axiomata Łvkasiewiczii et modvs ponens servant, probat qvasdam formvlas qvae dedvci deberent non dedvci, ac ne a (v1↓v2)(v_{1} \downarrow v_{2}) qvidem ad (¬¬v1↓v2)(\neg\neg v_{1} \downarrow v_{2}) transiri. Vnde seqvitvr necessitas alterivs regvlae, svbstitvtionis dvplicis negationis, qva lectio seqvens systema complet.

Proposita discendi

  1. Instantias schematvm A1, A2 et A3 agnoscere et decernere vtrvm series formvlarvm dedvctio ex classe praemissarvm sit.
  2. Dedvctiones in systemate Łvkasiewiczii constrvere, cvm axiomatibvs, praemissis et modo ponente, et dedvctiones de dedvctionibvs cvm reflexivitate, monotonia, sectione, theoremate dedvctionis eivsqve converso.
  3. Proprietates strvctvrales dedvctionis et theorema dedvctionis per indvctionem fortem secvndvm nvmervm versvvm demonstrare.
  4. Aeqvivalentias demonstrabiles statvere et adhibere aeqvivalentiam demonstrabilem reflexivam, symmetricam et transitivam esse.
  5. Demonstrare formvlam non esse dedvcibilem per notam qvam axiomata et modvs ponens servant, eaqve exponere limitem systematis Łvkasiewiczii in lingva vnivs connectivi et cvr altera regvla opvs sit.

Qvid sit systema dedvctivvm formale

Vnitas svperior lingvam constrvxit: decrevit qvae catenae circvlorvm et discorvm formvlae sint, nec qvicqvam amplivs. Atqvi lingva per se nihil affirmat nec demonstrat; ad demonstrandvm praeterea opvs est initio et modo progrediendi. Systema dedvctivvm formale igitvr tribvs rebvs constat: lingva formali, qvae formvlas statvit; classe axiomatvm, formvlarvm qvae sine demonstratione admittvntvr; et classe regvlarvm inferendi, qvae dicvnt qvae formvla ex aliis iam scriptis scribi possit. Qvod maximi momenti est, haec tria mere syntactica svnt: ad probandvm formvlam axioma esse, vel regvlam recte adhibitam esse, satis est catenas inspicere, non qvaerendo qvid significent. Qvod si ita est, demonstratio in systemate formali mechanice examinari potest, signo post signvm, et in hac possibilitate tota eivs vis posita est.

Ab initio monendvm est axioma hic non esse «veritatem per se evidentem», vt in antiqvo verbi vsv, sed formvlam vt initivm electam. Vtrvm electio recta sit (vtrvm axiomata vera sint sensv qvem semantica definiet, et vtrvm svfficiant ad omnia dedvcenda qvae dedvci debent) qvaestio est de systemate, cvi theorematibvs de eo respondetvr, non intvitione: vnitas de metatheoria ei respondet, et vltimvm capvt hvivs lectionis ostendit qvaestionem non esse otiosam.

Schemata axiomatvm et instantiae

Systemata logicae propositionalis axiomata sva non singillatim envntiant, qvia infinita svnt, sed per schemata: expressiones metalingvae cvm metavariabilibvs scriptas, vt (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)). Schema non est formvla; est forma fvsoria. Instantia schematis est formvla qvae oritvr cvm qvaeqve metavariabilis in formvlam mvtatvr, modo vniformi: omnes occvrrentiae eivsdem metavariabilis in eandem formvlam mvtantvr, qvamqvam metavariabiles diversae eandem formvlam vel formvlas diversas recipere possvnt.

ExemplvmInstantiae schematis

Cvm φ:=v1\varphi := v_{1} et ψ:=¬v2\psi := \neg v_{2}, schema (φ→(ψ→φ))(\varphi \rightarrow (\psi \rightarrow \varphi)) instantiam (v1→(¬v2→v1))(v_{1} \rightarrow (\neg v_{2} \rightarrow v_{1})) dat; cvm φ:=(v1↓v2)\varphi := (v_{1} \downarrow v_{2}) et ψ:=(v1↓v2)\psi := (v_{1} \downarrow v_{2}), dat ((v1↓v2)→((v1↓v2)→(v1↓v2)))((v_{1} \downarrow v_{2}) \rightarrow ((v_{1} \downarrow v_{2}) \rightarrow (v_{1} \downarrow v_{2}))), qvia nihil obstat qvominvs dvae metavariabiles eandem formvlam recipiant. Contra, (v1→(v2→v3))(v_{1} \rightarrow (v_{2} \rightarrow v_{3})) non est instantia illivs schematis: prima et vltima occvrrentia ipsivs φ\varphi formvlas diversas reciperent, nec mvtatio vniformis esset. Qvaeqve instantia, abbreviationibvs explicatis, catena circvlorvm et discorvm est; schema contra in sola metalingva vivit.