Metalogica: proprietà derivate per calcolo

Proprietà metalogiche della logica ontologica (LO, le tavole di src/core/tv.rs). Ogni affermazione marcata ✓ è verificata da questo script su tutte le assegnazioni; quelle marcate «argomento» seguono dalle precedenti per ragionamento e non per calcolo.

1. Conseguenza logica

Il solo valore designato è V:

Γ ⊨ φ sse ogni assegnazione che dà V a tutte le formule di Γ dà V a φ.

Una tautologia è una formula φ con ∅ ⊨ φ, cioè sempre V: è la convenzione di LEGGI_LOGICHE.md.

2. Chiusura sotto le operazioni

2.1 Sottoinsiemi chiusi

Per ogni sottoinsieme di valori, i connettivi sotto cui è chiuso.

L'unica sottoalgebra è l'insieme intero. {F, N} è chiuso sotto tutti i connettivi tranne → (F→F = V); {V, F} è chiuso sotto ∧, ∨, → ma non sotto ¬ (¬F = N).

2.2 Congruenze

Una partizione è una congruenza per un connettivo se la classe del risultato dipende solo dalle classi degli operandi.

• ✓ {V} | {F, N} è l'unica congruenza non banale.

3. Riduzione bivalente

Il quoziente di LO per {V} | {F, N} ha due elementi: D (designato, la classe di V) e U (non designato, la classe di F e N).

¬D = U, ¬U = U.

Letto come algebra a due valori (D = vero, U = falso):

• ∧, ∨, → sono i connettivi classici;
• ¬A è la costante falsa, qualunque sia A;
• A⊕B è la costante falsa;
• A↔B coincide con A∧B.

Da qui la traduzione τ verso la logica classica: τ(¬X) = ⊥, τ(X⊕Y) = ⊥, τ(X↔Y) = τ(X)∧τ(Y), τ(N) = ⊥, identità sul resto.

Teorema di riduzione. Γ ⊨ φ in LO sse τ(Γ) ⊨ τ(φ) in logica classica.

• ✓ le tavole quoziente sono quelle descritte sopra.
• ✓ 1378 istanze delle leggi di LEGGI_LOGICHE.md: il valore LO è V esattamente quando la traduzione è vera in BOOL (0 discrepanze).

Conseguenza: per la validità, F e N sono indistinguibili. La differenza tra falso e non apofantico non incide su ciò che segue da cosa; incide sul valore delle formule non vere, cioè sull'equivalenza epistemica e sugli insiemi F e N restituiti dal motore.

4. Correttezza e completezza

Calcolo HLO: gli schemi d'assioma seguenti e la sola regola del modus ponens.

• ✓ il modus ponens conserva V: A, A→B ⊨ B.
• ✓ A→B vale V sse A non vale V oppure B vale V (su tutte le 9 celle).

Correttezza (✓). Ogni assioma è una tautologia e il modus ponens conserva V, quindi ogni teorema di HLO è una tautologia e ogni derivazione da Γ è una conseguenza di Γ.

Teorema di deduzione (✓). Dalla seconda verifica: Γ, A ⊨ B sse Γ ⊨ A→B.

Completezza (✓, vedi §4.2). Ogni tautologia è un teorema di HLO, e ogni conseguenza di un insieme finito Γ è derivabile da Γ: con la correttezza, Γ ⊨ φ sse Γ ⊢ φ.

4.1 Regole come conseguenze

Una regola con una premessa negata vale a vuoto: nessuna assegnazione dà V a ¬A. Le due implicazioni non bastano a introdurre ↔, che chiede entrambi i membri affermati.

4.2 Verifica della completezza

La completezza è verificata in modo costruttivo, con due programmi indipendenti (strumenti/completezza.py).

Il generatore costruisce una derivazione in HLO di una tautologia φ con il metodo di Kalmár. Scritto ∼A per A→F (A non è affermato):

1. per ogni scelta di quali variabili sono vere, dalle ipotesi p (variabile vera) o ∼p (variabile non vera) deriva, per induzione sulla formula, ogni sottoformula ψ se è vera e ∼ψ se non lo è. I casi di ∧, ∨, → sono quelli classici; ¬ψ e ψ⊕χ non sono mai veri, e gli schemi ¬ e ⊕ ne danno subito la non-affermazione; ψ↔χ si riconduce a ψ∧χ con gli schemi ↔E e ↔I;
2. elimina le ipotesi una variabile alla volta: da p→φ e ∼p→φ segue φ, con il teorema di deduzione (schemi K e S) e lo schema di Peirce.

Bastano le due ipotesi p e ∼p per variabile, e non tre, per la congruenza del §2.2: il vero di una formula dipende solo da quali variabili sono vere. Il generatore usa soltanto le tavole e gli schemi, e riesce su ogni tautologia: è questo il contenuto della completezza.

Il verificatore controlla ogni derivazione riga per riga, senza sapere come è stata costruita: ogni riga deve essere un'istanza di uno schema, una premessa dichiarata, o seguire per modus ponens da due righe precedenti.

