Leggi logiche: derivazione computazionale

Tre semantiche a confronto: BOOL (logica booleana), LO (logica ontologica di riferimento, repository logica-ontologica) e ONTO (semantica implementata in src/core/tv.rs). Ogni legge è valutata su tutte le assegnazioni: 2ⁿ in BOOL, 3ⁿ in LO e ONTO.

Classi: tautologia (sempre V), contraddizione (sempre F), mai vera (solo F/N), mai falsa (solo V/N), contingente. Tra parentesi la distribuzione dei risultati V/F/N. La colonna ONTO è calcolata sulle tavole di tv.rs e verificata eseguendo ogni istanza con il binario onto.

La colonna ≡ ep. (equivalenza epistemica) dice se i due membri di un'equivalenza hanno la stessa tavola di verità, indipendentemente dal valore della formula con ↔.

Verifiche incrociate

• ✓ le 6 tavole LO coincidono con quelle calcolate da logica-ontologica/main.py.
• ✓ 1378 istanze LO ricalcolate con Processing di main.py: 0 discrepanze.
• ✓ 1378 istanze (¬, ∧, ∨, ⊕, →, ↔) eseguite dal binario onto run: 0 discrepanze col modello ONTO.

Tavole di verità usate

LO

¬

∧

∨

⊕

→

↔

ONTO

¬

∧

∨

⊕

→

↔

BOOL

¬

∧

∨

⊕

→

↔

Quadro sinottico

Principi

Negazione

Algebra

De Morgan

Definibilità

Inferenza

Assiomi

Implicazione

Controesempi

Per ogni legge che non è tautologica, le assegnazioni in cui non vale V.

Identità (forma bicondizionale)

A↔A

Forma x=y del CIE: riflessività del connettivo d'identità.

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ N
• ONTO: A=F ⇒ F; A=N ⇒ N

Non contraddizione

¬(A∧¬A)

• BOOL: nessuno
• LO: A=V ⇒ N; A=F ⇒ F; A=N ⇒ F
• ONTO: A=V ⇒ N; A=F ⇒ F; A=N ⇒ F

Terzo escluso

A∨¬A

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ F
• ONTO: A=F ⇒ F; A=N ⇒ F

Ex N quodlibet

N→A

Dal non apofantico segue qualsiasi conclusione.

• BOOL: nessuno
• LO: nessuno
• ONTO: nessuno

Doppia negazione

¬¬A↔A

• BOOL: nessuno
• LO: A=V ⇒ N; A=F ⇒ F; A=N ⇒ N
• ONTO: A=V ⇒ N; A=F ⇒ F; A=N ⇒ N

Introduzione della doppia negazione

A→¬¬A

• BOOL: nessuno
• LO: A=V ⇒ F
• ONTO: A=V ⇒ F

Tripla negazione

¬¬¬A↔¬A

• BOOL: nessuno
• LO: A=V ⇒ F; A=F ⇒ N; A=N ⇒ F
• ONTO: A=V ⇒ F; A=F ⇒ N; A=N ⇒ F

Assorbimento della doppia negazione in N

¬¬A↔¬¬¬¬A

Dopo la seconda negazione il valore resta nel ciclo F↔N.

• BOOL: nessuno
• LO: A=V ⇒ N; A=F ⇒ F; A=N ⇒ N
• ONTO: A=V ⇒ N; A=F ⇒ F; A=N ⇒ N

Idempotenza di ∧

(A∧A)↔A

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ N
• ONTO: A=F ⇒ F; A=N ⇒ N

Idempotenza di ∨

(A∨A)↔A

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ N
• ONTO: A=F ⇒ F; A=N ⇒ N

Commutatività di ∧

(A∧B)↔(B∧A)

• BOOL: nessuno
• LO: A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ F; A=N,B=F ⇒ N; A=N,B=N ⇒ F
• ONTO: A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ F; A=N,B=F ⇒ N; A=N,B=N ⇒ F

Commutatività di ∨

(A∨B)↔(B∨A)

• BOOL: nessuno
• LO: A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N
• ONTO: A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N

