Ratio stvdiorvm cvrsvs Logicae Mathematicae I

Consilivm

Omnes cvrsvs mathematici demonstrare ivbent, et omnes philosophici argvmentari; atqvi nvllvs eorvm ipsam ratiocinationem obiectvm svvm facit, et omnes pro intellecto habent qvid significet conclvsionem ex praemissis seqvi. Hic cvrsvs eam qvaestionem pro materia sva svmit. Consilivm eivs est, pro simplicissima logicae lingva, primam theoriam mathematicam completam aedificare cvivs obiectvm ratiocinatio est, qvattvor rebvs qvibvs constat in conspectv positis: lingva, cvivs formvlae agnoscvntvr et sine ambigvitate legvntvr; calcvlo, qvi dedvctiones gignit nvlla significationis signorvm ratione habita; significatione, qvae cviqve formvlae valorem veritatis svvm svb qvaqve aestimatione variabilivm eivs tribvit; et demonstratione calcvlvm et significationem congrvere.

Si hoc ita est, cvrsvs non est collectio regvlarvm ad signa tractanda, sed theoria cvm effectv principali, theoremate completvdinis, qvod omnia praecedentia praeparant. Pro classe formvlarvm $\Gamma$ et formvla $\varphi$, dedvcibilitas $\Gamma \vdash \varphi$ dicit exstare seriem finitam formvlarvm, ex axiomatibvs et regvlis constrvctam, qvae in $\varphi$ desinit; conseqventia semantica $\Gamma \models \varphi$ dicit omnem aestimationem qvae formvlas ex $\Gamma$ veras facit etiam $\varphi$ veram facere. Ambae relationes ex ideis contrariis nascvntvr, altera syntactica et exsistentialis, altera semantica et vniversalis; cvrsvs tamen demonstrat $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$. Ex qvo seqvitvr omnem qvaestionem de eo qvod ex praemissis seqvitvr ab eo latere responderi posse qvod facilivs sit: dedvctionem exhibendo, tabvlam percvrrendo vel, vt vltima lectio materiae docet, per resolvtionem refvtando.

Discipvli et cognitiones praeviae

Cvrsvs ad eos dirigitvr qvi stvdia mathematica, informatica vel philosophica incipivnt, et ad eos qvi, qvocvmqve institvtionis svae tempore, accvrate scire volvnt qvid sit demonstratio et cvr ei fidere liceat: discipvlos qvi mathematicam vniversitariam ingredivntvr et in demonstrationibvs offendvnt, discipvlos informaticae qvi logica circvitvvm, programmatvm et qvaestionvm satisfactibilitatis egent, et discipvlos philosophiae qvi a logica argvmentationvm ad eivs theoriam transire volvnt.

Cvrsvs est primi ordinis, sine reqvisitis et per se constans. Non praesvpponit logicam stvdvisse, nec theoriam classivm nosse, nec vmqvam theorema demonstravisse. Qvod de classibvs (pertinentia, inclvsio, vnio, classes formvlarvm), de fvnctionibvs (aestimatio est fvnctio a variabilibvs in $\{0, 1\}$), de catenis signorvm et de indvctione adhibet, id eo loco docet qvo eo eget: classes et catenas in lectione vnitatis primae de lingva, indvctionem in lectione seqventi, anteqvam ea vtatvr. Dvo tantvm praesvpponit: attente legere, qvia in lingva formali signvm additvm vel omissvm catenam mvtat, et arithmeticam elementarem nvmerorvm natvralivm, qvi in hoc cvrsv, vt in reliqvo sitv, a $1$ incipivnt.

Qvo dvcat

Ex praecedentibvs seqvitvr locvs cvrsvs in sitv. Reqvisita non habet et meta est trivm ordinvm stvdiorvm, Mathematicae, Informaticae et Philosophiae, qvia in omnibvs tribvs ratiocinatio simvl instrvmentvm et obiectvm est. Tres cvrsvs complementarios habet, qvi ante, simvl vel postea, qvolibet ordine, seqvi possvnt. Logica Aristotelica logicam terminorvm et syllogismvm stvdet, cvivs validitas a verbis vt «omnis» et «aliqvis» pendet, qvae hic cvrsvs omittit, et ostendit ex qva traditione ad calcvlvm perventvm sit. Algebra et Geometria I aedificivm dedvctivvm ex axiomatibvs Peanianis exstrvit, et in nvmeris methodvm axiomaticam et indvctionem exercet qvas hic cvrsvs vt obiectvm stvdet; ratio eivs commendat hvnc cvrsvm antea stvdvisse, vel simvl stvdere. Programmatio Lingva C++ I, postremo, ad vsvm dvcit qvod hic theoria est: decernere vtrvm catena bene formata sit, tabvlam veritatis percvrrere, formam normalem compvtare vel refvtationem qvaerere rationes svnt qvae vt programmata scribi possvnt.

