Semantica: synthesis et provocationes

Svmmarivm

Haec lectio vnitatem clavdit qvae semanticae dedicata est. Catenam dedvctivam restitvit qvae ab extensione aestimationis ad omnes formvlas et a lemmate coincidentiae ad conseqventiam, ad aeqvivalentiam et ad dvo eorvm theoremata operis pertinet, svbstitvtionem et svbstitvtionem vniformem; inde ad leges pro qvolibet nvmero terminorvm, ad completvdinem fvnctionalem et ad classes connectivorvm, et inde ad formas normales, ad earvm algorithmvm et ad circvitvs, et in qvoqve anvlo indicat qvibvs effectibvs vtatvr et in qva lectione demonstretvr. Distingvit qvae vnitas demonstraverit ab iis qvae a svperioribvs svmpserit, argvmentationem qvam cvrsvs inde a prima vnitate secvm fert tribvs modis decidit et exponit cvr qvaestio qvam vnitas apertam relinqvit, vtrvm id qvod in omni aestimatione vervm est cvm eo qvod derivabile est congrvat, ad metatheoriam dvcat. In probatione finali artes probationis initialis repetit, et sex provocationibvs finitvr, difficilioribvs qvam problemata lectionvm, qvae instrvmenta plvrivm lectionvm combinare postvlant.

Proposita discendi

Ordinem logicvm effectvvm vnitatis restitvere, effectvs priores qvibvs qvisqve innititvr et lectionem in qva demonstratvr agnoscendo.
Exponere qvomodo extensio recvrsiva, lemma coincidentiae, svbstitvtio semantica et leges generales ad completvdinem fvnctionalem, ad existentiam formarvm normalivm et ad rectitvdinem terminationemqve earvm algorithmi dvcant.
Distingvere qvae vnitas demonstraverit ab iis qvae a svperioribvs svmpserit et ab iis qvae metatheoriae reliqverit, praesertim congrventiam conseqventiae semanticae cvm derivabilitate, et compactitatem.
Problemata solvere qvae calcvlvm cvm valoribvs, conseqventiam, svbstitvtionem vniformem, classes connectivorvm, formas normales et circvitvs combinant.

Qvae vnitas consecvta est

Vnitas sibi proposverat formvlis lingvae in prima vnitate exstrvctae significationem dare, systemate dedvctivo secvndae intacto, et ex ea significatione rationes dvcere qvibvs qvaestiones decidantvr qvas logica de eis ponit: vtrvm formvla valida sit, vtrvm satisfactibilis, vtrvm ex aliis seqvatvr, vtrvm idem dicat atqve alia. Propositvm impletvm est cvm exceptionibvs qvibvsdam, qvaqve svo loco declarata: bivalentia et natvra veritati fvnctionalis, qvae non demonstrantvr sed eligvntvr, et qvarvm pretivm lectio de formalizatione ostendit; legibilitas vnica, definitio per recvrsionem, indvctio et abbreviationes officiales, qvae in prima vnitate demonstratae vel statvtae svnt et hic adhibentvr; et res necessariae de classibvs et fvnctionibvs, qvae vbi opvs erat in memoriam revocatae svnt. His exceptionibvs, iter confectvm vt vna catena dedvctiva legi potest sex segmentis, singvlis pro singvlis lectionibvs.

Valor formvlae

Lectio de semantica logicae propositionalis aestimationem definivit vt fvnctionem a variabilibvs in $\{0, 1\}$ et demonstravit, theoremate definitionis per recvrsionem in formvlis, eam vno tantvm modo ad omnes formvlas extendi vna sola clavsvla: $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ . Ex abbreviationibvs officialibvs, nihil alivd statvendo, valorem cvivsqve connectivi definiti compvtavit, vt polynomivm in valoribvs componentivm scriptvm, et cvm eo tabvlam implicationis, qvae hic theorema est. Per indvctionem in complexitate lemma coincidentiae demonstravit, ex qvo seqvitvr tabvlam veritatis, cvm svis $2^{n}$ versibvs, omnia continere qvae aestimationes infinitae de formvla $n$ variabilivm dicvnt; satisfactionem, validitatem, satisfactibilitatem, contradictionem et contingentiam definivit, accvrate monvit $\not\models \varphi$ dicere $\varphi$ non esse validam, non eam esse contradictionem, $\top := (v_{1} \rightarrow v_{1})$ et $\bot := \neg\top$ statvit, et decidibilitatem validitatis et satisfactibilitatis obtinvit, impendio exponentiali qvod inqvisitio directa aestimationis refvtantis minvit neqve tollit.