Commutatività di ⊕

(A⊕B)↔(B⊕A)

• BOOL: nessuno
• LO: A=V,B=V ⇒ F; A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=V ⇒ F; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N
• ONTO: A=V,B=V ⇒ F; A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=V ⇒ F; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N

Commutatività di ↔

(A↔B)↔(B↔A)

• BOOL: nessuno
• LO: A=V,B=F ⇒ F; A=V,B=N ⇒ N; A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N
• ONTO: A=V,B=F ⇒ F; A=V,B=N ⇒ N; A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N

Associatività di ∧

(A∧(B∧C))↔((A∧B)∧C)

• BOOL: nessuno
• LO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F; A=V,B=F,C=V ⇒ F; A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ N; A=V,B=N,C=V ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ N; A=F,B=V,C=V ⇒ F; A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ N; A=F,B=F,C=V ⇒ F; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ N; A=F,B=N,C=V ⇒ F; A=F,B=N,C=F ⇒ N; A=F,B=N,C=N ⇒ F; A=N,B=V,C=V ⇒ F; A=N,B=V,C=F ⇒ N; A=N,B=V,C=N ⇒ N; A=N,B=F,C=V ⇒ N; A=N,B=F,C=F ⇒ N; A=N,B=F,C=N ⇒ F; A=N,B=N,C=V ⇒ N; A=N,B=N,C=F ⇒ F; A=N,B=N,C=N ⇒ N
• ONTO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F; A=V,B=F,C=V ⇒ F; A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ N; A=V,B=N,C=V ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ N; A=F,B=V,C=V ⇒ F; A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ N; A=F,B=F,C=V ⇒ F; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ N; A=F,B=N,C=V ⇒ F; A=F,B=N,C=F ⇒ N; A=F,B=N,C=N ⇒ F; A=N,B=V,C=V ⇒ F; A=N,B=V,C=F ⇒ N; A=N,B=V,C=N ⇒ N; A=N,B=F,C=V ⇒ N; A=N,B=F,C=F ⇒ N; A=N,B=F,C=N ⇒ F; A=N,B=N,C=V ⇒ N; A=N,B=N,C=F ⇒ F; A=N,B=N,C=N ⇒ N

Associatività di ∨

(A∨(B∨C))↔((A∨B)∨C)

• BOOL: nessuno
• LO: A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ F; A=F,B=N,C=F ⇒ F; A=F,B=N,C=N ⇒ F; A=N,B=F,C=F ⇒ F; A=N,B=F,C=N ⇒ F; A=N,B=N,C=F ⇒ F; A=N,B=N,C=N ⇒ N
• ONTO: A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ F; A=F,B=N,C=F ⇒ F; A=F,B=N,C=N ⇒ F; A=N,B=F,C=F ⇒ F; A=N,B=F,C=N ⇒ F; A=N,B=N,C=F ⇒ F; A=N,B=N,C=N ⇒ N

Associatività di ⊕

(A⊕(B⊕C))↔((A⊕B)⊕C)

