FORMALIZZAZIONE DELL'ASSIOMATICA DI ADRIANO53s
===============================================================================
0. PRINCIPIO DI LETTURA
Il sistema distingue tre piani:
(a)
coerenza interna di una struttura concettuale;
(b) necessita' ontologica di
cio' che la struttura nomina;
(c) dimostrabilita' formale di tale necessita'.
La formalizzazione non dimostra Dio dal pensiero. Mostra quali conseguenze
seguono se valgono le premesse fondative.
Nucleo: contingenza ->
fondazione -> Assoluto
domanda di essere ricevuto -/-> ricezione
Lo
scarto non si chiude da se'. La domanda e' rivolta dal relativo
all'Assoluto.
La ricezione, se c'e', non e' conquista del relativo, ma atto
dell'Assoluto.
===============================================================================
1. ARCHITETTURA A DUE STADI
Tesi (da v2.2): l'Assoluto non e' un ente tra
gli enti; il relativo non e'
un Assoluto indebolito. La separazione deve
essere strutturale (sort
disgiunti), non soltanto un predicato su un dominio
comune.
Problema (emerso dall'analisi di v2.2): se i sort sono separati
fin dalla
prima riga, la dimostrazione dell'esistenza dell'Assoluto non puo'
essere
condotta. Parte da un ente contingente e risale a un fondante di cui,
in
partenza, non si sa se sia Assoluto o relativo: il linguaggio non avrebbe
un termine neutro per quel passaggio. Se invece l'Assoluto fosse gia' nel
tipo del fondante, sarebbe presupposto e non dimostrato.
Soluzione:
STADIO I (scoperta, strumentale): dominio neutro En con predicati Ass e
Rel. Serve SOLO come impalcatura dimostrativa. Qui si derivano
l'incompatibilita' Ass/Rel, l'esistenza e l'unicita' di g.
PONTE (sezione
12): si dimostra che, con AS-N, ogni ente e' o Ass o
Rel (esclusivamente) e
che la classificazione e' rigida. Ne
segue che l'Assoluto, una volta
riconosciuto, non appartiene al
dominio del relativo.
STADIO II (teoria,
vincolante): sort A e R disgiunti, firme eterogenee,
regola di eterogeneita'.
E' la formulazione ontologica del
sistema.
Dichiarazione di status: il
dominio En e' un dispositivo metalinguistico di
dimostrazione, non una tesi
ontologica. Un "genere comune ente" compare
solo nell'impalcatura, non nella
teoria. Resta un limite dichiarato: la
traduzione fra i due stadi usa un
dominio comune nel metalinguaggio; chi
rifiuta qualsiasi genere comune, anche
meta-teorico, dovra' leggere lo
Stadio I come analogia e non come univocita'.
Classificazione delle proposizioni:
AX assiomi strutturali; AS assunzioni
metafisiche; AN assunzioni
antropologiche; D definizioni; T teoremi (con le
premesse indicate).
I teoremi dello Stadio II ereditati dallo Stadio I
portano l'apice '.
###############################################################################
PARTE I - STADIO I: SCOPERTA (impalcatura)
###############################################################################
2. LINGUAGGIO (STADIO I)
Logica modale del primo ordine multi-sorted,
a dominio variabile, con
identita', modalita' S5.
Sort: En (enti: e,
f, h); P (fatti: p, q, r); Q (processi: u, v).
Abbreviazioni: forall a phi :=
forall e (Ass(e) -> phi);
forall x phi := forall e (Rel(e) -> phi).
Avvertenza (v2.5): Rel(e) include E(e); quindi 'forall x' nello Stadio I
quantifica sui soli relativi ESISTENTI nel mondo di valutazione. La
quantificazione rigida sul sort R e' forall e (Diamond Rel(e) -> ...).
Operatori: not, and, or, ->, <->, forall, exists, =, Box, Diamond.
Predicato primitivo E(e): non si definisce come exists f (f = e).
E(e) e'
vero in w sse il referente di e appartiene a D(w). I quantificatori
spaziano
sul dominio esterno (unione dei D(w)); E seleziona il dominio interno.
I
predicati relazionali sono veri in w solo di enti esistenti in w (AX3).
Primitivi: F(e,f) fondazione; Fp(e,p) l'ente e fonda il fatto p;
Cr(a,e)
creazione/sostegno; Exp(p,q) spiegazione adeguata;
PrincipioDi(e,f);
Totalizza(B); ex(e); Ver(p); Processo(u);
FondatoDa(u,e);
Caus(e,f) causa
prossima o seconda; Dom(e,a); Accoglie(a,e).
Nota decisiva: Dom(e,a) non
equivale ad Accoglie(a,e).
AX0 (nuovo v2.5). ex : En -> P e Ver(ex(e))
<-> E(e). Nei contesti modali
un fatto p sta per Ver(p); 'E(e)' come
argomento di Exp e' ex(e). (Il
costruttore ex era gia' presupposto da AS2 e
T5 ed e' usato nello Stadio II.)
3. FONDAZIONE (STADIO I)
AX1. not
F(e,e)
AX2. (F(e,f) and F(f,h)) -> F(e,h)
AX3. F(e,f) -> (E(e) and E(f))
AX4. F(e,f) -> Box(E(f) -> E(e))
AX5. Fp(e,p) -> E(e)
D1. Cont_P(p) :=
p and Diamond not p (fatto contingente)
D2. Nec_P(p) := Box p (fatto
necessario)
D3. Dip(e) := exists f F(f,e)
D4. Cont(e) := E(e) and Diamond
not E(e) [= Cont_P(E(e))]
D5. Nec(e) := E(e) and Box E(e) [= Nec_P(E(e))]
D6. Rel(e) := Cont(e) and Dip(e)
D7. Ass(e) := Nec(e) and not Dip(e)
T1. Ass(e) -> not Rel(e)
Dim.: Ass da' Box E(e), Rel da' Diamond not E(e):
incompatibili per
dualita'. (Inoltre Ass richiede not Dip, Rel richiede Dip.)
T2. F(e,f) -> not F(f,e) [da AX1, AX2]
T3. not exists e F(e,e) [AX1]
T4.
F(h,e) and Nec(e) -> Nec(h)
Dim.: AX3 da' E(h); AX4 da' Box(E(e) -> E(h));
con Box E(e) e K, Box E(h).
Nota: usa E come dominio interno (sezione 2).
T4b. Ass(a) -> not exists h F(h,a) [da D7 e D3: banale]
Motivo, nello Stadio
I, della firma dello Stadio II: nessun fondante
dell'Assoluto.
4.
SPIEGAZIONE E FONDAZIONE (STADIO I)
Exp(p,q) -> "esiste un fondante" NON
e' valido in forma globale.
D8. Ult(p) := not exists q Exp(q,p)
AS2.
Cont(e) and Exp(p,E(e)) and Ult(p) -> exists f F(f,e)
AS7. Exp e'
irriflessiva, transitiva e ben fondata (nessuna catena infinita
discendente).
Conseguenza: se Exp(p,q) per qualche p, esiste p* con
Ult(p*) e Exp(p*,q).
5. ESISTENZA DELL'ASSOLUTO (STADIO I)
AS1. Cont_P(p) -> exists q
Exp(q,p).
AS3. Esiste B con Cont_P(B) and Totalizza(B).
Totalizza e' un
predicato UNARIO su P: B e' il fatto che gli enti
contingenti esistenti sono
esattamente quelli che sono. Riguarda le
ENTITA' contingenti, non la
totalita' di tutti i fatti: cosi' si
evita la costante C0 e l'esposizione ai
paradossi di tipo
cantoriano/Russell-Myhill.
AS4. Cont_P(p) -> not
Exp(p,B).
AS5. Exp(p,B) and Ult(p) -> exists e (E(e) and Fp(e,B)).
AS6. F
e' ben fondata: nessuna catena infinita e0, e1, ... con
F(e(i+1), e(i)).
T5. E(e) and not Dip(e) -> Nec(e) [AS1, AS2, AS7]
Dim.: sia not Nec(e):
allora Cont(e) e il fatto E(e) e' contingente. AS1 e
AS7 danno una
spiegazione ultima di E(e); AS2 da' f con F(f,e), cioe'
Dip(e):
contraddizione.
T6. exists a Ass(a) [AS1, AS2, AS3, AS5, AS6, AS7]
Dim.: B contingente (AS3) ha spiegazione (AS1) e spiegazione ultima p*
(AS7).
Per AS5 esiste y con E(y) e Fp(y,B). Sia G = {y} U {h : F(h,y)}.
Se h in G e'
dipendente, esiste h' con F(h',h) e h' in G (AX2); per AS6
G ha un elemento z
con not Dip(z). E(z) (AX3), Nec(z) (T5): Ass(z).
Non e' un argomento
ontologico dal concetto: contingenza -> spiegazione
ultima -> fondamento
necessario e non dipendente. La verita' ontologica
di T6 e' quella delle
premesse.
Nota (v2.5): con AX7 e AX8, se esiste anche un solo relativo,
esiste
gia' un Assoluto (il suo creatore). T6 non e' dunque indipendente dal
blocco creazione. Il suo valore e' mostrare l'esistenza dell'Assoluto
SENZA
presupporre che qualcosa sia creato, a partire dalla sola
contingenza e dal
principio di ragion sufficiente (AS1).
T7. Nec_P(q) and Exp(q,B) and
Cont_P(B) -> not Box(q -> B)
Dim.: Box q e Box(q -> B) darebbero Box B (K),
contro Diamond not B.
Spiegare non e' necessitare. Con AS4, la spiegazione
ultima p* di B e'
non contingente e tuttavia non necessita B.
6.
UNICITA' (STADIO I)
Qual : predicati qualitativi RIGIDI (non menzionano
individui; stessa
definizione della sezione 25, con Ass al posto di A); PP in
Qual: le
perfezioni pure.
D9. StessoProfilo(a,b) := forall Phi in Qual
(Phi(a) <-> Phi(b))
AS8. StessoProfilo(a,b) -> a = b.
AS9. Ass(a) ->
forall Phi in PP Phi(a). (massimalita')
AS10. Ass(a) -> forall Phi in Qual
(Phi(a) -> Phi in PP).
(semplicita' qualitativa)
T8. forall a forall b
((Ass(a) and Ass(b)) -> a = b) [AS8, AS9, AS10]
Dim.: per AS9 e AS10, per
ogni Phi in Qual: Phi(a) <-> Phi in PP, e lo
stesso per b; quindi
StessoProfilo(a,b); AS8 da' a = b.
Corollario: exists! a Ass(a). D10. g :=
l'unico Assoluto (nome lecito solo
dopo T6 e T8).
7. CREAZIONE (STADIO
I)
AX6. Cr(a,e) -> F(a,e)
AX7. Cr(a,e) -> (Ass(a) and Rel(e))
AX8.
Rel(e) -> exists a Cr(a,e)
AX9. Cr(a,e) -> Box(E(e) -> Cr(a,e))
Chiarimento: AX9 rende la creazione essenziale. La contingenza del relativo
e' ESISTENZIALE (puo' non esserci), non RELAZIONALE (nessun mondo in cui
esiste senza essere sostenuto). Non c'e' conflitto con AX15: in un mondo
senza relativi, AX8 e AX9 sono vacuamente veri.
AX15. Diamond not exists x
Rel(x) (assioma modale)
AS-C. Caus(e,f) -> (Rel(e) and Rel(f))
AX16.
PrincipioDi(e,f) -> (E(e) and Rel(f)) [nuovo v2.5]
Un principio (materiale o
altro) e' principio di un relativo;
l'Assoluto non ha principio. Ponte
mancante per la traduzione
di PrincipioDi fra i due stadi.
D11. Creato(e)
:= exists a Cr(a,e)
D12. Creatore(a) := Ass(a) and exists e Cr(a,e)
D13.
ExNihilo(a,e) := Cr(a,e) and not exists h (E(h) and not Dip(h)
and h != a and
PrincipioDi(h,e))
T9. Rel(x) -> F(g,x) [T6, T8]
T10. not exists e
(Creatore(e) and Creato(e)) [T1, AX7]
T11. not exists y Caus(g,y) [T1, AS-C]
8. DOMANDA E RICEZIONE (STADIO I)
D14. Ricevuto(x) := exists a
(Ass(a) and Accoglie(a,x))
AX11. Accoglie(a,x) -> Dom(x,a)
AX12.
Accoglie(a,x) -> (Ass(a) and Rel(x))
AX13. Dom(x,a) -> (Ass(a) and Rel(x))
AN1. Rel(x) -> exists a (Ass(a) and Dom(x,a))
(assunzione antropologica, non
verita' logica)
AN2. Diamond exists x exists a (Dom(x,a) and not
Accoglie(a,x))
T12. Ricevuto(x) -> exists a (Ass(a) and Dom(x,a) and
Accoglie(a,x))
T13. (metateorema) forall x forall a (Dom(x,a) ->
Accoglie(a,x)) non e'
derivabile: vedi modelli M_A e M_B (sezione 11).
T14. Diamond exists x not Ricevuto(x) [AN2, T8, AX13]
Dim.: da AN2, in
qualche w: Dom(x,a), not Accoglie(a,x); per AX13 Ass(a),
per T8 a = g;
Ricevuto(x) richiederebbe Accoglie(g,x). Quindi not
Ricevuto(x). (Senza
l'unicita' la dimostrazione sarebbe incompleta.)
Formula centrale:
Dom(x,a) -/-> Accoglie(a,x); Accoglie(a,x) -> Dom(x,a).
Distinzione da
Badiou: per Badiou lo scarto produce fedelta'; per
adriano53s lo scarto
chiede, senza garantire la risposta.
9. DIALETTICA ASSOLUTA (STADIO I)
D15. RisultatoDiProcesso(e) := exists u (Processo(u) and FondatoDa(u,e))
AX14. FondatoDa(u,e) -> Dip(e)
T15. not exists e (Ass(e) and
RisultatoDiProcesso(e))
Dim.: AX14 da' Dip(e); D7 richiede not Dip(e).
Corollario: ogni dialettica che produca l'Assoluto e' incompatibile con D7.
###############################################################################
PARTE II - IL PONTE
###############################################################################
10. L'ASSUNZIONE AS-N E LA RIPARTIZIONE
Con le sole D6, D7 non ogni
ente e' Ass o Rel: restano possibili
"contingente non dipendente" (escluso da
T5) e "necessario dipendente"
(non escluso). Serve:
AS-N. (Aseita' del
necessario) Nec(e) -> not Dip(e).
Cio' che e' necessario non e' dipendente.
Giustificazione: la necessita'
e' aseita'. Costo dichiarato: AS-N e'
sostanziale; esclude enti
necessari ma dipendenti (per esempio oggetti
matematici come "fondati" da
Dio, o i modi spinoziani). Chi la rifiuta non
puo' passare allo Stadio
II: avrebbe una terza sorta, il "necessario
dipendente".
T16 (Ripartizione). [T5, AS-N]
Per ogni e esistente in
qualche mondo: esattamente uno fra Ass(e) e
Rel(e).
Dim.: per S5, Box E(e)
oppure Diamond not E(e) (tertium non datur
modale), dunque Nec(e) oppure
Cont(e). Se Nec(e): per AS-N not Dip(e),
quindi Ass(e). Se Cont(e): se not
Dip(e), T5 darebbe Nec(e), contro
Diamond not E(e); quindi Dip(e), Rel(e).
Esclusivita': T1.
T17 (Rigidita'). [T5, AS-N]
Ass(e) in w e E(e) in w'
-> Ass(e) in w'; Rel(e) in w e E(e) in w' ->
Rel(e) in w'.
Dim.: Nec e
Cont sono invarianti per S5. Per AS-N, Ass vale ovunque e
esiste. Per T5, un
contingente esistente e' sempre dipendente.
Perche' conta: la classificazione
non cambia da mondo a mondo; i sort
possono quindi essere fissi.
Esito: sulla base di T16 e T17 il dominio En si ripartisce in due blocchi
disgiunti, D_A e D_R, rigidi nei mondi. Qui il predicato diventa sort.
11. TRADUZIONE FRA GLI STADI
tau : formule dello Stadio I -> formule
dello Stadio II, per relativizzazione
dei quantificatori: exists e phi ==>
exists a tau(phi[a/e]) or
exists x tau(phi[x/e]); forall analogo con and. Sui
predicati:
Ass(e) ==> vero se e:A, falso se e:R;
Rel(e) ==> E_R(e) se e:R,
falso se e:A [correzione v2.5: Rel include
l'esistenza].
E(e) ==> E_A(e)
se e:A, E_R(e) se e:R.
F(e,f) ==> Fonda_AR(e,f) se (A,R); Fonda_RR(e,f) se
(R,R);
falso se (A,A) oppure (R,A) [per T4b: l'Assoluto non ha
fondanti;
F(x,a) darebbe Dip(a)].
Cr(a,e)==> Cr(a,e) con a:A, e:R (AX7); Caus ==>
Caus_RR (AS-C);
FondatoDa(u,e) ==> solo e:R (AX14, D7).
Dom, Accoglie ==>
Dom : R x A, Accoglie : A x R (AX12, AX13).
Identita' ==> solo fra termini
della stessa sorta.
PRINCIPIO DI FEDELTA'. Ogni modello dello Stadio I
che soddisfi AS-N si
ripartisce (T16, T17) in un modello dello Stadio II;
ogni modello dello
Stadio II si unisce in un modello dello Stadio I (unione
dei domini). Le due
costruzioni sono inverse. Dunque i teoremi dello Stadio I
si traducono in
teoremi dello Stadio II. (Dimostrato nella Parte V, Teorema
F, sezione 23.)
Questo risolve la perdita di contenuto segnalata per
v2.2: T1 non e' una
stipulazione sintattica dello Stadio II, ma un teorema
dello Stadio I che
giustifica la scelta di sorte distinte.
###############################################################################
PARTE III - STADIO II: TEORIA (vincolante)
###############################################################################
12. LINGUAGGIO (STADIO II)
Sort: A (a, b, c: Assoluto); R (x, y, z:
relativo); P (p, q, r: fatti);
Q (u, v: processi). Modalita' S5, domini
variabili.
Disgiunzione: la disgiunzione di A e R e' incorporata nel
linguaggio many-
sorted (A e R sono sort distinti, quindi un termine ha
un'unica sorta). La
scrittura "A intersezione R = vuoto" appartiene alla
SEMANTICA (D_A e D_R
disgiunti), non alle regole di formazione. Le formule
"A(x) and R(x)",
"x = a" con x:R e a:A, "Dip(a,x)" con a:A e x:R sono mal
formate.
REGOLA DI ETEROGENEITA' ONTOLOGICA. Nessun termine di sorta A
compare come
argomento di un predicato la cui firma richiede R, e viceversa.
Gli
eventuali predicati A(x), R(x) su un dominio En sono una codifica
metateorica (Stadio I) della distinzione di sorta, non la sua fondazione.
Esistenza: E_A(a) ed E_R(x) (non c'e' E unico). Cont_R(x) := E_R(x) and
Diamond not E_R(x). Nec_A(a) := E_A(a) and Box E_A(a).
13. FIRME
(correzioni rispetto a v2.2)
Fonda_AR : A x R (l'Assoluto fonda il
relativo)
Fonda_RR : R x R (fondazione seconda fra relativi)
Cr : A x R
Dom : R x A
Accoglie : A x R
Caus_RR : R x R
FondatoDa: Q x R
Fp : A
x P e R x P (Fp_A, Fp_R)
PrincipioDi_AR : A x R; PrincipioDi_RR : R x R
(v2.5)
Correzioni: (1) la firma "Fonda : A x R" di v2.2 rompeva la catena
fra
relativi (transitivita', ben-fondatezza, causalita' seconda); si pone
Fonda = Fonda_AR U Fonda_RR. (2) "Dip : R x A" e Dip unaria di D3 sono
nozioni diverse: si usa DipA(x,a) := Fonda_AR(a,x) (dipendenza diretta
dall'Assoluto) e Dip(x) := exists a Fonda_AR(a,x) or exists y Fonda_RR(y,x).
(3) E, Nec e Cont sono trasversali: si sdoppiano in E_A, E_R, Nec_A, Cont_R,
con corrispondenza data da T16, T17 e dalla traduzione tau.
14. ASSIOMI
STRUTTURALI (STADIO II)
L'elenco di questa sezione (v2.3) e' sostituito
dalla teoria Sigma2 della
sezione 22 (assiomi S1-S12, AN1', AN2'), che e'
l'unica lista vincolante.
Corrispondenza (v2.3 -> v2.5):
AX1'->S1;
AX2'->S2; AX3'->S4 (seconda riga); AX6'->S5; AX8'->S6;
AX9'->S7; AX11'->S10;
AX15'->S8; AS6'->S12; AX-A->S9;
AN1'->AN1'; AN2'->AN2'.
Nuovi in v2.4: S3
(AX3R'), S4 (AX4R'), S11.
15. TEOREMI EREDITATI (STADIO II)
T-A.
forall a Box E_A(a) (necessita' e' modalita' della sorta A)
T-R. forall x
(E_R(x) -> Diamond not E_R(x)) (contingenza e' modalita'
della sorta R)
T6'. exists a E_A(a) [da T6]
T8'. forall a forall b (a = b) [da T8:
l'identita' fra a, b e' ben
formata, essendo entrambi di sorta A]
T8b.
forall Phi in Qual (Phi(g) <-> Phi in PP) [da AS9', AS10']
T9''. forall x
(E_R(x) -> Dom(x,g)) [da AN1', T8']
T9'. forall x (E_R(x) -> Fonda_AR(g,x))
[da T9]
T10'. Creatore e Creato non sono compatibili: Creatore(a) richiede
a:A,
Creato(e) richiede e:R. La formula "Creatore(e) and Creato(e)" e'
mal
formata per qualsiasi e. [T10 resta il suo motivo di Stadio I]
T11'.
Caus(g,y) e' mal formata (Caus_RR : R x R). Il motivo di Stadio I e'
T11
(AS-C).
T12'. Ricevuto(x) := exists a Accoglie(a,x) -> Dom(x,g) and
Accoglie(g,x)
T13'. Dom -> Accoglie non e' derivabile (modelli M_A, M_B,
sezione 16).
T14'. Diamond exists x not Ricevuto(x) [AN2', T8']
T15'.
"Assoluto risultato di processo" e' mal formata (FondatoDa : Q x R).
[Il
motivo di Stadio I e' T15 (AX14, D7).]
Lettura ontologica dello Stadio
II:
- l'Assoluto non e' un ente nel dominio del relativo;
- il relativo
non e' un frammento dell'Assoluto;
- la fondazione eterogenea va da A a R;
fra relativi c'e' solo fondazione
seconda;
- la domanda e' un atto della
sorta R; l'accoglienza un atto della sorta A.
16. SEMANTICA E MODELLI
(STADIO II)
Modello M = <W, ~, D_A, D_R, I>:
W: mondi; ~: equivalenza
(S5);
D_A: dominio costante (non vuoto per T6');
D_R(w): dominio
variabile; D_A e D_R(w) disgiunti;
E_A vale di tutto D_A in ogni mondo;
E_R(x) in w sse x in D_R(w);
I(Fonda_AR)(w) sottoinsieme di D_A x D_R(w);
ecc.
M_A (controesempio a Dom -> Accoglie):
W = {w1, w2}; D_A = {g};
D_R(w1) = {x}; D_R(w2) = vuoto.
Cr = Fonda_AR = {(g,x)} in w1; vuoto in w2.
Dom = {(x,g)} in w1; vuoto in w2. Accoglie = vuoto.
x e' contingente (esiste
in w1, non in w2) e dipende da g; g e' necessario.
AX1'-AX11', AX15', AN1' e
AN2' sono soddisfatti. In w1 Dom(x,g) e
not Accoglie(g,x).
M_B: come M_A
con Accoglie = {(g,x)} in w1: Dom -> Accoglie vale
(AN2' falsa).
M_A e M_B
mostrano l'indipendenza (T13').
Estensione ai fatti e ai processi: vedi
sezione 24 (v2.4).
###############################################################################
PARTE IV - CONCLUSIONI
###############################################################################
17. PROGRAMMA DI DIMOSTRAZIONE
Stadio I: T1 T2 T3 T4 T4b T5 T6 T7 T8
T9 T10 T11 T12 T13 T14 T15
Ponte: T16 (ripartizione), T17 (rigidita'),
principio di fedelta'
Stadio II: T-A T-R T6' T8' T9' T10' T11' T12' T13' T14'
T15'
Dipendenze principali:
T5 <- AS1, AS2, AS7
T6 <- AS1, AS2,
AS3, AS5, AS6, AS7
T8 <- AS8, AS9, AS10
T16 <- T5, AS-N
Stadio II <-
Stadio I + T16 + T17 + AS-N
Completato nella v2.4 (Parte V):
dimostrazione del principio di fedelta'
(Teorema F, sezione 23), modelli
estesi a fatti e processi (sezione 24),
definizione di Qual e PP (sezione
25).
18. CIO' CHE NON SI FORMALIZZA COME TEOREMA
Non sono teoremi:
"Dio esiste" incondizionatamente; "Dio e' personale"; "il
mondo e' creato";
"la domanda viene ricevuta"; "la sofferenza e'
giustificata"; "la rivelazione
cristiana e' deducibile dalla metafisica";
AN1 (ogni relativo e' in domanda);
AS-N (aseita' del necessario).
Restano assunti, ipotesi, atti di
riconoscimento o tesi di fede. La
formalizzazione serve a impedire che la
struttura logica finga di produrre
cio' che deve essere dato, riconosciuto o
ricevuto.
19. FORMULA FINALE E PRINCIPIO
Il relativo non pecca
perche' e' finito; pecca quando rifiuta di essere
finito e pretende di
fondarsi da se'. La sofferenza nasce dalla
relativita'; il peccato nasce dal
rifiuto della relativita'; Dio solo e'
Assoluto per essenza.
Lo scarto
non e' ancora ricezione: e' domanda di essere ricevuto da un
Assoluto. La
domanda e' atto del relativo; l'accoglienza e' atto
dell'Assoluto.
Il
linguaggio formale non fonda l'Assoluto: disciplina il pensiero che lo
riconosce. I sort separati impediscono che la comodita' tecnica della
codifica trasformi l'Assoluto in un caso del dominio relativo; lo Stadio I
e'
lo scalpello usato per ottenere la forma, e va rimosso dalla statua.
Badiou chiama evento cio' che adriano53s chiama soglia. La disputa non e'
fra
fede e ragione, ma fra due assiomatiche dello scarto: una che lo
lascia senza
Fondamento, una che lo legge come apertura al Fondamento.
20. REGISTRO
DELLE MODIFICHE (v2.1/v2.2 -> v2.3)
1. Adottata l'architettura a due
stadi; En confinato a impalcatura.
2. Aggiunta AS-N (aseita' del necessario),
senza la quale la ripartizione
A/R non e' esaustiva. Dichiarata come
assunzione sostanziale.
3. Dimostrati T16 (ripartizione) e T17 (rigidita');
T1 resta teorema.
4. Corretta la firma Fonda (A x R piu' R x R) e separata
Dip in unaria e
DipA binaria.
5. Sdoppiati E, Nec, Cont in E_A, E_R,
Nec_A, Cont_R.
6. Precisato che la disgiunzione dei sort e' incorporata nel
linguaggio e
che "A intersezione R = vuoto" e' un enunciato semantico.
7.
Introdotta la traduzione tau e il principio di fedelta' (schema).
8. T10,
T11, T15 nello Stadio II diventano sintattici, con il motivo
sostanziale
conservato nello Stadio I (T1, AS-C, AX14).
9. T4 conservato come T4b per
spiegare la firma senza fondanti di A.
10. Ricostruiti i modelli M_A, M_B con
sort separati.
11. Dichiarato il limite meta-teorico: la traduzione usa un
dominio comune
nel metalinguaggio.
###############################################################################
PARTE V - COMPLEMENTO v2.4: FEDELTA' DEGLI STADI, FATTI E PROCESSI
###############################################################################
21. PREMESSA E CORREZIONI A v2.3
Questa parte sostituisce o completa:
il "principio di fedelta'" della sezione
11 (ora Teorema F, sezione 23); le
righe sui limiti dei modelli (sezione 16;
ora sezione 24); l'elenco "Da fare"
della sezione 17 (ora sezioni 23-25).
Il lavoro di completamento ha fatto
emergere quattro lacune di v2.3,
corrette qui:
L1. Nello Stadio II
mancavano gli assiomi di esistenza e di dipendenza
esistenziale per Fonda_RR
(corrispondenti ad AX3 e AX4 per le coppie
(R,R)). Senza di essi l'unione dei
modelli non soddisfa AX4. Aggiunti
come AX3R' e AX4R' (sezione 22).
L2. Le
assunzioni AS1-AS10 non erano state tradotte nello Stadio II.
Ora lo sono
(sezione 22), con il costruttore ex : En -> P.
L3. AS3 parlava di "totalita'
della realta' contingente" in modo
esposto a paradossi di tipo
cantoriano/Russell-Myhill. Si rilegge
cosi': Totalizza(B) e' un predicato
UNARIO su P; B e' il fatto che le
entita' contingenti esistenti sono
esattamente quelle che sono. B
riguarda le ENTITA' contingenti, non la
totalita' di tutti i fatti,
e dunque non e' un fatto "su tutti i fatti". La
costante C0 e'
eliminata.
L4. Qual doveva contenere solo proprieta' RIGIDE
(sezione 25): altrimenti
AS9 e AS10, applicate a una proprieta' come
"Creatore" (non rigida per
AX15), sarebbero in conflitto con il resto del
sistema.
-------------------------------------------------------------------------------
22. STADIO II COMPLETO: LA TEORIA Sigma2
Sort: A, R, P, Q. Costruttori:
ex_A : A -> P, ex_R : R -> P (il fatto che
l'ente esiste). Predicato Ver(p):
"p e' vero". Si pone
Cont_P(p) := Ver(p) and Diamond not Ver(p); Nec_P(p) :=
Box Ver(p).
Vincolo semantico di esistenza (EX): ogni predicato
relazionale con
argomenti di sort A o R e' vero in w solo di enti esistenti
in w.
Firme (come sezione 13):
Fonda_AR : A x R; Fonda_RR : R x R; Cr
: A x R; Dom : R x A;
Accoglie : A x R; Caus_RR : R x R; FondatoDa : Q x R;
Fp_A : A x P; Fp_R : R x P; PrincipioDi_AR : A x R; PrincipioDi_RR : R x R.
Predicati derivati: Dip(x) := exists a Fonda_AR(a,x) or exists y Fonda_RR(y,x);
Cont_R(x) := E_R(x) and Diamond not E_R(x).
Assiomi strutturali:
S1.
not Fonda_RR(x,x)
S2. Fonda_RR(x,y) and Fonda_RR(y,z) -> Fonda_RR(x,z)
Fonda_AR(a,y) and Fonda_RR(y,x) -> Fonda_AR(a,x)
S3. Fonda_RR(x,y) -> (E_R(x)
and E_R(y)) [AX3R']
Fonda_AR(a,x) -> E_R(x)
S4. Fonda_RR(x,y) ->
Box(E_R(y) -> E_R(x)) [AX4R']
Fonda_AR(a,x) -> Box(E_R(x) -> E_A(a))
S5.
Cr(a,x) -> Fonda_AR(a,x)
S6. E_R(x) -> exists a Cr(a,x)
S7. Cr(a,x) ->
Box(E_R(x) -> Cr(a,x))
S8. Diamond not exists x E_R(x) [AX15']
S9. forall
a Box E_A(a) (D_A costante) [AX-A]
S10. Accoglie(a,x) -> Dom(x,a)
S11.
FondatoDa(u,x) -> (E_R(x) and Dip(x)) [AX14']
S12. Fonda_RR e' ben fondata
[AS6']
Assunzioni antropologiche:
AN1'. E_R(x) -> exists a Dom(x,a)
AN2'. Diamond exists x exists a (Dom(x,a) and not Accoglie(a,x))
(AN2' e'
indipendente: vedi N_A e N_B; i teoremi valgono con o senza)
Assunzioni sui
fatti (traduzione di AS1-AS7):
AS1'. Cont_P(p) -> exists q Exp(q,p)
AS2'.
Cont_R(x) and Exp(p,ex_R(x)) and Ult(p) -> Dip(x)
AS3'. exists B (Cont_P(B)
and Totalizza(B)) (L3: unario)
AS4'. Cont_P(p) -> not Exp(p,B) per ogni B con
Totalizza(B)
AS5'. Exp(p,B) and Ult(p) and Totalizza(B) ->
exists a
Fp_A(a,B) or exists x (E_R(x) and Fp_R(x,B))
AS7'. Exp e' irriflessiva,
transitiva, ben fondata. D8: Ult(p) := not
exists q Exp(q,p).
Assunzioni
di unicita' (traduzione di AS8-AS10, con Qual e PP della sezione
25; sono
schemi, il quantificatore su Phi e' infinitario):
AS8'. StessoProfilo(a,b) ->
a = b
AS9'. Phi in PP -> Phi(a)
AS10'. Phi in Qual and Phi(a) -> Phi in PP
Nota su AS-N: nello Stadio II AS-N non compare come assioma: e' incorporata
nella partizione dei sort (S8 + S9: nessun relativo e' necessario; ogni
Assoluto e' necessario e non ha fondanti per la firma di Fonda).
-------------------------------------------------------------------------------
23. TEOREMA F (FEDELTA' FRA GLI STADI) - DIMOSTRAZIONE
Notazioni. Sigma1
e' la teoria dello Stadio I: AX1-AX5, AX6-AX9, AX11-AX15
(numerazione v2.3),
AX14 (processi), AS1-AS10, AS-C, AS-N, AX0, AX16, AN1 (con o senza
AN2).
Mod(S) e' la classe dei modelli di S.
Semantica standard. Un modello
dello Stadio I e'
M1 = <W, ~, U, D, P, Q, I>
con W insieme di mondi, ~
equivalenza (per la proprieta' dei sottomodelli
generati si assume ~
universale su W: la verita' di una formula modale in w
dipende solo dal
cluster di w); U dominio ESTERNO di En, D(w) sottoinsieme
di U dominio
INTERNO, U = unione dei D(w); P, Q insiemi (domini dei fatti e
dei processi)
comuni a entrambi gli stadi; I interpretazione. I
quantificatori su En
percorrono U; E(e) e' vero in w sse e e' in D(w).
Un modello dello Stadio II
e'
M2 = <W, ~, U_A, U_R, D_R, P, Q, I'>
con U_A, U_R disgiunti, D_R(w)
sottoinsieme di U_R con U_R = unione dei D_R(w) (convenzione v2.8,
sezione
29.4), e D_A(w) = U_A per ogni w. Quantificatori: su U_A, su U_R (esterni);
E_A(a) sempre vero; E_R(x) in w
sse x in D_R(w). Vale (EX).
Definizione 1 (Part: Stadio I -> Stadio II). Dato M1 in Mod(Sigma1):
U_A := {
e in U : esiste w, e in D(w) e M1,w |= Ass(e) }
U_R := { e in U : esiste w, e
in D(w) e M1,w |= Rel(e) }
D_R(w) := D(w) intersezione U_R
I'(Fonda_AR)(w)
:= I(F)(w) intersezione (U_A x U_R)
I'(Fonda_RR)(w) := I(F)(w) intersezione
(U_R x U_R)
Cr, Dom, Accoglie, Caus, FondatoDa, Fp, PrincipioDi: restrizioni
alle
firme dello Stadio II; P, Q, Exp, Totalizza, Ver invariati.
Definizione 2 (Union: Stadio II -> Stadio I). Dato M2:
U := U_A unione U_R;
D(w) := U_A unione D_R(w);
I(F)(w) := I'(Fonda_AR)(w) unione I'(Fonda_RR)(w);
Cr, Dom, Accoglie, Caus, FondatoDa, Fp, PrincipioDi: unioni delle
componenti;
P, Q, Exp, Totalizza, Ver invariati.
Lemma 1 (partizione). Sia M1 in
Mod(Sigma1). Allora:
(a) U = U_A unione U_R, unione disgiunta;
(b) per e
in U_A: e in D(w) per ogni w, e M1,w |= Ass(e) per ogni w;
(c) per e in U_R:
M1,w |= Rel(e) per ogni w con e in D(w);
(d) I(F)(w) e' contenuta in (U_A x
U_R) unione (U_R x U_R);
(e) Cr, Dom, Accoglie, Caus, FondatoDa, PrincipioDi
rispettano le firme
dello Stadio II.
Dim. (a) Ogni e in U sta in qualche
D(w); per T16 vale esattamente uno fra
Ass(e) e Rel(e) in tale w; quindi e e'
in U_A o in U_R, non in entrambi
(T1). (b) e in U_A: Nec(e) in qualche w.
Poiche' ~ e' universale, Box E(e)
vale in ogni w: e in D(w) per ogni w. Per
AS-N, not Dip(e) in ogni w, e
quindi Ass(e). (c) e in U_R: Cont(e) in qualche
w. Poiche' ~ e'
universale, Diamond not E(e) vale in ogni w; per T5, se E(e)
in w e
not Dip(e) allora Nec(e): impossibile. Quindi Dip(e), e Rel(e).
(d)
Se F(h,e) in w: per AX3 E(h), E(e) in w; e e' Dip, quindi per (b) non
e' in
U_A; quindi e in U_R; h e' in U_A o U_R per (a). (e) AX7, AX12,
AX13, AX16,
AS-C: la firma segue dai predicati Ass e Rel e da (a)-(c). Per
FondatoDa:
AX14 da' Dip(e) e AX3 da' E(e), quindi e e' non Ass (da (b)),
cioe' in U_R.
QED
Lemma 2 (unione). Sia M2 in Mod(Sigma2) e M1 := Union(M2). Allora:
(a) Ass(e) in w <-> e in U_A; Rel(e) in w <-> e in D_R(w);
(b) M1 soddisfa il
Lemma 1 (a)-(e) per costruzione.
Dim. e in U_A: per S9 Box E_A(e): Nec(e).
Per la firma di Fonda nessun
fondante: not Dip(e). Quindi Ass(e). e in
D_R(w): per S8 esiste w' con
D_R(w') vuoto, quindi Diamond not E(e): Cont(e).
Per S6 e S5 esiste a con
Fonda_AR(a,e): Dip(e). Quindi Rel(e). Inversamente,
un e in D_R(w) non
e' Ass (Dip) e un e in U_A non e' Rel (Nec). QED
Traduzione tau. Per ogni formula phi di Stadio I e per ogni assegnazione di
sorte sigma alle sue variabili libere in {A,R}, si definisce tau_sigma(phi):
tau_sigma(E(e)) = E_sigma(e)
tau_sigma(Ass(e)) = vero se sigma(e)=A, falso se
R
tau_sigma(Rel(e)) = E_R(e) se sigma(e)=R, falso se A [v2.5]
tau_sigma(F(e,f)) = Fonda_{sigma(e) sigma(f)}(e,f) per (A,R) e (R,R);
falso
per (A,A) e (R,A)
tau_sigma(e = f) = e = f se stessa sorta, falso altrimenti
tau_sigma(Cr, Dom, Accoglie, Caus, FondatoDa, PrincipioDi, Fp) = il
predicato
tipato corrispondente se la firma e'
rispettata, falso altrimenti
tau_sigma(ex(e)) = ex_{sigma(e)}(e) (costruttore di fatti)
tau_sigma su P, Q,
Exp, Totalizza, Ver: identita'
tau commuta con i connettivi e con Box,
Diamond
tau_sigma(exists e phi) = exists a tau_{sigma[e:A]}(phi)
or exists
x tau_{sigma[e:R]}(phi)
tau_sigma(forall e phi) = forall a
tau_{sigma[e:A]}(phi)
and forall x tau_{sigma[e:R]}(phi)
I predicati
definiti (Dip, Cont, Nec, Ult, ...) si traducono espandendo le
definizioni;
Dip(x) con sigma(x)=R diventa esattamente la Dip dello Stadio II
(sezione
22).
Lemma 3 (traduzione). Sia M1 in Mod(Sigma1), M2 := Part(M1), phi una
formula, sigma una sorta per le variabili libere, s un'assegnazione con
s(e)
in U_sigma(e). Per ogni w:
M1,w,s |= phi <-> M2,w,s |= tau_sigma(phi).
Dim. Per induzione su phi.
Atomiche. E(e): per sigma(e)=A, E_A(e) e' sempre
vero in M2 e E(e) e'
vero in M1 per Lemma 1(b). Per sigma(e)=R, E(e) in M1
sse e in D(w) sse
e in D_R(w) sse E_R(e) in M2. Ass: Lemma 1(b). Rel: se e in
D(w), Lemma 1(c); se e non e' in
D(w), Rel(e) e' falso in M1 (richiede E(e))
ed E_R(e) e' falso in M2
(correzione v2.5: con la tau di v2.4, 'vero', il
caso falliva). F(e,f): le
sorte (A,R) e (R,R): I'(Fonda_..)(w) e' per
definizione la restrizione di
I(F)(w). Le sorte (A,A) e (R,A): I(F)(w) non
contiene coppie del tipo
per Lemma 1(d), quindi falso in entrambi. Identita':
le due sorti sono
disgiunte per Lemma 1(a). Gli altri predicati: Lemma 1(e)
(nella stessa
maniera). Predicati su P e Q: invariati.
Connettivi:
immediato.
Box, Diamond: Box phi e' vero in w sse phi e' vero in ogni w' (~
universale).
L'assegnazione s resta ammissibile in w' perche' s(e) sta in
U_sigma(e),
che dal Lemma 1(a),(b),(c) e' indipendente dal mondo (rigidita').
Quantificatore esistenziale: exists e phi e' vero in w sse esiste e in U con
phi; per Lemma 1(a) e' in U_A o U_R; si applica l'ipotesi induttiva alla
rispettiva sorta. Il caso forall e' duale. QED
Lemma 4 (inversa). Part e
Union sono inverse. Dim. Union(Part(M1)): U e'
U_A unione U_R = U (Lemma
1(a)); D(w) = U_A unione (D(w) intersezione U_R)
= D(w) perche' D(w) contiene
U_A per Lemma 1(b); I(F) = AR unione RR =
I(F) per Lemma 1(d).
Part(Union(M2)): U_A, U_R, D_R ricostruiti per Lemma 2
(a). Le altre
relazioni coincidono. QED
TEOREMA F (FEDELTA').
(F1) Se M1 in
Mod(Sigma1), allora Part(M1) in Mod(Sigma2).
(F2) Se M2 in Mod(Sigma2),
allora Union(M2) in Mod(Sigma1).
(F3) Part e Union sono mutuamente inverse;
quindi Mod(Sigma1) e Mod(Sigma2)
sono in corrispondenza biunivoca.
(F4)
Per ogni formula chiusa phi dello Stadio I:
Sigma1 |= phi <-> Sigma2 |=
tau(phi).
Dim.
(F1) Per il Lemma 3 ogni assioma di Sigma2 e' traduzione di
un assioma o
teorema di Sigma1 vero in M1: S1 e S2 da AX1, AX2 (con le sorte
ammesse
da Lemma 1(d)); S3, S4 da AX3, AX4 (le due coppie (A,R) e (R,R) si
leggono direttamente); S5 da AX6; S6 da AX8 e AX7; S7 da AX9; S8 da
AX15
(Rel(x) in w' sse x in D_R(w')); S9 da Lemma 1(b); S10 da AX11; S11
da AX14;
S12 da AS6 (restrizione di F a R x R); AN1', AN2' da AN1, AN2;
AS1'-AS7' da
AS1-AS7 (via ex e per le sole entita' R, vedi Lemma 3 e
T16: se Cont(e)
allora e e' R); AS8'-AS10' da AS8-AS10 ristretti a
Qual (sezione 25). Restano
soddisfatti i vincoli (EX), per AX3.
(F2) Per il Lemma 2, M1 = Union(M2) ha
Ass = U_A e Rel = D_R(w).
Verifica degli assiomi di Sigma1, tramite il Lemma
3 applicato a
Part(M1) = M2 (Lemma 4): AX1: F(e,e) darebbe Fonda_AR(e,e) (e
in U_A e
in U_R) o Fonda_RR(e,e), vietato da S1. AX2: sorte possibili (A,R,R)
e
(R,R,R): S2. AX3, AX4: S3, S4 (per (A,R): E_A sempre vero). AX5: (EX).
AX6, AX7, AX8, AX9: S5, firma di Cr, S6, S7. AX11, AX12, AX13: S10 e
firme.
AX15: S8. AX14: S11. AX16: firme di PrincipioDi e (EX). AS-C: firma di Caus.
AS-N: Nec(e) significa
e in D(w) per ogni w; per S8 nessun relativo e' in
tutti i D(w); quindi
e in U_A e per la firma not Dip. AS1-AS7 e AS8-AS10:
AS1'-AS10' via Lemma
3. AS6: una catena infinita discendente e0, e1, ... con
F(e(i+1),e(i)) ha
ogni e(i) come secondo argomento di un F, quindi in U_R;
dunque e' una
catena di Fonda_RR, contro S12.
(F3) Lemma 4. (F4) Da
(F1)-(F3): per ogni M2 in Mod(Sigma2) vale
M2 |= tau(phi) sse Union(M2) |=
phi (Lemma 3 su Part(Union(M2)) = M2); e
ogni M1 in Mod(Sigma1) e'
Union(Part(M1)). Quindi Sigma1 |= phi sse
Sigma2 |= tau(phi). QED
Nota
sulla deduzione. (F4) e' un enunciato semantico. Per la parte di primo
ordine
(senza gli schemi infinitari AS8-AS10) la completezza della logica
modale
quantificata S5 many-sorted a domini variabili rispetto alla
semantica di
Kripke (risultato standard) trasferisce l'equivalenza alla
derivabilita':
Sigma1 |- phi sse Sigma2 |- tau(phi). Per AS8-AS10, che sono
schemi
infinitari, vale l'enunciato semantico.
-------------------------------------------------------------------------------
24. MODELLI ESTESI A FATTI E PROCESSI
Costruzione N0 (modello di Sigma2,
con P e Q).
W = {w1, w2}, ~ universale.
U_A = {g}. U_R = {x}. D_R(w1) =
{x}, D_R(w2) = vuoto.
P = insieme delle parti di W = { 0, alfa, beta, 1 },
con 0 = vuoto, alfa = {w1}, beta = {w2}, 1 = W.
Ver(p) in w sse w in p. Box(p
-> q) in w sse p e' contenuto in q.
ex_A(g) = 1; ex_R(x) = alfa.
Q = {u1};
Processo(u1) vero ovunque.
Relazioni a w1:
Fonda_AR = Cr = {(g,x)};
Fonda_RR = vuoto; Caus_RR = vuoto;
Dom = {(x,g)}; Fp_A = {(g,alfa),
(g,beta)}; Fp_R = vuoto;
FondatoDa = {(u1,x)}; PrincipioDi = vuoto.
Relazioni a w2: tutto vuoto salvo Fp_A (costante, come sopra).
Exp =
{(1,alfa), (1,beta)} (indipendente dal mondo).
Totalizza(B) in w sse B = { w'
: D_R(w') = D_R(w) }: a w1 vale per alfa,
a w2 per beta.
Qual = {Ph1,
Ph2}, PP = {Ph1}; Ph1(g) vero, Ph2(g) falso in tutti i mondi.
Verifica
degli assiomi (Sigma2).
S1-S4, S12: Fonda_RR e' vuota; S3 per (A,R): g esiste
sempre, x esiste a w1
dove vale la relazione.
S5, S6, S7: a w1, E_R(x) e
Cr(g,x); a w2 x non esiste; Cr(g,x) vale solo a
w1, dove x esiste.
S8: a
w2 non esiste alcun relativo. S9: D_A = {g} costante.
S10: Accoglie e' vuoto
(N_A) oppure {(g,x)} (N_B) a w1; in entrambi i casi
contenuto in Dom^-1.
S11: FondatoDa(u1,x) a w1, dove E_R(x) e Dip(x).
AN1': a w1 Dom(x,g).
AS1': i fatti contingenti veri a w1 sono i soli p con w1 in p e p != 1:
alfa.
A w2: beta. Exp(1,alfa), Exp(1,beta). OK.
AS2': Cont_R(x) a w1,
Exp(1,ex_R(x)) = Exp(1,alfa), Ult(1) perche' nessun
q spiega 1; Dip(x) vale
(Fonda_AR(g,x)). OK.
AS3': B = alfa a w1, B = beta a w2. Cont_P(B) e
Totalizza(B). OK.
AS4': l'unico fatto che spiega B e' 1, che e' necessario
(Nec_P). OK.
AS5': Exp(1,B), Ult(1): Fp_A(g,B) a entrambi i mondi. OK.
AS7': Exp ha catene di lunghezza 1: irriflessiva, transitiva, ben fondata.
AS8'-AS10': un solo Assoluto; g ha Ph1 (AS9'), nessuna altra proprieta'
qualitativa (AS10').
T7 verificato: 1 e' necessario, Exp(1,alfa), ma 1 ->
alfa non e' valido.
T13': N_A, N_B mostrano l'indipendenza di Dom ->
Accoglie:
N_A: Accoglie = vuoto; AN2' vero.
N_B: Accoglie = {(g,x)} a w1;
AN2' falso. Tutti gli altri assiomi veri.
T14' in N_A: a w1 x non e'
ricevuto.
Lettura dei processi. u1 e' un processo che produce x (second
causation) ed
e' compatibile con Cr(g,x): FondatoDa implica Dip(x), e Dip(x)
e' assicurato
da g. Il tentativo FondatoDa(u,g) e' escluso dalla firma (Q x
R) e, nello
Stadio I, da AX14 e dalla definizione di Ass: e' T15.
Modello N_N (indipendenza di AS-N, nello Stadio I).
W = {w1,w2}; U = {g, x,
n}; D(w1) = {g,x,n}, D(w2) = {g,n};
F = {(g,x),(g,n)} a w1, F = {(g,n)} a w2;
Cr = {(g,x)} a w1.
Fatti, Exp, Totalizza come in N0 (con ex(n) = 1).
n e'
necessario e dipendente: ne' Ass ne' Rel. Tutti gli assiomi di Sigma1
salvo
AS-N sono soddisfatti (AX4: F(g,n) -> Box(E(n) -> E(g)); AS2 non si
applica a
n, che non e' contingente; T5 vale perche' n e' dipendente).
AS-N e T16
falliscono in N_N. Dunque AS-N non e' derivabile dalle altre
assunzioni ed e'
effettivamente necessaria per la partizione A/R. N_N non
ha controparte nello
Stadio II: avrebbe bisogno di una terza sorta.
Consistenza. N0 (nelle
versioni N_A e N_B) e' un modello finito di
Sigma2; per il Teorema F (F2)
Union(N0) e' un modello di Sigma1. Quindi
entrambe le teorie sono
soddisfacibili, dunque consistenti.
-------------------------------------------------------------------------------
25. QUAL E PP: DEFINIZIONI RIGOROSE
Definizione Q. Una proprieta' di
Assoluti e' una funzione Phi : W -> insieme
delle parti di U_A. Phi e'
QUALITATIVA RIGIDA se:
(i) e' definita da una formula phi(a) di Stadio II
senza costanti
individuali, senza variabili libere diverse da a, e senza
atomi di
identita' in cui a compaia con un termine diverso da una variabile
legata;
(ii) Phi(w) = Phi(w') per ogni w, w' (rigidita').
Qual := insieme
delle proprieta' qualitative rigide.
Motivazione della rigidita' (L4).
"Creatore(a) := exists x Cr(a,x)" e'
qualitativa nel senso (i) ma non rigida:
per AX15 e' vera a w1 e falsa a w2.
Se fosse in Qual, AS10 imporrebbe
Creatore in PP ovunque valga, e AS9
imporrebbe Creatore(g) a w2, dove non
esistono creature: contraddizione. Il
sistema dice invece che la creazione e'
libera (T7: spiegare non e'
necessitare). Quindi la relazione con le creature
non fa parte del profilo
qualitativo dell'Assoluto.
Definizione PP. PP
e' un sottoinsieme primitivo di Qual che soddisfa:
PP-1 (co-istanziabilita'):
per ogni sottoinsieme finito {Phi1,...,Phin} di
PP: Diamond exists a (Phi1(a)
and ... and Phin(a)).
PP-2 (chiusura): Phi, Psi in PP -> (Phi and Psi) in PP.
PP-1 e' necessaria: con perfezioni incompatibili, AS9' darebbe un Assoluto
inesistente e contraddirebbe T6.
T8 (rivisto). Con Qual rigida e PP-1,
PP-2, la dimostrazione di T8 resta:
per AS9' e AS10', Phi(a) <-> Phi in PP
per ogni Phi in Qual, per qualsiasi
Assoluto a; quindi due Assoluti hanno lo
stesso profilo e AS8' da' a = b.
Il profilo di g e' esattamente PP.
-------------------------------------------------------------------------------
26. COROLLARI E TEOREMI AGGIUNTIVI
F5 (equivalenza di presentazione). Per
ogni formula chiusa psi dello
Stadio II esiste la sua controparte iota(psi)
nello Stadio I (si
relativizzano i quantificatori: forall a ==> forall e
(Ass(e) -> ...),
forall x ==> forall e (Diamond Rel(e) -> ...)
[quantificazione RIGIDA:
in Stadio II i quantificatori sono esterni, mentre
Rel(e) includerebbe
l'esistenza], E_A(a) ==> E(a), E_R(x) ==> E(x), ecc.) e
vale: Sigma2 |= psi sse Sigma1 |= iota(psi).
Dim.: per induzione, M2 |= psi
sse Union(M2) |= iota(psi); poi Teorema F
(F3).
F6 (mal formato =
refutato). Le formule mal formate dello Stadio II hanno
controparti
refutabili nello Stadio I:
"A(x) and R(x)" ~ not exists e (Ass(e) and Rel(e))
(T1)
"Creatore(e) and Creato(e)" ~ T10
"Caus(g,y)" ~ T11
"Assoluto
risultato di processo"~ T15
"Dip(a,x) con a:A" ~ T4b: not exists h F(h,a) per
Ass(a)
Dunque nessuna formula mal formata dello Stadio II esprime una
possibilita'
che lo Stadio I ammetterebbe: la mal formazione e' la forma
sintattica di
una refutazione dimostrata. Questo risponde all'obiezione sul
"contenuto
perso" nel passaggio da v2.1 a v2.2.
T18 (ex nihilo).
Cr(g,x) -> ExNihilo(g,x) [T5, T8, D13]
Dim.: D13 chiede che non esista h con
E(h), not Dip(h), h != g e
PrincipioDi(h,x). Se E(h) e not Dip(h), per T5
Nec(h), quindi Ass(h), e per
T8 h = g: contro h != g. Il principio
indipendente di x e' solo g.
(Il contenuto "ex nihilo" segue dall'unicita':
nessuna materia
preesistente e non dipendente puo' esistere accanto a g. Una
materia
dipendente da g non e' un principio indipendente di x.)
-------------------------------------------------------------------------------
27. STATO FINALE, LIMITI E REGISTRO
Provato in v2.4:
- Teorema F:
corrispondenza biunivoca fra i modelli dei due stadi e
equivalenza semantica
delle teorie (e deduttiva per la parte di primo
ordine, sotto completezza di
QS5 many-sorted).
- Consistenza di entrambe le teorie, con fatti e processi,
tramite N0.
- Indipendenza di AN2 (N_A, N_B) e di AS-N (N_N).
- F5, F6,
T18.
Limiti rimasti, dichiarati:
1. Le dimostrazioni sono matematiche,
non verificate da un assistente di
dimostrazione (Coq, Lean, Isabelle). La
meccanizzazione e' lavoro
futuro.
2. AS8'-AS10' sono schemi infinitari;
per questi Teorema F vale solo a
livello semantico.
3. L'indipendenza e'
mostrata per AN2, AS-N (sezione 24) e AS3-AS6 (sezione
29, v2.8); non per le
altre assunzioni.
4. N0 e' un modello finito e piccolo: mostra la
consistenza, non la
ricchezza. Non dice che il mondo reale lo soddisfi.
5.
L'equivalenza F5 mostra che lo Stadio II e' una presentazione
equivalente
dello Stadio I. Il "genere comune" En e' eliminato dalla
teoria, ma compare
ancora nel metalinguaggio in cui l'equivalenza e'
dimostrata. Questo limite
non e' rimovibile con mezzi puramente
formali: dipende da cosa si accetta
come discorso sul sistema.
6. AS-N, AN1, AS1-AS10 restano assunzioni; il
teorema F non le giustifica,
le rende soltanto esplicite e coerenti.
Registro delle modifiche v2.3 -> v2.4:
1. Dimostrato il principio di fedelta'
(Teorema F, Lemmi 1-4).
2. Aggiunti AX3R' e AX4R' (L1) e la traduzione di
AS1-AS10 (L2).
3. Rilettura di AS3 con Totalizza unario (L3).
4. Qual
rigida e definizione di PP (L4, sezione 25).
5. Modelli estesi a fatti e
processi (N0), con N_A, N_B, N_N.
6. Indipendenza di AS-N; consistenza; T18.
7. F5 e F6 (equivalenza di presentazione; mal formato = refutato).
###############################################################################
PARTE VI - VERIFICA MECCANICA E CORREZIONI (v2.5)
###############################################################################
28. VERIFICA DELLE DIMOSTRAZIONI
28.1 Verifica meccanica dei modelli
(esito v2.5; script esteso in sezione 29)
Lo script controlla, su modelli
finiti a due mondi, ogni assioma e i teoremi
indicati.
- N_A e N_B
(Sigma2): 18 controlli (S1-S8, S10, S11, S2a/S2b, EX, AN1',
AS1'-AS5'), tutti
superati.
- Union(N_A) e Union(N_B) (Sigma1): 32 controlli (AX1-AX9,
AX11-AX15,
AN1, AS1-AS5, AS7, T1, T2, T4, T5, T6, T7, T8, T15, T16, T17,
AS-N),
tutti superati.
- Part(Union(M)) = M in entrambi: la corrispondenza
fra gli stadi
funziona su questi esempi.
- AN2 vera in N_A e falsa in N_B;
T14 (esiste un relativo non ricevuto)
vera in N_A e falsa in N_B, come
atteso. Indipendenza di Dom -> Accoglie
confermata.
- N_N (Sigma1 con un
ente necessario e dipendente): falliscono
esattamente AS-N e T16; tutto il
resto vale. Indipendenza di AS-N
confermata.
28.2 Errore corretto:
Lemma 3, caso atomico Rel
Nella v2.4 la traduzione dava tau(Rel(x)) = vero
per ogni x di sorta R. Ma
in un mondo dove x non esiste Rel(x) e' falso (Rel
include E). Lo script lo
mostra su x in w2. Corretto: tau(Rel(x)) = E_R(x).
Di conseguenza F5 usa la
quantificazione rigida forall e (Diamond Rel(e) ->
...) per tradurre
forall x.
28.3 Lacune chiuse
L5. PrincipioDi non
era coperto dal Lemma 1(e): una coppia
relativo-relativo andava persa e
Part/Union non erano inverse.
Aggiunti AX16 e le firme PrincipioDi_AR,
PrincipioDi_RR.
L6. Totalizza era binario nello Stadio I e unario nello
Stadio II. Ora e'
unario ovunque (AS3 riformulato).
L7. Lo Stadio I usava
E(e) come fatto senza costruttore. Aggiunto AX0
(ex, Ver).
L8. Qual era
rigido solo nello Stadio II. Ora e' rigido in entrambi.
L9. La lista di
assiomi dello Stadio II compariva due volte (sezioni 14 e
22). La sezione 14
rimanda alla 22, con tabella di corrispondenza.
28.4 Osservazione su T6
Con AX7 e AX8, se esiste anche un solo relativo, esiste gia' un Assoluto.
T6
non e' indipendente dal blocco creazione: dimostra l'esistenza
dell'Assoluto
anche senza assumere che qualcosa sia creato, ma non e'
l'unica via. Chi usa
AX8 non ha bisogno di T6 per concludere che g esiste,
dato un relativo
esistente.
28.5 Limiti della verifica (aggiornati in sezione 29.3)
-
Il controllo meccanico copre solo modelli finiti a due mondi. Non
dimostra i
teoremi in generale ne' il Teorema F.
- Lo script non copre T3 (istanza di
AX1), T9-T13 e T18 (richiedono
PrincipioDi e ExNihilo, vuoti nel modello),
AS6 (equivale ad aciclicita'
in un modello finito), AS-C (Caus vuoto) e
AS8-AS10 (un solo Assoluto).
Questi restano verificati a mano.
- I Lemmi
1-4 e il Teorema F sono dimostrazioni su carta, non meccanizzate
in un
assistente di dimostrazione (Coq, Lean, Isabelle).
- AS8-AS10 sono schemi
infinitari: per essi vale solo l'enunciato
semantico.
- Restano ferme le
assunzioni AS-N, AN1 e AS1-AS10: la verifica ne mostra
la coerenza, non la
verita'.
28.6 Registro delle modifiche v2.4 -> v2.5
1. Corretto
tau(Rel) (Lemma 3) e F5.
2. Aggiunti AX16 e le firme
PrincipioDi_AR/PrincipioDi_RR.
3. Totalizza unario ovunque.
4. Aggiunto
AX0 (costruttore ex e predicato Ver).
5. Qual rigido anche nello Stadio I.
6. Unificata la lista assiomi dello Stadio II (sezione 14 -> sezione 22).
7.
Aggiunta l'osservazione su T6 (sezione 28.4).
8. Aggiunta l'avvertenza sui
quantificatori dello Stadio I.
9. Aggiunta la verifica meccanica (Appendice
A) e la sezione 28.
###############################################################################
PARTE VII - COMPLEMENTO v2.8: INDIPENDENZA, SEZIONI 30-32 RISCRITTE, PIANO LEAN
###############################################################################
29. MODELLI DI INDIPENDENZA E MODELLO N1 (verificati dallo script, Appendice
A)
Origine. Il testo v2.7 fornito dall'autore dichiarava modelli V_AS3,
V_AS4,
V_AS5 e N1 senza definirli, e una "meccanizzazione Lean 4" senza
codice. Qui i
modelli sono definiti e verificati; il piano Lean e' dichiarato
come piano
(sezione 33). Il numero dei controlli e' quello dello script
(Appendice A).
29.1 Modello N1 (tre mondi: creazione, causazione seconda,
principi)
W = {w1,w2,w3}, ~ universale. U_A = {g}; U_R = {m,x,y} (m
"materia", x e y
enti derivati).
D_R(w1) = {m,x,y}; D_R(w2) = {m,x};
D_R(w3) = vuoto.
Cr = Fonda_AR = {(g,e) : e in D_R(w)} in ogni mondo.
Fonda_RR: w1 {(m,x),(x,y),(m,y)}; w2 {(m,x)}; w3 vuoto.
Caus_RR: w1 {(x,y)}.
FondatoDa: w1 {(u1,y)}.
PrincipioDi_RR: w1 {(m,x),(m,y)}; w2 {(m,x)}.
PrincipioDi_AR: vuoto.
Dom = {(e,g) : e in D_R(w)}. Accoglie: w1 {(g,x)};
altrove vuoto.
Fatti: P = parti di W (8 fatti); Exp = {(1,p) : p
contingente}, con 1 = W;
Fp_A = {(g,p) : p in P}; Totalizza(B) a w sse B e'
l'insieme dei mondi con
gli stessi relativi esistenti di w. Qual = {Ph1,Ph2},
PP = {Ph1}; Ph1(g),
non Ph2(g).
Che cosa mostra:
- convivono la
creazione di ogni relativo da parte di g (Cr), la
fondazione seconda fra
relativi (m -> x -> y), la causazione seconda
(Caus_RR) e i principi
materiali dipendenti (PrincipioDi_RR);
- T18 (ex nihilo) vale: m e' principio
di x e di y ma dipende da g, quindi
non e' un "principio indipendente" ai
sensi di D13. Lettura imposta da
D13: ex nihilo = assenza di principio
indipendente, non assenza di
materia dipendente;
- ogni relativo e'
contingente (w3 e' vuoto) e AN2 e' vera: a w1 m e' in
domanda e non e'
accolto.
29.2 Modelli di violazione singola
V_AS3: N1 con Totalizza
vuoto. Viola solo AS3. Cautela: Totalizza e' un
primitivo libero, quindi
l'indipendenza e' "a buon mercato": mostra solo
che AS3 non si deriva dal
resto.
V_AS3b (degenere): nessun ente (U_A = U_R = vuoto), P = {0,1}, nessun
fatto
contingente. Viola AS3 e T6. Mostra che e' AS3, non il resto, a imporre
l'Assoluto: senza AS3, T6 non e' derivabile. Vale solo se la semantica
ammette sort vuoti; se richiede almeno un Assoluto in ogni modello, T6 e'
vero per costruzione e il ruolo di AS3 si legge soltanto con V_AS3.
V_AS4: N1
piu' Exp({w1,w2},{w1}). A w1 il fatto contingente {w1,w2} spiega
il fatto
totalizzante {w1}. Viola solo AS4. La transitivita' resta
(Exp(1,{w1,w2}) e
Exp({w1,w2},{w1}) danno Exp(1,{w1}), gia' presente).
V_AS5: N1 con Fp_A
vuoto: nessun ente fonda il fatto totalizzante pur
avendo una spiegazione
ultima. Viola solo AS5.
V_AS6 (infinito): W = {w1,w2}; U_A = {g}; U_R = {x_i
: i in N};
D_R(w1) = U_R, D_R(w2) = vuoto; Fonda_RR(x_j,x_i) a w1 sse j > i;
Cr = Fonda_AR = {(g,x_i)}; Dom = {(x_i,g)}; FondatoDa(u1,x_0); fatti ed
Exp
come in N0.
Verifica a mano: S1 (j > i e' irriflessiva); S2a (k > j > i
implica
k > i); S2b, S6, S7 (g fonda e crea ogni x_i); S3, S4 (tutti gli x_i
esistono negli stessi mondi); S5, S8, S10, S11; AN1'; AS1'-AS5', AS7'
come in
N0. Viola S12/AS6: la catena "x_(i+1) fonda x_i" e' infinita
discendente.
Verifica meccanica: lo script controlla una FINESTRA di 12 elementi: gli
assiomi universali passano e la catena e' presente, ma una finestra
finita e'
ben fondata, quindi lo script NON puo' falsificare AS6.
L'indipendenza di AS6
poggia sulla dimostrazione a mano.
Stato di indipendenza: AN2, AS-N, AS3,
AS4, AS5 (meccanica); AS6 (a mano).
Non mostrata: AS1, AS2, AS7, AS8-AS10,
AN1 e gli assiomi strutturali.
29.3 Risultati e copertura
Output dello
script (Appendice A), non modificato:
== N0_A (Accoglie vuoto)
Sigma2:
30 controlli, falliti: nessuno (attesi: -)
Sigma1 su Union: 43 controlli,
falliti: nessuno (attesi: -)
Part(Union(M)) == M : True | AN2=True | T14=True
Lemma 3 (atomi Ass/E/Rel/F): True | tau v2.4 (Rel=>vero) discordante su 1
coppie; tau v2.8 (Rel=>E_R) su 0
ESITO: OK
== N0_B (Accoglie = Dom^-1)
Sigma2: 30 controlli, falliti: nessuno (attesi: -)
Sigma1 su Union: 43
controlli, falliti: nessuno (attesi: -)
Part(Union(M)) == M : True |
AN2=False | T14=False
Lemma 3 (atomi Ass/E/Rel/F): True | tau v2.4
(Rel=>vero) discordante su 1 coppie; tau v2.8 (Rel=>E_R) su 0
ESITO: OK
==
N1 (tre mondi)
Sigma2: 30 controlli, falliti: nessuno (attesi: -)
Sigma1
su Union: 43 controlli, falliti: nessuno (attesi: -)
Part(Union(M)) == M :
True | AN2=True | T14=True
Lemma 3 (atomi Ass/E/Rel/F): True | tau v2.4
(Rel=>vero) discordante su 4 coppie; tau v2.8 (Rel=>E_R) su 0
ESITO: OK
==
V_AS3 (N1, Totalizza vuoto) [indipendenza di AS3]
Sigma2: 30 controlli,
falliti: ['AS3p'] (attesi: ['AS3p'])
Sigma1 su Union: 43 controlli, falliti:
['AS3'] (attesi: ['AS3'])
Part(Union(M)) == M : True | AN2=True | T14=True
Lemma 3 (atomi Ass/E/Rel/F): True | tau v2.4 (Rel=>vero) discordante su 4
coppie; tau v2.8 (Rel=>E_R) su 0
ESITO: OK
== V_AS3b (degenere: nessun
ente) [T6 non derivabile senza AS3; sort vuoti]
Sigma2: 30 controlli,
falliti: ['AS3p', 'T6p'] (attesi: ['AS3p', 'T6p'])
Sigma1 su Union: 43
controlli, falliti: ['AS3', 'T6'] (attesi: ['AS3', 'T6'])
Part(Union(M)) == M
: True | AN2=False | T14=False
Lemma 3 (atomi Ass/E/Rel/F): True | tau v2.4
(Rel=>vero) discordante su 0 coppie; tau v2.8 (Rel=>E_R) su 0
ESITO: OK
==
V_AS4 (N1 + Exp(p,B) con p contingente) [indipendenza di AS4]
Sigma2: 30
controlli, falliti: ['AS4p'] (attesi: ['AS4p'])
Sigma1 su Union: 43
controlli, falliti: ['AS4'] (attesi: ['AS4'])
Part(Union(M)) == M : True |
AN2=True | T14=True
Lemma 3 (atomi Ass/E/Rel/F): True | tau v2.4 (Rel=>vero)
discordante su 4 coppie; tau v2.8 (Rel=>E_R) su 0
ESITO: OK
== V_AS5 (N1,
Fp_A vuoto) [indipendenza di AS5]
Sigma2: 30 controlli, falliti: ['AS5p']
(attesi: ['AS5p'])
Sigma1 su Union: 43 controlli, falliti: ['AS5'] (attesi:
['AS5'])
Part(Union(M)) == M : True | AN2=True | T14=True
Lemma 3 (atomi
Ass/E/Rel/F): True | tau v2.4 (Rel=>vero) discordante su 4 coppie; tau v2.8
(Rel=>E_R) su 0
ESITO: OK
== V_AS6 (finestra N=12) [finestra finita:
AS6/S12 non falsificabili qui]
Sigma2: 30 controlli, falliti: nessuno
(attesi: -)
Sigma1 su Union: 43 controlli, falliti: nessuno (attesi: -)
Part(Union(M)) == M : True | AN2=True | T14=True
Lemma 3 (atomi Ass/E/Rel/F):
True | tau v2.4 (Rel=>vero) discordante su 12 coppie; tau v2.8 (Rel=>E_R) su 0
ESITO: OK
catena discendente x(i+1) fonda x(i) presente su tutta la finestra:
True
(la violazione di AS6 nel modello infinito e' per costruzione, vedi
sezione 29.2)
== N_N (necessario e dipendente) [indipendenza di AS-N]
Sigma1: 43 controlli, falliti: ['AS-N', 'T16'] (attesi: ['AS-N', 'T16'])
ESITO: OK
== N0 + relativo fantasma z (esiste in nessun mondo)
Part(Union(M)) == M : False (atteso False: serve la convenzione U_R = unione dei
D_R(w))
TUTTE LE ATTESE RISPETTATE
Test di sensibilita' (Appendice
B): 13 guasti introdotti in N1, ciascuno
rilevato da almeno un assioma;
nessun controllo risulta vacuo:
ciclo: Fonda_RR(y,m) a w1 Sigma2 ['S12',
'S2a', 'S4'] | Sigma1 ['AS6', 'AX2', 'AX4', 'T2']
manca il creatore di y a w1
Sigma2 ['S2b', 'S6', 'T9p'] | Sigma1 ['AX2', 'AX8', 'T9']
manca Dom di m a w1
Sigma2 ['AN1p', 'T9pp'] | Sigma1 ['AN1']
Accoglie(g,m) senza Dom Sigma2
['AN1p', 'S10', 'T9pp'] | Sigma1 ['AN1', 'AX11']
FondatoDa su ente
inesistente (m a w3) Sigma2 ['EX', 'S11'] | Sigma1 ['AX14']
Fonda_RR(m,y) a
w2, dove y non esiste Sigma2 ['EX', 'S2b', 'S3'] | Sigma1 ['AX2', 'AX3']
Fonda_RR(x,m) a w1 (ciclo con (m,x)) Sigma2 ['S12', 'S2a'] | Sigma1 ['AS6',
'AX2', 'T2']
manca (m,y): transitivita' violata Sigma2 ['S2a'] | Sigma1
['AX2']
secondo Assoluto h, principio indipendente di x Sigma2 ['AS9p',
'T18', 'T9p', 'T9pp'] | Sigma1 ['AS9', 'T18', 'T8', 'T9']
Exp non transitiva
Sigma2 ['AS4p', 'AS7p'] | Sigma1 ['AS4', 'AS7']
m esiste in ogni mondo
(diventa necessario) Sigma2 ['S8'] | Sigma1 ['AS-N', 'AX13', 'AX7', 'T16']
creazione non essenziale: Cr(g,x) assente a w2 Sigma2 ['S2b', 'S6', 'S7', 'T9p']
| Sigma1 ['AX2', 'AX8', 'AX9', 'T9']
PrincipioDi su relativo inesistente
(m,x) a w3 Sigma2 ['EX'] | Sigma1 ['AX16']
Tutti i guasti sono stati
rilevati.
Copertura aggiornata rispetto a 28.5: lo script controlla ora
anche AX0,
AX16, AS-C, AS8-AS10, T9, T10, T11, T18 e il Lemma 3 a livello di
atomi.
T3 e T12 sono istanze di AX1 e AX11 (controllate come tali); T13 e' il
metateorema mostrato da N0_A/N0_B; T14 e' valutato come informazione.
Restano
a carico della dimostrazione a mano i teoremi in generale (i
controlli
valgono sui modelli dati), i Lemmi 1-4 e il Teorema F.
29.4 Errata emerse
dalla verifica
L10. Relativi fantasma. Se U_R contiene un elemento che non
esiste in alcun
mondo, Union lo include in U ma Part non lo recupera (Rel
richiede
l'esistenza): Part(Union(M)) != M. Lo script lo mostra con un
relativo z.
Convenzione adottata: U_R = unione dei D_R(w), analoga a U =
unione dei
D(w) nello Stadio I. Lemma 2, Lemma 4 e Teorema F (F3) valgono sui
modelli che la rispettano.
L11. Lemma 3, verifica a livello di atomi. Su ogni
modello lo script
controlla che tau v2.8 (Rel(x) => E_R(x)) concordi con la
valutazione
nello Stadio I, mentre tau v2.4 (Rel(x) => vero) discorda su
tutte le
coppie (relativo, mondo) in cui il relativo non esiste: 1 coppia in
N0,
4 in N1, 12 nella finestra di V_AS6. La correzione della v2.5 e' quindi
confermata.
L12. AX15 e AS-N. Nello Stadio I, AX15 e' formulata con Rel,
quindi in un
modello che viola AS-N puo' essere vacuamente vera: se un
relativo
esiste in ogni mondo diventa necessario e dipendente, non e' piu'
Rel,
e AX15 resta vera senza alcun Rel (il test di sensibilita' lo mostra:
cade S8 nello Stadio II, non AX15 nello Stadio I). AX15 va letta
insieme ad
AS-N. Il Teorema F non e' toccato: F1 usa il Lemma 1(c), che
dipende da AS-N.
30. STATUTO DEI SORT (riscrittura della sezione 30 della v2.7)
La
v2.7 sosteneva che l'obiezione di "petizione di principio sintattica" fosse
risolta. Cosi' formulato e' troppo. La posizione corretta e':
(a) La
separazione dei sort non e' postulata: segue da T16 e T17 (Stadio I)
sotto
AS-N, ed e' tradotta fedelmente dal Teorema F.
(b) Il peso della petizione si
sposta su AS-N (aseita': cio' che e'
necessario non e' dipendente). AS-N e'
sostanziale e dichiarata; N_N
mostra che e' indipendente dal resto.
(c)
Chi rifiuta AS-N non puo' passare allo Stadio II: ammette un
"necessario
dipendente" (l'ente n di N_N), che richiede una terza
sorta. Dunque la scelta
dei sort e' condizionale ad AS-N: non
arbitraria, ma nemmeno incondizionata.
(d) Limite non eliminabile: la dimostrazione dell'equivalenza usa un dominio
comune nel metalinguaggio (27, limite 5). L'affermazione "il genere
comune
compare solo nell'impalcatura" vale per la teoria, non per il
discorso sulla
teoria.
31. LO SCARTO: INDIPENDENZA, NON NON-COMPUTABILITA' (riscrittura
della 31)
(a) T13 e' un risultato di INDIPENDENZA logica: l'enunciato
Dom -> Accoglie non e' derivabile dagli assiomi (modelli N0_A, N0_B).
Non e'
un teorema di non-computabilita': l'indipendenza di un enunciato
da una
teoria e' compatibile con teorie decidibili e non dice nulla
sulla natura
algoritmica dell'Assoluto. La lettura "l'Assoluto non e'
una funzione
algoritmica" non segue e non va asserita come teorema.
(b) AN2' e' piu' forte
dell'indipendenza: afferma la POSSIBILITA' di una
domanda non accolta. T14'
ne e' conseguenza (con T8' e AX13).
(c) Per sostenere la tesi teologica
(l'accoglienza non e' un output del
relativo) serve una premessa a parte, qui
solo PROPOSTA e NON inclusa
in Sigma2:
AL (proposta): l'accoglienza non e'
determinata dal profilo
qualitativo del relativo:
Diamond exists x exists
y (StessoProfiloR(x,y) and Accoglie(g,x)
and not Accoglie(g,y)),
con
StessoProfiloR definito sulle proprieta' qualitative rigide dei
relativi (da
definire, per analogia con Qual). AL non e' modellata ne'
verificata.
32. AS1 E STOCASTICITA' (riscrittura della sezione 32 della v2.7)
(a) La
risposta della v2.7 funziona grazie a T7 (spiegare non e'
necessitare): Exp
non impone determinismo, quindi un sistema
stocastico e' compatibile con AS1.
I modelli N0 e N1 lo mostrano: un
fatto necessario (1) spiega fatti
contingenti senza collasso modale
(T7 e' verificato in ogni modello).
(b)
Resta il problema classico del collasso modale del principio di ragion
sufficiente (Van Inwagen; Pruss): se la spiegazione necessitasse
l'esplicando, ogni fatto sarebbe necessario; se non lo necessita
(T7),
occorre dire che cosa renda "adeguata" una spiegazione che non
seleziona
l'esito. Nel sistema Exp e' PRIMITIVO e "adeguata" non e'
definita: i modelli
mostrano consistenza, non giustificazione.
(c) Due letture possibili
dell'adeguatezza, entrambe esterne al sistema
attuale: (i) esplicazione
personale: il fatto ultimo e' un atto libero
dell'Assoluto per una ragione
che inclina senza necessitare;
(ii) esplicazione probabilistica: p rende q
probabile in senso non
banale. Nessuna delle due e' assiomatizzata.
(d)
Tensione con AS4. AS4 vuole che l'ultima spiegazione di B sia non
contingente; un atto libero che spieghi B non potrebbe essere un fatto
contingente nel senso di D1. Il rapporto fra spiegazione ultima non
contingente e libera creazione e' il punto piu' delicato del sistema e
resta
APERTO.
33. PIANO LEAN 4 (NON ESEGUITO)
Stato: in questa sessione
non e' stato scritto ne' verificato alcun codice
Lean. La v2.7 parlava di
"formalizzazione completa in Lean 4 per audit
tramite #print axioms": non
esiste. Piano:
1. Tipi: mondi W con ~ universale; sort A e R come tipi
distinti; fatti
P := Set W.
2. Modelli finiti N0, N1, N_N, V_AS* come
strutture su Fin n, con gli
assiomi come proposizioni decidibili (decide).
3. Teoremi T1-T8, T16, T17 nello Stadio I.
4. Teorema F: Part e Union come
funzioni, Lemmi 1-4.
5. Audit: #print axioms su ogni teorema, per mostrare
quali assiomi usa.
Difficolta': alta per il Teorema F (modelli come strutture
dipendenti);
AS8-AS10 (schemi infinitari) richiederebbero quantificazione
sulle
proprieta' (second'ordine).
Criterio di accettazione: un teorema e'
"meccanizzato" solo se compila senza
sorry e #print axioms mostra soltanto
gli assiomi dichiarati.
34. STATO FINALE v2.8
Verificato
meccanicamente (modelli finiti): consistenza di Sigma1 e Sigma2
(N0, N1);
indipendenza di AN2, AS-N, AS3, AS4, AS5; corrispondenza
Part/Union sui
modelli; Lemma 3 a livello di atomi; T7, T9, T10, T11, T18 e
gli assiomi nei
modelli; sensibilita' dei controlli.
Dimostrato a mano: Lemmi 1-4 e Teorema
F; indipendenza di AS6 (modello
infinito).
Preso dalla v2.7: T8b e
T9'' (sezione 15); le sezioni 30-32, riscritte;
l'idea dei modelli N1 e V_AS*
(ora definiti e verificati).
Non ripreso o corretto: la "chiusura meccanica"
e la "meccanizzazione Lean"
(non esistono); la lettura dello scarto come
non-computabilita'; il taglio
di dimostrazioni, Lemmi e script (ripristinati
dalla v2.5).
Limiti rimasti:
1. Le dimostrazioni generali sono su
carta; Lean e' solo un piano.
2. Il controllo meccanico copre modelli finiti
(al piu' tre mondi) e, per
AS6, una finestra finita.
3. L'indipendenza di
AS6 poggia su una prova a mano.
4. V_AS3 e' a buon mercato; V_AS3b richiede
sort vuoti.
5. AS8-AS10 sono schemi infinitari: il Teorema F vale per essi
solo a
livello semantico; nei modelli Qual e' finito.
6. L'adeguatezza
della spiegazione (32) e il rapporto fra AS4 e libera
creazione restano
aperti.
7. AL e' solo proposta, non modellata.
8. Indipendenza non
mostrata per AS1, AS2, AS7, AS8-AS10, AN1.
9. Un dominio comune compare
ancora nel metalinguaggio dell'equivalenza.
10. AS-N, AN1 e AS1-AS10 restano
assunzioni: i modelli ne mostrano la
coerenza, non la verita'.
Registro delle modifiche v2.5 -> v2.8:
1. Definiti e verificati N1, V_AS3,
V_AS3b, V_AS4, V_AS5, V_AS6 (sezione 29).
2. Script esteso (T9, T10, T11,
T18, AX0, AX16, AS-C, AS8-AS10, Lemma 3,
convenzione sui fantasmi); aggiunto
il test di sensibilita'.
3. Errata L10 (relativi fantasma), L11 (Lemma 3
verificato), L12 (AX15).
4. Teorema F: ipotesi U_R = unione dei D_R(w).
5.
T8b e T9'' aggiunti alla sezione 15.
6. Sezioni 30-32 riscritte (sort
condizionali ad AS-N; indipendenza e non
computabilita'; collasso modale e
spiegazione).
7. Piano Lean dichiarato come piano (sezione 33).
8. Sezione
27, limite 3, aggiornato.
###############################################################################
APPENDICE A - SCRIPT DI VERIFICA (check_models_v28.py)
###############################################################################
Esecuzione: python3 -I check_models_v28.py (Python 3, nessuna dipendenza)
#!/usr/bin/env python3
# check_models_v28.py - verifica meccanica
dell'assiomatica di adriano53s v2.8
# Python 3, nessuna dipendenza.
Esecuzione: python3 -I check_models_v28.py
import sys
import itertools
def powerset(W):
W = list(W)
return [frozenset(c) for r in
range(len(W) + 1) for c in itertools.combinations(W, r)]
def
acyclic(edges):
g = {}
for a, b in edges:
g.setdefault(a, set()).add(b)
state = {}
def dfs(n):
state[n] = 1
for m in g.get(n, ()):
s =
state.get(m, 0)
if s == 1 or (s == 0 and not dfs(m)):
return False
state[n] = 2
return True
return all(dfs(n) for n in list(g) if
state.get(n, 0) == 0)
def facts_and_exp(W):
"""P = parti di W;
Exp(1,p) per ogni fatto contingente p."""
P = powerset(W)
ONE, ZERO =
frozenset(W), frozenset()
return P, {(ONE, p) for p in P if p not in (ZERO,
ONE)}
def tot_standard(W, rels):
"""Totalizza(B) a w sse B =
insieme dei mondi con gli stessi relativi esistenti di w."""
return {w:
{frozenset(v for v in W if rels[v] == rels[w])} for w in W}
PROPS =
{'Ph1': {'g'}, 'Ph2': set()}
PP = {'Ph1'}
#
----------------------------------------------------------------- modelli ---
def n0(acc_full):
W = ['w1', 'w2']
DR = {'w1': {'x'}, 'w2': set()}
P,
EXP = facts_and_exp(W)
Cr = {'w1': {('g', 'x')}, 'w2': set()}
return dict(
name='N0_B (Accoglie = Dom^-1)' if acc_full else 'N0_A (Accoglie vuoto)',
W=W, UA={'g'}, UR={'x'}, DR=DR, FAR=Cr, FRR={w: set() for w in W}, Cr=Cr,
Dom={'w1': {('x', 'g')}, 'w2': set()},
Acc={'w1': {('g', 'x')} if acc_full
else set(), 'w2': set()},
Caus={w: set() for w in W}, FD={'w1': {('u1',
'x')}, 'w2': set()},
FpA={w: {('g', p) for p in P} for w in W}, FpR={w: set()
for w in W},
PrAR={w: set() for w in W}, PrRR={w: set() for w in W},
P=P,
EXP=EXP, TOT=tot_standard(W, DR), props=PROPS, PP=PP)
def n1():
"""Tre mondi: creazione, fondazione fra relativi, causazione seconda,
principi."""
W = ['w1', 'w2', 'w3']
DR = {'w1': {'m', 'x', 'y'}, 'w2':
{'m', 'x'}, 'w3': set()}
P, EXP = facts_and_exp(W)
Cr = {w: {('g', e) for
e in DR[w]} for w in W}
return dict(
name='N1 (tre mondi)', W=W, UA={'g'},
UR={'m', 'x', 'y'}, DR=DR,
FAR=Cr, FRR={'w1': {('m', 'x'), ('x', 'y'), ('m',
'y')}, 'w2': {('m', 'x')}, 'w3': set()},
Cr=Cr, Dom={w: {(e, 'g') for e in
DR[w]} for w in W},
Acc={'w1': {('g', 'x')}, 'w2': set(), 'w3': set()},
Caus={'w1': {('x', 'y')}, 'w2': set(), 'w3': set()},
FD={'w1': {('u1', 'y')},
'w2': set(), 'w3': set()},
FpA={w: {('g', p) for p in P} for w in W}, FpR={w:
set() for w in W},
PrAR={w: set() for w in W},
PrRR={'w1': {('m', 'x'),
('m', 'y')}, 'w2': {('m', 'x')}, 'w3': set()},
P=P, EXP=EXP,
TOT=tot_standard(W, DR), props=PROPS, PP=PP)
def variant(m, name,
**kw):
v = dict(m)
v['name'] = name
v.update(kw)
return v
def v_as3():
m = n1()
return variant(m, 'V_AS3 (N1, Totalizza vuoto)',
TOT={w: set() for w in m['W']})
def v_as3b():
W = ['w1', 'w2']
P = powerset(W)
e = {w: set() for w in W}
return dict(name='V_AS3b
(degenere: nessun ente)', W=W, UA=set(), UR=set(), DR=e,
FAR=e, FRR=e, Cr=e,
Dom=e, Acc=e, Caus=e, FD=e, FpA=e, FpR=e, PrAR=e, PrRR=e,
P=[frozenset(),
frozenset(W)], EXP=set(), TOT={w: set() for w in W},
props={}, PP=set())
def v_as4():
m = n1()
EXP = set(m['EXP']) | {(frozenset({'w1',
'w2'}), frozenset({'w1'}))}
return variant(m, 'V_AS4 (N1 + Exp(p,B) con p
contingente)', EXP=EXP)
def v_as5():
m = n1()
return variant(m,
'V_AS5 (N1, Fp_A vuoto)', FpA={w: set() for w in m['W']})
def
v_as6_window(N=12):
W = ['w1', 'w2']
xs = ['x%d' % i for i in range(N)]
DR = {'w1': set(xs), 'w2': set()}
P, EXP = facts_and_exp(W)
Cr = {'w1':
{('g', x) for x in xs}, 'w2': set()}
FRR = {'w1': {(xs[j], xs[i]) for j in
range(N) for i in range(N) if j > i}, 'w2': set()}
return dict(name='V_AS6
(finestra N=%d)' % N, W=W, UA={'g'}, UR=set(xs), DR=DR,
FAR=Cr, FRR=FRR,
Cr=Cr, Dom={'w1': {(x, 'g') for x in xs}, 'w2': set()},
Acc={w: set() for w
in W}, Caus={w: set() for w in W},
FD={'w1': {('u1', xs[0])}, 'w2': set()},
FpA={w: {('g', p) for p in P} for w in W}, FpR={w: set() for w in W},
PrAR={w: set() for w in W}, PrRR={w: set() for w in W},
P=P, EXP=EXP,
TOT=tot_standard(W, DR), props=PROPS, PP=PP)
def to_stage1(m):
W,
UA, UR = m['W'], set(m['UA']), set(m['UR'])
D = {w: UA | set(m['DR'][w]) for
w in W}
s = dict(name=m['name'], W=W, U=UA | UR, D=D,
F={w:
set(m['FAR'][w]) | set(m['FRR'][w]) for w in W},
Cr=m['Cr'], Dom=m['Dom'],
Acc=m['Acc'], Caus=m['Caus'], FD=m['FD'],
Fp={w: set(m['FpA'][w]) |
set(m['FpR'][w]) for w in W},
Pr={w: set(m['PrAR'][w]) | set(m['PrRR'][w])
for w in W},
P=m['P'], EXP=m['EXP'], TOT=m['TOT'], props=m['props'],
PP=m['PP'])
s['ex'] = {e: frozenset(w for w in W if e in D[w]) for e in
s['U']}
return s
def n_n():
"""Stadio I: ente necessario ma
dipendente (viola AS-N)."""
W = ['w1', 'w2']
D = {'w1': {'g', 'x', 'n'},
'w2': {'g', 'n'}}
P, EXP = facts_and_exp(W)
rels = {w: D[w] & {'x'} for w
in W}
s = dict(name='N_N (necessario e dipendente)', W=W, U={'g', 'x', 'n'},
D=D,
F={'w1': {('g', 'x'), ('g', 'n')}, 'w2': {('g', 'n')}},
Cr={'w1':
{('g', 'x')}, 'w2': set()}, Dom={'w1': {('x', 'g')}, 'w2': set()},
Acc={w:
set() for w in W}, Caus={w: set() for w in W},
FD={'w1': {('u1', 'x')}, 'w2':
set()},
Fp={w: {('g', p) for p in P} for w in W}, Pr={w: set() for w in W},
P=P, EXP=EXP, TOT=tot_standard(W, rels), props=PROPS, PP=PP)
s['ex'] = {e:
frozenset(w for w in W if e in D[w]) for e in s['U']}
return s
#
------------------------------------------------------------ Sigma2 (II) ---
def check_sigma2(m):
W, UA, UR, DR, P, EXP = m['W'], m['UA'], m['UR'],
m['DR'], m['P'], m['EXP']
FAR, FRR, Cr, Dom, Acc = m['FAR'], m['FRR'],
m['Cr'], m['Dom'], m['Acc']
Caus, FD, FpA, FpR, PrAR, PrRR = m['Caus'],
m['FD'], m['FpA'], m['FpR'], m['PrAR'], m['PrRR']
props, PPs, TOT = m['props'],
m['PP'], m['TOT']
R = []
def chk(label, cond):
R.append((label,
bool(cond)))
dip = lambda x, w: any((a, x) in FAR[w] for a in UA) or any((y,
x) in FRR[w] for y in UR)
contR = lambda x, w: x in DR[w] and any(x not in
DR[v] for v in W)
exR = lambda x: frozenset(w for w in W if x in DR[w])
contp = lambda p, w: w in p and any(v not in p for v in W)
necp = lambda p:
all(v in p for v in W)
ult = lambda p: not any((q, p) in EXP for q in P)
tot = lambda B, w: B in TOT[w]
ONE = frozenset(W)
chk('AX0p', ONE in P
and all(exR(x) in P for x in UR))
chk('S1', all((x, x) not in FRR[w] for w in
W for x in UR))
chk('S2a', all((x, z) in FRR[w] for w in W for (x, y) in
FRR[w] for (y2, z) in FRR[w] if y == y2))
chk('S2b', all((a, x) in FAR[w] for
w in W for (a, y) in FAR[w] for (y2, x) in FRR[w] if y == y2))
chk('S3', all(x
in DR[w] and y in DR[w] for w in W for (x, y) in FRR[w])
and all(x in DR[w]
for w in W for (a, x) in FAR[w]))
chk('S4', all(x in DR[v] for w in W for (x,
y) in FRR[w] for v in W if y in DR[v]))
chk('S5', all((a, x) in FAR[w] for w
in W for (a, x) in Cr[w]))
chk('S6', all(any((a, x) in Cr[w] for a in UA) for
w in W for x in DR[w]))
chk('S7', all((a, x) in Cr[v] for w in W for (a, x)
in Cr[w] for v in W if x in DR[v]))
chk('S8', any(not DR[w] for w in W))
chk('S10', all((x, a) in Dom[w] for w in W for (a, x) in Acc[w]))
chk('S11',
all(x in DR[w] and dip(x, w) for w in W for (u, x) in FD[w]))
chk('S12', all(acyclic(FRR[w])
for w in W))
chk('EX', all(x in DR[w] for w in W
for (a, x) in list(Cr[w])
+ list(Acc[w]) + list(PrAR[w]) + list(FAR[w]))
and all(x in DR[w] for w in W
for (x, a) in Dom[w])
and all(x in DR[w] and y in DR[w] for w in W for (x, y)
in list(Caus[w]) + list(PrRR[w]) + list(FRR[w]))
and all(x in DR[w] for w in
W for (u, x) in FD[w])
and all(x in DR[w] for w in W for (x, p) in FpR[w]))
chk('AN1p', all(any((x, a) in Dom[w] for a in UA) for w in W for x in DR[w]))
chk('AS1p', all(any((q, p) in EXP for q in P) for w in W for p in P if contp(p,
w)))
chk('AS2p', all(dip(x, w) for w in W for x in UR if contR(x, w)
for p
in P if (p, exR(x)) in EXP and ult(p)))
chk('AS3p', all(any(contp(B, w) and
tot(B, w) for B in P) for w in W))
chk('AS4p', all((p, B) not in EXP for w in
W for B in P if tot(B, w)
for p in P if contp(p, w)))
chk('AS5p', all(any((a,
B) in FpA[w] for a in UA) or any((x, B) in FpR[w] for x in DR[w])
for w in W
for B in P if tot(B, w) for p in P if (p, B) in EXP and ult(p)))
chk('AS7p',
all((p, p) not in EXP for p in P)
and all((p, r) in EXP for (p, q) in EXP for
(q2, r) in EXP if q == q2)
and acyclic(EXP))
prof = lambda a: frozenset(k
for k in props if a in props[k])
chk('AS8p', all(a == b for a in UA for b in
UA if prof(a) == prof(b)))
chk('AS9p', all(a in props[k] for a in UA for k in
PPs))
chk('AS10p', all(k in PPs for a in UA for k in props if a in props[k]))
chk('PP1', (not PPs) or any(all(a in props[k] for k in PPs) for a in UA))
chk('T6p',
len(UA) > 0)
chk('T7', all(not all(v in B for v in q) for w in W for B in P
if contp(B, w)
for q in P if necp(q) and (q, B) in EXP))
chk('T9p', all((a,
x) in FAR[w] for w in W for x in DR[w] for a in UA))
chk('T9pp', all((x, a)
in Dom[w] for w in W for x in DR[w] for a in UA))
chk('T18', all(not any(h !=
a and (h, x) in PrAR[w] for h in UA)
and not any(not dip(y, w) and (y, x) in
PrRR[w] for y in UR)
for w in W for (a, x) in Cr[w]))
info = {'AN2p': any((a,
x) not in Acc[w] for w in W for (x, a) in Dom[w])}
return R, info
# ------------------------------------------------------------ Sigma1 (I) ----
def defs(s):
W, D, F, U = s['W'], s['D'], s['F'], s['U']
E = lambda e, w:
e in D[w]
dip = lambda e, w: any((f, e) in F[w] for f in U)
cont = lambda
e, w: E(e, w) and any(not E(e, v) for v in W)
nec = lambda e, w: E(e, w) and
all(E(e, v) for v in W)
rel = lambda e, w: cont(e, w) and dip(e, w)
ass =
lambda e, w: nec(e, w) and not dip(e, w)
return E, dip, cont, nec, rel, ass
def check_sigma1(s):
W, U, D, F, P, EXP, TOT, ex = (s[k] for k in
('W', 'U', 'D', 'F', 'P', 'EXP', 'TOT', 'ex'))
Cr, Dom, Acc, Caus, FD, Fp, Pr
= (s[k] for k in ('Cr', 'Dom', 'Acc', 'Caus', 'FD', 'Fp', 'Pr'))
props, PPs =
s['props'], s['PP']
E, dip, cont, nec, rel, ass = defs(s)
R = []
def chk(label, cond):
R.append((label, bool(cond)))
contp = lambda p,
w: w in p and any(v not in p for v in W)
necp = lambda p: all(v in p for v in
W)
ult = lambda p: not any((q, p) in EXP for q in P)
tot = lambda B, w: B
in TOT[w]
ABS = {e for e in U for w in W if ass(e, w)}
chk('AX0', all(ex[e]
in P and all((w in ex[e]) == E(e, w) for w in W) for e in U))
chk('AX1', all((e,
e) not in F[w] for w in W for e in U))
chk('AX2', all((e, h) in F[w] for w in
W for (e, f) in F[w] for (f2, h) in F[w] if f == f2))
chk('AX3', all(E(e, w)
and E(f, w) for w in W for (e, f) in F[w]))
chk('AX4', all(E(e, v) for w in W
for (e, f) in F[w] for v in W if E(f, v)))
chk('AX5', all(E(e, w) for w in W
for (e, p) in Fp[w]))
chk('T1', all(not (ass(e, w) and rel(e, w)) for w in W
for e in U))
chk('T2', all((f, e) not in F[w] for w in W for (e, f) in F[w]))
chk('T4', all(nec(h, w) for w in W for (h, e) in F[w] if nec(e, w)))
chk('T5',
all(nec(e, w) for w in W for e in U if E(e, w) and not dip(e, w)))
chk('AS-N',
all(not dip(e, w) for w in W for e in U if nec(e, w)))
chk('T16', all(ass(e,
w) != rel(e, w) for w in W for e in U if E(e, w)))
chk('T17', all((not any(ass(e,
w) for w in W)) or all(ass(e, w) for w in W if E(e, w)) for e in U)
and all((not
any(rel(e, w) for w in W)) or all(rel(e, w) for w in W if E(e, w)) for e in U))
chk('AX6', all((a, e) in F[w] for w in W for (a, e) in Cr[w]))
chk('AX7', all(ass(a,
w) and rel(e, w) for w in W for (a, e) in Cr[w]))
chk('AX8', all(any((a, e)
in Cr[w] for a in U) for w in W for e in U if rel(e, w)))
chk('AX9', all((a,
e) in Cr[v] for w in W for (a, e) in Cr[w] for v in W if E(e, v)))
chk('AX15',
any(not any(rel(e, w) for e in U) for w in W))
chk('AX11', all((x, a) in Dom[w]
for w in W for (a, x) in Acc[w]))
chk('AX12', all(ass(a, w) and rel(x, w) for
w in W for (a, x) in Acc[w]))
chk('AX13', all(ass(a, w) and rel(x, w) for w
in W for (x, a) in Dom[w]))
chk('AN1', all(any((x, a) in Dom[w] and ass(a, w)
for a in U) for w in W for x in U if rel(x, w)))
chk('AX14', all(dip(e, w)
for w in W for (u, e) in FD[w]))
chk('AX16', all(E(e, w) and rel(f, w) for w
in W for (e, f) in Pr[w]))
chk('AS-C', all(rel(e, w) and rel(f, w) for w in W
for (e, f) in Caus[w]))
chk('AS1', all(any((q, p) in EXP for q in P) for w in
W for p in P if contp(p, w)))
chk('AS2', all(dip(e, w) for w in W for e in U
if cont(e, w)
for p in P if (p, ex[e]) in EXP and ult(p)))
chk('AS3', all(any(contp(B,
w) and tot(B, w) for B in P) for w in W))
chk('AS4', all((p, B) not in EXP
for w in W for B in P if tot(B, w) for p in P if contp(p, w)))
chk('AS5', all(any(E(e,
w) and (e, B) in Fp[w] for e in U) for w in W for B in P if tot(B, w)
for p
in P if (p, B) in EXP and ult(p)))
chk('AS6', all(acyclic(F[w]) for w in W))
chk('AS7', all((p, p) not in EXP for p in P)
and all((p, r) in EXP for (p, q)
in EXP for (q2, r) in EXP if q == q2) and acyclic(EXP))
prof = lambda a:
frozenset(k for k in props if a in props[k])
chk('AS8', all(a == b for a in
ABS for b in ABS if prof(a) == prof(b)))
chk('AS9', all(a in props[k] for a
in ABS for k in PPs))
chk('AS10', all(k in PPs for a in ABS for k in props if
a in props[k]))
chk('T6', len(ABS) > 0)
chk('T7', all(not all(v in B for v
in q) for w in W for B in P if contp(B, w)
for q in P if necp(q) and (q, B)
in EXP))
chk('T8', len(ABS) <= 1)
chk('T9', all((g, e) in F[w] for w in W
for e in U if rel(e, w) for g in ABS))
chk('T10', all(not (ass(e, w) and any((e,
x) in Cr[w] for x in U) and any((a, e) in Cr[w] for a in U))
for w in W for e
in U))
chk('T11', all(not ass(e, w) for w in W for (e, f) in Caus[w]))
chk('T15',
all(not (ass(e, w) and any(x == e for (u, x) in FD[w])) for w in W for e in U))
chk('T18', all(not any(E(h, w) and not dip(h, w) and h != a and (h, e) in Pr[w]
for h in U)
for w in W for (a, e) in Cr[w]))
info = {'AN2': any((a, x) not
in Acc[w] for w in W for (x, a) in Dom[w]),
'T14 (esiste un relativo non
ricevuto)':
any(rel(x, w) and not any(ass(a, w) and (a, x) in Acc[w] for a in
U) for w in W for x in U)}
return R, info
#
--------------------------------------------- Part / Union / Lemma 3 -------
def part(s):
W, U, D, F = s['W'], s['U'], s['D'], s['F']
E, dip, cont, nec,
rel, ass = defs(s)
UA = {e for e in U for w in W if ass(e, w)}
UR = {e for
e in U for w in W if rel(e, w)}
sel = lambda rl, f: {w: {t for t in rl[w] if
f(t)} for w in W}
out = dict(
UA=UA, UR=UR, DR={w: D[w] & UR for w in W},
FAR=sel(F, lambda t: t[0] in UA and t[1] in UR), FRR=sel(F, lambda t: t[0] in UR
and t[1] in UR),
Cr=sel(s['Cr'], lambda t: t[0] in UA and t[1] in UR),
Dom=sel(s['Dom'],
lambda t: t[0] in UR and t[1] in UA),
Acc=sel(s['Acc'], lambda t: t[0] in UA
and t[1] in UR),
Caus=sel(s['Caus'], lambda t: t[0] in UR and t[1] in UR),
FD=sel(s['FD'], lambda t: t[1] in UR),
FpA=sel(s['Fp'], lambda t: t[0] in
UA), FpR=sel(s['Fp'], lambda t: t[0] in UR),
PrAR=sel(s['Pr'], lambda t: t[0]
in UA and t[1] in UR),
PrRR=sel(s['Pr'], lambda t: t[0] in UR and t[1] in
UR))
lemma1 = (UA | UR == U and not (UA & UR)
and all(t in out['FAR'][w]
or t in out['FRR'][w] for w in W for t in F[w])
and all(sum(len(out[k][w])
for k in ('Cr',)) == len(s['Cr'][w]) for w in W)
and all(len(out['Dom'][w])
== len(s['Dom'][w]) and len(out['Acc'][w]) == len(s['Acc'][w])
and len(out['Caus'][w])
== len(s['Caus'][w]) and len(out['FD'][w]) == len(s['FD'][w])
and len(out['FpA'][w])
+ len(out['FpR'][w]) == len(s['Fp'][w])
and len(out['PrAR'][w]) + len(out['PrRR'][w])
== len(s['Pr'][w]) for w in W))
return out, lemma1
def
check_lemma3(m, s):
W, UA, UR, DR = m['W'], m['UA'], m['UR'], m['DR']
E,
dip, cont, nec, rel, ass = defs(s)
ok_ass = all(ass(e, w) for e in UA for w
in W) and not any(ass(e, w) for e in UR for w in W)
ok_E = all(E(e, w) == (e
in DR[w]) for e in UR for w in W) and all(E(e, w) for e in UA for w in W)
ok_rel = all(rel(e, w) == (e in DR[w]) for e in UR for w in W) and not any(rel(e,
w) for e in UA for w in W)
old_tau_bad = sum(1 for e in UR for w in W if not
rel(e, w)) # tau di v2.4: Rel(x) => vero
new_tau_bad = sum(1 for e in UR for
w in W if rel(e, w) != (e in DR[w]))
ok_F = all(((e, f) in s['F'][w]) ==
(((e, f) in m['FAR'][w]) or ((e, f) in m['FRR'][w]))
for w in W for e in
s['U'] for f in s['U'])
return ok_ass, ok_E, ok_rel, ok_F, old_tau_bad,
new_tau_bad
KEYS = ['UA', 'UR', 'DR', 'FAR', 'FRR', 'Cr', 'Dom', 'Acc',
'Caus', 'FD', 'FpA', 'FpR', 'PrAR', 'PrRR']
def roundtrip(m):
s =
to_stage1(m)
p, lemma1 = part(s)
return lemma1 and all(p[k] == m[k] for k
in KEYS), s
#
------------------------------------------------------------------ main ----
failures = []
def line(txt):
print(txt)
def run(m,
exp1=(), exp2=(), note=''):
r2, i2 = check_sigma2(m)
rt, s = roundtrip(m)
r1, i1 = check_sigma1(s)
f2 = sorted(l for l, c in r2 if not c)
f1 =
sorted(l for l, c in r1 if not c)
ok = f1 == sorted(exp1) and f2 == sorted(exp2)
if not ok:
failures.append(m['name'])
line('== %s%s' % (m['name'], (' [' +
note + ']') if note else ''))
line(' Sigma2: %d controlli, falliti: %s
(attesi: %s)' % (len(r2), f2 or 'nessuno', sorted(exp2) or '-'))
line('
Sigma1 su Union: %d controlli, falliti: %s (attesi: %s)' % (len(r1), f1 or
'nessuno', sorted(exp1) or '-'))
line(' Part(Union(M)) == M : %s | %s=%s |
%s=%s' % (rt, 'AN2', i1['AN2'], 'T14', i1['T14 (esiste un relativo non
ricevuto)']))
l3 = check_lemma3(m, s)
line(' Lemma 3 (atomi Ass/E/Rel/F):
%s | tau v2.4 (Rel=>vero) discordante su %d coppie; tau v2.8 (Rel=>E_R) su %d'
% (all(l3[:4]), l3[4], l3[5]))
if not all(l3[:4]) or l3[5]:
failures.append(m['name'] + ' (Lemma 3)')
line(' ESITO: %s' % ('OK' if ok
else 'DISCORDANZA'))
return s
run(n0(False))
run(n0(True))
run(n1())
run(v_as3(), exp1=['AS3'], exp2=['AS3p'], note='indipendenza di
AS3')
run(v_as3b(), exp1=['AS3', 'T6'], exp2=['AS3p', 'T6p'], note='T6 non
derivabile senza AS3; sort vuoti')
run(v_as4(), exp1=['AS4'], exp2=['AS4p'],
note='indipendenza di AS4')
run(v_as5(), exp1=['AS5'], exp2=['AS5p'],
note='indipendenza di AS5')
mw = v_as6_window()
run(mw, note='finestra
finita: AS6/S12 non falsificabili qui')
chain_ok = all(('x%d' % (i + 1), 'x%d'
% i) in mw['FRR']['w1'] for i in range(11))
line(' catena discendente x(i+1)
fonda x(i) presente su tutta la finestra: %s' % chain_ok)
line(' (la
violazione di AS6 nel modello infinito e\' per costruzione, vedi sezione 29.2)')
sN = n_n()
rN, iN = check_sigma1(sN)
fN = sorted(l for l, c in rN if
not c)
okN = fN == ['AS-N', 'T16']
if not okN:
failures.append('N_N')
line('== N_N (necessario e dipendente) [indipendenza di AS-N]')
line('
Sigma1: %d controlli, falliti: %s (attesi: [\'AS-N\', \'T16\'])' % (len(rN), fN
or 'nessuno'))
line(' ESITO: %s' % ('OK' if okN else 'DISCORDANZA'))
#
convenzione sui relativi fantasma (errata v2.8)
g = n0(False)
g['name'] =
'N0 + relativo fantasma z (esiste in nessun mondo)'
g['UR'] = set(g['UR']) |
{'z'}
rtg, _ = roundtrip(g)
line('== %s' % g['name'])
line('
Part(Union(M)) == M : %s (atteso False: serve la convenzione U_R = unione dei
D_R(w))' % rtg)
if rtg:
failures.append('fantasma')
line('')
line('TUTTE LE ATTESE RISPETTATE' if not failures else 'DISCORDANZE: %s' %
failures)
sys.exit(1 if failures else 0)
###############################################################################
APPENDICE B - TEST DI SENSIBILITA' (mutation_test_v28.py)
###############################################################################
Salvare nella stessa cartella di check_models_v28.py.
Esecuzione: python3
-I mutation_test_v28.py
#!/usr/bin/env python3
# mutation_test_v28.py
- test di sensibilita': introduce guasti noti nel modello N1
# e mostra quali
assiomi falliscono (nessun controllo deve essere vacuo).
# Richiede
check_models_v28.py nella stessa cartella. Esecuzione: python3 -I
mutation_test_v28.py
import copy
import os
here = os.path.dirname(os.path.abspath(__file__))
src = open(os.path.join(here, 'check_models_v28.py'), encoding='utf-8').read()
exec(src[:src.index('#
------------------------------------------------------------------ main ----')])
def labels(m):
r2, _ = check_sigma2(m)
r1, _ =
check_sigma1(to_stage1(m))
return sorted(l for l, c in r2 if not c), sorted(l
for l, c in r1 if not c)
def mut(name, fn):
m = copy.deepcopy(n1())
fn(m)
f2, f1 = labels(m)
assert f1 or f2, 'guasto non rilevato: ' + name
print('%-52s Sigma2 %s | Sigma1 %s' % (name, f2, f1))
ONE = frozenset(['w1',
'w2', 'w3'])
W12 = frozenset(['w1', 'w2'])
W1 = frozenset(['w1'])
def no_creator(m):
m['Cr']['w1'].discard(('g', 'y'))
m['FAR']['w1'].discard(('g',
'y'))
def acc_no_dom(m):
m['Dom']['w1'].discard(('m', 'g'))
m['Acc']['w1'].add(('g',
'm'))
def second_absolute(m):
m['UA'].add('h')
m['PrAR']['w1'].add(('h',
'x'))
def exp_not_transitive(m):
m['EXP'].discard((ONE, W1))
m['EXP'].add((W12, W1))
def m_everywhere(m):
m['DR']['w3'] = {'m'}
m['Cr']['w3'] = {('g', 'm')}
m['FAR']['w3'] = {('g', 'm')}
m['Dom']['w3']
= {('m', 'g')}
mut('ciclo: Fonda_RR(y,m) a w1', lambda m:
m['FRR']['w1'].add(('y', 'm')))
mut('manca il creatore di y a w1', no_creator)
mut('manca Dom di m a w1', lambda m: m['Dom']['w1'].discard(('m', 'g')))
mut('Accoglie(g,m)
senza Dom', acc_no_dom)
mut('FondatoDa su ente inesistente (m a w3)', lambda
m: m['FD']['w3'].add(('u1', 'm')))
mut('Fonda_RR(m,y) a w2, dove y non
esiste', lambda m: m['FRR']['w2'].add(('m', 'y')))
mut('Fonda_RR(x,m) a w1
(ciclo con (m,x))', lambda m: m['FRR']['w1'].add(('x', 'm')))
mut('manca (m,y):
transitivita\' violata', lambda m: m['FRR']['w1'].discard(('m', 'y')))
mut('secondo
Assoluto h, principio indipendente di x', second_absolute)
mut('Exp non
transitiva', exp_not_transitive)
mut('m esiste in ogni mondo (diventa
necessario)', m_everywhere)
mut('creazione non essenziale: Cr(g,x) assente a
w2', lambda m: m['Cr']['w2'].discard(('g', 'x')))
mut('PrincipioDi su
relativo inesistente (m,x) a w3', lambda m: m['PrRR']['w3'].add(('m', 'x')))
print('Tutti i guasti sono stati rilevati.')
FINE
indice sito