logica minimale

logica minimale

logica minimale calcolo logico, introdotto nel 1936 dal matematico norvegese I. Johansson. È una rielaborazione della → logica intuizionista in cui non è prevista la legge cosiddetta ex falso quodlibet secondo la quale da una premessa contraddittoria è possibile derivare qualsiasi affermazione. Le dimostrazioni della logica minimale sono sviluppate nel calcolo dei → sequenti utilizzando un insieme di regole logiche che non comprenda né il principio del → terzo escluso né l’ex falso quodlibet. In base all’isomorfismo di → Curry-Howard le deduzioni logiche, così formalizzate, possono essere associate a dei programmi. Più precisamente, in logica minimale il processo di eliminazione del taglio (→ taglio, regola del) dalle dimostrazioni avviene in maniera deterministica e ciò rende il calcolo minimale interessante dal punto di vista computazionale.