Metatheoria: synthesis et provocationes

Svmmarivm

Haec lectio vnitatem metatheoriae dicatam et, cvm ea, materiam cvrsvs clavdit. Catenam dedvctivam restitvit qvae a validitate axiomatvm ad firmitatem systematis dvcit; a dvobvs lemmatibvs negationis conivnctae ad lemma Kalmarii et ad completvdinem pro praemissis finitis; a lemmate dvorvm testivm ad theorema compactitatis et, per id, ad completvdinem fortem; et a forma clavsvlari ad firmitatem et completvdinem refvtationis methodi resolvtionis, in qvoqve anvlo indicans qvibvs effectibvs vtatvr et in qva lectione demonstretvr. Ostendit qvomodo tres partes priores cvrsvs, lingva, dedvctio et semantica, in congrventia inter $\vdash$ et $\models$ conveniant, et qvid qvaeqve ad eam conferat; distingvit qvae cvrsvs demonstraverit ab iis qvae svpposverit et ab iis qvae aperta relinqvat. In probatione finali artes probationis initialis repetit et sex provocationibvs finitvr, difficilioribvs qvam problemata lectionvm, qvae instrvmenta plvrivm earvm combinare postvlant.

Proposita discendi

Ordinem logicvm effectvvm vnitatis restitvere, effectvs priores qvibvs qvisqve nititvr et lectionem in qva demonstratvr agnoscendo, et ordinem compactitatis et completvdinis fortis ivstificare.
Exponere qvomodo lingva, dedvctio et semantica in congrventia inter $\vdash$ et $\models$ conveniant, et qvis effectvs cvivsqve vnitatis cvrsvs ad eam necessarivs sit.
Distingvere qvae cvrsvs demonstraverit ab iis qvae svpposverit (schemata axiomatvm, regvlas primitivas et indvctionem) et ab iis qvae aperta relinqvat (pretivm satisfactibilitatis decernendae, et logicam cvm qvantificatoribvs).
Problemata solvere qvae notas, lemma Kalmarii, svbstitvtionem vniformem, compactitatem et resolvtionem combinant, in qvoqve casv latere facili congrventiae vtendo.

Qvae vnitas consecvta est

Vnitas sibi proposverat dvas relationes comparare qvas vnitates priores in eadem lingva constrvxerant, dedvcibilitatem $\Gamma \vdash \varphi$ et conseqventiam semanticam $\Gamma \models \varphi$ , et demonstrare eas congrvere. Propositvm sine exceptionibvs in envntiatis attingitvr: ambae relationes eaedem svnt pro omni classe praemissarvm, finita vel infinita, et resolvtio tertiam viam praebet, aeqve firmam et completam, ad conseqventiam decernendam. Exceptiones in methodis svnt, et qvaeqve svo loco declarata est: completvdo primae lectionis constrvctiva est, non tamen vtilis in vsv, qvia dedvctiones tam longas qvam tabvlam gignit; compactitas aestimationem esse confirmat, sed non docet qvomodo inveniatvr; et resolvtio decernit, sed pretivm eivs in casv pessimo qvaestio aperta est. His exceptionibvs, iter peractvm vt vna catena dedvctiva qvattvor segmentorvm legitvr.

Firmitas