Atqvi cvrsvs qvaestionem expressionis apertam relinqvit: lingva eivs nec «omnis» nec «aliqvis» dicere potest, et formalizatio argvmentationvm Latinarvm inde ab vnitate prima qvantificatores amittit. Itaqve continvatio eivs praevisa est Logica Mathematica II, logicae praedicatorvm dedicata, qvae eandem viam cvm qvantificatoribvs et variabilibvs per obiecta discvrrentibvs percvrret: firmitatem, completvdinem et compactitatem servabit, methodis qvas hic cvrsvs anticipat, sed in ea conseqventia decidibilis esse desinet.

Proposita discendi generalia

Proposita seqventia describvnt qvid facere possit qvi cvrsvm perficit. Qvodqve vt actio observabilis formvlatvr, ita vt opere certo probari possit; qvaeqve lectio materiae vicissim sva proposita declarat, qvae vni vel plvribvs generalivm servivnt, et lectio conclvsionis ostendit in qvibvs vnitatibvs et lectionibvs qvodqve tractetvr. Septem proposita nvmerantvr vt citari possint.

1. Propositvm 1. Lingvam obiecti a metalingva distingvere, et regvlis formationis decernere vtrvm catena formvla sit.
2. Propositvm 2. Envntiata et argvmentationes lingvae natvralis formalizare, indicando qvid formalizatio servet et qvid amittat.
3. Propositvm 3. Dedvctiones in systemate cvrsvs (axiomatibvs Łvkasiewiczii, modo ponente et svbstitvtione dvplicis negationis) constrvere, axiomata, regvlas primitivas et regvlas derivatas combinando.
4. Propositvm 4. Metatheoremata per indvctionem in nvmeris natvralibvs, secvndvm complexitatem formvlarvm et secvndvm longitvdinem dedvctionvm demonstrare.
5. Propositvm 5. Validitatem, satisfactibilitatem, conseqventiam et aeqvivalentiam semanticas tabvlis veritatis et aeqvivalentiis decernere.
6. Propositvm 6. Formvlas in formas normales transformare et per eas fvnctiones veritatis et circvitvs exprimere.
7. Propositvm 7. Firmitatem, completvdinem et compactitatem exponere et adhibere, et insatisfactibilitatem per resolvtionem decernere.

Proposita tertivm et septimvm svam qvodqve vnitatem habent, dedvctionem et metatheoriam; proposita qvintvm et sextvm vnitatem semanticae inter se dividvnt, illvd in priore eivs dimidio, hoc in altero. Propositvm secvndvm lectionem propriam habet, eam de formalizatione, et deinde exercetvr qvotiens problema verbis proponitvr. Proposita primvm et qvartvm contra transversa svnt: distinctio inter id qvod intra lingvam et id qvod de ea dicitvr qvattvor vnitates percvrrit, et indvctio forma est omnivm demonstrationvm gravivm cvrsvs, a legibilitate vnica formvlarvm vsqve ad firmitatem systematis et lemma Kalmarii. Ex qvo seqvitvr ea asseqvi nvlli lectioni soli attribvi posse, et per totvm cvrsvm ea colere convenire.

Systema cvrsvs eivsqve decreta

Cvrsvs logicae propositionalis mvltis modis constrvi potest, et libri vsitati lingva, connectivis primitivis et systemate dedvctivo differvnt. Hic cvrsvs tria decreta facit qvae ab initio nosse convenit, qvia exponvnt qvod primo aspectv mirvm videri potest.

Lingva circvlorvm et discorvm

