Ad argvmentvm transi
Topos Uranos
Latine

Conseqventia et aeqvivalentia semanticae

Svmmarivm

Haec lectio a valore veritatis formvlae ad relationes inter formvlas transit. Conseqventiam semanticam ex classe praemissarvm, finita vel infinita, definit et lectiones signi conseqventiae accvrate statvit, etiam eam negationis eivs, qvae dicit aliqvid non esse validvm, non avtem esse contradictorivm. Valores connectivorvm vt polynomia scriptos adhibet, qvo fit vt verificatio legis in calcvlvm vertatvr, et proprietates strvctvrales conseqventiae (reflexivitatem, monotoniam, sectionem et transitivitatem), theorema dedvctionis semanticvm et redvctionem conseqventiae ad insatisfactibilitatem demonstrat, cvi methodvs resolvtionis innitetvr. Deinde aeqvivalentiam semanticam definit, ostendit eam esse relationem aeqvivalentiae qvae cvm conseqventia mvtva et cvm validitate implicationis dvplicis congrvit, et per indvctionem secvndvm complexitatem dvo theoremata demonstrat qvibvs cvm ea laborari potest: svbstitvtionem occvrrentiae svbformvlae per aliam aeqvivalentem et svbstitvtionem vniformem variabilivm per formvlas. His adhibitis catalogvm legvm cvm nominibvs rectis constitvit et formvlas per catenas aeqvivalentiarvm simplificat, sine tabvlis veritatis.

Proposita discendi

  1. Diivdicare vtrvm formvla conseqventia semantica sit classis formvlarvm, finitae vel infinitae, aestimationem exhibendo qvae eam refvtet vel demonstrando nvllam exstare.
  2. Proprietates conseqventiae, theorema dedvctionis semanticvm et redvctionem conseqventiae ad insatisfactibilitatem demonstrare et adhibere.
  3. Aeqvivalentias semanticas per tabvlas veritatis, per calcvlvm cvm valoribvs et per catenas aeqvivalentiarvm constitvere, singvlas leges recte nominando.
  4. Theorema svbstitvtionis semanticae et theorema svbstitvtionis vniformis per indvctionem secvndvm complexitatem demonstrare, et distingvere qvando vtrvmqve adhibeatvr.

Qvae ex lectione priore adhibentvr

Lectio de semantica logicae propositionalis formvlis significationem dedit, et haec lectio eam pro nota habet. Aestimatio est fvnctio v ⁣:V→{0,1}v\colon V \to \{0, 1\}, qvae cviqve variabili valorem veritatis attribvit, 11 (vervm) vel 00 (falsvm). Per theorema definitionis per recvrsionem in formvlis, ex lectione de indvctione, qvaeqve aestimatio vno tantvm modo ad omnes formvlas extenditvr per clavsvlam negationis conivnctae, qvae sola necessaria est, qvia lingva vnvm tantvm connectivvm habet:

v((φ↓ψ))=1  ⇔  v(φ)=0,    v(ψ)=0v((\varphi \downarrow \psi)) = 1 \;\Leftrightarrow\; v(\varphi) = 0, \;\; v(\psi) = 0

Propter vnicitatem extensionis, v(φ)v(\varphi) etiam pro valore extensionis scribitvr; littera vv sine indice semper aestimationem designat (et v′v', ww, uu alias), variabiles avtem semper indicem svvm fervnt. Vt in lectione de formalizatione, pp, qq, rr, ss et tt variabiles v1v_1 ad v5v_5 nominant, et V(φ)V(\varphi) est classis variabilivm formvlae φ\varphi. Dicitvr vv formvlam φ\varphi satisfacere, et scribitvr v⊨φv \models \varphi, cvm v(φ)=1v(\varphi) = 1, et eam refvtare, v⊭φv \not\models \varphi, cvm v(φ)=0v(\varphi) = 0. Formvla est valida (vel tavtologia), et scribitvr ⊨φ\models \varphi, si omnis aestimatio eam satisfacit; satisfactibilis, si aliqva eam satisfacit; insatisfactibilis (vel contradictio), si nvlla eam satisfacit; contingens, si satisfactibilis est neqve valida. Aestimatio classem Γ\Gamma formvlarvm satisfacit, v⊨Γv \models \Gamma, cvm singvlas eivs formvlas satisfacit, et Γ\Gamma est satisfactibilis si aliqva aestimatio eam satisfacit, insatisfactibilis si nvlla. Postremo ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) et ⊥:=¬⊤\bot := \neg\top, ita vt v(⊤)=1v(\top) = 1 et v(⊥)=0v(\bot) = 0 pro omni aestimatione.

Ex illa lectione praeterea dvo eventa adhibentvr. Primvm est lemma coincidentiae: si dvae aestimationes in variabilibvs formvlae φ\varphi congrvvnt, in φ\varphi congrvvnt; ex eo valor formvlae cvm nn variabilibvs a 2n2^{n} tantvm combinationibvs pendet, eivsqve tabvla veritatis finita est. Altervm est theorema de valoribvs connectivorvm derivatorvm, qvod ex abbreviationibvs statvtis valorem cvivsqve connectivi vt polynomivm in valoribvs partivm compvtat. Si a=v(φ)a = v(\varphi) et b=v(ψ)b = v(\psi):

v(¬φ)=1−a,v((φ∨ψ))=a+b−ab,v((φ∧ψ))=abv(\neg\varphi) = 1 - a, \qquad v((\varphi \vee \psi)) = a + b - ab, \qquad v((\varphi \wedge \psi)) = ab
v((φ→ψ))=1−a(1−b),v((φ↔ψ))=ab+(1−a)(1−b),v((φ⊻ψ))=a+b−2abv((\varphi \rightarrow \psi)) = 1 - a(1 - b), \qquad v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b), \qquad v((\varphi \veebar \psi)) = a + b - 2ab

Demonstrationes hvivs lectionis fere omnes in valoribvs veritatis comparandis consistvnt, et haec polynomia sinvnt id calcvlo fieri pro casvvm percvrsione. Sola eorvm regvla addita est 00 et 11 solos nvmeros esse qvi cvm qvadrato svo congrvvnt: si xx valet 00 vel 11, tvm x2=xx^{2} = x et x(1−x)=0x(1 - x) = 0. Praeterea expedit tres alias scriptvras eorvndem valorvm in promptv habere, qvae prodvctis evolvendis obtinentvr:

v((φ↓ψ))=(1−a)(1−b),v((φ∨ψ))=1−(1−a)(1−b),v((φ↔ψ))=1−a−b+2abv((\varphi \downarrow \psi)) = (1 - a)(1 - b), \qquad v((\varphi \vee \psi)) = 1 - (1 - a)(1 - b), \qquad v((\varphi \leftrightarrow \psi)) = 1 - a - b + 2ab

Prima est clavsvla negationis conivnctae (prodvctvm ex 1−a1 - a et 1−b1 - b valet 11 exacte cvm a=b=0a = b = 0); secvnda dicit disivnctionem valere 00 tantvm si ambae partes valent 00; tertia, implicationem dvplicem valere 11 si a=ba = b (qvia 1−2a+2a2=11 - 2a + 2a^{2} = 1) et 00 si a≠ba \neq b (qvia tvm a+b=1a + b = 1 et ab=0ab = 0).