• BOOL: nessuno
• LO: A=V,B=V,C=V ⇒ F; A=V,B=V,C=F ⇒ N; A=V,B=V,C=N ⇒ F; A=V,B=F,C=V ⇒ F; A=V,B=F,C=F ⇒ N; A=V,B=F,C=N ⇒ F; A=V,B=N,C=V ⇒ F; A=V,B=N,C=F ⇒ N; A=V,B=N,C=N ⇒ F; A=F,B=V,C=V ⇒ N; A=F,B=V,C=F ⇒ N; A=F,B=V,C=N ⇒ N; A=F,B=F,C=V ⇒ N; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ N; A=F,B=N,C=V ⇒ N; A=F,B=N,C=F ⇒ N; A=F,B=N,C=N ⇒ F; A=N,B=V,C=V ⇒ F; A=N,B=V,C=F ⇒ N; A=N,B=V,C=N ⇒ F; A=N,B=F,C=V ⇒ F; A=N,B=F,C=F ⇒ N; A=N,B=F,C=N ⇒ F; A=N,B=N,C=V ⇒ F; A=N,B=N,C=F ⇒ F; A=N,B=N,C=N ⇒ N
• ONTO: A=V,B=V,C=V ⇒ F; A=V,B=V,C=F ⇒ N; A=V,B=V,C=N ⇒ F; A=V,B=F,C=V ⇒ F; A=V,B=F,C=F ⇒ N; A=V,B=F,C=N ⇒ F; A=V,B=N,C=V ⇒ F; A=V,B=N,C=F ⇒ N; A=V,B=N,C=N ⇒ F; A=F,B=V,C=V ⇒ N; A=F,B=V,C=F ⇒ N; A=F,B=V,C=N ⇒ N; A=F,B=F,C=V ⇒ N; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ N; A=F,B=N,C=V ⇒ N; A=F,B=N,C=F ⇒ N; A=F,B=N,C=N ⇒ F; A=N,B=V,C=V ⇒ F; A=N,B=V,C=F ⇒ N; A=N,B=V,C=N ⇒ F; A=N,B=F,C=V ⇒ F; A=N,B=F,C=F ⇒ N; A=N,B=F,C=N ⇒ F; A=N,B=N,C=V ⇒ F; A=N,B=N,C=F ⇒ F; A=N,B=N,C=N ⇒ N

Distributività di ∧ su ∨

(A∧(B∨C))↔((A∧B)∨(A∧C))

• BOOL: nessuno
• LO: A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ F; A=F,B=V,C=V ⇒ F; A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ F; A=F,B=F,C=V ⇒ F; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ F; A=F,B=N,C=V ⇒ F; A=F,B=N,C=F ⇒ F; A=F,B=N,C=N ⇒ N; A=N,B=V,C=V ⇒ F; A=N,B=V,C=F ⇒ F; A=N,B=V,C=N ⇒ F; A=N,B=F,C=V ⇒ F; A=N,B=F,C=F ⇒ N; A=N,B=F,C=N ⇒ N; A=N,B=N,C=V ⇒ F; A=N,B=N,C=F ⇒ N; A=N,B=N,C=N ⇒ F
• ONTO: A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ F; A=F,B=V,C=V ⇒ F; A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ F; A=F,B=F,C=V ⇒ F; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ F; A=F,B=N,C=V ⇒ F; A=F,B=N,C=F ⇒ F; A=F,B=N,C=N ⇒ N; A=N,B=V,C=V ⇒ F; A=N,B=V,C=F ⇒ F; A=N,B=V,C=N ⇒ F; A=N,B=F,C=V ⇒ F; A=N,B=F,C=F ⇒ N; A=N,B=F,C=N ⇒ N; A=N,B=N,C=V ⇒ F; A=N,B=N,C=F ⇒ N; A=N,B=N,C=N ⇒ F

Distributività di ∨ su ∧

(A∨(B∧C))↔((A∨B)∧(A∨C))

• BOOL: nessuno
• LO: A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ F; A=F,B=F,C=V ⇒ F; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ F; A=F,B=N,C=V ⇒ F; A=F,B=N,C=F ⇒ F; A=F,B=N,C=N ⇒ F; A=N,B=V,C=F ⇒ F; A=N,B=V,C=N ⇒ F; A=N,B=F,C=V ⇒ F; A=N,B=F,C=F ⇒ F; A=N,B=F,C=N ⇒ N; A=N,B=N,C=V ⇒ F; A=N,B=N,C=F ⇒ N; A=N,B=N,C=N ⇒ F
• ONTO: A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ F; A=F,B=F,C=V ⇒ F; A=F,B=F,C=F ⇒ F; A=F,B=F,C=N ⇒ F; A=F,B=N,C=V ⇒ F; A=F,B=N,C=F ⇒ F; A=F,B=N,C=N ⇒ F; A=N,B=V,C=F ⇒ F; A=N,B=V,C=N ⇒ F; A=N,B=F,C=V ⇒ F; A=N,B=F,C=F ⇒ F; A=N,B=F,C=N ⇒ N; A=N,B=N,C=V ⇒ F; A=N,B=N,C=F ⇒ N; A=N,B=N,C=N ⇒ F