Lingva cvrsvs alphabetvm dvorvm tantvm signorvm habet, circvlvm $\sigO$ et discvm $\sigI$. Variabilis $n$-a est catena $n$ circvlorvm qvos discvs seqvitvr, $v_{n} = \sigO^{n}\sigI$, ita vt $v_{1} = \sigO\sigI$ et $v_{2} = \sigO\sigO\sigI$; et vna sola regvla formationis est: si $\varphi$ et $\psi$ formvlae svnt, etiam $\sigI\varphi\psi$ est, qvae $(\varphi \downarrow \psi)$ abbreviatvr et «nec $\varphi$ nec $\psi$» legitvr. Negatio conivncta $\downarrow$ igitvr vnicvm connectivvm primitivvm est, et cetera omnia abbreviationes semel definitae svnt: $\neg\varphi$ est $(\varphi \downarrow \varphi)$, disivnctio $(\varphi \vee \psi)$ est $\neg(\varphi \downarrow \psi)$, et ex eis conivnctio, implicatio, implicatio dvplex et disivnctio exclvsiva definivntvr. Qvilibet alivs modvs eas scribendi theorema est, qvod demonstratvr, non definitio.

Electio pretivm habet, legibilitatem, qvod cvrsvs in metalingva solvit: nemo cotidie catenas circvlorvm et discorvm scribit, sed nomina earvm abbreviata, qvae qvovis tempore vsqve ad catenam qvam designant explicari possvnt. Atqvi mvltipliciter reddit. Dvo signa infinitis variabilibvs svfficivnt, ita vt omnis formvla catena finita in alphabeto dvorvm elementorvm sit. Connectivvm ante argvmenta sva scribitvr, ideoqve parentheses non reqvirvntvr: legibilitas vnica argvmento ponderis demonstratvr, qvod $+1$ cviqve variabili et $-1$ cviqve disco connectenti tribvit. Et cvm omnis formvla composita negatio conivncta sit, qvaeqve demonstratio per indvctionem secvndvm complexitatem vnvm tantvm casvm compositvm habet, qvod omnes vnitatvm seqventivm contrahit. Vnvm connectivvm svfficere ad qvodlibet alivd exprimendvm non praesvpponitvr: vnitas semanticae id demonstrat.

Secvnda regvla primitiva

Systema dedvctivvm a systemate Iani Łvkasiewiczii proficiscitvr: tribvs schematibvs axiomatvm, negatione et implicatione scriptis, et modo ponente vt regvla vnica. Ea schemata pro lingvis formvlata svnt qvarvm connectiva primitiva negatio et implicatio svnt; in lingva circvlorvm et discorvm formvla vt $(v_{1} \downarrow v_{2})$ nec hoc nec illvd est, et axiomatibvs opaca est. Prima lectio vnitatis dedvctionis demonstrat, nota qvam omnia axiomata habent, qvam modvs ponens servat et qvam formvla non habet, systema Łvkasiewiczii $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ non dedvcere.

Si hoc ita est, systema complendvm est, et remedivm natvrale videtvr dvplicem negationem demonstrare, $\varphi \dashv\vdash \neg\neg\varphi$, qvam secvnda lectio ex tribvs schematibvs dedvcit. Nota ostendit id non svfficere: theoremata dvplicis negationis eam servant et tamen ne cvm eis qvidem $v_{1}$ cvm $\neg\neg v_{1}$ intra negationem conivnctam permvtatvr. Itaqve, dvplici negatione demonstrata, secvnda lectio secvndam regvlam primitivam addit, svbstitvtionem dvplicis negationis: ex formvla $\chi$ infertvr ea qvae oritvr cvm in ea occvrrentia svbformvlae $\theta$ per $\neg\neg\theta$ svbstitvitvr, vel occvrrentia ipsivs $\neg\neg\theta$ per $\theta$. Systema cvrsvs igitvr constat tribvs schematibvs Łvkasiewiczii, modo ponente et hac regvla.

Alia systemata pro negatione conivncta idem schematibvs axiomatvm ad mensvram factis asseqvvntvr. Cvrsvs regvlam praefert dvabvs de cavsis: simplicior etiam est qvam modvs ponens, qvia vnvm versvm svmit et vnam occvrrentiam mvtat, et nihil artificiosi habet, qvia exprimit qvod dvplex negatio iam dicit, $\theta$ et $\neg\neg\theta$ inter se permvtabiles esse, ad omnem locvm formvlae extensvm. Praeterea firma est, qvia valorem veritatis cvivsqve versvs servat, et theorema dedvctionis conservat, vno casv in eivs demonstratione addito. Eam svfficere ad dedvcendvm omne qvod dedvci debet theorema completvdinis vltimae vnitatis est.

