Ad argvmentvm transi
Topos Uranos
Latine

Formalizatio lingvae natvralis

Svmmarivm

Haec lectio docet qvomodo envntiata et argvmentationes sermonis natvralis in lingvam logicae propositionalis vertantvr. Primvm conventionem accvratam statvit: litterae pp, qq, rr, ss et tt qvinqve variabiles certas lingvae fvndamentalis nominant, litterae avtem Graecae metavariabiles manent; et formalizatio semper a lexico incipit qvod cviqve envntiato atomico svam variabilem attribvit. Deinde lexicon connectivorvm exponit, cvm lectione informali vnivscvivsqve ex lectione negationis conivnctae dedvcta, eorvmqve svbtilitates: «sed» et «qvamqvam», disivnctionem inclvsivam et exclvsivam, «nec… nec», qvod ipsvm est connectivvm primitivvm cvrsvs, «solvm si», «nisi», condiciones necessarias et svfficientes. Ambitvm connectivorvm investigat et per legibilitatem vnicam demonstrat dvas diversas partivm compositiones formvlas diversas efficere; longitvdinem abbreviationvm explicatarvm compvtat, qva decerni potest qvando dvae formalizationes eadem catena sint. Implicationem materialem eivsqve paradoxa apparentia examinat, ea qvae logica propositionalis exprimere non potest (qvantificatores, tempvs, cavsam, modalitatem) et, postremo, formalizationem argvmentationvm integrarvm, qvas vnitates seqventes dedvctioni et semanticae svbicient.

Proposita discendi

  1. Envntiata sermonis natvralis cvm lexico expresso formalizare, connectiva eorvmqve ambitvm eligendo, et electionem ivstificare cvm envntiatvm ambigvvm est.
  2. Abbreviationes vsqve ad catenam circvlorvm et discorvm, vel vsqve ad scriptvram sola negatione conivncta, explicare, vt decernatvr nvm dvae formalizationes eadem formvla sint.
  3. Implicationem materialem a «si… tvm» sermonis distingvere et indicare qvid formalizatio propositionalis amittat: qvantificatores, tempvs, cavsam et modalitatem.
  4. Argvmentationem integram vt classem praemissarvm et conclvsionem formalizare.

Ab envntiato ad formvlam

Lectio de lingva logicae propositionalis lingvam sine significatione constrvxit: catenas circvlorvm et discorvm, regvlam formationis et aliqvot abbreviationes. Lectio de indvctione in formvlis demonstravit qvamqve formvlam vno tantvm modo legi. Atqvi ea lingva ad aliqvid constrvcta est: ad formam envntiatorvm repraesentandam qvibvs in vita cotidiana, in scientiis, in ivre et in mathematica ratiocinamvr, ita vt rectitvdo ratiocinationis in ipsa forma, materia neglecta, investigari possit. Haec lectio pontem inter vtrvmqve mvndvm facit. Non est pons mechanicvs: sermo natvralis dives est, ambigvvs et a contextv pendens, lingva formalis pavper, accvrata et rigida. Ex qvo seqvitvr formalizare esse interpretari, et omnem formalizationem ivstificandam esse.

Envntiatvm, sensv hvivs lectionis, est sententia declarativa qvae in svo contextv vera avt falsa est: «Aqva ad libramentvm maris centvm gradibvs fervet», «Tvllia sero advenit», «77 nvmervs primvs est». Interrogationes, ivssa et optationes («Advenitne Tvllia?», «Clavde ianvam», «Vtinam plvat») envntiata non svnt. Envntiatvm est compositvm cvm alia envntiata continet particvlis ivncta vt «non», «et», «vel», «si… tvm»; est atomicvm cvm hoc modo non dividitvr. Logica propositionalis interiora envntiatorvm atomicorvm non analysat: ei «Tvllia sero advenit» frvstvm individvvm est, qvod tantvm vervm avt falsvm esse potest.

Conventio litterarvm

Formvlae lingvae fvndamentalis svnt catenae circvlorvm et discorvm; variabilis nn-esima est vn=∘n∙v_n = \sigO^{n}\sigI, id est nn circvli qvos discvs seqvitvr. Tales catenas scribere tam tvtvm est qvam molestvm, et ad formalizandvm expedit nomina brevia habere. Conventionem seqventem adhibemvs, qvae in hac lectione et in reliqvo cvrsv valet, nisi aliter expresse monetvr:

p:=v1=∘∙,q:=v2=∘∘∙,r:=v3=∘∘∘∙,s:=v4,t:=v5p := v_1 = \sigO\sigI, \quad q := v_2 = \sigO\sigO\sigI, \quad r := v_3 = \sigO\sigO\sigO\sigI, \quad s := v_4, \quad t := v_5

Qvod si ita est, litterae Latinae pp, qq, rr, ss et tt svnt nomina qvinqve variabilivm certarvm, eodem modo qvo 77 nomen est nvmeri certi: pp non variat, sed semper catenam ∘∙\sigO\sigI designat. Litterae Graecae φ\varphi, ψ\psi, χ\chi et θ\theta, contra, metavariabiles manent, vt in lectione de lingva: formvlas qvaslibet designant, et envntiatvm iis scriptvm, vt (φ↓ψ)(\varphi \downarrow \psi), schema est qvod infinitas formvlas complectitvr. Ex qvo seqvitvr discrimen qvod magni refert: (p↓q)(p \downarrow q) vna formvla est, catena ∙∘∙∘∘∙\sigI\sigO\sigI\sigO\sigO\sigI; (φ↓ψ)(\varphi \downarrow \psi) forma est formvlarvm, cvivs casvs svnt (p↓q)(p \downarrow q), (p↓p)(p \downarrow p) et (q↓(p↓r))(q \downarrow (p \downarrow r)). Qvidam libri pp et qq vt metavariabiles adhibent; hic non, qvia formalizando opvs est vt dvae litterae diversae certo variabiles diversas designent, et metavariabilis hanc fidem non praestat: nihil vetat qvominvs φ\varphi et ψ\psi eandem formvlam designent.

Lexicon formalizationis

Envntiatvm formalizare tribvs operationibvs constat: envntiata eivs atomica agnoscere, cviqve variabilem attribvere et envntiatvm compositvm connectivis restitvere. Attribvtio secvndae operationis lexicon formalizationis appellatvr, et semper declaranda est, qvia sine ea formvla nihil dicit. Lexicon dvabvs regvlis paret: idem envntiatvm atomicvm semper eandem variabilem accipit, et envntiata atomica diversa variabiles diversas accipivnt. Prima praestat vt formvla repetitiones textvs servet; secvnda, ne identitates fingat qvas textvs non affirmat.

ExemplvmLexicon

Sit envntiatvm «Si temperatvra crescit et pressio non mvtatvr, volvmen gasis avgetvr». Eivs envntiata atomica tria svnt, et lexicon hoc est: pp, «temperatvra crescit»; qq, «pressio mvtatvr»; rr, «volvmen gasis avgetvr». Notandvm est atomicvm esse «pressio mvtatvr», non «pressio non mvtatvr»: negatio connectivvm est, et lexicon sola envntiata sine connectivis recipit. Formalizatio est ((p∧¬q)→r)((p \wedge \neg q) \rightarrow r). Si textvs postea diceret «pressio mvtatvr», itervm qq scriberetvr, non variabilis nova.