Assorbimento ∧/∨

(A∧(A∨B))↔A

• BOOL: nessuno
• LO: A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N
• ONTO: A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N

Assorbimento ∨/∧

(A∨(A∧B))↔A

• BOOL: nessuno
• LO: A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N
• ONTO: A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N

Elemento neutro di ∧

(A∧V)↔A

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ N
• ONTO: A=F ⇒ F; A=N ⇒ N

Elemento neutro di ∨

(A∨F)↔A

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ N
• ONTO: A=F ⇒ F; A=N ⇒ N

Elemento assorbente di ∧

(A∧F)↔F

• BOOL: nessuno
• LO: A=V ⇒ F; A=F ⇒ F; A=N ⇒ N
• ONTO: A=V ⇒ F; A=F ⇒ F; A=N ⇒ N

Complemento di ∧

(A∧¬A)↔F

• BOOL: nessuno
• LO: A=V ⇒ F; A=F ⇒ N; A=N ⇒ N
• ONTO: A=V ⇒ F; A=F ⇒ N; A=N ⇒ N

Complemento di ∨

(A∨¬A)↔V

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ F
• ONTO: A=F ⇒ F; A=N ⇒ F

De Morgan: ¬(A∧B) ≡ ¬A∨¬B

¬(A∧B)↔(¬A∨¬B)

• BOOL: nessuno
• LO: A=V,B=V ⇒ F; A=V,B=F ⇒ N; A=V,B=N ⇒ N; A=F,B=V ⇒ N; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ F; A=N,B=N ⇒ N
• ONTO: A=V,B=V ⇒ F; A=V,B=F ⇒ N; A=V,B=N ⇒ N; A=F,B=V ⇒ N; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ F; A=N,B=N ⇒ N

De Morgan: ¬(A∨B) ≡ ¬A∧¬B

¬(A∨B)↔(¬A∧¬B)

• BOOL: nessuno
• LO: A=V,B=V ⇒ F; A=V,B=F ⇒ N; A=V,B=N ⇒ F; A=F,B=V ⇒ N; A=F,B=F ⇒ N; A=F,B=N ⇒ N; A=N,B=V ⇒ F; A=N,B=F ⇒ N; A=N,B=N ⇒ F
• ONTO: A=V,B=V ⇒ F; A=V,B=F ⇒ N; A=V,B=N ⇒ F; A=F,B=V ⇒ N; A=F,B=F ⇒ N; A=F,B=N ⇒ N; A=N,B=V ⇒ F; A=N,B=F ⇒ N; A=N,B=N ⇒ F

De Morgan: A∧B ≡ ¬(¬A∨¬B)

(A∧B)↔¬(¬A∨¬B)

• BOOL: nessuno
• LO: A=V,B=V ⇒ N; A=V,B=F ⇒ N; A=V,B=N ⇒ N; A=F,B=V ⇒ N; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N
• ONTO: A=V,B=V ⇒ N; A=V,B=F ⇒ N; A=V,B=N ⇒ N; A=F,B=V ⇒ N; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N

De Morgan: A∨B ≡ ¬(¬A∧¬B)

(A∨B)↔¬(¬A∧¬B)

• BOOL: nessuno
• LO: A=V,B=V ⇒ N; A=V,B=F ⇒ F; A=V,B=N ⇒ N; A=F,B=V ⇒ F; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ F; A=N,B=N ⇒ N
• ONTO: A=V,B=V ⇒ N; A=V,B=F ⇒ F; A=V,B=N ⇒ N; A=F,B=V ⇒ F; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ N; A=N,B=F ⇒ F; A=N,B=N ⇒ N

Implicazione materiale

(A→B)↔(¬A∨B)

• BOOL: nessuno
• LO: A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=F ⇒ F; A=N,B=N ⇒ F
• ONTO: A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=F ⇒ F; A=N,B=N ⇒ F

Implicazione come ¬(A∧¬B)

(A→B)↔¬(A∧¬B)