Compactitas ante completvdinem fortem

Completvdo tres formas admittit: debilis dicit omnem tavtologiam theorema esse; finita, omnem conseqventiam classis finitae praemissarvm ex ea dedvci; fortis, idem valere pro classe qvavis, etiam infinita. Methodvs cvrsvs, lemma Kalmarii, cvm variabilibvs formvlae, nvmero finitis, et cvm praemissis finitis operatvr, ideoqve dvas primas formas attingit, tertiam non. Vt ad eam perveniatvr, svfficit vt, si $\Gamma \models \varphi$, aliqva portio finita $\Gamma_{0}$ ipsivs $\Gamma$ iam $\Gamma_{0} \models \varphi$ praestet; atqvi id ipsvm est qvod theorema compactitatis affirmat.

Mvlti libri privs completvdinem fortem alia methodo demonstrant et ex ea compactitatem dedvcvnt. In hoc cvrsv contra completvdo fortis id est qvod qvaeritvr, et compactitatem ex ea obtinere circvlare esset. Vnde ordo invertitvr: lectio de compactitate eam intra semanticam demonstrat, nvlla dedvctione memorata, valores ipsivs $v_{1}, v_{2}, \ldots$ singillatim figendo, et tvm demvm, tribvs versibvs, completvdinem fortem obtinet, id est $\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi$ pro omni classe $\Gamma$.

Contenta

Cvrsvs in sex vnitates disponitvr: hanc praesentationem, qvattvor vnitates materiae et conclvsionem. Qvaeqve vnitas materiae lectione introdvctionis aperitvr, qvae lectiones eivs, locvm eivs in cvrsv, qvae vt nota praesvpponit et qvaestionem qvam solvit exhibet, et a probatione initiali incipit; lectione synthesis clavditvr, qvae catenam dedvctivam vnitatis reficit, eam cvm reliqvo cvrsv conectit, in probatione finali facvltates probationis initialis repetit et sex provocationes proponit difficiliores qvam problemata lectionvm.

Vnitas 0. Praesentatio cvrsvs

Hac lectione constat, qvae consilivm, proposita generalia, decreta, contenta, laborem et designationem cvrsvs statvit.

Vnitas 1. Lingva

Eivs propositvm est lingvam qvam cvrsvs stvdet aedificare, demonstrare qvamqve formvlam vno tantvm modo legi, eamqve cvm argvmentationibvs Latinis conectere.

1. Lingva: introdvctio.
2. Qvid est logica mathematica: validitas coram veritate, exemplvm contrarivm, paradoxa et distinctio inter lingvam obiecti et metalingvam.
3. Lingva logicae propositionalis: classes et catenae, lingva circvlorvm et discorvm, regvla formationis eivs et abbreviationes eivs.
4. Indvctio in nvmeris natvralibvs et in formvlis: indvctio simplex, fortis et strvctvralis, lemma ponderis, legibilitas vnica et definitiones per recvrsionem.
5. Formalizatio lingvae natvralis: lexicon, translatio envntiatorvm et argvmentationvm, et qvid implicatio materialis amittat.
6. Lingva: synthesis et provocationes.

Vnitas 2. Dedvctio

Eivs propositvm est lingvae calcvlvm dare, systema cvrsvs, et in eo, semel singvlas, rationes ratiocinandi derivare qvibvs mathematica sine nomine vtitvr.

1. Dedvctio: introdvctio.
2. Systemata dedvctiva formalia: systema Łvkasiewiczii, dedvctio ex praemissis, theorema dedvctionis et nota qvae eivs limitem ostendit.
3. Qvattvor artes dedvctionis: syllogismvs hypotheticvs, permvtatio praemissarvm, dvplex negatio, contrapositio et svbstitvtio dvplicis negationis.
4. Symmetriae connectivorvm: lemma fvndamentale negationis conivnctae, svbstitvtio aeqvivalentivm, formae aeqvivalentes disivnctionis et conivnctionis et qvinqve earvm symmetriae.
5. Artes logicae classicae: regvlae cvivsqve connectivi, tertivm exclvsvm, demonstratio per casvs et redvctio ad absvrdvm, cvm praemissis.
6. Leges De Morgani et leges distribvtivae: earvm demonstrationes in vtrvmqve sensvm et svbstitvtio aeqvivalentivm intra alias formvlas.
7. Dedvctio: synthesis et provocationes.

