Ad argvmentvm transi
Topos Uranos
Latine

Lingva: introdvctio

Svmmarivm

Haec lectio primam cvrsvs vnitatem aperit, lingvae logicae propositionalis dicatam. Qvattvor eivs lectiones et filvm qvo conivngvntvr exponit, a distinctione inter validitatem et veritatem vsqve ad formalizationem argvmentationvm Latinarvm; vnitatem in toto cvrsvs itinere collocat, qvod a lingva ad dedvctionem, ad semanticam et ad metatheoriam progreditvr, et explicat cvr syntaxis ceteris tribvs praecedere debeat; electionem lingvae dvorvm tantvm signorvm, circvli et disci, cvm vnica regvla formationis ivstificat; pavca qvae pro cognitis habentvr definit, scilicet attente legere et arithmeticam elementarem; qvaestionem qvam vnitas solvit proponit, scilicet ita scribere vt qvaeqve expressio vnam tantvm lectionem habeat, idqve pro infinitis formvlis demonstrare; et consilia dat ad eam discendam.

Proposita discendi

  1. Seriem rervm vnitatis describere et explicare qvid qvaeqve lectio seqventi afferat.
  2. Vnitatem in itinere cvrsvs collocare (lingva, dedvctio, semantica et metatheoria) et explicare cvr syntaxis ante ceteras tres partes discatvr.
  3. Exemplo explicare cvr notatio, qvae connectivvm inter argvmenta sva ponit et parenthesibvs caret, ambigva sit, et cvr lingva circvlorvm et discorvm non sit.
  4. Pavca qvae vnitas svpponit agnoscere et stvdivm eivs ordinare, svi ipsivs exploratione initiali vt initio svmpta.

Probatio initialis

Anteqvam vnitas percvrritvr, initivm ipsvm metiri expedit. Haec probatio est svi ipsivs exploratio: nvllo gradv notatvr, et solvm eivs propositvm est stvdivm dirigere. Vndecim eivs qvaestiones ordine qvattvor vnitatis lectiones attingvnt: tres primam, tres secvndam, dvae tertiam et tres qvartam. Qvi nvmqvam logicam didicit omnes recte solvere non debet exspectare, neqve id refert: qvodqve responsvm, rectvm sive falsvm, rem explicat et lectionem nominat qvae eam tractat. Eaedem facvltates in fine itervm metivntvr, in lectione synthesis; cvm haec sit prima vnitas cvrsvs qvi nihil ad ingrediendvm postvlat, nvllae svnt qvaestiones de vnitatibvs prioribvs.

Probatio initialis

Antequam vnitatem incipias, pvnctvm vnde proficisceris metire. Brevis est sui ipsivs probatio: non aestimatvr, et eivs exitvs in solo tvo navigatro servatvr.

  1. Qvaestio 1Argvmentatio valida est, et conclvsio eivs falsa. Qvid de praemissis eivs affirmari potest?

  2. Qvaestio 2De qva re loqvitvr sententia «“Roma” qvattvor litteras habet», et estne vera?

  3. Qvaestio 3De elencho nvmerorvm 44, 66, 77 affirmatvr: «omnes nvmeri elenchi primi non svnt». Qvid de hac sententia dici potest?

  4. Qvaestio 4Qvot catenae diversae longitvdinis 44 dvobvs signis ∘\sigO et ∙\sigI scribi possvnt?

  5. Qvaestio 5Si u=∘∙u = \sigO\sigI et w=∙w = \sigI, qvae catena est concatenatio uw\cadena{uw}, qvae in eo consistit vt ww post uu scribatvr?

  6. Qvaestio 6In lingva cvrsvs variabiles svnt catenae ∘∙\sigO\sigI, ∘∘∙\sigO\sigO\sigI, ∘∘∘∙\sigO\sigO\sigO\sigI, et sic deinceps, et vnica regvla dicit, si φ\varphi et ψ\psi formvlae svnt, etiam ∙φψ\sigI\varphi\psi formvlam esse. Qvae ex catenis seqventibvs formvla est?

  7. Qvaestio 7Aliqvis demonstrat, pro omni nvmero natvrali kk, si 3k3^{k} par est, etiam 3k+13^{k + 1} parem esse. Qvid inde conclvdere potest?

  8. Qvaestio 8Vt demonstretvr omnes formvlas lingvae circvlorvm et discorvm proprietatem qvandam habere, qvid demonstrare svfficit?

  9. Qvaestio 9Lexico pp, «plvit», et qq, «certamen differtvr», qvomodo formalizatvr «certamen differtvr solvm si plvit»?

  10. Qvaestio 10Lexico pp, «plvit», et qq, «friget», qvae formvla ad litteram constrvctionem «nec plvit nec friget» seqvitvr?

  11. Qvaestio 11Qvibvs casibvs falsa est implicatio (p→q)(p \rightarrow q) cvrsvs, qvae implicatio materialis appellatvr?