• BOOL: nessuno
• LO: A=V,B=V ⇒ N; A=V,B=F ⇒ N; A=V,B=N ⇒ N; A=F,B=V ⇒ N; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ F; A=N,B=F ⇒ N; A=N,B=N ⇒ F
• ONTO: A=V,B=V ⇒ N; A=V,B=F ⇒ N; A=V,B=N ⇒ N; A=F,B=V ⇒ N; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ F; A=N,B=F ⇒ N; A=N,B=N ⇒ F

Coimplicazione come doppia implicazione

(A↔B)↔((A→B)∧(B→A))

«Compressione di due espansioni».

• BOOL: nessuno
• LO: A=V,B=F ⇒ F; A=V,B=N ⇒ N; A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N
• ONTO: A=V,B=F ⇒ F; A=V,B=N ⇒ N; A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ N; A=N,B=V ⇒ N; A=N,B=F ⇒ N; A=N,B=N ⇒ N

XOR come (A∧¬B)∨(¬A∧B)

(A⊕B)↔((A∧¬B)∨(¬A∧B))

• BOOL: nessuno
• LO: A=V,B=V ⇒ F; A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=V ⇒ F; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N
• ONTO: A=V,B=V ⇒ F; A=V,B=F ⇒ F; A=V,B=N ⇒ F; A=F,B=V ⇒ F; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N

XOR come ¬(A↔B)

(A⊕B)↔¬(A↔B)

• BOOL: nessuno
• LO: A=V,B=V ⇒ F; A=V,B=F ⇒ N; A=V,B=N ⇒ F; A=F,B=V ⇒ N; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N
• ONTO: A=V,B=V ⇒ F; A=V,B=F ⇒ N; A=V,B=N ⇒ F; A=F,B=V ⇒ N; A=F,B=F ⇒ N; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ N

Riduzione all'assurdo

((A→B)∧(A→¬B))→¬A

• BOOL: nessuno
• LO: A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ F
• ONTO: A=F,B=V ⇒ F; A=F,B=F ⇒ F; A=F,B=N ⇒ F; A=N,B=V ⇒ F; A=N,B=F ⇒ F; A=N,B=N ⇒ F

Consequentia mirabilis

(¬A→A)→A

• BOOL: nessuno
• LO: A=F ⇒ F; A=N ⇒ F
• ONTO: A=F ⇒ F; A=N ⇒ F

Assioma di contrapposizione (Łukasiewicz)

(¬A→¬B)→(B→A)

• BOOL: nessuno
• LO: A=F,B=V ⇒ F; A=N,B=V ⇒ F
• ONTO: A=F,B=V ⇒ F; A=N,B=V ⇒ F

Contrapposizione

(A→B)↔(¬B→¬A)

• BOOL: nessuno
• LO: A=V,B=F ⇒ F; A=V,B=N ⇒ F
• ONTO: A=V,B=F ⇒ F; A=V,B=N ⇒ F

Esportazione

((A∧B)→C)↔(A→(B→C))

• BOOL: nessuno
• LO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F
• ONTO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F

Distribuzione di → su ∧

(A→(B∧C))↔((A→B)∧(A→C))

• BOOL: nessuno
• LO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F; A=V,B=F,C=V ⇒ F; A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ F; A=V,B=N,C=V ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ F
• ONTO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F; A=V,B=F,C=V ⇒ F; A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ F; A=V,B=N,C=V ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ F

Prove per casi

((A∨B)→C)↔((A→C)∧(B→C))

• BOOL: nessuno
• LO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F; A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ F; A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ F; A=N,B=V,C=F ⇒ F; A=N,B=V,C=N ⇒ F
• ONTO: A=V,B=V,C=F ⇒ F; A=V,B=V,C=N ⇒ F; A=V,B=F,C=F ⇒ F; A=V,B=F,C=N ⇒ F; A=V,B=N,C=F ⇒ F; A=V,B=N,C=N ⇒ F; A=F,B=V,C=F ⇒ F; A=F,B=V,C=N ⇒ F; A=N,B=V,C=F ⇒ F; A=N,B=V,C=N ⇒ F