La logica ontologica di ONTO

Documento di riferimento sulla logica trivalente su cui poggiano ONTO e TheoryFlow. Raccoglie i valori di verità, le tavole canoniche, il criterio di identità epistemico, la derivazione computazionale di leggi e principi logici confrontati con la logica booleana, e le proprietà metalogiche del sistema. onto-rs implementa esattamente queste tavole.

Fonti:

• repository logica-ontologica (README.md, main.py, config.ini): tavole canoniche e motore di calcolo di riferimento;
• articoli 13 e 14 della wiki di TheoryFlow («La logica ontologica», prima e seconda parte);
• src/core/tv.rs, src/storage/index.rs, src/query/mod.rs, src/lang/interprete.rs: implementazione in ONTO.

I risultati numerici citati qui provengono da LEGGI_LOGICHE.md e METALOGICA.md, generati da strumenti/leggi_logiche.py e strumenti/metalogica.py (vedi Riproducibilità).

1. I tre valori

Sono stati epistemici delle proprietà. La verità non è data a priori: si determina a posteriori, come proprietà delle teorie che sopravvivono alla confutazione.

L'analisi è dicotomica a due livelli. Prima si separano apofantico e non apofantico (la presupposizione esistenziale è soddisfatta oppure no); poi, dentro l'apofantico, si distingue tra vero e falso.

Il principio che regge il sistema è asimmetrico. Il vero si ottiene solo per aggiunta di informazione, cioè per affermazione. Nessuna negazione restituisce V: la negazione fa ciclare F e N, e V resta fuori dal ciclo.

     ¬            ¬
V ───────► F ◄───────► N

In un processo deduttivo il passaggio dal non apofantico all'apofantico è precluso. Diventa possibile aggiungendo informazioni che completano l'enunciato; il passaggio inverso avviene riducendo le informazioni.

2. Tavole canoniche

Sono le tavole della logica ontologica, verificate computazionalmente contro il motore di riferimento logica-ontologica (§7). Accanto a ogni connettivo, il suo archetipo ontologico.

Negazione ! (dissoluzione)

Congiunzione ^ (compressione)

Disgiunzione v (estensione)

Disgiunzione esclusiva x (estensione tra una compressione e una dissoluzione)

Implicazione → (espansione)

Coimplicazione - (compressione di due espansioni)

Proprietà strutturali che si leggono direttamente dalle tavole:

• ¬ non produce mai V, e ¬¬¬A ha sempre lo stesso valore di ¬A;
• ∧ produce V solo da V∧V; N∧N = F e F∧N = N, quindi la congiunzione di due non apofantici è falsa e quella di un falso con un non apofantico resta non apofantica;
• ∨ produce V se almeno un operando è V; F∨N = F;
• ↔ produce V solo da V↔V: anche F↔F = F e N↔N = N. Ne segue che ogni formula della forma X ↔ Y è vera solo dove X e Y sono entrambe vere (§5.2);
• → produce V da ogni antecedente F o N (ex falso, ex N quodlibet). È l'unico connettivo che raggiunge V da premesse prive di V, e lo fa per vacuità dell'antecedente.

3. L'implementazione in ONTO

ONTO implementa le sei tavole del §2, più la negazione stretta del §8.5 come abbreviazione di A => !A. La corrispondenza è verificata eseguendo con il binario onto ogni istanza di ogni legge del §5 (§7).

Precedenza, dalla più bassa: <=>, => (associativa a destra), v e xor, ^, confronti, aritmetica, !. V ^ F => F si legge quindi (V ^ F) => F, e A => B => C si legge A => (B => C). I simboli di logica-ontologica (x per lo XOR, - per la coimplicazione) restano esclusi perché in ONTO x è un identificatore valido e - è la sottrazione.

La semantica è replicata in tre punti del codice, che vanno tenuti allineati a ogni modifica:

Nei bitset il set F di un operatore binario si calcola come complemento di V e N sui soli record vivi. Il motivo è la compressione: un record retratto ha tutti i bit a zero e verrebbe letto come N, ma N ^ N = F lo porterebbe nel set F. LazyQuery porta per questo una maschera vivi.

La membership delle classi usa solo il set V. In tutte le tavole V nasce da V ^ V e da almeno un V in v, quindi i membri di una classe sono gli stessi che si avrebbero con le tavole di Kleene; cambiano gli insiemi F e N restituiti da .f() e .n().