Conseqventia et aeqvivalentia

Lectio de conseqventia et aeqvivalentia semanticis conseqventiam ex classe praemissarvm, finita vel infinita, definivit et demonstravit eam proprietates strvctvrales dedvctionis habere (reflexivitatem, monotoniam, sectionem et transitivitatem), demonstrationibvs qvae per aestimationes procedvnt pro versibvs tractandis. Theorema dedvctionis semanticvm, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , ad vnicvm versvm falsvm implicationis redactvm est, et conseqventia ad insatisfactibilitatem: $\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\}$ insatisfactibilis est. Aeqvivalentia semantica, vt aeqvalitas valorvm definita, cvm conseqventia mvtva et cvm validitate implicationis dvplicis congrvere apparvit. Dvo eivs theoremata operis per indvctionem in complexitate demonstrata svnt: svbstitvtio occvrrentiae svbformvlae per aliam aeqvivalentem, cvm casv occvrrentiae totalis, qvi omitti non potest, et svbstitvtio vniformis variabilivm in formvlas qvaslibet, qvae validitatem, aeqvivalentiam et conseqventiam servat. His, leges catalogi, vt identitates inter polynomia comprobatae, qvovis loco cvivsvis formvlae adhibentvr et ivngi possvnt.

Leges pro qvolibet nvmero terminorvm

Lectio de legibvs De Morgani et legibvs distribvtivis generalibvs per recvrsionem, ad sinistram associando, conivnctionem et disivnctionem $n$ formvlarvm definivit, et per indvctionem in nvmero terminorvm lemma valoris demonstravit, qvod dicit conivnctionem veram esse si et solvm si omnes eivs termini veri svnt, et disivnctionem si et solvm si aliqvis vervs est. Eo et compatibilitate connectivorvm cvm aeqvivalentia associativitatem generalem obtinvit, qvae catena aeqvivalentiarvm demonstrata est vt etiam pro aeqvivalentia demonstrabili valeat, independentiam ab ordine et a repetitionibvs, leges De Morgani generales et distribvtivitatem generalem, cvivs indvctio in dvobvs indicibvs ita ordinata est vt hypothesis indvctionis omnes longitvdines secvndi elenchi complectatvr; lex dvalis per De Morganvm obtenta est, indvctione dvplici non repetita.

Fvnctiones veritatis

Lectio de completvdine fvnctionali iter contrarivm percvrrit, a tabvla ad formvlam. Fvnctiones veritatis $n$ argvmentorvm nvmeravit, $2^{2^{n}}$ , ostendit qvamqve formvlam vnam earvm exacte repraesentare et dvas formvlas aeqvivalentes esse si et solvm si eandem repraesentant, et theorema completvdinis fvnctionalis demonstravit: conivnctio versvs vera est exacte in svo versv, et disivnctio conivnctionvm versvvm in qvibvs fvnctio valorem $1$ habet eam repraesentat. Cvm illa formvla catena circvlorvm et discorvm sit, negatio conivncta per se sola svfficit; criterio negationis conivnctae, etiam $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ et negatio alternativa svfficivnt; et principio clavsvrae demonstravit omnes formvlas classis $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ valorem $1$ servare, ita vt ea classis non svfficiat.

Formae normales

Lectio de formis normalibvs in qvaqve classe formvlarvm aeqvivalentivm repraesentantes formae fixae elegit. Litteralia, clavsvlas et conivnctiones elementares definivit, et demonstravit negationem formae normalis aeqvivalentem esse svae dvali, qvae qvamqve conivnctionem in disivnctionem et qvodqve litterale in svvm oppositvm mvtat. Ex tabvla formas canonicas constrvxit, vnicas variabilibvs fixis, et existentiam vtrivsqve formae normalis dvobvs modis demonstravit: per tabvlam, vt corollarivm completvdinis fvnctionalis, et per indvctionem in complexitate, cvm vnico casv negationis conivnctae, qvae conivnctioni negationvm svarvm componentivm aeqvivalet, et cvm hypothesi indvctionis qvae vtramqve formam simvl postvlat, qvia negatio eas permvtat. Ostendit deniqve validitatem formae conivnctivae et satisfactibilitatem disivnctivae primo aspectv in earvm paribvs complementariis legi.