Qvae vnitas continet

Haec vnitas ante omnia primo cvrsvs proposito servit, lingvam obiecti a metalingva distingvere et regvlis formationis decernere vtrvm catena formvla sit; servit etiam secvndo, envntiata et argvmentationes lingvae natvralis formalizare, et qvartvm praeparat, metatheoremata per indvctionem demonstrare, qvod cvrsvm vsqve ad vltimam eivs vnitatem comitabitvr. Finis eivs est vt qvi eam absolverit sciat qvid logica investiget, lingvam formalem svmmo rigore constrvctam in promptv habeat, proprietates omnivm eivs formvlarvm demonstrare sciat et envntiata argvmentationesqve Latinas in eam vertere possit, sciens qvid conversio servet et qvid amittat. Qvattvor eivs lectiones catenam efficivnt in qva qvaeqve prioribvs innititvr.

  1. Qvid est logica mathematica. Obiectvm disciplinae definit: non veritatem envntiatorvm singvlarivm, sed validitatem, relationem inter praemissas et conclvsionem qvae praestat vt veritas illarvm ad hanc transeat. Validitatem a veritate distingvit, ostendit cvr lingva natvralis, ambigva et de se ipsa loqvi potens, ad eam investigandam non svfficiat, et distinctionem inter lingvam obiecti et metalingvam statvit. Paradoxa mendacis, Berrianvm, tonsoris et Rvssellianvm cvm hypothesibvs svis explicatis examinat, et tabvla cvrsvs finitvr.
  2. Lingva logicae propositionalis. Ea qvae de classibvs et de catenis signorvm necessaria svnt docet, catenas nvmerat qvae dvobvs signis scribi possvnt et lingvam fvndamentalem constrvit: infinitas variabiles circvlis et discis scriptas, vnicam regvlam formationis et clavsvlam clavsvrae, ex qva principivm dedvcitvr ad proprietates omnivm formvlarvm demonstrandas. Rationem decernendi tradit vtrvm catena formvla sit et svper lingvam fvndamentalem metalingvam constrvit qva deinceps vtemvr: metavariabiles, negationem conivnctam cvm parenthesibvs scriptam et abbreviationes statvtas ceterorvm connectivorvm.
  3. Indvctio in nvmeris natvralibvs et in formvlis. Indvctionem in nvmeris natvralibvs docet, simplicem et fortem, eamqve ad formvlas transfert. Ea lemma ponderis demonstrat et, ex eo, theorema legibilitatis vnicae, qvod lectio svperior envntiaverat: qvaeqve formvla composita vno tantvm modo dividitvr. Legibilitas vnica deniqve definitiones per recvrsionem in formvlis (longitvdinem, svbformvlas, profvnditatem) et svbstitvtionem svbformvlae per aliam legitimas reddit.
  4. Formalizatio lingvae natvralis. Pontem inter lingvam Latinam et lingvam formalem iacit: lexicon formalizationis, lectionem cvivsqve connectivi ex lectione connectivi primitivi dedvctam, svbtilitates vocvm «sed», «solvm si» et «nisi», ambitvm connectivorvm, implicationem materialem et ea qvae logica propositionalis exprimere non potest. Finitvr argvmentationibvs integris formalizatis vt classe praemissarvm et conclvsione, qvas vnitates seqventes dedvctioni et semanticae svbicient.

Vnitas lectione synthesis et provocationvm finitvr, qvae parta in catenam dedvctivam colligit, in probatione finali facvltates probationis initialis repetit et provocationes proponit qvae plvres lectiones conivngvnt.

Locvs vnitatis in cvrsv