== e ▷ tra valori sono bivalenti e riflessivi: A == A e A ▷ A valgono V per ogni valore di A. Il §4 spiega perché questo comportamento va letto come criterio epistemico.

3.1 Effetti sugli esempi

Con la compressione un criterio indeterminato non propaga incertezza: rende non affermata la congiunzione. È la differenza rispetto alle tavole di Kleene:

Negli esempi diagnosi.onto e rischio_credito.onto l'esito F di una diagnosi si legge quindi «non confermato», e una domanda di credito con un requisito indeterminato passa al test sulle garanzie (V ^ N = F).

3.2 I connettivi come selezioni ed esclusioni

Sugli insiemi del motore ogni connettivo si riduce a operazioni tra insiemi di elementi: la selezione (intersezione ∩), l'unione (∪) e l'esclusione (differenza \). Per una proprietà A siano V(A), F(A) e N(A) gli insiemi degli elementi vivi in cui A vale V, F e N. I tre insiemi sono disgiunti e insieme danno U, l'insieme degli elementi vivi (la maschera vivi del §3). Un connettivo è allora una coppia di ricette, una per l'insieme V del risultato e una per l'insieme N. L'insieme F è ciò che resta di U.

Sono le formule con cui LazyQuery calcola i bitset in src/query/mod.rs. Un singolo valore, come in V ^ N, è il caso di un solo elemento.

Dato U, l'esclusione basta da sola, perché selezione e unione si ricavano da essa:

A ∩ B = A \ (A \ B)
A ∪ B = U \ ((U \ A) \ B)

La riduzione riguarda le operazioni del motore sugli insiemi. La definibilità di un connettivo a partire dagli altri è una questione diversa, trattata nel §8.6.

Dalla tabella si leggono tre conseguenze.

• L'esclusione è distinta dalla negazione. !A ha l'insieme V vuoto, quindi non seleziona alcun elemento. Il complemento di V(A) è l'insieme V della negazione stretta ~A (§8.5). I selettori delle classi ammettono solo ^ e v, e lì si esclude selezionando sull'insieme F: class { V=uomo ^ F=mortale } raccoglie gli uomini per cui mortale è smentito e lascia fuori quelli per cui è indeterminato.
• => e ~ sono i soli connettivi la cui ricetta per V usa U. Per !, ^, v, xor e <=> l'insieme V del risultato è contenuto in V(A) ∪ V(B): selezionano o uniscono ciò che è già vero in un operando. => rende V anche elementi in cui nessun operando è V. È la lettura insiemistica del fatto che → non è definibile dagli altri connettivi (§8.6).
• Le ricette per V e per N di uno stesso connettivo non sono duali. Per questo le leggi di De Morgan cadono (§5.4) pur lavorando con insiemi ordinari: l'insieme N di !(A ^ B) è tutto l'insieme F di A ^ B, mentre l'insieme N di !A v !B è il solo F(A) ∩ F(B).

4. Il principio di identità

4.1 Tesi

Il principio di identità non vale come principio logico né ontologico. È un principio epistemico che descrive come gli enti si formano a partire dai determinati, secondo il motto di Quine «no entity without identity».

La logica formale classica si fonda sul principio di identità, che ammette che l'essere sia un genere; il terzo escluso tratta verità e menzogna come contraddittori, generi a cui partecipare. Concepire invece l'ente come genere e verità e menzogna come contrari (estremi di due opposti) è la formalizzazione del pensiero di Meinong, anch'essa respinta. Dei principi della logica formale resta valido quello di non contraddizione (§5.1).

C'è inoltre una ragione ontologica. Il terzo escluso implica l'identità, e l'identità presuppone la ripetizione. Con il concetto di perfezione ontologica la ripetizione risulta impossibile, perché non ci sono istanti uguali da ripetere: semplicemente non ci sono istanti. Le fasi pre-sé dello sviluppo universale valgono allora esclusivamente come condizioni di possibilità dell'essere.

4.2 Criterio di identità epistemico (CIE)

x è un ente se e solo se condivide le stesse proprietà epistemiche (K) di un determinato η.

(K x = K η) ↔ x = η

Il CIE è un «criterio di traduzione». Descrive come l'io passa dal determinato all'ente e fonda il senso comune secondo cui è ente solo ciò che si dà nello spaziotempo; nulla dice sulla verità degli enti. La sedia esiste come determinato dell'essere; l'ente sedia è la sedia in sé assunta solo nelle sue proprietà epistemiche.

Conseguenze:

1. È falso che l'ente sia identico a sé stesso; al massimo è identico all'astrazione delle sue proprietà epistemiche.
2. La coimplicazione si legge nei due sensi, quindi si può verificare se un ente postulato dalla metafisica ha un determinato corrispondente. Se non esiste alcun determinato con le stesse proprietà epistemiche, l'ente esiste solo nel contesto modale della metafisica.

4.3 Riscontro computazionale

Il calcolo conferma la tesi. Le due forme proposizionali dell'identità si separano:

L'identità come connettivo (↔, la forma x = y del CIE) cade su ogni valore apofantico falso e su ogni non apofantico. Sopravvive soltanto la forma implicativa A → A, che vale come principio epistemico. L'identità vale dunque per ciò che è stato affermato (V) e per nessun altro valore.

4.4 Conseguenze per ONTO

Il CIE ha una traduzione diretta nel paradigma POP. Un elemento ONTO è un aggregato di proprietà trivalenti, cioè di proprietà epistemiche; due elementi con lo stesso profilo hanno le stesse proprietà epistemiche e valgono come lo stesso ente pur restando record distinti nel motore (id diversi, cioè determinati diversi). È la distinzione tra identità per proprietà, ammessa, e identità della determinazione, respinta.

In ONTO due costrutti sono riflessivi su ogni valore:

• == tra valori trivalenti restituisce V per N == N e F == F;
• ▷ tra valori (aggregato_da) restituisce V sulla diagonale.

Entrambi vanno letti come operatori di confronto epistemico tra profili (stesse proprietà, stesso valore), mai come asserzione d'identità dell'essere.

Lo stesso criterio regge, nel metalinguaggio, il confronto tra leggi del §5: due formule con la stessa tavola di verità hanno le stesse proprietà epistemiche e valgono come la stessa legge (equivalenza epistemica, colonna «≡ ep.»).

5. Leggi e principi: derivazione computazionale

Ogni legge è valutata su tutte le assegnazioni delle sue variabili (2ⁿ in BOOL, 3ⁿ in LO e ONTO). Le classi sono:

• tautologia: sempre V;
• mai falsa: solo V o N;
• mai vera: solo F o N;
• contraddizione: sempre F;
• contingente: assume sia V sia F.

In BOOL ogni legge elencata è una tautologia, salvo dove indicato. LO e ONTO danno lo stesso risultato su ogni istanza, per cui le tabelle riportano una sola colonna. Il quadro completo, con distribuzioni e controesempi, è in LEGGI_LOGICHE.md.

5.1 Principi

Non contraddizione. ¬(A∧¬A) vale N per A = V e F altrimenti. Come formula non è una tautologia. Il principio va però letto sulla contraddizione stessa: A∧¬A è mai vera (vale F, N, N per A = V, F, N). Nessuna assegnazione rende vera una contraddizione, e questo è il contenuto del principio che il sistema conserva. L'espressione ¬(A∧¬A) non può esprimerlo perché la negazione non restituisce mai V.

Terzo escluso. A∨¬A vale V solo per A = V; per A = F e A = N vale F. Verità e falsità non esauriscono i casi, come previsto: tra apofantico e non apofantico c'è un terzo.

Ex N quodlibet. Dal non apofantico segue qualsiasi conclusione, come dal falso. In BOOL non è esprimibile, mancando N.

5.2 Negazione e leggi d'equivalenza

La doppia negazione non è involutiva: ¬¬V = N. Si può eliminare (¬¬A → A è tautologica) ma non introdurre: da V non si torna a V negando due volte. La tripla negazione si riduce alla singola, quindi ogni catena di negazioni equivale a ¬A o a ¬¬A.

La colonna ≡ ep. mostra perché le leggi d'equivalenza vanno giudicate anche nel metalinguaggio. Poiché ↔ dà V solo su V↔V, una formula X ↔ Y è vera solo dove X e Y sono entrambe vere; la tripla negazione, che pure ha i due membri identici in ogni riga, è «mai vera» come formula perché ¬A non vale mai V. Il giudizio di equivalenza epistemica (stessa tavola, §4.4) separa le due questioni.

5.3 Algebra di ∧ e ∨

Equivalenza epistemica dei due membri (stessa tavola di verità):

La congiunzione perde idempotenza, associatività e l'elemento neutro: è un'operazione di compressione che non conserva il valore degli operandi quando uno di essi è N. La disgiunzione conserva idempotenza, associatività e distributività su ∧.