Algorithmvs et circvitvs

Lectio de algorithmo formarvm normalivm eivsqve vsibvs secvndam demonstrationem existentiae in rationem convertit qvae in scriptvras agit: connectiva praeter $\neg$ , $\wedge$ et $\vee$ tollere, negationes vsqve ad variabiles demittere et distribvere. Rectitvdinem eivs demonstravit svbstitvtione in scriptvra, qvae theorema svbstitvtionis ad abbreviationes accommodat, et terminationem tribvs mensvris qvae in qvaqve operatione decrescvnt, qvarvm vltima conivnctionem vt prodvctvm legit; praeterea demonstravit formam conivnctivam formvlae $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ necessario $2^{n}$ clavsvlas habere, ita vt incrementvm non sit vitivm algorithmi. Deinde formas normales capsae nigrae ex eivs tabvla obtinvit, eas versibvs vicinis conflandis contraxit et in circvitvs interrvptorvm convertit, qvorvm condvctio valor eorvm formvlae est.

Figvra seqvens sex segmenta in vnam catenam colligit. Qvisqve nodvs colvmnae definitio vel effectvs est, nvmeratvs secvndvm ordinem logicvm et arcv cvm anvlis prioribvs qvibvs eivs demonstratio vtitvr nexvs; circvm flvitant fvlcra, id est principia et instrvmenta ad qvae catena itervm atqve itervm recvrrit, qvodqve linea solida cvm anvlis qvi ei innitvntvr et pvnctata cvm anvlo vbi statvitvr nexvm, praeter ea qvae haec catena non demonstrat (legibilitas vnica cvm recvrsione, indvctio et abbreviationes officiales, ex prima vnitate), qvae vt armillae pingvntvr. Fvlcro pvlsato omnes anvli qvi eo vtvntvr illvstrantvr, et qvisqve anvlvs ad lectionem refert in qva demonstratvr. Animadvertendvm est indvctionem et valores connectivorvm esse fvlcra in vnitate saepissime adhibita, et lemma valoris, qvamqvam in tertia lectione demonstratvr, fere omnia svstinere qvae tres vltimae de conivnctionibvs et disivnctionibvs dicvnt.

Fvlcra catenae

ALegibilitas vnica et recvrsio. Si $\sigI\varphi\psi = \sigI\varphi'\psi'$ , qvattvor catenis formvlis, tvm $\varphi = \varphi'$ et $\psi = \psi'$ ; qvare regvla qvae valorem formvlae $\sigI\varphi\psi$ ex $\varphi$ , ex $\psi$ et ex eorvm valoribvs compvtat vnam fvnctionem in formvlis definit. In prima vnitate demonstratvm est. In hac vnitate sine demonstratione admittitvr.
BIndvctio. Simplex et fortis in nvmeris natvralibvs, et in complexitate formvlarvm, cvivs soli casvs svnt variabiles et negatio conivncta $(\varphi \downarrow \psi)$ . In prima vnitate demonstrata est. In hac vnitate sine demonstratione admittitvr.
CAbbreviationes officiales. $\neg\varphi := (\varphi \downarrow \varphi)$ , $(\varphi \vee \psi) := \neg(\varphi \downarrow \psi)$ , $(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)$ , $(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi)$ , $(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$ et $(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)$ . In prima vnitate statvtae svnt. In hac vnitate sine demonstratione admittitvr.
DValores connectivorvm. Cvm $a = v(\varphi)$ et $b = v(\psi)$ : $v(\neg\varphi) = 1 - a$ , $v((\varphi \vee \psi)) = a + b - ab$ , $v((\varphi \wedge \psi)) = ab$ , $v((\varphi \rightarrow \psi)) = 1 - a(1 - b)$ , $v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b)$ et $v((\varphi \veebar \psi)) = a + b - 2ab$ , vbi $a^{2} = a$ . Constitvitvr in: 1. Extensio aestimationis.
ELemma coincidentiae. Si dvae aestimationes in variabilibvs formvlae $\varphi$ congrvvnt, formvlae $\varphi$ evndem valorem dant; qvare tabvla $2^{n}$ versvvm omnia dicit. Constitvitvr in: 2. Lemma coincidentiae et tabvlae.
FSvbstitvtio semantica. Si $\theta \eqsem \theta'$ et $\chi'$ oritvr ex $\chi$ occvrrentia formvlae $\theta$ per $\theta'$ svbstitvta, tvm $\chi \eqsem \chi'$ . Constitvitvr in: 7. Theorema svbstitvtionis semanticae.
GLeges aeqvivalentiae. Dvplex negatio, idempotentia, commvtativitas, associativitas, distribvtivitas, leges De Morgani, absorptio, identitas, dominatio, tertivm non datvr et non contradictio, pro formvlis qvibvslibet. Constitvitvr in: 9. Leges aeqvivalentiae.
HLemma valoris. $v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1$ si et solvm si $v(\varphi_i) = 1$ pro omni $i$ ; $v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1$ si et solvm si $v(\varphi_i) = 1$ pro aliqvo $i$ . Constitvitvr in: 10. Lemma valoris et compatibilitas.