Cvrsvs pro simplicissima logicae lingva totvm iter theoriae logicae percvrrit, idqve qvattvor partibvs, qvae svnt qvattvor eivs vnitates materiae. Prima, haec, lingvam statvit. Secvnda, dedvctio, definit qvid sit formvlam φ\varphi ex classe formvlarvm Γ\Gamma per axiomata et regvlas inferendi obtineri, qvod scribetvr Γ⊢φ\Gamma \vdash \varphi; est facies syntactica validitatis, in qva signa tractantvr nvlla significationis ratione habita. Tertia, semantica, cviqve formvlae valorem veritatis in qvaqve aestimatione tribvit et definit qvid sit φ\varphi conseqventiam esse classis Γ\Gamma, qvod scribetvr Γ⊨φ\Gamma \models \varphi; est facies semantica validitatis. Qvarta, metatheoria, demonstrat ambas facies congrvere: firmitas dicit omne dedvcibile conseqventiam esse, completvdo avtem omnem conseqventiam dedvcibilem esse.

Qvae si ita svnt, syntaxis non est prooemivm qvod contrahi possit, sed condicio ceterarvm trivm partivm. Dedvctio series formvlarvm est, et vt decernatvr vtrvm series sit dedvctio, sine haesitatione sciendvm est qvae catenae formvlae sint et qvomodo dividantvr; aestimatio a variabilibvs ad omnes formvlas per recvrsionem extenditvr, et recvrsio cviqve formvlae vnvm valorem dat solvm si qvaeqve formvla vno tantvm modo legitvr; theoremata metatheoriae per indvctionem demonstrantvr, secvndvm complexitatem formvlarvm vel secvndvm longitvdinem dedvctionvm. Ex qvo ordo vnitatis seqvitvr: primvm, qvid investigare velimvs et cvr lingva formalis necessaria sit; deinde, lingva ipsa; postea, instrvmentvm ad aliqvid de omnibvs eivs formvlis demonstrandvm, qvo legibilitas vnica probatvr; postremo, pons ad argvmentationes lingvae Latinae, qvae svnt cavsa omnivm qvae praecedvnt.

Cvr lingva circvlorvm et discorvm

Lingva cvrsvs alphabetvm dvorvm tantvm signorvm habet, circvli ∘\sigO et disci ∙\sigI, et vnicam regvlam formationis: si φ\varphi et ψ\psi formvlae svnt, etiam ∙φψ\sigI\varphi\psi formvla est. Variabilis nn-ta est catena nn circvlorvm qvos discvs seqvitvr, vn=∘n∙v_{n} = \sigO^{n}\sigI. Prima specie electio mira est, qvia formvlae sic scriptae difficiles lectv svnt. Qvattvor tamen certas rationes habet.

Prima est dvo signa svfficere ad infinitas variabiles scribendas sine alphabeto finito relicto, ita vt omnis formvla sit, ad litteram, catena finita signorvm ex classe dvorvm elementorvm, et qvaestiones de lingva sint qvaestiones de catenis, qvae nvmerari et comparari possvnt. Secvnda est vnicam regvlam vnvm tantvm casvm in qvaqve demonstratione per indvctionem relinqvere: qvod pro variabilibvs et pro ∙φψ\sigI\varphi\psi probatvr, pro omnibvs formvlis probatvm est, sine casv pro qvoqve connectivo. Tertia est regvlam connectivvm ante dvo argvmenta sva ponere, vt in notatione qvam Ian Łvkasiewicz decennio tertio saecvli vicesimi proposvit, ideoqve parenthesibvs non egere: legibilitas vnica argvmento vnivs paginae demonstratvr, qvod cviqve variabili pondvs +1+1 et cviqve disco connectenti pondvs −1-1 tribvit. Qvarta est vnicvm connectivvm, negationem conivnctam, «nec φ\varphi nec ψ\psi», ad omnia cetera exprimenda svfficere, vt Charles Sanders Peirce circa annvm 1880 animadvertit et Henry Sheffer anno 1913 edidit, et vt vnitas de semantica demonstrabit; ita vt oeconomia lingvae nihil eorvm qvae logica propositionalis dicere potest sacrificet.

Iam vero pretivm hvivs oeconomiae est legibilitas, et vnitas id in metalingva solvit: nemo cotidie catenas circvlorvm et discorvm scribet, sed earvm nomina, (φ↓ψ)(\varphi \downarrow \psi), ¬φ\neg\varphi, (φ→ψ)(\varphi \rightarrow \psi), semel tantvm definita et qvovis tempore vsqve ad catenam qvam designant explicabilia. Itaqve cvrsvs dvobvs gradibvs simvl operatvr: lingva fvndamentali minima, de qva demonstratvr, et notatione commoda, qva scribitvr; et distinctio inter lingvam obiecti et metalingvam, qvam prima lectio introdvcit, ea est qvae efficit ne confvndantvr.

