Eng (Sambo) Boris

PhD Student in Computer Science, Team LoVe, LIPN (Université Sorbonne Paris Nord, France) domain_name@hotmail.fr
« Return to Thoughts

On Intuitionism and Classicism

proof theory philosophy history technical

Prerequisite: natural deduction, sequent calculus, intuitionistic logic, classical logic

Introduction

Are there several logics? A unique and right logic? Intuitionism was introduced during the foundational crisis of mathematics in the beginning of the 20th century by mathematicians such as H. Poincaré and L.E.J Brouwer [1]. It constitutes both a critic of the mathematical practice and an opposition to formalism in favor of intuition and construction. I provide an interpretation of intuitionism and classicism to the ones who are only familiar with their technical interpretation. We start from the question of the reliability of logic and mathematics.

The location of certainty

Practice shows that mathematics has a great reliability but in the time of Brouwer, the existence of non-euclidean geometries resulted in the emergence of doubts. What allows us to consider a proposition as axiom or to use a particular rule of deduction? Where does the certainty of mathematics lie? Two school of philosophy tried to answer that last question:

They still have a common point: the rejection of the correlation between mathematical laws and the laws of nature. In other words they’re both subjectivist conceptions of logic and mathematics. We focus on intuitionism and its viewpoint regarding logic.

Subjectivism and constructivism

Science rely on empirical artefacts thus defining certainty on observation and experience. From the viewpoint of intuitionism, certainty appears when we can make the existence of mathematical objects explicit (opposing semantic realism and its external existence of mathematical objects). It has several consequences:

The rejection of these logical laws was quite surprising since they were strongly used in the mathematical practice. Intuitionism is a subjectivist ideology because it only accepts what we, humans, can know, understand and construct, opposing any theory of truth and realism (adherence to a preconception of reality). Intuitionism accepts that we don’t necessarily know and that we have to consider the undecidability of propositions (a fatality).

Brouwer defended pure intuition instead of a mechanical thus belittling view of mathematics based on linguistics so he was against any formalist conception of logic even though himself and his own student, A. Heyting (and independently A. Kolmogorov) are behind the formalization of constructivism through the BHK interpretation. Logic is now divided in two: classical logic and intuitionistic logic.

Now, let’s explore the technical content of intuitionism.

Technical interpretation

Classical logic tells us if a proposition is a true or false and Intuitionistic logic tells us why it is so.

Model-theoretic interpretation

Classical logic is naturally interpreted with truth values either $0$ or $1$ associated to a logical proposition. As the concept of provability changed in the intuitionistic framework, we have to switch to Heyting models or Kripke models internalizing the “unknowable” and thus ignoring the deep mechanism and dynamics of intuitionism.

In Heyting models we usually interpret propositions in either a symbol representing truth, one for falsity or an “intermediate truth values”. These values represent the absence of knowledge that we can assign to generally undecidable propositions such as the law of excluded middle. In Kripke models we do something similar by reifying a “world of all possibilities” allowing us to model the unknown/unknowable. These models are quite poor because while working in a model-theoretic setting they don’t have the power of explaining why a proposition is true or not.

Proof-theoretic interpretation

The proof-theoretical interpretation is a bit more interesting. Let’s explore it in the Natural Deduction $NJ$ and the Sequent Calculus $LJ$.

Computational interpretation

The system $NJ$ being isomorphic to the $\lambda$-calculus through the Curry-Howard isomorphism, the computational interpretation is straightforward:

In particular, intuitionism captures computational decidability. What is provable is what is computable by a sequential functional program. We have a correspondence between “computationally decidable” and “logically decidable” in this framework. The focus on a unique conclusion becomes the construction of a unique result.

Classicism strikes back

Is intuitionism weaker due to its rejection of logical rules?

No, intuitionism isn’t weaker. It can even be considered as stronger because intuitionistic logic is a logic where only explicit constructions emerge. Not only it has a power that classical logic don’t have but moreover, the conception of classical truth isn’t lost (we can encode classical provability in the intuitionistic framework).

To recover the classical truth, there exists several encodings called double-negation translations such that if $A$ is provable classically then is provable in intuitionistic logic. These translations usually work by putting double-negations $\lnot\lnot$ at the right position in formulas. Here is an example with a proof of the encoding of the excluded-middle in natural deduction $NJ$ and sequent calculus $LJ$.

Note that we have $\lnot A \equiv A \Rightarrow \bot$ in intuitionistic systems. We also use the notation $\Gamma = {(A \lor \lnot A) \Rightarrow \bot}$.

$ \infer[\Rightarrow i]{ \infer[\Rightarrow e]{ \infer[ax]{\qquad\qquad\qquad\qquad}{\Gamma \vdash (A \lor \lnot A) \Rightarrow \bot} \qquad \infer[\lor i]{ \infer[\Rightarrow i]{ \infer[\Rightarrow e]{ \infer[ax]{\qquad\qquad\qquad\qquad\qquad}{\Gamma, A \vdash (A \lor \lnot A) \Rightarrow \bot} \qquad \infer[\lor i]{ \infer[ax]{\qquad\qquad\qquad}{\Gamma, A \vdash A} }{\Gamma, A \vdash A \lor \lnot A} }{\Gamma, A \vdash \bot} }{\Gamma \vdash \lnot A} }{\Gamma \vdash A \lor \lnot A} } {(A \lor \lnot A) \Rightarrow \bot \vdash \bot} }{\vdash_{NJ} ((A \lor \lnot A) \Rightarrow \bot) \Rightarrow \bot} $