Segmentvm 1 Valor formvlae
- Valorem formvlae clavsvla negationis conivnctae compvtare et ex abbreviationibvs valorem cvivsqve connectivi definiti derivare.
- Lemma coincidentiae demonstrare et eo ostendere tabvlam $2^{n}$ versvvm svfficere.
- Formvlas et classes digerere, $\not\models \varphi$ cvm contradictione non confvndendo, et validitatem decidere aestimationem refvtantem qvaerendo.
1. Extensio aestimationis. Qvaeqve aestimatio $v$ vno tantvm modo ad omnes formvlas extenditvr clavsvla $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ ; abbreviationibvs explicatis valor formvlarvm $\neg$ , $\vee$ , $\wedge$ , $\rightarrow$ , $\leftrightarrow$ et $\veebar$ compvtatvr.
  Nititvr: A (Legibilitas vnica et recvrsio), C (Abbreviationes officiales). Demonstratvr in: Semantica logicae propositionalis.
2. Lemma coincidentiae et tabvlae. Si $v$ et $v'$ in $V(\varphi)$ congrvvnt, tvm $v(\varphi) = v'(\varphi)$ , per indvctionem in complexitate; qvare valores formvlae $\varphi$ in omnibvs aestimationibvs exacte svnt valores $2^{n}$ versvvm eivs tabvlae.
  Vtitvr: 1. Extensio aestimationis. Nititvr: B (Indvctio). Demonstratvr in: Semantica logicae propositionalis.
3. Divisio et decisio. Omnis formvla exacte vna ex tribvs est: valida, contingens vel contradictio; $\varphi$ valida est si et solvm si $\neg\varphi$ contradictio est, et contradictio est si et solvm si $\models \neg\varphi$ . $\top$ et tertivm non datvr valida svnt, $\bot$ contradictio est, et validitas et satisfactibilitas versibvs percvrrendis decidvntvr.
  Nititvr: D (Valores connectivorvm), E (Lemma coincidentiae). Demonstratvr in: Semantica logicae propositionalis.
Segmentvm 2 Conseqventia et aeqvivalentia
- Conseqventias ex classibvs finitis vel infinitis decidere, exemplar contrarivm exhibendo vel demonstrando nvllvm exstare.
- Theorema dedvctionis semanticvm et redvctionem conseqventiae ad insatisfactibilitatem adhibere.
- Svbstitvtionem occvrrentiae a svbstitvtione vniformi distingvere, et vtramqve per indvctionem in complexitate demonstrare.
- Aeqvivalentias per catenas statvere, qvamqve legem recte nominando.
1. Conseqventia eivsqve proprietates. $\Gamma \models \varphi$ si omnis aestimatio qvae $\Gamma$ satisfacit etiam $\varphi$ satisfacit; $\emptyset \models \varphi$ si et solvm si $\models \varphi$ ; reflexivitas, monotonia, sectio et transitivitas valent, et ex classe insatisfactibili qvaelibet formvla seqvitvr.
  Vtitvr: 3. Divisio et decisio. Demonstratvr in: Conseqventia et aeqvivalentia semanticae.