Vnitas 3. Semantica

Eivs propositvm est formvlis significationem dare, ea validitatem et conseqventiam decernere, et omnem formvlam ad formas normales redvcere.

1. Semantica: introdvctio.
2. Semantica logicae propositionalis: aestimationes earvmqve extensio per recvrsionem, lemma coincidentiae, tabvlae veritatis, validitas et satisfactibilitas.
3. Conseqventia et aeqvivalentia semanticae: conseqventia ex classibvs, theorema dedvctionis semanticvm, svbstitvtio semantica et svbstitvtio vniformis.
4. Leges De Morgani et leges distribvtivae generales: conivnctiones et disivnctiones $n$ terminorvm earvmqve leges, per indvctionem.
5. Completvdo fvnctionalis: omnis fvnctio veritatis formvlam habet, negatio conivncta sola svfficit, et classes connectivorvm idoneae.
6. Formae normales: litteralia, clavsvlae, formae disivnctiva et conivnctiva, earvm dvalitas et exsistentia.
7. Algorithmvs formarvm normalivm eivsqve vsvs: algorithmvs rectvs qvi terminatvr, et designatio et simplificatio circvitvvm interrvptorvm.
8. Semantica: synthesis et provocationes.

Vnitas 4. Metatheoria

Eivs propositvm est demonstrare dedvctionem et conseqventiam congrvere, primvm pro praemissis finitis, deinde pro praemissis qvibvsvis, et tertivm modvm eas decernendi praebere.

1. Metatheoria: introdvctio.
2. Firmitas et completvdo: firmitas per indvctionem in versibvs, consistentia, lemma Kalmarii et completvdo debilis et finita.
3. Theorema compactitatis: eivs demonstratio semantica, formae eivs aeqvivalentes, completvdo fortis qvae ex eo seqvitvr et vsvs eivs combinatorii.
4. Methodvs resolvtionis: forma clavsvlaris, regvla resolvtionis, eivs firmitas et completvdo refvtationis, et eivs impendivm.
5. Metatheoria: synthesis et provocationes.

Vnitas 5. Conclvsio cvrsvs

Constat lectione Recognitio finalis cvrsvs Logicae Mathematicae I, qvae septem proposita generalia in memoriam revocat, figvra ostendit in qvibvs vnitatibvs et lectionibvs qvodqve tractetvr, primvm conatvm probationvm finalivm per proposita colligit et indicat qvo stvdivm pergat.

Labor et credita

Labor cvrsvs non horis expositionis metitvr, qvae in cvrsv asynchrono non exstant, sed toto labore eivs qvi evm stvdet: legere, demonstrationes et dedvctiones seqvi, problemata solvere et repetere. Compvtatio eadem ratione in omnibvs cvrsibvs sitvs procedit: tempvs legendi textvm cvivsqve lectionis compvtat centenis verbis singvlis minvtis, vnaqvaqve formvla vt verbo nvmerata, viginti minvtis in singvla problemata solvta, triginta qvinqve in proposita, qvadraginta qvinqve in provocationes et dvodecim in probationes initiales vel finales, et marginem decimae portionis ad repetendvm addit.

Eventvs

Lectiones cvrsvs vniversae continent $90$ problemata solvta, $90$ problemata proposita et $24$ provocationes, praeter octo probationes vnitatvm. Labor per vnitates compvtatvs, ad horam rotvndatvs, hic est:

• Vnitas 0, praesentatio cvrsvs: minvs qvam $1$ hora.
• Vnitas 1, lingva: $30$ horae.
• Vnitas 2, dedvctio: $36$ horae.
• Vnitas 3, semantica: $43$ horae.
• Vnitas 4, metatheoria: $25$ horae.
• Vnitas 5, conclvsio cvrsvs: minvs qvam $1$ hora.

Svmma est circiter $137$ horae laboris. Hvnc nvmervm legere convenit vt id qvod est: compvtationem pro eo qvi omnes demonstrationes stvdet et omnia problemata et provocationes solvit. Qvi iam logicam stvdvit, vel qvi problematis propositis contentvs provocationes non aggreditvr, mvlto minvs impendet; qvi nvmqvam theorema demonstravit plvribvs fortasse egebit, praesertim in vnitatibvs dedvctionis et semanticae, qvae etiam longissimae svnt.

