Ad argvmentvm transi
Topos Uranos
Latine

Firmitas et completvdo

Svmmarivm

Dvae vnitates priores in eadem lingva dvas notiones eivs qvod ex praemissis datis seqvitvr constitvervnt: dedvctionem, Γ⊢φ\Gamma \vdash \varphi, qvae catenas ex aliis catenis per axiomata et regvlas obtinet, non qvaerens qvid significent, et conseqventiam semanticam, Γ⊨φ\Gamma \models \varphi, qvae aestimationes percvrrit, nvllam dedvctionem scribens. Haec lectio demonstrat ambas notiones pro classibvs finitis praemissarvm congrvere. Firmitas (Γ⊢φ⇒Γ⊨φ\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi) per indvctionem fortem in nvmero versvvm dedvctionis demonstratvr, cvm casv pro qvoqve axiomate et pro qvaqve regvla, svbstitvtione dvplicis negationis comprehensa; ex ea seqvvntvr consistentia systematis et methodvs ad demonstrandvm formvlam non esse dedvcibilem. Conversvm, completvdo, novvm instrvmentvm reqvirit: lemma Kalmarii, qvod qvemqve versvm tabvlae veritatis formvlae in dedvctionem convertit et cvivs indvctio in complexitate vnvm tantvm casvm compositvm habet, qvia negatio conivncta vnicvs connectivvs primitivvs est; pro eo casv dvo lemmata de negatione conivncta in systemate dedvcvntvr. Deinde, hypothesibvs qvae versvm figvnt per demonstrationem per casvs singillatim eliminatis, obtinetvr omnem tavtologiam theorema esse et, dvobvs theorematibvs dedvctionis adhibitis, omnem conseqventiam classis finitae praemissarvm ex ea dedvcibilem esse. Inde seqvvntvr decidibilitas dedvcibilitatis ex praemissis finitis et congrventia aeqvivalentiae demonstrabilis cvm semantica. Casvs praemissarvm infinitarvm lectioni seqventi reservatvr, qvia theorema compactitatis reqvirit.

Proposita discendi

  1. Firmitatem et completvdinem in formis debili, finita et forti envntiare, eas vt proprietates independentes distingvere et exponere cvr argvmentvm qvod completvdinem «per firmitatem» obtinet circvlare sit.
  2. Firmitatem per indvctionem fortem in nvmero versvvm demonstrare, casv regvlae svbstitvtionis dvplicis negationis comprehenso, eaqve vti ad demonstrandam consistentiam systematis et non dedvcibilitatem formvlarvm certarvm.
  3. In systemate cvrsvs dvo lemmata de negatione conivncta dedvcere et, his adhibitis, lemma Kalmarii per indvctionem in complexitate demonstrare.
  4. Completvdinem debilem demonstrare hypothesibvs per demonstrationem per casvs eliminatis, et completvdinem pro classibvs finitis praemissarvm dvobvs theorematibvs dedvctionis adhibitis.
  5. Congrventiam dedvctionis et conseqventiae adhibere ad dedvcibilitates, aeqvivalentias demonstrabiles et consistentiam decernendas, et ad perpendendvm qvid accidat cvm regvlae systemati addvntvr.

Dvae qvaestiones de systemate cvrsvs

Vnitas de dedvctione systema cvrsvs statvit: schemata axiomatvm A1, A2 et A3 Łvkasiewiczii et dvas regvlas, modvm ponentem (MP) et svbstitvtionem dvplicis negationis (SDN), qvam lectio de qvattvor technicis dedvctionis addidit postqvam dvplicem negationem demonstravit. Dedvctio ex classe Γ\Gamma est series finita formvlarvm in qva qvaeqve est axioma, elementvm classis Γ\Gamma, effectvs modi ponentis dvabvs formvlis prioribvs adhibiti vel effectvs SDN vni priori adhibitae; Γ⊢φ\Gamma \vdash \varphi significat esse dedvctionem ex Γ\Gamma cvivs vltima formvla sit φ\varphi. Vnitas de semantica vicissim in lectione de conseqventia et aeqvivalentia semantica relationem Γ⊨φ\Gamma \models \varphi definivit: omnis aestimatio qvae omnibvs formvlis classis Γ\Gamma satisfacit, satisfacit φ\varphi. Ambae relationes eodem schemate scribvntvr, classe ad sinistram et formvla ad dextram; natvra tamen earvm contraria est. Prior syntactica est et exsistentialis: affirmat esse obiectvm finitvm, dedvctionem, qvod signvm post signvm examinari potest. Posterior semantica est et vniversalis: aliqvid de omnibvs aestimationibvs affirmat, qvae infinitae svnt et qvarvm qvaeqve infinitis variabilibvs valorem dat.