2. Dedvctio semantica et insatisfactibilitas. $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , per vnicvm versvm falsvm implicationis; $\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots))$ ; et $\Gamma \models \varphi$ si et solvm si $\Gamma \cup \{\neg\varphi\}$ insatisfactibilis est.
  Vtitvr: 4. Conseqventia eivsqve proprietates. Nititvr: D (Valores connectivorvm). Demonstratvr in: Conseqventia et aeqvivalentia semanticae.
3. Aeqvivalentia semantica. $\varphi \eqsem \psi$ si et solvm si $\varphi \models \psi$ et $\psi \models \varphi$ , si et solvm si $\models (\varphi \leftrightarrow \psi)$ ; aeqvivalentia reflexiva, symmetrica et transitiva est, et dvae formvlae aeqvivalentes vt praemissae et vt conclvsiones inter se permvtari possvnt.
  Vtitvr: 4. Conseqventia eivsqve proprietates. Nititvr: D (Valores connectivorvm). Demonstratvr in: Conseqventia et aeqvivalentia semanticae.
4. Theorema svbstitvtionis semanticae. Si $\theta \eqsem \theta'$ , in $\chi$ occvrrentiam formvlae $\theta$ per $\theta'$ svbstitvere, occvrrentia totali comprehensa, formvlam formvlae $\chi$ aeqvivalentem dat; idemqve omnes occvrrentias simvl svbstitvere.
  Vtitvr: 1. Extensio aestimationis, 6. Aeqvivalentia semantica. Nititvr: A (Legibilitas vnica et recvrsio), B (Indvctio). Demonstratvr in: Conseqventia et aeqvivalentia semanticae.
5. Svbstitvtio vniformis. Si $w(v_n) = v(\sigma(v_n))$ , tvm $v(\sigma(\chi)) = w(\chi)$ ; qvare, si $\models \chi$ , etiam $\models \sigma(\chi)$ , et svbstitvtio vniformis aeqvivalentiam et conseqventiam servat, non avtem satisfactibilitatem neqve contingentiam.
  Vtitvr: 1. Extensio aestimationis, 4. Conseqventia eivsqve proprietates, 6. Aeqvivalentia semantica. Nititvr: A (Legibilitas vnica et recvrsio), B (Indvctio). Demonstratvr in: Conseqventia et aeqvivalentia semanticae.
6. Leges aeqvivalentiae. Leges catalogi vt identitates inter polynomia comprobantvr cvm $a^{2} = a$ ; svbstitvtione et transitivitate ad svbformvlas adhibentvr et ivngvntvr.
  Vtitvr: 3. Divisio et decisio, 6. Aeqvivalentia semantica. Nititvr: D (Valores connectivorvm), F (Svbstitvtio semantica). Demonstratvr in: Conseqventia et aeqvivalentia semanticae.
Segmentvm 3 Leges pro qvolibet nvmero terminorvm
- Conivnctiones et disivnctiones $n$ terminorvm vt catenas ad sinistram associatas explicare et earvm valorem compvtare.
- Per indvctionem in nvmero terminorvm associativitatem generalem, independentiam ab ordine et leges De Morgani generales demonstrare.
- Distribvtivitatem generalem indvctione in dvobvs indicibvs demonstrare, et terminos qvos gignit nvmerare.
1. Lemma valoris et compatibilitas. Si $\alpha \eqsem \alpha'$ et $\beta \eqsem \beta'$ , tvm $\neg\alpha \eqsem \neg\alpha'$ , $(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta')$ et $(\alpha \vee \beta) \eqsem (\alpha' \vee \beta')$ ; conivnctio $n$ terminorvm valorem $1$ habet si et solvm si omnes eivs termini valorem $1$ habent, disivnctio si et solvm si aliqvis terminvs valorem $1$ habet, et termini aeqvivalentes conivnctiones et disivnctiones aeqvivalentes dant.
  Vtitvr: 6. Aeqvivalentia semantica. Nititvr: D (Valores connectivorvm), B (Indvctio). Demonstratvr in: Leges De Morgani et leges distribvtivae generales.
2. Associativitas et ordo. Conivnctio conivnctionvm dvorvm elenchorvm aeqvivalet conivnctioni eorvm concatenationis, et omnis consociatio aeqvivalet consociationi ad sinistram associatae; dvo elenchi eosdem terminos habentes conivnctiones et disivnctiones aeqvivalentes dant, qvicvmqve svnt ordo et repetitiones.
  Nititvr: H (Lemma valoris), G (Leges aeqvivalentiae), B (Indvctio). Demonstratvr in: Leges De Morgani et leges distribvtivae generales.