• ✓ le 19 leggi che sono tautologie: derivazioni corrette, da 76 a 10555 righe.
• ✓ le 10 regole valide del §4.1: la conclusione è derivata dalle premesse.
• ✓ tutte le 2906 formule su A, B con al più due livelli di connettivi: 432 tautologie, tutte derivate (345485 righe verificate).
• ✓ tutte le 2906 formule su A, N con al più due livelli di connettivi: 568 tautologie, tutte derivate (98408 righe verificate).
• ✓ controprova: su A∨¬A, che non è una tautologia, il generatore non produce alcuna derivazione.

La verifica è eseguita da programmi e non da un dimostratore formale: il verificatore certifica ogni singola derivazione, mentre che il generatore riesca su ogni tautologia segue dall'induzione descritta sopra.

5. Decidibilità ed efficienza

LO è decidibile: una formula con n variabili si decide valutandola su 3ⁿ assegnazioni. Per il teorema di riduzione ne bastano 2ⁿ, quelle a valori in {V, F}, sulla traduzione τ.

• ✓ sulle 60 leggi le due procedure danno lo stesso verdetto: 19 tautologie a 3ⁿ, 19 a 2ⁿ.

Complessità (argomento): il problema delle tautologie è coNP-completo e quello della soddisfacibilità (esiste un'assegnazione che dà V) è NP-completo. L'appartenenza segue dalla valutazione in tempo lineare di una singola assegnazione; la durezza dall'immersione della logica classica del §7, che è lineare se ∼X si scrive X→F (stessa tavola di X→¬X, senza duplicare X).

6. Compattezza

(Argomento.) Γ ⊨ φ sse esiste un sottoinsieme finito Γ₀ di Γ con Γ₀ ⊨ φ. Segue dal teorema di riduzione e dalla compattezza della logica classica: se τ(Γ) ⊨ τ(φ) allora un sottoinsieme finito di τ(Γ) basta, ed è l'immagine di un sottoinsieme finito di Γ. In particolare un insieme di formule è soddisfacibile sse lo è ogni suo sottoinsieme finito.

7. Conservatività rispetto alla logica classica

• ✓ {V, F} è chiuso sotto ∧, ∨, →.
• ✓ su {V, F} le tavole di ∧, ∨, → sono quelle booleane.

Con il teorema di riduzione: una formula che usa solo ∧, ∨, → è una tautologia di LO sse lo è in logica classica, e lo stesso vale per la conseguenza. LO è quindi un'estensione conservativa della logica classica positiva.

Con la negazione le due logiche sono inconfrontabili: ciascuna ha tautologie che l'altra non ha.

La logica classica resta però interamente esprimibile con la negazione stretta ∼A (in ONTO ~A): vale F se A è V e V altrimenti, cioè si comporta come la negazione classica su V e F. Si legge «A non è affermato», è definibile come A→¬A e serve solo a isolare una porzione di logica che simula quella classica.

• ✓ A→¬A vale F, V, V per A = V, F, N.
• ✓ {V, F} è chiuso sotto ∼, ∧, ∨, →, con le tavole booleane.
• ✓ 59 leggi: una legge è una tautologia classica sse lo è in LO la sua immersione (¬ sostituita da ∼, ⊕ e ↔ dalle definizioni classiche): 0 discrepanze.
• ✓ 243 istanze della porzione classica (tavola di ~ e leggi immerse a valori in {V, F}) eseguite dal binario onto run: 0 discrepanze.

Terzo escluso e non contraddizione, per esempio, tornano tautologie nella forma A∨∼A e ∼(A∧∼A). LO contiene quindi la logica classica come logica dell'affermato e del non affermato, e vi aggiunge la distinzione tra falso e non apofantico, che la validità non vede (§3).

8. Esplosione e non contraddizione

• ✓ ¬A non vale mai V: nessuna formula negata è una tautologia, né è mai soddisfatta.
• ✓ A∧¬A non vale mai V.
• ✓ A, ¬A ⊨ B vale, a vuoto: nessuna assegnazione dà V sia ad A sia a ¬A.

Nel senso tecnico corrente una logica è paraconsistente se A, ¬A ⊨ B fallisce. Con V designato LO non lo è: una contraddizione non può essere affermata, quindi non c'è nulla da cui far esplodere. ¬(A∧¬A) non è una tautologia perché la negazione non restituisce mai V, non perché esistano contraddizioni vere.

9. Adeguatezza funzionale

I sei connettivi generano 588 delle 19683 funzioni binarie su {V, F, N} e 12 delle 27 unarie. LO non è funzionalmente completa.

La ragione è la congruenza del §2.2: ogni funzione definibile la rispetta, e le funzioni binarie che la rispettano sono 1275. Le 588 definibili ne sono una parte propria.

9.1 Basi

Sottoinsiemi minimali di connettivi che generano tutte le funzioni definibili:

• {¬, ∧, ∨, →}
• {¬, ∨, →, ↔}
• {∧, ∨, ⊕, →}
• {∨, ⊕, →, ↔}

Funzioni binarie generate da alcuni sottoinsiemi:

9.2 Definibilità reciproca

Ogni connettivo definito con gli altri cinque, con una formula di lunghezza minima (— se non è definibile).

Gli stessi connettivi a partire dai soli {¬, ∧, ∨}:

• ✓ i connettivi non definibili con gli altri sono ∨, →.
• ✓ ⊕ e ↔ sono definibili da {¬, ∧, ∨}.
• ✓ → non lo è: {F, N} è chiuso sotto ¬, ∧, ∨ (§2.1) e F→F = V.

9.3 Operatori unari definibili

Ogni funzione unaria è scritta come terna dei valori su V, F, N.

Le 15 non definibili: VVF, VVN, VFV, VNV, VNF, VNN, FVF, FVN, FFV, FNV, NVV, NVF, NVN, NFV, NNV.

Tra le definibili ci sono le tre costanti (VVV, FFF, NNN), per cui aggiungere V, F, N al linguaggio non aumenta le funzioni definibili, e c'è FVV, la negazione stretta ∼A del §7.

Delle non definibili, 12 romperebbero la congruenza (mandano in V uno solo tra F e N). Le altre 3 la rispettano e restano comunque fuori: VNF, VNN, NVV. Tra queste VNF: nessuna formula scambia F e N lasciando fermo V.

9.4 Quali funzioni sono definibili

Una relazione binaria è invariante se è chiusa sotto i sei connettivi applicati componente per componente; una funzione la preserva se, applicata a coppie della relazione, dà una coppia della relazione. Ogni funzione definibile preserva ogni relazione invariante. Le relazioni binarie invarianti sono queste:

Bastano due di esse; le altre sono l'uguaglianza, la relazione totale, l'inversa di ρ e l'intersezione di ρ con la sua inversa.

• θ, la congruenza del vero (§2.2): due valori sono in relazione se sono entrambi V o nessuno dei due lo è;

• ρ, tutte le coppie tranne (N, V): «non si passa dal non apofantico al vero».

• ✓ le relazioni binarie invarianti sono 6, tutte ricavabili da θ e ρ.

• ✓ le funzioni binarie che preservano θ e ρ sono 588: esattamente le definibili.

• ✓ le funzioni unarie che preservano θ e ρ sono 12: esattamente le definibili.

Una funzione di uno o due argomenti è definibile con i sei connettivi se e solo se preserva θ e ρ.

Preservare θ dice che il vero del risultato dipende solo da quali argomenti sono veri. Preservare ρ dice che, 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 per cui il vero si ottiene per aggiunta di informazione e non per negazione. Le funzioni compatibili con θ sono 1275; ρ le riduce a 588.

10. Teoremi di limite

(Argomento.) Il frammento proposizionale è decidibile e HLO è completo, quindi non vi si applicano teoremi d'incompletezza o d'indecidibilità: questi richiedono un linguaggio capace di esprimere l'aritmetica, cioè la quantificazione. La logica predicativa non è supportata dall'ontologia espressa e i quantificatori non sono usati (LOGICA.md §9).

11. Struttura modale

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

• ◇ₑA, possibilità epistemica: A è apofantico (V o F);
• ◇ₗA, possibilità logica: A è non apofantico (N).

• ✓ nessuno dei due è definibile con i sei connettivi (§9.3): sono primitivi.
• ✓ entrambi separano F da N, quindi rompono la congruenza del §2.2: con le modalità la validità distingue il falso dal non apofantico, e la riduzione bivalente del §3 non si estende al linguaggio modale.

11.1 Leggi

∼ è la negazione stretta del §7.

Le due possibilità sono complementari: ◇ₗA ha la tavola di ∼◇ₑA, e ne basta una come primitivo. La possibilità logica esclude l'affermazione (◇ₗA → ∼A): è il contenuto formale di «si rivela sempre impossibilità nel mondo reale». L'iterazione collassa: un giudizio di possibilità vale V o F, quindi è sempre apofantico, e non c'è una gerarchia di modalità annidate.

11.2 Modalità e negazione

La negazione di un falso è non apofantica (◇ₗ¬F = V): negando una premessa falsa si esce dall'apofantico. La doppia negazione è apofantica solo sul falso. La negazione stretta resta sempre apofantica, coerentemente col suo uso nella porzione classica.

11.3 Potere espressivo

Aggiungendo ◇ₑ ai sei connettivi le funzioni unarie definibili passano da 12 a 16 su 27, e le binarie da 588 a 1156 su 19683. Le nuove unarie: VVF, VFV, FVF, FFV.

Anche con le modalità LO non è funzionalmente completa. Restano fuori VVN, VNV, VNF, VNN, FVN, FNV, NVV, NVF, NVN, NFV, NNV: tra queste lo scambio di F e N (VNF).