L'associatività mancante di ^ ha una conseguenza pratica in ONTO: una catena a ^ b ^ c si valuta da sinistra, (a ^ b) ^ c, e con valori N il risultato può cambiare se si spostano le parentesi. Le combinazioni divergenti sono sei su ventisette:

Il set V non cambia mai (vale solo con tre V), quindi le classi conservano gli stessi membri; cambiano gli insiemi F e N di selettori composti.

Come formule con ↔, tutte queste leggi sono contingenti o mai vere (vedi LEGGI_LOGICHE.md).

5.4 De Morgan e definibilità dei connettivi

Le leggi di De Morgan non valgono in nessuna forma. La definizione dello XOR è esatta: ⊕ è derivabile da ¬, ∧, ∨, e tv.rs lo verifica in un test. Né l'implicazione materiale né la «compressione di due espansioni» riproducono invece le tavole canoniche di → e ↔. Una chiusura esaustiva delle funzioni binarie generate da {¬, ∧, ∨} (562 funzioni su 3⁹) mostra che ↔ vi appartiene attraverso un'altra formula, mentre → resta fuori (§8.6). Per questo ONTO implementa => come operatore nativo.

5.5 Regole d'inferenza e assiomi

Il nucleo deduttivo tiene: modus ponens, modus tollens, i sillogismi, le leggi di pseudo Scoto, Peirce e i due assiomi K e S di Hilbert/Frege sono tautologie. Il frammento implicativo positivo della logica classica (K, S, modus ponens) è quindi conservato, e con esso il teorema di deduzione nella forma di Hilbert.

Cadono le leggi che chiedono di recuperare V attraverso la negazione: la contrapposizione (il caso A=V, B=F dà (V→F)↔(¬F→¬V) = F↔(N→F) = F↔V = F), la riduzione all'assurdo, la consequentia mirabilis e l'assioma di contrapposizione di Łukasiewicz. È la traduzione formale del principio del §1: dalla negazione non si arriva al vero.

6. Sintesi

7. Riproducibilità

cd onto-rs
cargo build -p onto-cli
python3 strumenti/leggi_logiche.py \
    --verifica-lo percorso/di/logica-ontologica \
    --verifica-onto target/debug/onto \
    --markdown docs/LEGGI_LOGICHE.md

Lo script:

1. definisce le tavole BOOL, LO e ONTO e un parser di formule;
2. con --verifica-lo ricava le sei tavole interrogando main.py e ricalcola ogni istanza di ogni legge con la classe Processing di logica-ontologica (1378 istanze, 0 discrepanze);
3. con --verifica-onto scrive uno script .onto con ogni istanza di ogni legge (connettivi !, ^, v, xor, =>, <=>) e lo esegue con onto run (1378 istanze, 0 discrepanze);
4. con --markdown rigenera LEGGI_LOGICHE.md.

Esce con codice 1 se una verifica fallisce. Per aggiungere una legge basta una riga nella lista LEGGI dello script.

Sintassi delle formule nello script: variabili A–E, costanti V F N, operatori ! ^ v x > (implicazione) = (coimplicazione), parentesi.

Le proprietà del §8 si rigenerano con

python3 strumenti/metalogica.py --verifica-onto target/debug/onto \
    --markdown docs/METALOGICA.md

che usa le stesse tavole e lo stesso parser, costruisce e controlla le derivazioni di completezza (strumenti/completezza.py), esegue con onto run la porzione classica scritta con ~ (243 istanze, 0 discrepanze) ed esce con codice 1 se una verifica fallisce. La congruenza su cui poggiano è inoltre un test di src/core/tv.rs (test_congruenza_del_vero).

8. Proprietà metalogiche

Compattezza, completezza, correttezza, decidibilità, adeguatezza, conservatività, efficienza e chiusura sotto le operazioni sono derivate in METALOGICA.md, insieme alla struttura modale; qui il riassunto.

8.1 Conseguenza logica

Il solo valore designato è V: Γ ⊨ φ se ogni assegnazione che dà V a tutte le formule di Γ dà V a φ. È la convenzione già usata nel §5, dove una tautologia è una formula sempre V.

8.2 La congruenza del vero

La partizione {V} | {F, N} è una congruenza per tutti e sei i connettivi, ed è l'unica non banale: che una formula valga V dipende solo da quali sue variabili valgono V. Nell'algebra quoziente a due valori (affermato, non affermato):

Ne segue il teorema di riduzione: Γ ⊨ φ in LO se e solo se τ(Γ) ⊨ τ(φ) in logica classica, dove τ sostituisce ¬X e X⊕Y con il falso e X↔Y con X∧Y. Verificato su tutte le 1378 istanze delle leggi del §5.