Atqvi nvmervs nominalis est: is est qvi credita cvrsvs statvit, et lectionem constanti celeritate et dodrantem horae in singvlas provocationes praesvpponit. Donec cvm veris discipvlis mensvs sit, spatio probabili comitandvs est. Si lectio dimidia celeritate svpposita procederet, vt fit cvm qvaeqve dedvctio charta et stilo describitvr et qvaeqve catena circvlorvm et discorvm manv dissolvitvr, et singvlae provocationes septvaginta qvinqve minvta pro qvadraginta qvinqve postvlarent, eadem ratio circiter $174$ horas daret. Itaqve labor exspectandvs inter circiter $137$ et circiter $174$ horas iacet. Terminvs svperior limes prvdens est, non mensvra; spativm corrigetvr cvm tempvs cognitvm erit qvod ii qvi cvrsvm stvdent impendvnt, et interea credita nvmero nominali compvtantvr.

Celeritas svasa

Ad celeritates nominandas, haec ratio eodem ivdicio vtitvr ac ceterae rationes sitvs: stvdivm plenvm est annvs academicvs $60$ creditorvm, circiter $1650$ horae per qvadraginta fere hebdomades distribvtae, id est circiter $40$ horae in hebdomade, et stvdivm dimidivm eivs dimidivm, circiter $20$ horae in hebdomade. Ex qvo seqvitvr celeritas commendata vnivs semestris sedecim hebdomadvm, cvm circiter $8$ vel $9$ horis stvdii in hebdomade, pavlo plvs qvam qvinta portione stvdii pleni; cvm spatio probabili, a $9$ ad $11$ horas in hebdomade. Id semestre cvm Algebra et Geometria I commvnicari potest, cvivs demonstrationes melivs legvntvr cvm dedvctio iam obiectvm notvm est.

Celeritas intenta, circiter $20$ horarvm in hebdomade, id est stvdii dimidii, cvrsvm septem hebdomadibvs perficit. Celeritas remissior, circiter $4$ vel $5$ horarvm in hebdomade, evm ad dvo semestria prodvcit, qvae evm fere aeqvaliter dividvnt: vnitates 0 ad 2, lingva et dedvctio, circiter $67$ horas occvpant, et vnitates 3 ad 5, semantica, metatheoria et conclvsio, circiter $69$.

Aeqvivalentia in creditis transferibilibvs

Systemata creditorvm transferibilivm cvrsvm toto labore metivntvr qvem a discipvlo postvlat, non horis scholarvm praesentivm, eo consilio vt stvdia in vna institvtione peracta in alia agnosci possint. Systema Evropaevm Creditorvm Transferendorvm et Accvmvlandorvm, ab vniversitatibvs Evropaeis post Declarationem Bononiensem receptvm, $60$ credita anno academico stvdii pleni tribvit, et singvla credita inter $25$ et $30$ horas laboris statvit. Systema Creditorvm Transferibilivm Chiliae, ab vniversitatibvs Chilianis simili designatione receptvm, item $60$ credita anno academico tribvit et singvla credita inter $24$ et $31$ horas laboris statvit.

Atqvi, si $137$ horae compvtatae per terminos cvivsqve intervalli dividvntvr, cvrsvs circiter $5$ credita Evropaea aeqvat (a 4,6 ad 5,5), et inter $4$ et $6$ credita transferibilia Chiliana (a 4,4 ad 5,7). Si valor medivs vtrivsqve intervalli, 27,5 horae in singvla credita, pro norma svmitvr, in vtroqve systemate idem nvmervs prodit, 4,98, qvi ad 5 rotvndatvr. Pro creditis Evropaeis nvmervs $C$ creditorvm sic circvmscribitvr:

Itaqve commendatvr vt cvrsvi $5$ credita Evropaea et $5$ credita transferibilia Chiliana tribvantvr, id est dvodecima portio anni academici stvdii pleni, pavlo minvs qvam disciplina semestris vsitata sex creditorvm.

Designatio cvrsvs

Modvs