3. Leges De Morgani generales. $\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i$ et $\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i$ , lege binaria ad vltimam ivnctionem et hypothesi indvctionis ad id qvod intvs manet adhibitis.
  Nititvr: H (Lemma valoris), G (Leges aeqvivalentiae), B (Indvctio). Demonstratvr in: Leges De Morgani et leges distribvtivae generales.
4. Distribvtivitas generalis. $\left( \bigvee_{i=1}^{n} \varphi_i \right) \wedge \left( \bigvee_{j=1}^{m} \psi_j \right) \eqsem \bigvee_{i,j} (\varphi_i \wedge \psi_j)$ , cvm $nm$ terminis ordine lexicographico; et eivs dvalis, qvae disivnctionem dvarvm conivnctionvm distribvit, per De Morganvm.
  Vtitvr: 11. Associativitas et ordo, 12. Leges De Morgani generales. Nititvr: H (Lemma valoris), G (Leges aeqvivalentiae), B (Indvctio). Demonstratvr in: Leges De Morgani et leges distribvtivae generales.
Segmentvm 4 Fvnctiones veritatis
- Fvnctiones veritatis nvmerare et aeqvivalentiam decidere fvnctiones comparando qvas dvae formvlae repraesentant.
- Formvlam tabvlae constrvere et qvamlibet fvnctionem sola negatione conivncta scribere.
- Demonstrare classem connectivorvm idoneam esse criterio negationis conivnctae, vel non esse proprietate qvam eivs formvlae servant.
1. Fvnctiones veritatis. Svnt $2^{2^{n}}$ fvnctiones veritatis $n$ argvmentorvm; formvla cvivs variabiles inter $v_1, \ldots, v_n$ svnt vnam earvm exacte repraesentat, $f_\varphi$ , et $\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi$ .
  Vtitvr: 6. Aeqvivalentia semantica. Nititvr: E (Lemma coincidentiae). Demonstratvr in: Completvdo fvnctionalis.
2. Completvdo fvnctionalis. Conivnctio versvs valorem $1$ habet exacte in svo versv; disivnctio conivnctionvm versvvm in qvibvs $f$ valorem $1$ habet, vel $(v_{1} \wedge \neg v_{1})$ si nvllvs est, fvnctionem $f$ repraesentat; et omnis formvla aeqvivalet formvlae svae tabvlae.
  Vtitvr: 14. Fvnctiones veritatis. Nititvr: H (Lemma valoris), D (Valores connectivorvm). Demonstratvr in: Completvdo fvnctionalis.
3. Classes idoneae et non idoneae. Negatio conivncta svfficit, qvia abbreviationes explicari possvnt; si formvlae classis $K$ valorem $(1 - a)(1 - b)$ exprimvnt, $K$ idonea est, itemqve $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ et $\{\uparrow\}$ ; formvlae classis $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ valorem $1$ habent cvm omnes variabiles valorem $1$ habent, et ea classis idonea non est.
  Vtitvr: 15. Completvdo fvnctionalis. Nititvr: C (Abbreviationes officiales), B (Indvctio), D (Valores connectivorvm). Demonstratvr in: Completvdo fvnctionalis.
Segmentvm 5 Formae normales
- Litteralia, clavsvlas et formas normales agnoscere, figvram catenae a significatione eivs distingvendo.
- Formas canonicas ex tabvla constrvere et earvm vnicitatem demonstrare.
- Per indvctionem existentiam formarvm normalivm demonstrare, cvm hypothesi indvctionis qvae vtramqve postvlat.
- Primo aspectv validitatem formae conivnctivae et satisfactibilitatem disivnctivae decidere.
1. Litteralia et dvalitas. $\neg\ell \eqsem \ell^{*}$ ; conivnctio elementaris satisfactibilis est si et solvm si nvllvm par complementarivm continet, et clavsvla valida est si et solvm si aliqvod continet; negatio formae normalis aeqvivalet svae dvali, ita vt forma conivnctiva formvlae $\varphi$ dvalis sit formae disivnctivae formvlae $\neg\varphi$ .
  Vtitvr: 12. Leges De Morgani generales. Nititvr: G (Leges aeqvivalentiae), F (Svbstitvtio semantica), H (Lemma valoris). Demonstratvr in: Formae normales.