Per la validità, quindi, F e N sono indistinguibili. La distinzione tra falso e non apofantico conta per il valore delle formule non vere: l'equivalenza epistemica del §4.4 e gli insiemi restituiti da .f() e .n() in ONTO.

8.3 Correttezza e completezza

Il calcolo HLO ha il modus ponens come unica regola e questi schemi:

• Correttezza: ogni schema è una tautologia e il modus ponens conserva V (verificato).
• Teorema di deduzione: Γ, A ⊨ B se e solo se Γ ⊨ A→B, perché A→B vale V esattamente quando A non vale V oppure B vale V (verificato).
• Completezza: ogni tautologia è un teorema di HLO, e ogni conseguenza di un insieme finito di premesse è derivabile da esse. È verificata in modo costruttivo (METALOGICA.md §4.2): un generatore costruisce la derivazione con il metodo di Kalmár, e un verificatore indipendente la controlla riga per riga. I primi tre gruppi di schemi sono la logica classica positiva; gli altri fissano ¬, ⊕, ↔ al loro comportamento sul quoziente. Tutte le tautologie con al più due livelli di connettivi su due atomi (1000 su 5812 formule), le 19 leggi tautologiche del §5 e le regole valide sono state derivate e controllate senza errori.

Come conseguenze (non come formule con ↔) valgono modus ponens, modus tollens, i due sillogismi e la contrapposizione A→B ⊨ ¬B→¬A. Non valgono A ⊨ ¬¬A, la riduzione all'assurdo e A→B, B→A ⊨ A↔B: le due implicazioni non bastano a introdurre ↔, che chiede entrambi i membri affermati.

8.4 Decidibilità, efficienza, compattezza

LO è decidibile con le tavole di verità: 3ⁿ assegnazioni, che il teorema di riduzione porta a 2ⁿ. Il problema delle tautologie è coNP-completo e la soddisfacibilità NP-completa, come in logica classica. La compattezza segue dalla riduzione e dalla compattezza classica. I teoremi di limite non si applicano al frammento proposizionale, che è decidibile e completo.

8.5 Conservatività e rapporto con la logica classica

• Sulle formule con soli ∧, ∨, → LO e BOOL hanno le stesse tautologie e la stessa conseguenza: LO è un'estensione conservativa della logica classica positiva.
• Con la negazione le due logiche sono inconfrontabili. BOOL ha il terzo escluso e A→¬¬A, che LO non ha; LO ha ¬A→B e (A↔B)→(A∧B), che BOOL non ha.
• La logica classica resta esprimibile per intero con la negazione stretta ∼A, che vale F se A è V e V altrimenti («A non è affermato»). Si comporta come la negazione classica su V e F, ed è definibile: ha la tavola di A→¬A. {V, F} è chiuso sotto ∼, ∧, ∨, → con le tavole booleane, e ogni legge classica del §5 torna una tautologia nella sua immersione (¬ sostituita da ∼, ⊕ e ↔ dalle definizioni classiche: 59 leggi, 0 discrepanze). Per esempio A∨∼A e ∼(A∧∼A).

La negazione stretta serve solo a questo: isolare una porzione di logica che simula quella classica. Fuori da quell'uso la negazione è ¬. In ONTO si scrive ~A (o ∼A); <=> e xor restano ontologici anche nella porzione classica, dove l'equivalenza si scrive (A => B) ^ (B => A).

Esplosione. A, ¬A ⊨ B vale, a vuoto: nessuna assegnazione dà V sia ad A sia a ¬A. Nel senso tecnico corrente LO non è quindi paraconsistente. ¬(A∧¬A) non è una tautologia perché la negazione non restituisce mai V, non perché esistano contraddizioni vere (§5.1).

8.6 Chiusura e adeguatezza funzionale