Cvrsvs asynchronvs est, in rete, celeritate propria: dies, sessiones vivas et terminos non habet, et vnvsqvisqve discipvlvs ea celeritate progreditvr qvam praeparatio et tempvs eivs sinvnt. In qvattvordecim lingvis sitvs offertvr, eadem logica in omnibvs: formvlae, dedvctiones et actvs demonstrationvm in vnaqvaqve versione idem svnt, et solvs textvs vertitvr. Lectiones declarant qvas alias lectiones ante stvdere conveniat, ita vt ordo commendatvs manifestvs sit.

Strvctvra lectionis

Omnes lectiones materiae eandem strvctvram seqvvntvr. Incipivnt a svmmario et a catalogo propositorvm discendi propriorvm, vt actiones observabiles formvlatorvm. Seqvvntvr theoria, cvm definitionibvs, effectibvs accvrate envntiatis eorvmqve demonstrationibvs, et exempla. Demonstrationes vt reprodvctores actv post actvm exhibentvr: qvisqve actvs versvm scribit, illvstrat qvod mvtatvr et, cvm effectvi priori innititvr, ad evm redit. Dedvctiones systematis versibvs nvmeratis scribvntvr, cvm ivstificatione cvivsqve ad dextram (axioma, praemissa, modvs ponens cvm versibvs qvibvs vtitvr, vel regvla derivata), et progrediendo versvs citati illvstrantvr. Lectionem clavdvnt qvinqve problemata solvta, cvm solvtione actv post actvm, et qvinqve problemata proposita, qvodqve cvm indicio complicato et deinde responso finali; problemata proposita demonstrationis, post responsvm complicatam, solvtionem elaboratam addvnt, qvam aperire convenit non nisi postqvam discipvlvs svam conscripsit.

Qvaeqve lectio praeterea voce alta avdiri potest lectore sitvs, qvi signa formvlarvm verbis pronvntiat, circvlo, disco et signis dedvctionis et conseqventiae comprehensis.

Probatio

Cvrsvs non censvrae svbicit: probatio eivs formativa est et svi ipsivs exploratione nititvr. Problemata proposita sinvnt probare vtrvm proposita cvivsqve lectionis assecvta sint, et provocationes, vtrvm ea cvivsqve vnitatis. His accedvnt probationes vnitatvm: initialis, initio introdvctionis, pvnctvm vnde proficiscitvr vndecim ad qvindecim qvaestionibvs metitvr, qvia qvaestionibvs vnitatis aliqvas addit de eo qvod vnitas vt notvm praesvpponit; finalis, in synthesi et ante provocationes, qvod assecvtvm est dvodecim qvaestionibvs metitvr et cvm initiali comparatvr. Ambae in ipso navigatro corrigvntvr, cvm expositione pro qvoqve responso et remissione ad lectionem qvam repetere convenit; eventvs earvm in navigatro tantvm eivs qvi respondet servantvr, et recognitio finalis primvm conatvm cvivsqve probationis finalis in tabvlam per propositvm generale colligit.

Qvomodo hic cvrsvs stvdendvs sit

Cvrsvs ita excogitatvs est vt ordine stvdeatvr. Qvaeqve vnitas praecedentes praesvpponit: dedvctio lingva primae scribitvr, semantica formvlis eivs valorem dat, et metatheoria secvndam cvm tertia comparat; qvi lectionem praeterit, serivs ocivs ad eam redire cogitvr.

In qvaqve lectione convenit primvm svmmarivm et proposita legere; deinde theoriam charta et stilo stvdere, catenas circvlorvm et discorvm describendo, variabiles et discos earvm separando, et qvemqve versvm dedvctionis anticipando anteqvam reprodvctor evm scribat; problemata solvta temptare anteqvam solvtio eorvm inspiciatvr, et proposita sine avxilio solvere, indicivm non nisi conatv exhavsto aperiendo. Problema cvivs responsvm ante conatvm consvltvm est non solvtvm, sed lectvm est.

Postremo convenit semper distingvere cvivs ordinis sit qvaeqve assertio: vtrvm aliqvid intra lingvam dicat, vt formvla, an aliqvid de ea, vt $\Gamma \vdash \varphi$ vel $\Gamma \models \varphi$. Haec distinctio, qvae primvm propositorvm cvrsvs est, ea qvoqve est qvae effectvm eivs principalem intellegere sinit, qvi non nisi in metalingva envntiari potest.