Dvae igitvr qvaestiones de systemate ponvntvr. Prima: nvm id solvm dedvcit qvod debet? Systema firmvm dicitvr si, pro omni classe Γ\Gamma et omni formvla φ\varphi, ex Γ⊢φ\Gamma \vdash \varphi seqvitvr Γ⊨φ\Gamma \models \varphi: qvod ex praemissis datis dedvcitvr vervm est svb omni aestimatione qvae praemissas veras reddit. Secvnda: nvm omne id dedvcit qvod debet? Systema completvm dicitvr si ex Γ⊨φ\Gamma \models \varphi seqvitvr Γ⊢φ\Gamma \vdash \varphi. Completvdo tres gradvs admittit, secvndvm classes praemissarvm qvas complectitvr:

  • completvdo debilis: si ⊨φ\models \varphi, tvm ⊢φ\vdash \varphi; omnis tavtologia theorema est;
  • completvdo pro classibvs finitis praemissarvm: si {γ1,…,γk}⊨φ\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi, tvm {γ1,…,γk}⊢φ\{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi;
  • completvdo fortis: si Γ⊨φ\Gamma \models \varphi, tvm Γ⊢φ\Gamma \vdash \varphi, pro classe Γ\Gamma qvacvmqve, etiam infinita.

Haec lectio firmitatem et dvos primos gradvs completvdinis demonstrat. Tertivs in lectione de theoremate compactitatis demonstratvr, et ratio hvivs partitionis in fine lectionis exponitvr.

Qvae non dicenda svnt

Hispanice firmitas interdvm «solvencia» appellatvr, vocabvlvm ad imitationem Anglici sovndness fictvm; vocabvlvm Hispanicvm est «corrección», eoqve cvrsvs Hispanice vtitvr. Neqve definienda est vt proprietas systematis «expressionem ex classe expressionvm inferendi», qvia haec est ipsa dedvcibilitas, non proprietas systematis. Errores tamen rei dvo alii svnt.

Primvs est affirmare firmitatem et completvdinem «alteram ex altera inferri». Proprietates independentes svnt: systema Łvkasiewiczii sine regvla SDN firmvm est (demonstratio hvivs lectionis id ostendit, vno casv dempto) nec completvm (lectio de systematibvs dedvctivis formalibvs tavtologiam exhibvit qvam non dedvcit); et systema qvod omnes formvlas vt axiomata admitteret completvm esset sine firmitate. Problema solvtvm 2 ambo exempla perpendit.

Secvndvs error gravior est, qvia argvmentvm circvlare pro demonstratione completvdinis venditat. Svmmatim dicit: si φ⊬ψ\varphi \nvdash \psi, tvm per theorema dedvctionis ⊬(φ→ψ)\nvdash (\varphi \rightarrow \psi); «per firmitatem» ⊭(φ→ψ)\not\models (\varphi \rightarrow \psi); et per theorema dedvctionis semanticvm φ⊭ψ\varphi \not\models \psi. Atqvi firmitas affirmat qvod dedvcibile est validvm esse, et eivs contrapositio qvod validvm non est dedvcibile non esse:

⊢χ  ⇒  ⊨χ,⊭χ  ⇒  ⊬χ\vdash \chi \;\Rightarrow\; \models \chi, \qquad \not\models \chi \;\Rightarrow\; \nvdash \chi

Illatio argvmenti in contrariam partem procedit, a ⊬χ\nvdash \chi ad ⊭χ\not\models \chi, et haec est contrapositio propositionis ⊨χ⇒⊢χ\models \chi \Rightarrow \vdash \chi, id est completvdinis debilis. Si ita est, argvmentvm praesvmit qvod demonstrare vvlt. Inde seqvitvr completvdinem non «modo simplici inferri»: est altissimvm cvrsvs effectvm, eivsqve demonstratio maiorem partem hvivs lectionis occvpat. Deniqve parvm accvratvm est completvdinem compendio dicere «omnes expressiones veras demonstrationem habere»; demonstrationem habet qvod validvm est, vervm svb omni aestimatione, non qvod svb aliqva vervm est: variabilis v1v_{1} svb mvltis aestimationibvs vera est nec theorema est.