• Chiusura: l'unico sottoinsieme di valori chiuso sotto tutti i connettivi è {V, F, N}. {F, N} è chiuso sotto tutti tranne → (F→F = V); {V, F} è chiuso sotto ∧, ∨, → ma non sotto ¬.
• Adeguatezza: i sei connettivi generano 588 delle 19683 funzioni binarie e 12 delle 27 unarie. LO non è funzionalmente completa.
• Quali funzioni sono definibili: una funzione di uno o due argomenti è definibile se e solo se preserva due relazioni. La prima è la congruenza del vero θ (§8.2): il vero del risultato dipende solo da quali argomenti sono veri. La seconda è ρ, tutte le coppie di valori tranne (N, V): tra due assegnazioni il risultato può passare da N a V solo se almeno un argomento passa da N a V. È la forma algebrica del principio del §1, per cui il vero si ottiene per aggiunta di informazione. Le funzioni binarie compatibili con θ sono 1275; ρ le riduce alle 588 definibili (verificato per calcolo, come per le 12 unarie).
• Basi: gli insiemi minimali che generano tutto il definibile sono {¬, ∧, ∨, →}, {¬, ∨, →, ↔}, {∧, ∨, ⊕, →} e {∨, ⊕, →, ↔}. ∨ e → compaiono in tutte: sono i due connettivi non definibili con gli altri. ¬, ∧, ⊕, ↔ sono invece definibili (per esempio ¬A come A⊕(A∧A)).
• Costanti: V, F, N sono definibili (A→A, ¬(A→A), ¬¬(A→A)), quindi non aggiungono potere espressivo.
• Operatori unari non definibili: tra gli altri lo scambio di F e N (V↦V, F↦N, N↦F) e ogni operatore che mandi in V uno solo tra F e N.

8.7 Struttura modale

La logica ontologica distingue due possibilità: quella logica (o modale), ammessa dentro la metafisica e che nel mondo reale si rivela sempre impossibilità, e quella epistemica, che sta nel mondo reale e resta da accertare con la scienza. Sui tre valori:

Epistemicamente possibile è ciò che è apofantico, cioè ha un valore da accertare; possibile solo logicamente è il non apofantico.

• Nessuna delle due è definibile con i sei connettivi: separano F da N, e ogni formula del linguaggio base li tratta allo stesso modo rispetto al vero (§8.2). Con le modalità la validità distingue il falso dal non apofantico e la riduzione bivalente non vale più.
• Sono complementari: ◇ₗA ha la tavola di ∼◇ₑA. Valgono ◇ₑA ∨ ◇ₗA, ∼(◇ₑA ∧ ◇ₗA) e A → ◇ₑA; non vale ◇ₑA → A.
• ◇ₗA → ∼A è una tautologia: il possibile solo logico non è mai affermato. È la forma che prende «si rivela sempre impossibilità nel mondo reale».
• L'iterazione collassa: un giudizio di possibilità vale V o F, quindi ◇ₑ◇ₑA e ◇ₑ◇ₗA sono tautologie e ◇ₗ◇ₑA è una contraddizione. Non c'è una gerarchia di modalità annidate.
• ◇ₗ¬F = V: la negazione di un falso è non apofantica, cioè negare una premessa falsa porta fuori dall'apofantico. ¬A e ¬¬A non sono mai entrambe apofantiche.
• Con ◇ₑ le funzioni definibili passano da 12 a 16 unarie su 27 e da 588 a 1156 binarie su 19683. LO resta funzionalmente incompleta; lo scambio di F e N non è definibile nemmeno così.

In ONTO le due modalità si scrivono già con il confronto, che è bivalente: A != N per ◇ₑA e A == N per ◇ₗA.

9. Limiti e questioni aperte

• Logica predicativa. Non è supportata, né al primo né al secondo ordine, e i quantificatori non sono usati. La definizione di individuo non regge: se un individuo è la somma delle sue proprietà e non c'è una sostanza che le porti, nulla vieta di chiamare P la proprietà che è la somma di tutte le proprietà dell'individuo. L'individuo è a sua volta un aggregato di proprietà, e cade la distinzione tra individui e predicati su cui poggia la quantificazione. Nel linguaggio ci si riferisce solo a proprietà: dire «l'uomo è un animale» non seleziona individui, afferma che l'aggregato uomo ha tra le sue proprietà animale (uomo ▷ animale). ONTO esprime queste relazioni con l'aggregazione e con le classi, senza quantificare.
• Completezza di HLO. La verifica del §8.3 è eseguita da programmi: il verificatore certifica ogni derivazione prodotta, ma il teorema generale non è formalizzato in un dimostratore.
• Adeguatezza oltre i due argomenti. La caratterizzazione del §8.6 è verificata per funzioni di uno e due argomenti; per tre o più resta da dimostrare.
• Modalità sugli enti. Il §8.7 legge le due possibilità sui valori di verità. La lettura sugli enti e sui determinati (un ente che esiste solo nel contesto modale della metafisica) non ha ancora una forma nel calcolo.