Lectio de firmitate et completvdine a vocabvlario statvendo incepit: systema firmvm est si $\Gamma \vdash \varphi \Rightarrow \Gamma \models \varphi$ , et completvm si conversvm valet, tribvs gradibvs (debilis, pro praemissis finitis et fortis). Argvmentvm circvlare dissolvit qvod completvdinem «per firmitatem» obtinere contendit transevndo a $\nvdash \chi$ ad $\not\models \chi$ , qvae illatio contrapositio est completvdinis debilis, et ostendit dvas proprietates inter se independentes esse. Deinde demonstravit omnem instantiam axiomatvm A1, A2 et A3 validam esse, aestimationem svpponendo qvae eam refvtaret et per versvm falsvm implicationis ad valores impossibiles perveniendo; et, per indvctionem fortem in nvmero versvvm, firmitatem, cvm casv pro axiomatibvs, altero pro praemissis, modo ponente semantico et, pro regvla svbstitvtionis dvplicis negationis, aeqvivalentia $\theta \eqsem \neg\neg\theta$ cvm theoremate svbstitvtionis semanticae. Proprietas qvae a versv ad versvm transmittitvr non est validitas, sed satisfactio ab aestimatione fixa qvae praemissis satisfacit, et ideo firmitas cvm praemissis valet, etiam infinitis. Ex ea secvtae svnt consistentia omnis classis satisfactibilis, praesertim systematis ipsivs, et methodvs qvae vnitati de dedvctione deerat: exemplar contrarivm demonstrat dedvctionem non esse.

Kalmár et completvdo finita

Eadem lectio conversvm dvabvs partibvs demonstravit. Prima est lemma Kalmarii: si variabiles formvlae $\varphi$ inter $u_{1}, \ldots, u_{n}$ svnt, tvm $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ pro omni aestimatione $v$ , vbi $\psi^{v}$ est $\psi$ si $v(\psi) = 1$ et $\neg\psi$ aliter; systema ex qvoqve versv dedvcit qvod versvs de formvla dicit. Eivs indvctio in complexitate vnicvm casvm compositvm habet, $(\alpha \downarrow \beta)$ , qvia negatio conivncta vnicvs connectivvs primitivvs est, et intra evm tres svbcasvs, qvi dvo lemmata systematis poscvnt, altervm dvabvs formis: $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ , dedvctvm cvm introdvctione conivnctionis, dvplici negatione et dvabvs applicationibvs regvlae SDN, et $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ et $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , dedvcta cvm introdvctione disivnctionis. Altera pars praemissas tollit: si $\varphi$ tavtologia est, ex praemissis cvivsqve ex $2^{n}$ versibvs dedvcitvr, et demonstratio per casvs litterale vltimae variabilis tollit, deinde paenvltimae, donec ad $\vdash \varphi$ perveniatvr, completvdinem debilem. Theoremate dedvctionis semantico et converso syntactici, completvdo ad praemissas finitas extensa est; vnde, praemissis finitis, dedvctio et conseqventia congrvvnt, aeqvivalentia demonstrabilis cvm semantica congrvit et dedvcibilitas decidibilis est, qvia tabvla pro ea respondet.

Compactitas et completvdo fortis

Lectio de theoremate compactitatis casvm infinitvm aggressa est, qvem lemma Kalmarii non attingit, qvia infinitae praemissae in implicationem exonerari non possvnt. Demonstravit, nvlla dedvctione memorata, classem satisfactibilem esse si et solvm si qvaeqve eivs svbclassis finita satisfactibilis est. Series valorvm pro $v_{1}, \ldots, v_{n}$ bona est si omnis svbclassis finita classis ab aliqva aestimatione satisfit qvae eam prolongat; lemma dvorvm testivm confirmat seriem bonam in bonam prolongari, qvia, si nevtra ex dvabvs prolongationibvs bona esset, vnio dvorvm testivm finitorvm repvgnaret seriei bonae; et aestimatio qvae oritvr si semper valor $1$ praefertvr cvm fieri potest omni formvlae satisfacit, per lemma coincidentiae, qvia qvaeqve formvla finitas variabiles habet. Constrvctio axiomate electionis non eget, qvia variabiles nvmeratae svnt et qvaeqve operatio regvlam habet. Ex compactitate secvtae svnt eivs formae aeqvivalentes, forma insatisfactibilitatis et forma conseqventiae; ex hac, ex completvdine pro praemissis finitis et ex monotonia, completvdo fortis; et ex hac et ex firmitate, congrventia plena: $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ pro omni $\Gamma$ , et classis consistens est si et solvm si satisfactibilis est. Lectio monvit hvnc ordinem non esse rem arbitrii: compactitatem ex completvdine forti nondvm praesto obtinere circvlare esset. Finem fecit in coloratione graphorvm nvmerabilivm, qvae problema infinitvm in classem formvlarvm vertit cvivs partes finitae satisfactibiles svnt, et in finibvs eorvm qvae classis formvlarvm exprimere potest.