Qvae pro cognitis habentvr

Vnitas a paene nihilo proficiscitvr. Non svpponit logicam didicisse, nec theoriam classivm novisse, nec vmqvam theorema demonstravisse: qvae de classibvs adhibet secvnda lectio docet, et qvae de indvctione, tertia. Dvo tantvm svpponit. Primvm, attente legere: in lingva formali signvm additvm vel omissvm catenam mvtat, et ordo verborvm definitionis tanti refert qvanti verba ipsa. Altervm, arithmeticam elementarem nvmerorvm natvralivm, qvi in hoc cvrsv svnt 1,2,3,…1, 2, 3, \ldots: addere et mvltiplicare, potestates nvmeri 22 compvtare, pares ab imparibvs distingvere et nvmervm primvm agnoscere.

Qvi adivmentvm amplivs ad indvctionem desiderat, lectiones de axiomatibvs Peani et de svmmis et indvctione cvrsvs Algebra et Geometria I consvlere potest; qvod necessarivm non est, qvia tertia hvivs vnitatis lectio indvctionem ab ipsa eivs envntiatione docet.

Qvaestio qvam vnitas solvit

Logica validitatem investigat, et validitas ex forma argvmentationvm pendet. Sed vt de forma cvm rigore loqvamvr, oportet qvamqve expressionem vnam tantvm formam habere, et lingva natvralis id non praestat: «bis tres et qvattvor» potest esse 1010 avt 1414, provt conivngitvr. Hoc dvas qvaestiones movet, qvae svnt vnitatis. Prima est lingvam constrvere in qva qvaeqve expressio vno tantvm modo legatvr. Altera est id demonstrare: formvlae infinitae svnt, et nvlla probatio singvlorvm casvvm, qvamvis longa, statvit omnes vno tantvm modo legi. Exemplvm seqvens ambas qvaestiones in vna expressione ostendit.

ExemplvmVna expressio, dvae catenae

Expressio v1↓v2↓v3v_{1} \downarrow v_{2} \downarrow v_{3}, connectivo inter argvmenta sva et sine parenthesibvs scripta, non indicat vter ex dvobvs connectivis principalis sit. In lingva circvlorvm et discorvm contra qvaeqve partivm consociatio diversa catena est, et catena ipsa dicit qvomodo partes consocientvr.

Demonstratio

  1. ((v1↓v2)↓v3)=∙∙v1v2v3((v_{1} \downarrow v_{2}) \downarrow v_{3}) = \resaltar{\sigI\sigI} v_{1} v_{2} v_{3}

    Prima lectio: primvm connectivvm v1v_{1} cvm v2v_{2} conivngit, et secvndvm principale est. In lingva fvndamentali dvo disci praecedvnt.

  2. (v1↓(v2↓v3))=∙v1∙v2v3(v_{1} \downarrow (v_{2} \downarrow v_{3})) = \sigI v_{1} \resaltar{\sigI} v_{2} v_{3}

    Secvnda lectio: secvndvm connectivvm v2v_{2} cvm v3v_{3} conivngit, et primvm principale est. Secvndvs discvs inter v1v_{1} et v2v_{2} ponitvr.

  3. ∙∙∘∙∘∘∙∘∘∘∙≠∙∘∙∙∘∘∙∘∘∘∙\sigI\resaltar{\sigI}\sigO\sigI\sigO\sigO\sigI\sigO\sigO\sigO\sigI \neq \sigI\resaltar{\sigO}\sigI\sigI\sigO\sigO\sigI\sigO\sigO\sigO\sigI

    Circvlis et discis scriptae, dvae catenae iam secvndo signo differvnt: formvlae diversae svnt.

  4. ∙  ∙  v1  v2  v3:−1,0,+1\sigI \; \resaltar{\sigI \; v_{1} \; v_{2}} \; v_{3}: \quad -1, \quad 0, \quad +1

    Vt prima catena legatvr, nvmerare svfficit: post discvm initialem qvisqve discvs connectens 11 demit et qvaeqve variabilis 11 addit, et prima pars ibi desinit vbi svmma primvm +1+1 attingit.

  5. ∙ (∙v1v2) v3\sigI \, \resaltar{(\sigI v_{1} v_{2})} \, \resaltar{v_{3}}

    Vnde prima pars est ∙v1v2\sigI v_{1} v_{2} et secvnda v3v_{3}: catena secvndvm primam lectionem legitvr, nec vllo alio modo. Hanc nvmerationem pro omnibvs formvlis valere, non solvm pro hac, est theorema legibilitatis vnicae, qvod tertia lectio per indvctionem demonstrat.

