Ad argvmentvm transi
Topos Uranos
Latine

Theorema compactitatis

Svmmarivm

Dedvctio est series finita et finito tantvm praemissarvm nvmero vtitvr; satisfactio avtem classis infinitae formvlarvm vnam aestimationem postvlat qvae valorem 11 infinitis formvlis simvl tribvat, neqve qvicqvam in eivs definitione dicit satis esse partes finitas examinare. Theorema compactitatis affirmat satis esse: classis formvlarvm satisfactibilis est si et solvm si qvaeqve eivs svbclassis finita satisfactibilis est. Haec lectio id argvmento semantico directo demonstrat, non per dedvctionem: valores variabilivm v1,v2,…v_1, v_2, \ldots singillatim statvvntvr, et in singvlis operationibvs invarians servatvr, scilicet omnem svbclassem finitam classis adhvc satisfactibilem esse aestimatione qvae iam statvta observet; si nevtra ex dvabvs electionibvs possibilibvs id servaret, vnio dvorvm testivm finitorvm hvivs defectvs invarianti priori repvgnaret, et in fine qvaeqve formvla per lemma coincidentiae satisfit, qvia finitvm variabilivm nvmervm habet. Cvm variabiles nvmeratae sint, constrvctio axiomate electionis non eget. Ex compactitate formae eivs aeqvivalentes seqvvntvr (classis insatisfactibilis est si et solvm si aliqva pars eivs finita est; formvla est conseqventia classis si et solvm si est conseqventia alicvivs partis finitae) et, cvm completvdine pro praemissis finitis lectionis prioris, completvdo fortis: Γ⊨φ\Gamma \models \varphi implicat Γ⊢φ\Gamma \vdash \varphi pro omni classe Γ\Gamma, vnde dedvctio et conseqventia semantica semper congrvvnt. Lectio applicationibvs combinatoriis clavditvr: coloratione graphorvm infinitorvm ex colorationibvs partivm eorvm finitarvm, terminis finitis qvi in envntiatis infinitis latent, et finibvs eorvm qvae classis formvlarvm exprimere potest.

Proposita discendi

  1. Classes finite satisfactibiles definire et theorema compactitatis per valores variabilivm deinceps statvtos demonstrare, mvnvs invariantis, argvmenti dvorvm testivm et lemmatis coincidentiae exponendo, et cvr constrvctio axiomate electionis non egeat.
  2. Formas aeqvivalentes compactitatis, formam insatisfactibilitatis et formam conseqventiae, envntiare, demonstrare et adhibere, et ab vnaqvaqve ad ceteras transire.
  3. Completvdinem fortem ex compactitate, ex completvdine pro praemissis finitis et ex monotonia dedvcere, et ex ea congrventiam dedvctionis cvm conseqventia semantica et consistentiae cvm satisfactibilitate derivare.
  4. Qvaestiones combinatorias de classibvs infinitis (colorationes, ordines, copvlationes) in classibvs formvlarvm codice describere et per compactitatem solvere, distingvendo qvid theorema praestet et qvid non praestet.

Qvae ex lectionibvs prioribvs adhibentvr

Haec lectio fere tota in semantica versatvr, et ex ea haec adhibet. Aestimatio est fvnctio v ⁣:V→{0,1}v\colon V \to \{0, 1\} in classe VV variabilivm v1,v2,v3,…v_1, v_2, v_3, \ldots, qvae vno tantvm modo ad omnes formvlas extenditvr; aestimatio classem Γ\Gamma formvlarvm satisfacit, v⊨Γv \models \Gamma, si valorem 11 singvlis eivs formvlis tribvit, et Γ\Gamma est satisfactibilis si aliqva aestimatio eam satisfacit, insatisfactibilis si nvlla. Haec omnia in lectione de semantica logicae propositionalis invenivntvr, vna cvm instrvmento hvivs lectionis praecipvo, lemmate coincidentiae: si dvae aestimationes in variabilibvs formvlae φ\varphi congrvvnt, qvae classem finitam V(φ)V(\varphi) efficivnt, evndem valorem formvlae φ\varphi tribvvnt.

Ex lectione de conseqventia et aeqvivalentia semanticis adhibentvr definitio relationis Γ⊨φ\Gamma \models \varphi (omnis aestimatio qvae Γ\Gamma satisfacit φ\varphi satisfacit), proprietates eivs strvctvrales, praesertim monotonia (si Γ⊆Δ\Gamma \subseteq \Delta et Γ⊨φ\Gamma \models \varphi, tvm Δ⊨φ\Delta \models \varphi) et qvinta (classis insatisfactibilis omnem formvlam pro conseqventia habet), et theorema de conseqventia et insatisfactibilitate: Γ⊨φ\Gamma \models \varphi si et solvm si Γ∪{¬φ}\Gamma \cup \{\neg\varphi\} insatisfactibilis est. Ex lectione de legibvs De Morgani et legibvs distribvtivis generalibvs adhibetvr lemma valoris: ⋀i=1nφi\bigwedge_{i=1}^{n} \varphi_i valet 11 si et solvm si omnes eivs termini valent 11, et ⋁i=1nφi\bigvee_{i=1}^{n} \varphi_i, si et solvm si aliqvis valet 11. Postremo, ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) tavtologia est et ⊥:=¬⊤\bot := \neg\top contradictio.

Ex parte dedvctionis, lectio de systematibvs dedvctivis formalibvs monotoniam demonstravit (Mon: si Γ⊆Δ\Gamma \subseteq \Delta et Γ⊢φ\Gamma \vdash \varphi, tvm Δ⊢φ\Delta \vdash \varphi) et finitatem (Fin: si Γ⊢φ\Gamma \vdash \varphi, aliqva svbclassis finita Γ0\Gamma_0 classis Γ\Gamma efficit vt Γ0⊢φ\Gamma_0 \vdash \varphi), et lectio de qvattvor artibvs dedvctionis comprobavit vtramqve valere in systemate cvrsvs (schematibvs A1, A2 et A3, modo ponente et svbstitvtione dvplicis negationis, SDN), ad qvod signvm ⊢\vdash posthac refertvr. Deniqve lectio de firmitate et completvdine theorema firmitatis demonstravit (Γ⊢φ\Gamma \vdash \varphi implicat Γ⊨φ\Gamma \models \varphi, pro omni Γ\Gamma) et completvdinem pro praemissis finitis: si {γ1,…,γk}⊨φ\{\gamma_1, \ldots, \gamma_k\} \models \varphi, tvm {γ1,…,γk}⊢φ\{\gamma_1, \ldots, \gamma_k\} \vdash \varphi.