intuitionistisk logik

Intuitionistisk logik, et alternativ til klassisk logik, som ikke anerkender, at et udsagn altid enten er sandt eller falsk. p∨¬p er ikke en logisk sandhed. I intuitionistisk logik kan man kun hævde, at et udsagn er sandt, hvis man har en konstruktiv metode til at bevise det.

Fx er udsagnet "der findes uendeligt mange primtal" sandt, fordi man kan finde en metode, som producerer større og større tal og samtidig godtgør, at disse tal er primtal. Men for andre udsagn vedrørende uendelig mange tal kan man ikke finde en sådan metode.

Fx findes der i dag ingen metode til at afgøre, om udsagnet "alle lige tal større end fire kan dannes som sum af to ulige primtal" (Goldbachs formodning) er sandt eller falsk. Hvis dette udsagn kaldes p, så har p ingen sandhedsværdi. Dets negation ¬p ("der findes lige tal større end fire, som ikke er sum af to ulige primtal") har heller ingen sandhedsværdi. Altså har p∨¬p ingen sandhedsværdi.

En konsekvens af dette strenge krav til sandhed bliver, at det ikke generelt er tilladt at udføre indirekte beviser, som man kender dem fra matematik. Det er fx ikke tilladt at vise eksistensen af et tal med en given egenskab ved at argumentere for, at hvis alle tal ikke havde egenskaben, så ville det føre til en logisk modstrid.

Et sådant bevis ville ikke give en metode til at finde tallet. Den intuitionistiske logik er netop udsprunget af en kritik af klassiske matematiske metoder, som, når de anvendes ukritisk på uendelige mængder, fører til paradokser. Den blev grundlagt af L.E.J. Brouwer og aksiomatiseret i 1930 af Brouwers elev Arend Heyting (1898-1980).

Spørgsmålet om, hvad man nærmere skal forstå ved intuitionistisk sandhed, er blevet grundigt studeret i de seneste år. I dag findes der flere semantikker, som gør intuitionistisk logik fuldstændig på samme måde, som klassisk logik er fuldstændig mht. sandhedsfunktionel semantik. Disse moderne undersøgelser af intuitionistisk logik spiller en stor rolle i teoretisk datalogi. En række bevisførere er baseret på intuitionistisk logik, fx Agda, Coq og Lean.