Responsvm igitvr vnitatis ad has dvas qvaestiones dvas partes habet. Ad primam, lingvam cvivs vnica regvla connectivvm praeponit, ita vt parentheses svpervacvae sint, et metalingvam cvivs abbreviationes singvlae vnam tantvm catenam designant. Ad alteram, principivm demonstrandi, indvctionem secvndvm complexitatem formvlarvm, qvae a finito nvmero probationvm (variabilibvs et regvla) ad omnes formvlas transit, sicvt indvctio in nvmeris natvralibvs a 11 et a gradv ab kk ad k+1k + 1 ad omnes nvmeros transit. Vtraqve parte forma argvmentationis obiectvm certvm fit, et qvaestio de eivs validitate in vnitatibvs seqventibvs cvm rigore poni potest.

Qvomodo vnitas discenda sit

Expedit ab hac probatione initiali incipere et qvaestiones male solvtas notare, qvae lectiones indicant in qvibvs morandvm est. Qvattvor lectiones ordine discendae svnt, qvia qvaeqve adhibet qvae priores statvvnt. In secvnda et tertia stvdivm chartam et stilvm postvlat: catenae circvlorvm et discorvm in scrinio visorio male legvntvr, et expedit eas describere, verba earvm separare (qvamqve variabilem et qvemqve discvm solitarivm) et pondvs cvivsqve notare, donec nvmeratio legibilitatis vnicae in consvetvdinem veniat. Demonstrationes vt seqventiae gradatim percvrrendae edvntvr, et qvisqve gradvs ivstificari posse debet anteqvam progrediaris. In prima et qvarta labor est attentae lectionis: coram qvaqve sententia Latina qvaerere qvid exacte affirmet, qvas lectiones admittat et qvae formvla eam repraesentet. Postremo, indicivm et responsvm cvivsqve problematis propositi non aperivntvr nisi postqvam serio temptatvm est.

Qvo dvcat

Vnitate absolvta lingva statvta erit, et vnitates seqventes svper eam aedificabvnt, nec eam itervm dispvtabvnt. Vnitas de dedvctione systema axiomatvm et dvarvm regvlarvm inferendi definiet, modi ponentis et, dvplici negatione demonstrata, svbstitvtionis dvplicis negationis, cvivs dedvctiones series formvlarvm svnt; axiomata eivs abbreviationibvs statvtis scribvntvr, qvas haec vnitas definit, et theorema dedvctionis eivs per indvctionem secvndvm longitvdinem dedvctionvm demonstratvr, instrvmento qvod hic discitvr. Prima eivs lectio est ea de systematibvs dedvctivis formalibvs. Vnitas de semantica variabilibvs valores veritatis tribvet eosqve ad omnes formvlas per recvrsionem extendet, qvod solvm legibilitatis vnicae gratia fieri potest; tabvlis lectiones informales connectivorvm ivstificabit qvas qvarta lectio adhibet, et in lectione de completvdine fvnctionali demonstrabit negationem conivnctam ad qvodlibet connectivvm exprimendvm svfficere. Vnitas de metatheoria deniqve per indvctionem firmitatem et completvdinem demonstrabit, et argvmentationes qvas haec vnitas formalizare docet tandem per dedvctionem vel per semanticam indifferenter diivdicari potervnt.

Extra hvnc cvrsvm syntaxis lingvae formalis est ea cvivsqve lingvae programmandi: compilator, qvalis in cvrsv Programmatio Lingva C++ I tractatvr, primvm decernit vtrvm programma bene formatvm sit et id vno tantvm modo dividit. Distinctio inter validitatem et veritatem etiam initivm est Logicae Aristotelicae, qvae formam syllogismorvm investigat; et indvctio tertiae lectionis eadem est qvae proprietates nvmerorvm in cvrsv Algebra et Geometria I demonstrat. In omnibvs his regionibvs, vt in legibvs et contractibvs conscribendis, eadem est doctrina: qvid affirmetvr accvrate dicere lingvam postvlat in qva qvaeqve expressio vnam tantvm lectionem habeat.