Resolvtio

Lectio de methodo resolvtionis classes formvlarvm classibvs clavsvlarvm svbstitvit, qvaeqve clavsvla classis finita litteralivm, cvm dvabvs repraesentationibvs: forma clavsvlari, qvae eadem exemplaria habet, et forma definitionali, qvae variabilem novam pro qvaqve svbscriptvra composita introdvcit, solam satisfactibilitatem servat et vt formvla crescit, non vt potentia binarii. Vnica regvla in clavsvlas agit: ex $C$ et $D$ , cvm $\ell \in C$ et $\ell^{*} \in D$ , infertvr $(C \setminus \{\ell\}) \cup (D \setminus \{\ell^{*}\})$ , et refvtatio est derivatio qvae ad $\Box$ pervenit. Firmitas vt systematis demonstrata est, per indvctionem in derivatione et cvm resolvente vt conseqventia praemissarvm svarvm; completvdo refvtationis, per indvctionem in nvmero variabilivm, cvm eliminatione variabilis, qvae satisfactibilitatem servat et cvivs demonstratio exemplar constrvit; et pro classibvs infinitis, rvrsvs cvm compactitate. Secvtvm est $\Gamma \models \varphi$ si et solvm si forma clavsvlaris formvlae $\Gamma \cup \{\neg\varphi\}$ refvtationem habet, et satvrationem, finitam qvia cvm $n$ variabilibvs non plvres qvam $4^{n}$ clavsvlae svnt, satisfactibilitatem sine tabvlis decernere. Lectio problema satisfactibilitatis praebvit, cvivs pretivm in casv pessimo nemo novit, et dvos casvs qvi celeriter decernvntvr, clavsvlas Hornianas et clavsvlas dvorvm litteralivm.

Figvra seqvens qvattvor segmenta in vnam catenam colligit. Qvisqve nodvs colvmnae effectvs est, secvndvm ordinem logicvm nvmeratvs et arcv ivnctvs cvm anvlis prioribvs qvibvs eivs demonstratio vtitvr; circa eos fvlcra flvitant, id est principia et instrvmenta ad qvae catena itervm atqve itervm recvrrit, qvodqve linea continva ivnctvm cvm anvlis qvi in eo nitvntvr et linea pvnctata cvm anvlo vbi statvitvr, praeter ea qvae ex vnitatibvs prioribvs venivnt, qvae vt armillae pingvntvr. Fvlcro pvlsato omnes anvli qvi eo vtvntvr illvstrantvr, et qvisqve anvlvs ad lectionem refert in qva demonstratvr. Notetvr firmitatem et compactitatem, alteram in primo segmento, alteram in tertio statvtas, in segmentis seqventibvs redire, et fvlcrvm vnitatis saepissime visitatvm esse aestimationes et coincidentiam, qvas indvctio seqvitvr, tribvs svis formis: in versibvs dedvctionis, in complexitate formvlae et in nvmero variabilivm classis clavsvlarvm.

Fvlcra catenae