$ \infer[\Rightarrow r]{ \infer[c]{ \infer[\Rightarrow l]{ \infer[\lor r]{ \infer[\Rightarrow r]{ \infer[\Rightarrow l]{ \infer[\lor l]{ \infer[ax]{\qquad}{A \vdash A} }{A \vdash A \lor \lnot A} \qquad \infer[ax]{\qquad}{\bot \vdash \bot} }{\Gamma, A \vdash \bot} }{\Gamma \vdash \lnot A} }{\Gamma \vdash A \lor \lnot A} \qquad \infer[ax]{\qquad}{\bot \vdash \bot} }{(A \lor \lnot A) \Rightarrow \bot, (A \lor \lnot A) \Rightarrow \bot \vdash \bot} }{(A \lor \lnot A) \Rightarrow \bot \vdash \bot} }{\vdash_{LJ} ((A \lor \lnot A) \Rightarrow \bot) \Rightarrow \bot} $

These translations not only recover the classical power of proofs but also give a computational interpretation to classical proofs. Why does $\vdash \lnot\lnot(A \lor \lnot A)$ work? Double-negation isn’t a magical technicality coming out of nowhere. Actually, it works because adding negations allows us to bypass the restriction of the unique conclusion by taking advantage of the free contraction on the assumptions. We clearly see that negation acts as a spatial manipulation in a proof (it puts information in the context, similarly to the action of saving data). Double-negation makes the proofs and programs aware of the context (as we can see in CPS translations).

If we take a close look at the two proofs above, we can see that a kind of mechanism of “saving information” is at work. The double-negation allows us to put information in the context which is not restricted and thus we can reuse it for both the branches with $A$ and the one with $\lnot A$ in $A \lor \lnot A$ while we had a choice destructing information (irreversibility of disjunction) in the intuitionistic case.

Going further, we can see that classical laws (especially introduction of double-negation) correspond to an ability of freely saving information while maintaining constructivity and sequentiality. The Curry-Howard isomorphism tells us that the computational contents of classical logic lies in continuation-passing style and control operators such as call/cc.

Conclusion: classical logic and non-determinism

To conclude, right-hand restriction on space forbids infinity on the conclusion but enforces constructivity and sequentiality. We may think that some classical truths are lost in this new intuitionistic framework but an encoding with double-negation allows to simulate classical proofs in a sequential way by a mechanism of jump/pointer/saving on the left-hand side which acts as a kind of memory.

But still, classical logic remains the most natural way of reasoning for humans. But why? Intuitionism fits the point of view of sequential machines but pure classicism apparently doesn’t. What makes $\vdash A \lor \lnot A$ provable? It seems to be the ability of retraction of choices (which is destructive for sequential machines). The excluded-middle is indeed provable if we choose to prove $\lnot A$, then introduce $A$ in the context and change our mind to prove $A$ instead (as suggested with P. Wadler’s devil):

$ \infer[\lor r]{ \infer[\lnot r]{ \infer[ax]{\qquad}{A \vdash A} }{\vdash A, \lnot A} }{\vdash_{LK} A \lor \lnot A} $

But $LK$ lacking confluence as stated by the below critical pair [2], it is irrelevant in the computational world.

$ \infer[cut]{ \infer[RW]{ \infer{\vdots}{A \vdash B} }{A \vdash C, B} \qquad \infer[LW]{ \infer{\vdots}{D \vdash E} }{D, C \vdash E} }{A, D \vdash B, E} $

reducing to either

$\infer[{RW, RC, LW, LC}^\ast]{A, D \vdash B, E}{A \vdash B}$

or

$\infer[{RW, RC, LW, LC}^\ast]{A, D \vdash B, E}{D \vdash E}$

To study logical phenomena further we can normalize the rules of $LK$ thanks to the involutivity of negation to only consider right rules producing a monolateral version of $LK$. Sequents are now of the shape $\vdash A_1, …, A_n$ corresponding to a kind of space of concurrent interactions with partial/unfinished proofs we can postpone:

Classicism gives more space to work on proofs and seems to be aware of its environement for both pure classicism and negation-translations. Intuitionism provide a “why” explaining the observations/results of Classical logic. But why is this explanation correct? The “how” still remains. The answer will we partially provided by Linear Logic which describes the operation behavior of Logic.

References

[1] Brouwer, L. E. J. (1913). Intuitionism and Formalism. Bulletin of the American Mathematical Society 20:81-96.

[2] Girard, J. Y., Taylor, P., & Lafont, Y. (1989). Proofs and types (Vol. 7). Cambridge: Cambridge University Press.