2. Formae canonicae. Si $\varphi$ satisfactibilis est, aeqvivalet svae formae canonicae disivnctivae, et si valida non est, conivnctivae; variabilibvs $v_1, \ldots, v_n$ fixis, dvae formae canonicae aeqvivalentes svnt si et solvm si eadem catena svnt, et dvae formvlae satisfactibiles aeqvivalentes svnt si et solvm si eandem formam canonicam disivnctivam habent.
  Vtitvr: 15. Completvdo fvnctionalis, 17. Litteralia et dvalitas. Nititvr: H (Lemma valoris), E (Lemma coincidentiae). Demonstratvr in: Formae normales.
3. Existentia per indvctionem. $(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi)$ ; formae normales conivnctione et disivnctione servantvr, forma disivnctiva conivnctionis et conivnctiva disivnctionis per distribvtivitatem generalem; per indvctionem, cvm hypothesi indvctionis pro vtraqve forma, omnis formvla formam disivnctivam et conivnctivam habet.
  Vtitvr: 17. Litteralia et dvalitas, 11. Associativitas et ordo, 13. Distribvtivitas generalis. Nititvr: B (Indvctio), F (Svbstitvtio semantica). Demonstratvr in: Formae normales.
4. Qvae primo aspectv videntvr. Forma conivnctiva valida est si et solvm si qvaeqve clavsvla par complementarivm continet; forma disivnctiva satisfactibilis est si et solvm si aliqva conivnctio elementaris nvllvm continet.
  Vtitvr: 17. Litteralia et dvalitas. Nititvr: H (Lemma valoris). Demonstratvr in: Formae normales.
Segmentvm 6 Algorithmvs et circvitvs
- Algorithmvm rescribendi adhibere et eam eliminationem implicationis dvplicis eligere qvae expedit.
- Rectitvdinem et terminationem eivs demonstrare, et exponere cvr forma conivnctiva modo exponentiali crescere possit.
- Formas normales capsae nigrae obtinere et simplificare, et eis circvitvs interrvptorvm designare.
1. Rectitvdo et terminatio algorithmi. Svbscriptvram per aliam aeqvivalentem svbstitvere scriptvram aeqvivalentem dat; qvaeqve regvla aeqvivalentia est, et scriptvra irredvcibilis est forma normalis aliqvo modo consociata; mensvrae $M_1$ , $M_2$ , cvm $M_2(\neg\varphi) = 2^{M_2(\varphi)}$ , et $M_3$ , cvm $M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi)$ , in qvaqve operatione decrescvnt.
  Vtitvr: 19. Existentia per indvctionem, 11. Associativitas et ordo. Nititvr: G (Leges aeqvivalentiae), D (Valores connectivorvm), B (Indvctio). Demonstratvr in: Algorithmvs formarvm normalivm eivsqve vsvs.
2. Incrementvm exponentiale. $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ aeqvivalet formae conivnctivae $2^{n}$ clavsvlarvm, et omnis forma conivnctiva aeqvivalens saltem $2^{n}$ clavsvlas non validas habet.
  Vtitvr: 19. Existentia per indvctionem, 17. Litteralia et dvalitas. Nititvr: H (Lemma valoris). Demonstratvr in: Algorithmvs formarvm normalivm eivsqve vsvs.
3. Versvs vicini et circvitvs. $(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa$ eivsqve dvalis; circvitvs in serie et in parallelo in statv $v$ condvcit si et solvm si $v(\varphi_C) = 1$ , et omnis fvnctio veritatis aliqvo circvitv efficitvr.
  Vtitvr: 15. Completvdo fvnctionalis, 18. Formae canonicae, 17. Litteralia et dvalitas, 11. Associativitas et ordo. Nititvr: G (Leges aeqvivalentiae), F (Svbstitvtio semantica), D (Valores connectivorvm), B (Indvctio). Demonstratvr in: Algorithmvs formarvm normalivm eivsqve vsvs.

Ad metatheoriam. Catena ibi consistit vbi semantica rationem pro omni qvaestione de formvlis attingit. Restat vt sciatvr vtrvm id qvod in omni aestimatione vervm est exacte id sit qvod in systemate dedvcitvr: vnitas seqvens dvas notiones comparabit.