AIndvctio et recvrsio. Indvctio fortis in nvmeris natvralibvs, indvctio in complexitate formvlarvm, cvm vnico casv composito $(\alpha \downarrow \beta)$ , et definitio per recvrsionem. In prima vnitate demonstratae svnt. In hac vnitate sine demonstratione admittitvr.
BSystema cvrsvs. A1, A2 et A3, modvs ponens et regvla SDN; reflexivitas, monotonia, modvs ponens inter dedvctiones, finitas et $\Gamma \cup \{\varphi\} \vdash \psi \Leftrightarrow \Gamma \vdash (\varphi \rightarrow \psi)$ . In secvnda vnitate statvta svnt. In hac vnitate sine demonstratione admittitvr.
CArtes derivatae. Dvplex negatio, ex lectione de qvattvor artibvs; introdvctio conivnctionis et disivnctionis et demonstratio per casvs (si $\Gamma \cup \{\psi\} \vdash \chi$ et $\Gamma \cup \{\neg\psi\} \vdash \chi$ , tvm $\Gamma \vdash \chi$ ), ex lectione de artibvs logicae classicae. In secvnda vnitate demonstratae svnt. In hac vnitate sine demonstratione admittitvr.
DAestimationes et coincidentia. $v((\alpha \downarrow \beta)) = (1 - v(\alpha))(1 - v(\beta))$ ; si dvae aestimationes in $V(\varphi)$ consentivnt, formvlae $\varphi$ evndem valorem dant; validitas $2^{n}$ versibvs decernitvr. In tertia vnitate demonstrata svnt. In hac vnitate sine demonstratione admittitvr.
EConseqventia semantica. Versvs falsvs implicationis, monotonia, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , $\Gamma \models \varphi$ si et solvm si $\Gamma \cup \{\neg\varphi\}$ insatisfactibilis est, et theorema svbstitvtionis semanticae. In tertia vnitate demonstrata svnt. In hac vnitate sine demonstratione admittitvr.
FFormae conivnctivae. Lemma valoris; omnis formvla formae normali conivnctivae aeqvivalet, qvae $2^{n}$ clavsvlis egere potest; disivnctio litteralivm valida est si et solvm si par complementarivm continet. In tertia vnitate demonstrata svnt. In hac vnitate sine demonstratione admittitvr.
GFirmitas. Si $\Gamma \vdash \varphi$ , tvm $\Gamma \models \varphi$ , pro omni classe $\Gamma$ ; exemplar contrarivm demonstrat dedvctionem non esse. Constitvitvr in: 2. Firmitas.
HCompactitas. Classis formvlarvm satisfactibilis est si et solvm si omnis eivs svbclassis finita satisfactibilis est; vnde qvod insatisfactibile est iam in parte finita tale est. Constitvitvr in: 11. Theorema compactitatis.

Segmentvm 1 Firmitas
- Comprobare omnem instantiam schematvm validam esse sine eivs tabvla constrvenda.
- Firmitatem per indvctionem fortem in nvmero versvvm demonstrare, cvm casv regvlae svbstitvtionis dvplicis negationis.
- Exemplari contrario demonstrare formvlam non dedvci, et consistentiam ex firmitate obtinere.
1. Validitas axiomatvm. Omnis instantia axiomatvm A1, A2 et A3 valida est: aestimatio qvae eam refvtaret, per versvm falsvm implicationis, valores impossibiles postvlaret.
  Nititvr: E (Conseqventia semantica). Demonstratvr in: Firmitas et completvdo.
2. Firmitas. Si $\Gamma \vdash \varphi$ , tvm $\Gamma \models \varphi$ , pro omni $\Gamma$ : per indvctionem fortem in nvmero versvvm, cvm casv pro axiomatibvs, altero pro praemissis, modo ponente semantico et, pro regvla SDN, $\theta \eqsem \neg\neg\theta$ cvm svbstitvtione semantica.
  Vtitvr: 1. Validitas axiomatvm. Nititvr: A (Indvctio et recvrsio), B (Systema cvrsvs), E (Conseqventia semantica). Demonstratvr in: Firmitas et completvdo.
3. Consistentia et exemplaria contraria. Omnis classis satisfactibilis consistens est; systema consistens est et $\nvdash v_{1}$ ; si aestimatio formvlis $\Gamma$ satisfacit et $\varphi$ refvtat, tvm $\Gamma \nvdash \varphi$ , et tabvla testatvr qvod validvm non est theorema non esse.
  Nititvr: G (Firmitas), D (Aestimationes et coincidentia). Demonstratvr in: Firmitas et completvdo.
Segmentvm 2 Kalmár et completvdo finita
- Dvo lemmata negationis conivnctae in systemate dedvcere, cvm regvla svbstitvtionis dvplicis negationis vbi opvs est.
- Lemma Kalmarii per indvctionem in complexitate demonstrare, cvm vnico casv composito.
- Demonstratione per casvs praemissas versvvm tollere, et praemissas finitas dvobvs theorematibvs dedvctionis exonerare.
- Tabvla dedvcibilitatem, aeqvivalentiam demonstrabilem et consistentiam ex praemissis finitis decernere.
1. Introdvctio negationis conivnctae. $\{\neg\alpha, \neg\beta\} \vdash (\alpha \downarrow \beta)$ et $\vdash (\neg\alpha \rightarrow (\neg\beta \rightarrow (\alpha \downarrow \beta)))$ : conivnctio negationvm est $\neg\neg(\neg\neg\alpha \downarrow \neg\neg\beta)$ ; dvplex negatio exteriorem tollit, et regvla SDN dvas interiores.
  Nititvr: B (Systema cvrsvs), C (Artes derivatae). Demonstratvr in: Firmitas et completvdo.
2. Negatio negationis conivnctae. $\vdash (\alpha \rightarrow \neg(\alpha \downarrow \beta))$ et $\vdash (\beta \rightarrow \neg(\alpha \downarrow \beta))$ , qvia $\neg(\alpha \downarrow \beta)$ est $(\alpha \vee \beta)$ et introdvctio disivnctionis svfficit.
  Nititvr: B (Systema cvrsvs), C (Artes derivatae). Demonstratvr in: Firmitas et completvdo.
3. Lemma Kalmarii. Si $V(\varphi) \subseteq \{u_{1}, \ldots, u_{n}\}$ , tvm $\{u_{1}^{v}, \ldots, u_{n}^{v}\} \vdash \varphi^{v}$ pro omni aestimatione $v$ ; gradvs indvctivvs vnicvm casvm habet, $(\alpha \downarrow \beta)$ , cvm tribvs svbcasibvs secvndvm valores formvlarvm $\alpha$ et $\beta$ .
  Vtitvr: 4. Introdvctio negationis conivnctae, 5. Negatio negationis conivnctae. Nititvr: A (Indvctio et recvrsio), D (Aestimationes et coincidentia), B (Systema cvrsvs). Demonstratvr in: Firmitas et completvdo.
4. Completvdo debilis. Si $\models \varphi$ , tvm $\vdash \varphi$ : lemma Kalmarii $\varphi$ ex qvoqve versv dedvcit, et demonstratio per casvs litteralia ab vltima variabili ad primam tollit, cvm $2^{n}$ vsibvs lemmatis et $2^{n} - 1$ demonstrationis per casvs.
  Vtitvr: 6. Lemma Kalmarii. Nititvr: C (Artes derivatae). Demonstratvr in: Firmitas et completvdo.
5. Completvdo pro praemissis finitis. $\{\gamma_{1}, \ldots, \gamma_{k}\} \models \varphi \Rightarrow \{\gamma_{1}, \ldots, \gamma_{k}\} \vdash \varphi$ : theorema dedvctionis semanticvm ad tavtologiam dvcit, completvdo debilis eam dedvcit et conversvm theorematis dedvctionis praemissas reddit.
  Vtitvr: 7. Completvdo debilis. Nititvr: E (Conseqventia semantica), B (Systema cvrsvs). Demonstratvr in: Firmitas et completvdo.
6. Congrventia finita et decisio. Pro $\Gamma$ finita, $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ , et $\varphi \dashv\vdash \psi \Leftrightarrow \varphi \eqsem \psi$ ; vnde dedvcibilitas ex praemissis finitis decidibilis est, per tabvlam.
  Vtitvr: 8. Completvdo pro praemissis finitis. Nititvr: G (Firmitas), D (Aestimationes et coincidentia). Demonstratvr in: Firmitas et completvdo.
Segmentvm 3 Compactitas et completvdo fortis
- Compactitatem demonstrare valores variabilivm singillatim figendo, cvm invariante seriervm bonarvm et argvmento dvorvm testivm.
- Inter formam satisfactibilitatis, formam insatisfactibilitatis et formam conseqventiae transire.
- Completvdinem fortem ex compactitate obtinere, sine circvlo, et ex ea congrventiam consistentiae cvm satisfactibilitate.
- Problemata de obiectis infinitis in classes formvlarvm transferre et compactitate solvere.
1. Lemma dvorvm testivm. Si series $s$ valorvm fixorvm bona est (omnis svbclassis finita classis ab aestimatione satisfit qvae eam prolongat), etiam $(s, 1)$ vel $(s, 0)$ bona est: si nevtra esset, vnio dvorvm testivm finitorvm repvgnaret seriei $s$ bonae.
  Nititvr: D (Aestimationes et coincidentia). Demonstratvr in: Theorema compactitatis.
2. Theorema compactitatis. $\Gamma$ satisfactibilis est si et solvm si omnis svbclassis finita est: $v_{n + 1}$ figitvr in $1$ si $(s_{n}, 1)$ bona est et in $0$ aliter, et aestimatio qvae oritvr omni formvlae satisfacit per lemma coincidentiae. Axiomate electionis non est opvs, qvia variabiles nvmeratae svnt.
  Vtitvr: 10. Lemma dvorvm testivm. Nititvr: A (Indvctio et recvrsio), D (Aestimationes et coincidentia). Demonstratvr in: Theorema compactitatis.
3. Formae aeqvivalentes. $\Gamma$ insatisfactibilis est si et solvm si aliqva pars finita est; $\Gamma \models \varphi$ si et solvm si $\Gamma_{0} \models \varphi$ pro aliqva $\Gamma_{0} \subseteq \Gamma$ finita; et haec vltima forma vicissim theorema implicat.
  Vtitvr: 11. Theorema compactitatis. Nititvr: E (Conseqventia semantica). Demonstratvr in: Theorema compactitatis.
4. Completvdo fortis. Si $\Gamma \models \varphi$ , tvm $\Gamma \vdash \varphi$ , pro omni $\Gamma$ : forma conseqventiae $\Gamma_{0}$ finitam dat, completvdo pro praemissis finitis $\Gamma_{0} \vdash \varphi$ dat, et monotonia $\Gamma \vdash \varphi$ .
  Vtitvr: 8. Completvdo pro praemissis finitis, 12. Formae aeqvivalentes. Nititvr: B (Systema cvrsvs). Demonstratvr in: Theorema compactitatis.
5. Dedvctio est conseqventia. $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ pro omni $\Gamma$ ; theoremata svnt exacte tavtologiae, et classis consistens est si et solvm si satisfactibilis est.
  Vtitvr: 13. Completvdo fortis. Nititvr: G (Firmitas). Demonstratvr in: Theorema compactitatis.
6. Coloratio graphorvm nvmerabilivm. Variabili $x_{i,c}$ pro qvoqve vertice et colore, et formvlis qvae dicvnt qvemqve verticem vnvm colorem et vnvm tantvm habere et vicinos differre, graphvs nvmerabilis colorationem $k$ coloribvs admittit si omnis svbgraphvs finitvs eam admittit.
  Nititvr: H (Compactitas), F (Formae conivnctivae). Demonstratvr in: Theorema compactitatis.
Segmentvm 4 Resolvtio
- Classem formvlarvm vt classem clavsvlarvm repraesentare, per formam conivnctivam vel per definitionalem.
- Refvtationes constrvere sine dvobvs paribvs complementariis vna illatione tollendis.
- Firmitatem et completvdinem refvtationis resolvtionis demonstrare, pro classibvs finitis et, cvm compactitate, pro qvibvslibet.
- Conseqventias per satvrationem decernere et casvs agnoscere qvi celeriter decernvntvr.
1. Forma clavsvlaris. Clavsvla est classis finita litteralivm, qvae satisfit si aliqvod litterale valorem $1$ accipit, et $\Box$ insatisfactibilis est; forma clavsvlaris formvlae $\Gamma$ eadem exemplaria habet, et $\Gamma \models \varphi$ si et solvm si forma clavsvlaris formvlae $\Gamma \cup \{\neg\varphi\}$ insatisfactibilis est.
  Nititvr: F (Formae conivnctivae), E (Conseqventia semantica). Demonstratvr in: Methodvs resolvtionis.
2. Forma clavsvlaris definitionalis. Variabili nova pro qvaqve svbscriptvra et eivs clavsvlis definitionis, $T(\varphi)$ aeqve satisfactibilis est ac $\varphi$ et habet ad svmmvm $4k + 1$ clavsvlas ad svmmvm trivm litteralivm; formae definitionales conseqventiam ex praemissis finitis decernvnt.
  Vtitvr: 16. Forma clavsvlaris. Nititvr: A (Indvctio et recvrsio), D (Aestimationes et coincidentia). Demonstratvr in: Methodvs resolvtionis.
3. Firmitas resolvtionis. $\{C, D\} \models R_{\ell}(C, D)$ , per casvs in valore $\ell$ ; per indvctionem fortem in derivatione, $S \models C$ pro omni clavsvla $C$ ex $S$ derivata, et si $S$ refvtationem habet, insatisfactibilis est.
  Vtitvr: 16. Forma clavsvlaris. Nititvr: A (Indvctio et recvrsio). Demonstratvr in: Methodvs resolvtionis.
4. Eliminatio variabilis. $E_{p}(S)$ , qvae clavsvlas sine $p$ et sine $\neg p$ servat et resolventes in $p$ addit, $p$ non continet et aeqve satisfactibilis est ac $S$ ; ex eivs exemplari exemplar classis $S$ obtinetvr eligendo valorem $p$ .
  Vtitvr: 18. Firmitas resolvtionis. Nititvr: D (Aestimationes et coincidentia). Demonstratvr in: Methodvs resolvtionis.
5. Completvdo refvtationis finita. Omnis classis finita insatisfactibilis clavsvlarvm refvtationem habet, per indvctionem in nvmero variabilivm: vltima eliminatvr et praemissae cvivsqve resolventis inservntvr.
  Vtitvr: 19. Eliminatio variabilis. Nititvr: A (Indvctio et recvrsio). Demonstratvr in: Methodvs resolvtionis.
6. Completvdo refvtationis. Classis clavsvlarvm, finita vel infinita, insatisfactibilis est si et solvm si refvtationem habet; vnde $\Gamma \models \varphi$ si et solvm si forma clavsvlaris classis $\Gamma \cup \{\neg\varphi\}$ refvtationem habet.
  Vtitvr: 16. Forma clavsvlaris, 18. Firmitas resolvtionis, 20. Completvdo refvtationis finita. Nititvr: H (Compactitas). Demonstratvr in: Methodvs resolvtionis.
7. Satvratio decernit. Cvm $n$ variabilibvs, classis clavsvlarvm derivatarvm ad svmmvm $4^{n}$ elementa habet; satvratio finitvr et satisfactibilitatem sine tabvlis decernit, qvamqvam non semper celerivs qvam illae.
  Vtitvr: 18. Firmitas resolvtionis, 20. Completvdo refvtationis finita. Demonstratvr in: Methodvs resolvtionis.

Finis cvrsvs. Catena ibi finitvr vbi dvae facies cvrsvs vt vna relatio agnoscvntvr et methodvs ad eam decernendam praesto est. Qvod apertvm manet iam non est qvaestio de logica propositionali, sed de eivs pretio et de eivs extensione ad qvantificatores.