It seems natural to believe that logic
gives us some *a priori* knowledge. When I know
that X is logically valid, then I know that any instance of X is empirically
true before taking any information from the world. When I know empirically that
P and logically that PQ, the detachment rule allows me to assert Q (empirically). It seems
that in such a case I come to the empirical knowledge of Q with the help of
some *a priori* knowledge.

After all, Carnap formulated the main
tenets of logical empiricism in such terms: we are going on with Kantian
epistemology, only we remove the intuitive strata of the *a priori*, while keeping the logical one (even if the theoretical
interpretation of the logical *a priori* changes,
in order to reflect Fregean advance of logic). Jolle Proust argued about this
point in her habilitation thesis *Questions de forme*, nowadays translated in English.

It is not very easy to decide what Freges
position on the issue of *a priori* was, at the
same time because he writes and thinks in a historical context dominated by
Kantian language and framework – but his assumption of such a context
should not be equated with agreement – and, more deeply, because he
seems to be attracted both by platonician and empiricist views. But we still
may say, at least it seems to me so, that his strong rejection of psychologism
and his plea for objectivity of logic indeed favor the conception of logical
knowledge as *a priori* more than any alternative
conception.

For sure, we may also hear, in analytical tradition, another voice, fighting against logical absolutism. I will take here the example of Goodman, who explicitly raises the question of proof, our question for this conference.

Trying to evaluate where we are with the
problem of induction, in the beginning of the lecture The new enigma of
induction [1], he cites and resumes Humes conception, and wonders if there
really is such an absolute gap between induction and deduction, the latter
allowing us to apply universal schemes with complete certainty, while
performing the former we may only introduce universality as a fragile guess.
He contends that such is not the case, arguing that we also have, with
deduction, something like an uneffectiveness or an openness of the rules and
its applications. Goodman says that we formulate inference rules and apply them
in particular cases, considering justified inferences to be the one
accomplished in accordance with the rules. But we also think that correct inference
rules are the one which ground inferences that we already know as good ones. If
that much is true, there is a circle: we rely on rules for evaluating
inferences, and on inferences for evaluating rules. Now Goodman claims the
circle is not *vitiosus*: we always already give
credit to some inferences and some rules, and we correct both sets, by mutual
adjustment: we reject an inference if it is excluded by rules we cannot thing
of canceling, we cancel a rule if it forbids some inference estimated as beyond
any critic.

Such an explanation, it is worth to
observe, differs very little, if in any precise way, from the one given by
Heidegger in 32 or 63 of *Sein und Zeit*, trying
to convince us that the *hermeneutical circle* is
not a vicious one. It is strange to meet the evocation of such a circle in the
description by an analytical philosopher of what is nothing but the blueprint
of logical reasoning: the laws of deduction, the principles of proof. Is it
really possible, is it really meaningful to concede in such a way what looks
like the relativization of the rules of proof, and for that reason, of proof
itself?

On could argue historically that the laws
of proof, be it the Hilbert-Ackermann system or Gentzen-Prawitzs natural
deduction system, were not given from the beginning at Sinai. I may even quote
the not minor example of Tarski – former Teitelbaum – arguing
in his paper ber den Begriff der logischen Folgerung of 1935 in favor of what we now call his concept of semantic
logical consequence[2]. In this paper, Tarski does not expose his notion of logical
consequence as simply another point of view about proof, but rather as the
potentially true one against the syntactical concept arising from Hilberts
work. He invokes the inference transiting from the infinite data *P(0)*, *P(1)*,, *P(n)*, [one assertion for every natural number] to the assertion "*k* *P(k)*, the range for the
variable *k* being understood as the set of
natural numbers. Such an inference is absolutely certain, he says, but the
finitary hilbertian setting forbids what we now call the w-rule. So we should change this setting for the semantic one he has
in mind and comes to expose. Tarski surely behaves in that paper as if the laws
of proof were nothing else that the always revisable product of some special
kind of hermeneutics, arising from the mutual adjustment of rules and
inferences, as Goodman was formulating it.

This kind of vision of logic and of the
rules of proof has some posterity in the analytical movement. After all, Quine,
in his famous paper Two dogmas about empiricism , denies any sharp
and definite frontier between analytical and synthetic statements, advocating a
picture of rational knowledge as made of a huge set of sentences enjoying some
kind of solidarity, and showing some hierarchical organization: logical laws
stand in the center, mathematical assertions in the first circle, physical
current truths in the following larger circle, and empirical sentences build
the outside of the whole structure. Nothing, in all this, is supposed to be
immune to revision, and Neuraths sailor may modify anything in order to go on
shipping, be it logical laws. Sometimes Youngs wholess experiments in quantum
mechanics are understood as yielding an example of such a revision, enforced by
empirical data (leading to the cancellation of the distributivity law for
propositional calculus). Some sophisticated debates of that kind come even
to consider the principle of contradiction as subject to revision (only the
free action of the inconsistent rule P(P) – Q – whatever Q is – should
be avoided, in the name of an *a priori*
principle).

One may feel that these extreme empiricist positions are somehow dishonest. It is not clear that any one, in any case, really discarded usual first order logic. Does the physicist really thinks universally in accordance to some formulation of quantum logic? More likely, he does so in the best case only with respect to a certain range of ontological or experimental situations, if he ever does (are we really compelled to formulate logically what happens in Youngs wholes experiments? Is the quantum logic account anything else than an interpretation?).

The idea that there is no *a priori* framework of any kind, be it logical, claims to be a genuine
empiricist claim, but it really is the disavowal of rationality, because the
concept of rationality does nothing else than referring to such a presupposed
set of *a priori* standards. We dont call
rational knowledge anything appearing to be induced by some mighty uppercut
from the great boxing world, and the difference may not consist in anything
else than such standards.

Let us climb, after all, one step higher,
and ask if the philosophical question about *a priori* should be solved *a posteriori* or *a
priori*. Even if one wants to answer that it has to
be answered by bringing some *a posteriori*
evidence (of epistemological kind, like the Youngs experiment), this answer
looks like enjoying *a priori* certainty. Radical
empiricists know the unavoidability of *a posteriori* in an *a priori* way. Very simply,
philosophical formulations of empiricism often come in the form of
transcendental arguments: for example, when Searle insists, aiming at refuting
Putnam, that he is an external realist, and when he argues that the very
concept of objective truth requires that some external reality imposes its
message, he is arguing in terms of what we always already understand as
objective truth, and cannot help doing so, which is precisely the general form
of transcendental arguments.

Last point: knowledge has to be knowledge
through language, we would not be ready to call scientific knowledge something
that would not result in sentences and texts (Im making, here, another
transcendental point, but this one is generally admitted in analytical
tradition, I believe). Further, a language in terms of which our scientific
truths are stated has to be a language that we are able to speak. This forces
the language of science not only to follow some logic, but to follow some logic
that humans are able to stand, to assume. And this very elementary and simple
constraint of language already brings some *a priori* framework.

Most probably, these general issues about
radical empiricism deserve some special discussion, which could motivate
another (and quite big) paper . But I will now forget about them, taking for
granted that there is some *a priori* knowledge
encapsulated in logic, and that our theoretical apparatus for logic correctly
identifies, in some way or another, such an *a priori* level. Only I am going to argue that we cannot help acknowledging,
behind or under this logical *a priori*, also an
intuitive one, which goes hand by hand with the first one: if Im right, Carnap
failed in rejecting Kants motto of space and time as pure intuitions,
something of the same kind is already taken with logic, to the effect that *a
priori* has still to be recognized as two-folded,
even for someone not ready to accept Kants epistemological argument about
Newtonian physics any more. This will be the task of my first part. Then, in
the second part, I will attempt to vindicate, advocating contemporary
developments, Kants conception of the specificity of mathematical proofs. In
that purpose, I will describe logical proofs as they are nowadays understood by
proof theory as mathematical in Kants sense.

Frege, for sure, gave us the logical
mastering of multiplicity speech, he brought to the fore quantification as
logical operator and a way of analyzing language in terms of quantification: we
summarize this point by saying that he inaugurated what we now call first order
logic. But he did so, in his famous *BegriffsSchrift*, while at the same time settling a formal device for expressing
logical statements and writing proofs. And Frege was no less influential in
this formalizing behavior than in making the role of quantification clear. We
now understand that it is not possible to deal with logic outside of some
peculiar kind of textuality: real logic happens in formalized mode, has to be
couched in some specific idiom. *Terms* incarnate *names*, *formulas* correspond to *sentences*, *formal proofs* play the part of *texts*. All the technical background of logic for analytical philosophy is
not supposed to be commonsense logic, as it happened for example for the
nominalist school during middle age, but rather contemporary formalized logic.

But we have now to state what the general evolution was after logic became formalized. Clearly, one aspect of this evolution was that many non standard logics happened to be defined or studied. Logicians introduced intuitionnistic logic, free logic, second order logic, modal logic, quantum logic, paraconsistent logic, and so on. For every one of these in some way alternative logic, they had to define some inference system, some semantics, and to wonder whether it was possible to demonstrate some completeness result, like for first order predicate logic. More generally they tried to test in the case of each particular logic the validity of some key results, some of them semantical, some of them syntactical.

This work, which goes on in a prolific and fruitful way since more than one century, resulted in an impressive imaginative set of logical experiments: any particular logical principle happened to be relativized in the context of at least one of these experiments (like involutivity of in intuitionnistic logic or contradiction principle in paraconsistent logic).

As a consequence of one century of logical studies, it appears therefore in a striking way that what human beings agree upon with the greatest certainty is not any logical law, be it the contradiction principle, but the finitary intuitive statements that something is correctly derived in the context of some inference system. There is a debate about the powers and qualities of the various logics, and these powers and qualities are judged on the basis of what one can prove inside any one of theses logics. The general concept of theorem with respect to some inference system is the true universal of logical research.

But this concept is not defined in a logical way. It appears as a special case of the concept of constructive class, introduced by exhibition of primitive objects of the class and building rules[3]. Something is member of the class if it may be constructed on the basis of the primitive objects using the building rules. That it is the case may be shown by exhibiting a construction tree for the object, witnessing its membership in reference to the rules.

This seems to mean that our most universal
agreement, contrary to what logicists had in mind and insisted upon, rests on
some intuitive share: that some formal text yields some acceptable proof-tree,
and therefore counts a formal proof, is something that we cannot but see,
relying on some very limited *a priori* spatial
knowledge, involving the *right*/*left* and the *top*/*down* distinctions. Our recognition consists in binding the actual
concrete signs as a whole to some symbolic scheme belonging to the weakened
space to which our intuition relates : when we grasp the proof-structure
in the proof-tree, we see this scheme in this space rather than the concrete
signs in Euclidean space.

Such an assertion is nothing else that what Brouwer objected in the beginning of formalist adventure to Hilbert: one has first to share intuitionistic conception of mathematical objects in order to be able to play the game of formulas and proofs.

This may appear to be a kind of paradox, as
far as the philosophical will to secure rationality by founding it on a new
logic conceived of as objective and dispensing humanity of any dependence on
intuition seems to have lead to an epistemological situation where everything
is under the control of a very specific and minimal intuition. Ultimately, I
think that we should not consider the situation as paradoxical or as rationally
disturbing in any way: it only expresses that the logical *a priori* is at the same time discursive and intuitive, that it consists in
two layers, the discursive one being so to say superimposed to the intuitive
one. But may be you have to be Kantian enough in order to accept such a
picture: this is precisely what I ask from contemporary philosophy of logic!

Without trying know to deepen this discussion, let us simply ask: what could one argue in order to deny the foregoing presentation? I can think basically of two philosophical moves: the first one will consist in arguing that constructive intuition, as I just outlined it, is not really ruling everything, that it does not enjoy this key or control position I just pictured; and the second one will consist in arguing that there is nothing really intuitive in this intuition, that it is free of any of the features that motivated the Fregean and more generally analytical rejection of intuition.

These two moves gives rise to four objections, the second one being manageable in three ways. I will now consider each one of these objections, trying first to formulate them in the best possible way.

Let us formulate things in the simplest possible way. We are going to say, for example, that, whatever may be organized as the formal inference system for predicate logic, be it some Hilbert-like system (like the one devised originally by Hilbert and Ackermann), some natural deduction system or some sequent calculus system, the concept of correctness for proofs connected with the adoption of such a system does not overrule the purely logical authority of logic.

For example, if Im deducing P[x/t] from "x P(x), Im acting in agreement with my fundamental understanding of universality and instantiation, Im not obeying a meaningless inference rule. Or, this rule is based on the remark that the truth of "x P(x) encompasses the truth of every instance of P(x), the inference rule does nothing but expressing some law of the being true.

Same comment in the case of the *modus
ponens*: when I infer Q from PQ and P, Im not
obeying some degenerate form of the *cut* rule of
the sequent calculus, Im rather inspired by the truth table of PQ, known
(because decided) since the ancient (Stoic) Philo. So again, the rule is based
on some properties of truth.

And certainly I would be right on these two points, in a way.

But can I go as far as claiming that logical necessity does not belong at all to the level of logical correctness, as intuitively checkable? This would be that the necessity expressed by formal systems, the fact that some formulas are theorems of these systems, is of a completely different nature that the necessity conveyed by any one of the axioms or rules belonging to the only true system. To my eye, such a position is not tenable.

1) In some cases, the morphological necessity conveyed by the formal rule seems to say the same as the logical necessity, like in the case of the introduction rule for . In any case the formal rules capture the logical content, which seems to suggest that the formal/morphological setting is not an extraneous irrelevant device with respect to it.

2) More radically, if one persists in
bestowing predicate logic some value beyond the formal necessity incorporated
in any logical system (including the ones designed for predicate logic itself)
then one has to recognize some conceptual level, which *a priori* structures thought independently of everything contemporary logic
is able to show and prove. And it would be the task of philosophy to make such
a logical core explicit, to say which logical principles are unavoidable,
because they are not only inserted in some formal/intuitive device, but are
connected to our deep understanding of what truth about objects is (for
predicate logic) or of what truth is (for propositional calculus). But in that
case, it seems to me that logic receives a status very analogous to the one of
transcendental logic in Kants critical philosophy, even if know presented
and exposed in a different way (but not absolutely different). So, at least,
rationality is ruled by some ultimate subjective principles: may be there is no
intuition, but there is some non technical understanding of truth as conveyed
by language which dominates any possible reasoning, an understanding that can
only be stated and established in its foundational authority by some kind of
transcendental subject.

3) But this is not enough. As a matter of
fact, we dont only use formal devices as external translations of subjective
absolute principles. The convenience of formal morphology with logical content,
which was evoked in 1), leads us to live the formal-intuitive level as the
level of *legality*, in such a way that our certainty
concerning logical knowledge happens at that level.

I think I cannot do better, in order to
illustrate that point, than referring to some recent paper of Stewart Shapiro,
where he discusses Priests work[4]. In his paper[5], Shapiro criticizes the way Priest advocates for some
para-consistent logic, called *dialethic logic*.
Shapiro examines what becomes of Gdels incompleteness theorem in this
context. If we work in the theory named PA* – basically, PA with
dialethic logic and with adjunction of the truth predicate T – we
certainly can build Gdels statement G* for that theory, but we cannot
conclude that G* is undecidable, in absence of the consistency hypothesis. It
turns out that G* is actually provable in PA*. If we introduce some integer *g* as a code for the proof of G*, and the integer *q* as the code for G* itself, and if we denote by PRFPA*(*x*,*y*) the provability predicate in PA*, then it happens that in the very
peculiar situation yielded by G*, both PRFPA*(**g**,**q**) and PRFPA*(**g**,**q**) are provable (using **k** for the
numeral associated to the integer *k* in general).
Shapiro comments this situation in following terms:

I must admit that I cannot make
anything of this supposedly possibility. But rather than rely on my lack of
imagination, let us elaborate what is being claimed by the most thorough
dialetheist. The predicates PRFPA*(*g*,*q*) et non PRFPA*(*g*,*q*) have essentially the same informal verification procedure. We
first unpack g, to see what sequence it codes (if any). We write out this
sequence (if there is one). Then we check to see if each line is either an
axiom of PA* or follows from previous lines via one of the rules. If that is
completed successfully, we then check to see if the last line is G*. If all
goes well, we will have conclusive reason to hold that *g* is indeed the code of a PA*-derivation of G*. If there is a step
where something does not go well, we will have conclusive reason to conclude to
hold that *g* is not the code of a PA*-derivation
of G*. All goes well everywhere, and something goes wrong somewhere. But which
step in the verification can yield contradictory results? Is it that the last
line in the derivation is G* and the last line of the derivation is not G*, or
is it that line 72 is an axiom and line 72 is not an axiom, or is it that line
62 does and does not follow from lines 44 and 51 by *modus ponens*? [6].

Shapiro, clearly, contends that, even granted that we would be ready to admit at the logical level that in some cases X and X are both provable, we cannot admit that something is and at the same time is not a correct formal proof. I think we can compare his argument with Aristotles discourse in favor of the contradictions principle, in Met. g : Aristotle first says that the contradiction principle should not be proved, because it belongs to the original basis of what allows us to prove ; then he goes on justifying in a certain sense the contradiction principle, by showing that any one who advocates its negation really parts from rational community, escapes the share of rationality. Shapiro shows in a similar way that Priest has to deny our certainty about the basic fact of being a correct formal proof, and he silently suggests – at least, thats how I read him – that such a denial brings Priest outside of our rational sharing.

More generally, we rely on formal devices
to decide cases about which our logical *a priori*
insight hesitates, we constantly bestow some legal strength to formal exercise.
We dont treat formal behavior, formal intuition and formal entities as
external clothes of logic, but as conveying and partly supporting by themselves
logicity. I can formulate it in terms of this papers discussion by stating
that the intuitive *a priori* involved in formal
recognition appears to be superimposed to the discursive logical *a priori* given by logic as such. Even if the first level, enjoying some
autonomy, allows some critical attempts on the principles retained at the
second level, they ultimately both reinforce each other in our approval,
understanding and practice of the canonical core of logic (of lower predicate
standard calculus).

Let us now turn to the other option for denying my picture of contemporary logic: by claiming that the standard of formal proof does not carry any commitment to intuition. This can be sustained, as far as I know and understand, in three ways.

The idea is that construction belongs to
the realm of action rather than to the realm of intuition. So the objection
says that, when we recognize some statement as correctly deduced, we are only
stating that the building of the conclusion obeyed the building rules. Proof is
an action, the action of writing a sequence of formulas according to some set
of rules at each step. Recognition of correctness for some proof has to be described
as a kind of juridical estimate, and should in no way be construed as *intuition* of anything.

So we have to ask whether it is really possible to subtract from the idea of construction its intuitionist content, which was so important for the founding father of constructive thought, Brouwer.

As we very well know, each individual inference rule is expressed in terms of how formulas look like, in terms of their morphological aspect. Each one of these rules calls for having a structural look on formulas, and for acting on such a material in a structural or morphological way, by building the required form on the basis of the relevant extracted pieces. This is why you cannot act without seeing, not in the ordinary sense of visual perception, but in the schematic specific sense of formal seeing, which is adapted to the challenge of writing down some inferentially legitimate new statement.

The construction tree of the proof does not do anything else than summarizing the sequence of these morphologically minded acts, in such a way that the temporal and morphological relations between the individual acts become clear. Thanks to this tree, the proof in all its systematic structure becomes exhibited, both at the juridical and the intuitive level. When we are writing down the proof in a linear way without drawing the tree, the intuitive content of the tree is still there, although not synthetically showed.

This means that in the constructive experience of proof, intuition, action and law are intimately connected. The proof tree shows as some formally intuitive object the proof, but it shows nothing else, at the same time, than some formal behavior going through its constitutive steps, and than the legality of this behavior (as far as what is drawn is drawn as it has to be in accordance to the rules, what is shown is the graphical fulfillment of the rules schemes expectation).

We may insist philosophically on that
point. After all, Freges rejection of intuition rests on a very limited
conception of intuition. Intuition, in his perspective, is only purely
individual representational content, and the passive result of some external
objects influence or some internal psychological pressure. But there is a
tradition for which intuition is at the same time more and something else. Even
if we can find the fregean definition in Kants writings, we also find and in
the same texts the conception of intuition as schematic, *a priori*, as very near from imagination, as a kind of action, eventually
carrying some legality. Clearly Brouwers intuitionism, involving intuition of
what gets constructed as constructed, has to be referred to this Kantian
alternative concept of intuition.

But let us now consider another way of objecting: by insisting on the objective character of formulas and formal texts.

For these new opponents, the important fact about formal proofs is that they are laid down on the paper sheet, or blackboard or computer screen. Logic enfolds the laws of the being true, these laws have nothing subjective, and formalization is not doing anything else than exhibiting the objectivity of logic.

There is always a kind of wordplay in the international use – which is at the same time the international celebration – of the word objectivity. Semantically the word should depend on some notion of object, objectivity should be the character of what rests on the object or stems from the object, but this would imply that we have first to know enough about the object before understanding objectivity. Unfortunately, usually or very often this condition is not fulfilled, in such a way that objectivity only counts as the character of what is in no way personal or private. Maybe, even in these cases, there is an implicit reference to some figure of the object, but it would be the figure of the common sense medium size sensory object of ordinary spatial and temporal experience, only alluded as supporting the famous vivid sense of reality mentioned by Russell.

Well, if formal proofs are exhibiting logics objectivity, can it be because they are ordinary concrete objects? I think no one would seriously maintain such a statement.

It is, for sure, perfectly true that contemporary formalization raised proofs to the level of objects: now proofs are some particular case of mathematical object, motivating theories, discussions, internal categorization, and so on. I think it is important to insist on this historical point, connected with the one of textualization of logic (we already briefly mentioned it in the beginning of our discussion). Logic, as the most general science of truth and proof, was classically supposed to inhabit natural language and spontaneous reasoning. Logic was held to be a way or a form of thought, impossible to seize in external products of traces, and it was at the same time not considered as requiring some specific linguistic equipment. Nowadays, we think that logic is really logic only when it is formalized, which means that some special kind of language and some special concept of text have been designed in order to host logical activity. And the consequence of this new linguistic context of logic is that everything pertaining to logic may now be grasped under the figure of some object: formulas and proofs, to begin with, are defined as some particular kinds of objects, and logic is able, for example, to prove things about objects called proofs.

But very clearly, if such is the case, it
is only because proofs, terms or formulas are not *concrete* objects, are objects of a very peculiar form. These objects that
are conceived of as standing beyond the particular sequence of material signs
making them each time actual on some material substrate. The *modus ponens* implication [(P (PQ)]Q does not really locate in the little set of ink letting it appear
in the printing of the formula I just wrote let appear in order to evoke it,
but it stands as the unique type unifying the unlimited multiplicity of
analogous tokens.

If one accepts to reflect seriously on what characterizes the formal objects that are used to give to logical activity its public face, then one has to concede, at least it seems to me to be so, that the relevant feature is their constructive nature. Constructive objects are symbolic object, of the linguistic type, made of repeatable signs, and whose precise building obeys to rules, in such a way that a recursive definition is available for any kind of particular object (terms, formulas, proofs, and so on). One does not have to be a trained mathematician understanding what sets of set theory, or what toposes or schemes of Grothendieck are, in order to study logic, but one has to be able to play the game of constructive objects, and to understand proofs about such objects given by way of recursion on the building of the object.

Brouwer pointed this and argued that the mathematical level of construction, that he was highlighting, enjoyed some foundational privilege: both the formalist and the intuitionist mathematician have to be able to deal with objects of that level. For us, the important point is that such a foundational value is based on the non concrete character of formal (that is to say constructive) objects. What elicits formal object as the one on the basis of which we are going to build the whole castle of logic and mathematics is that they are at the same time mental, practical and symbolical objects. When some object of that type is disclosed on the paper sheet, you may come back from the written symbols to some sequence of mental acts as well as to some rule governed discourse. Constructive objects are as a matter of fact a kind of universal money enfolding some practical-symbolical meaning which we are able to actualize internally, in our thoughts, at least when it is simple enough. Certainly it is important that these objects are public and materially instantiated, but the objectivity they give to logic is the one of construction understood as this mixture of intuition, action and legality we were just describing.

Let us now consider the fourth and last objection.

There has arisen recently in our logical
and philosophical circles another way of insisting on the objectivity rather
than on the constructive-intuitive character of formal equipment. Some people
argue now that logic is basically about *processes*, and that formal logic is nothing but an attempt to represent and
study some special kind of processes: such a view seems, again, to deny the
intuitive relevance of construction. In a way, we could say that this objection
adds or mixes the two preceding ones: it says at the same time that
constructions are actions and empirical objects, insofar as *action* considered from a third person objectivist point of view becomes *process*.

This view, I think, takes its roots in the
history of logic. Around the thirties, computation was addressed as a new
logical or mathematical problem, and the modern theory of computability arose
in the works of Gdel, Turing and Church. The theoretical settings of recursive
functions, Turing machines and lambda-calculus were designed in order to
picture and anticipate in a formal way what a computation was when considered
at the highest level of generality. As it is well known, these theoretical
devices have been extensionally identified: the recursive functions are
provably the same as the Turing-computable or the lambda-definable functions.
But this way of identifying insists on the idea of some process
– arising in a kind of black box – and leading from some
input, taken out of some collection, to the computed output. Computation is
basically seen as a kind of process, and *computer science* would be the science of these kind of processes that do not follow
the laws of physical motion (always expressed in terms of mathematical
continuum, in the quantum case as well as in the relativist one even if,
eventually, less directly), but rather go through finite sequence of discrete
steps and deal with similar discrete items.

It has indeed to be acknowledged that from
the very beginning, computer science was associated in a very close and
intimate manner with logic, for a lot of reasons. The idea of elaborating the
modern concept of computation came from Hilberts *Entscheidungsproblem*, from the wish to learn whether the standard mathematical theories
were syntactically complete, and from the study of the question whether some
mechanistic device would be able to recognize any formula as a theorem if it is
one, as a non theorem if it is not one. Gdel proved his incompleteness theorem
using the trick of arithmetization of syntax, which was itself based, in his
approach, on the proof of representability of recursive function, witnessing
some deep convenience between computations and logic. To the gdelian moment,
we may also associate the general consideration that the giving of some formal
inference system could be equated with the giving of some Turing machine, the
theorems of the first one being identified with the successive outputs of the
second, if codes for the successive natural integers are offered to it.

The connection between computer science and
logic is nowadays so strong that quite an important number of the contributions
to logical science are published in computer science collections. Very clearly,
the Curry-Howard correspondence played a very important role in this story. Let
us recall that Howard, following Currys indications, established in his 1969
paper that proofs of Heytings logic could be perfectly translated into terms
of lambda-calculus or of typed lambda-calculus. In the second case, the fact
that some term *t* expresses or translates the
proof of the formula *A* is equivalent with the
fact that *A* tells the type of the term *t*. For us the important point is that *proof*, along these lines, is essentially considered as a kind of process
acting on premises. It may also be mirrored as *program*, the question of the type of the proof process coded as some
lambda-term being analogous to the question of the specification of the program
(what does this program do, how is it going to act on data?) So it has become
natural to see proofs as processes of a special kind, translatable as
lambda-terms.

But the resulting insight, as I have
announced, is that logic appears as nothing but discrete physics of
computational processes. And therefore, one is tempted to see logic as
objective again. The lesson of formalization would be that logic has been
recognized as concerned by some particular computational processes, which are *de
jure* perfectly objective, and which are even
nowadays objectively exhibited by computers behaviors. So apparently, the
intuitive side of proof and of logic is completely lost.

I may add some contextual and partly polemical remark: a classical analytical philosopher is more inclined to follow this perspective on logic and proof than the brouwerian one that I sustained implicitly some paragraphs before. She does so because such an attitude sounds more naturalistic, technical, scientifically objective. When such a philosopher hears that there is a way of looking at logic that makes it the general study of discrete processes, be it as supported by neurophysiology or as achieved by computers, she feels much more attracted than by the old song of psychologism and subjectivity, that she recognizes in the reference I made to intuition in the first part of my argument. For this reason, I believe, the Curry-Howard correspondence is commented with always increasing philosophical respect, while the so called BHK-explanation, justifying the rules of Heyting logic by clarifying the two related notions of proof and construction, was never considered in such an advantageous way.

But I come now to the point. For me, there are two difficulties in this new conception.

The first one could be called epistemological. The study of computational processes goes beyond logic and enters the field of what may more accurately be termed mathematics. This is because a recursive function, for example, is not a constructive object, but a rule for producing some output if some constructive object is given as an input. In this sense, any recursive function enfolds (a kind of) infinity. The Church thesis highlights the inter-translatability of the different theoretical definitions of computation (recursive functions, lambda-calculus or Turing machines for example), but they are identified at the extensional level, as far as they give rise to the same computable functions. And the concept of a function defined on whatever n-uple of integers is the concept of an infinite range of possible elementary processes and results. For sure, the class of recursive functions is defined in a recursive way, making it possible to grasp any particular one through its construction-tree, as built on the basis of the basic ones with the use of the allowed rules. But this is just a way of naming and knowing them, and it does not account for their behavioral meaning. Computable functions give an alternative to the idealistic development of set-theoretical entities, first of all to set-theoretical maps, conceived as triples of the form (domain, graph, codomain). So it is not sure, after all, that the reinterpretation of logic as the physics of discrete processes does justice to it. At least, if we commit to such an interpretation, we seem to forget the foundational aspect of logic, the fact that it has to speak and theorize before we enter the mathematical complexity of the object, which stems from the assumption of mappings, recursive ones or set-theoretical ones. This first argument or resistance in a way already expresses our desire to maintain the philosophical face of logic, seen here as its foundational intent, or as its character of not being already involved in mathematical development.

This brings me to the second difficulty,
which pertains to truth and language. Logic has always been considered as the
science of truth, and as a result of the Fregean revolution, at the turning
point of nineteenth and twentieth century, it was seen as bound by some
privileged bond to language. And in this conjuncture, the connection between
logic and legitimacy was not forgotten: the general idea was that, as in a way
originally embedded in language (as for example Quines book *Word and Object* so convincingly shows), logic had even more rights to be seen as
the key for every foundational work than it was previously. May be logic was
partly re-defined as the radical or general theory of language, but it did not
loose its epistemological and foundational value in that circumstance. On the
contrary, if we now turn to the definition of logic as physics of discrete
processes, then we make it, at least apparently, some empirical specification
of the encompassing realm of physics. The connection with the general problem
of truth and with the question of legitimacy would only remain as an old
memory, depending on our remembering that speech or writing processes are
examples of discrete processes, and that many speech acts bear some claim for
truth, or that every speech act raises, inside human community, the question of
its legitimacy.

This situation is entirely different of the one we enter if we accept, one century after, the teaching of Brouwer, which was, roughly speaking, that there is a deep connection with logic and intuition. Because intuition is well known as a central protagonist of the classical discussion about truth and legitimacy, at least for someone who considers the works of Descartes, Kant and Husserl, only to cite three major names. And as far as intuitionism shows us how intuition is involved in our grasping of basic linguistic structures, our reference to Brouwer helps us to save the deep Fregean conception of the privileged connection between logic and language, in the new scientific context underlining computations and processes.

We recommend therefore to consider proof as essentially organized as the construction of some special structure that gets at the same time intuited in its tree-structure, rather than as a process having to be understood in the context of infinite computational mappings. We suggest to understand that truth calls for such kind of proofs because proving is rooted in the recognition by language itself of its linguistic structure, and because, as Chomsky and Montague have both shown it from two different point of views, sentences are constructions in the sense of Brouwer.

To sum up, the Brouwerian conception of construction as intuition makes the link between contemporary computational theory and philosophical and epistemological concerns associating proof with language and truth.

I now turn to the second part of this paper, where I try to analyze contemporary developments in proof theory by going back to Kants fundamental insight about proof as mathematical.

As one knows, Kant makes a strong
distinction between philosophical and mathematical proofs. Philosophical proofs
are, in Kants words, purely discursive which means also that they are purely
logical proofs, and for that reason are unable to convey any information, they
cannot do better than to state the already given relations between concepts in
language, they cannot lead to anything but *analytical* truths (expressing how conclusions are included in premises). Kant
calls theses proofs acroamatic. They are also qualified as apodictic,
because what we assert under the authority of such a proof may be asserted
universally and unconditionally, with necessity. But it is at the same time
uninteresting, as far as it does not allow us to add to some concept
properties which were not known in advance to be part of that concept.

Mathematical proofs, on the contrary, are
for Kant apodictic *and* intuitive, and for that
reason, they allow synthetic statements. This peculiarity of mathematical
methodology is described by Kant in three ways:

1) Mathematics has a special way of
defining. When the mathematician defines some object, his saying counts as some
kind of prescription: what the object is, how and when it may be recognized, is
decided by the definition, which gives the law on that subject. Outside
mathematics, the *definiendum* is given prior to
the definition, and the definition as a matter of fact tries to enumerate the
conceptual features which characterize the given object (which is typically not
singular: it is a *species* named by a common
noun). This is especially the case of philosophy: Kant gives (in a footnote)
the example of the philosophical attempt to define *juridical law*, and claims that judges and lawyers are unable of it[7]; he clearly sees the
philosophical contribution to such a definition as some kind of interpretation,
where we confront at the level of meaning the by us discovered list of
conceptual features to the traditionally understood concept of juridical law,
and go on improving and correcting our list until we have the feeling of having
explicated the notion of *juridical law*.

2) Mathematics may refer to axioms, that is to say, statements enfolding some synthesis of concepts which appears as necessary in intuition.

3) But, finally, inferential moves in
mathematical proof are governed by *concepts construction* (and this explanation also concerns point 2)).

Let us say some words about concepts construction, which is going to be the key of the foregoing discussion. Kant claims that we have the ability of producing some singular referent for our mathematical concepts in the framework of pure intuition, and at the same time, not to deal with that singular as singular, but rather to take it as representative for the universal content of the concept. This singular will then cumulate two apparently contradictory advantages: it will stand in front of our thoughts glance, as some concrete singular would, and as such it will allow us to look at it and manipulate it, but at the same time every kind of behavior that is going to be ours, be it of description or of reasoning, will be only based on the illustrated concept and not on the peculiar features of the singular illustration, not even to speak of the material properties of the sensitive mark elected for representing that singular. And Kant argues that the whole process of such a generic illustration of mathematical concepts is by no way extraordinary or new, we may recognize in it common mathematical practice: to make an easy example, when we draw some triangle because we try to solve some problem about triangles, we are doing nothing else that constructing the concept of triangle.

So we can describe the way Kants sees the mathematical activity of proof roughly as follows: facing some specific problem, the mathematician constructs the relevant concepts in pure intuition (and she does so with the help of some sensitive drawings); more than this, she will generally add some constructions to the so realized configuration showing the involved concepts; but in the end, when she sees the answer to the question in the resulting picture, she is by definition able to formulate the connection with the concepts from which everything comes in a logical way, because everything that happens at the intuitive level may be re-assumed at the conceptual level; the intuitive items never cease to mean the generality of the concepts. We may therefore understand mathematical proof as obeying a kind of ternary rhythm: we begin at the conceptual level, we so to say dive into the sea of pure intuition, and from our swimming we come back to some neat logical formulation.

The usually asked question is whether such a description can survive the dawn of Euclidian geometrical intuition: the main example of Kant, the one of the proof that the sum of the triangles angles is equal to two right angles, seems to belong to some definitely obsolete mathematical framework. Still we have at least one cue, in Kants text, favoring the idea that his concept of concepts construction was going far more: he describes what he calls the algebraic method as another example of concepts construction. We may quote him:

Even the method of algebra with its equations, from which the correct answer, together with its proof, is deduced by reduction, is not indeed geometrical in nature, but is still constructive in a way characteristic of the science. The concepts attached to the symbols, especially concerning the relations of magnitudes, are presented in intuition; and this method,in addition to its heuristic advantages, secures all inferences against error by setting each one before our eyes [8]

I think this quotation indicates that Kant would have been ready to understand contemporary symbolic abilities in the light of concepts construction. The idea, expressed in this quotation, that handling with symbols yields truth and proof at the same time, and the complementary idea that the possibility of mistake is forbidden by the very fact that every relevant thing or act stands in front of the eyes both advocate it. For Kant, the important point in literal algebra as we practice it after Vite is that not only indeterminate concepts of quantities but also elementary acts of reasoning concerning such concepts are exhibited by the signs and moves on signs.

To sum up, Kant tries to understand the difference between logic and mathematics, which in this case and for him is the same that the difference between philosophy and mathematics: logic, like philosophy, has to drive reasoning without ever showing the object and the truth of the object; it proves so to say blindly, only using the rules of discourse and grammar. Mathematics, on the contrary, has the ability to show the object as some singular, nevertheless counting as generality of the presented concept. Mathematical proofs, for that reason, show the object as much as they prove the truth. Proof and evidence join themselves in mathematical proof, up to a certain point.

In what follows, I will argue that the requirement that evidence should be added to purely discursive proofs has not been forgotten. May be we can even say that this requirement has been extended to the technically logical part or aspect of proving: this is not so surprising, if one considers that the arousal of contemporary mathematical logic has come to blur the frontier between logic and mathematics (which does not mean that the philosophical task of formulating the distinction between them died or became impossible). But the situation changed substantially in following sense: while Kant believed that mathematics as such always granted proofs to provide evidence with them or even inside their spontaneous movement, we now see proof as first appearing at a non showing level, strictly logical, and having then to be complemented with some intuitive counterpart bringing the evidence. This complementation or addition I choose to call generally semantics of proofs, taking the expression from contemporary literature without trying to respect the meaning usually given to it[9].

I will now try to illustrate these ideas firstly with the so called BHK-explanation of the rules for intuitionist logic.

As it is well known, the three letters BHK stand for Brouwer, Heyting and Kolmogoroff[10]. This explanation, technically, is supposed to justify Heytings logic.

Brouwer did not believe in logic: he did not consider that some separate kind of knowledge could govern in a legitimate way mathematics. The kind of certainty that mathematics enfolds, for Brouwer, is the only and the ultimate one: it cannot be submitted to another part of rationality. This also means that logic, as far as we may define it, is not technically protected from mathematics: Brouwer also asked for mathematics the right to use tools or modes of reasoning having first appeared in the realm of logic. Nevertheless, he defined principles that should be followed at least as long as one wishes to gain real truths, that is to say constructive truths: so he institutionalized some kind of truth. But when there is a kind of truth, there must be a kind of logic, if logic is the set of rules that allow us to infer true statements on the basis of true statements. So there must be an intuitionist logic attached to the search for intuitionist truths as well as there is a classical logic attached to the search for classical truths. This logic Heyting claimed to have made explicit, giving us his well known deductive system (in the Hilbert-Ackermann way, if Im correct[11]).

But one cannot completely forget about the difference of Brouwers conception of logic. We may formulate this difference in another language by simply saying that Brouwer conceived of mathematical proof as not purely discursive: he regarded proofs as having to be self justifying in the sense that they were supposed to show the object while deducing truth about it. So we may be recognize that Brouwer more or less shared Kantian view on proof.

In a way, BHK-explanation makes the link
between Heytings logic as a formal device, and Brouwerian deep views about
proof. As far as intuitive grounding of truth, for an intuitionist, is well
known to be *construction*, BHK-explanation cannot
do such job without connecting proof with construction. As Troelstra makes it
clear in her comments, the BHK-explanation indeed takes proof and construction
as primitive un-definable notions, which nevertheless get clarified in their
relation by the BHK-explanation[12]. And such a clarification is brought by simply making explicit
under which conditions a complex sentence may be considered as proved, in
reference to its simpler constituent. Thus BHK-explanation, let us recall it,
goes like following:

1) We have a proof of *A**B* when we have a proof of *A* and a
proof of *B*.

2) We have a proof of *A**B* when we have the choice of 0 or 1, and a proof of *A* in case 0 was chosen, a proof of *B*
in case 1 was chosen.

3) We have a proof of *A**B* when we have a construction which, given a proof *p* of *A*, builds out of *p* a proof of *B*.

4) We have a proof of $*x* *A(x)* when we have an explicit object
*n*, and a proof of *A(n)*.

5) We have a proof of "*x* *A(x)* when we have a construction
which, given an object *n*, builds a proof of *A(n)*.

In each of the fifth cases, the rule tells how to construct the certainty of the complex statement. So, if constructive certainty is available for the component statements, it will transfer to the complex statement. And for that reason it seems that a logic fitting with the BHK-explanation will never lead us to assert anything without being able to present some complex construction justifying our claim: we only have to ground the tree of our justification on the individual constructions underlying every atomic statement, and then build the global justifying construction by obeying BHK-explanation; if the proof-system fits to BHK-explanation, the construction indicated by BHK-explanation adds the evidence to the proof, either by showing the justification-process of the statement if it is logically valid, or by offering this process as something which has to operate on constructions yielding evidence for elementary statements in order to achieve evidence for the complex proved statement, in case the latter is not universally valid. Ultimately, the notion of proof and of construction may come to coincide if atomic statement can be constructively justified.

So BHK really seems to explain what a proof
is, how a proof meets Kantian standards. We should add, here, that in a Brouwerian
perspective, it is not only the proof that P and the construction of P as true
that can be brought to coincidence, but as well the mental consideration of P,
the internal action that P, and in a way the declaration that P: for Brouwer,
if I understand his philosophy correctly, all that is P *as construction*. Brouwers philosophy, for that reason, goes beyond the semantic
contribution of BHK-explanation, adding evidence to technical Heytings proof
while justifying its rules. One way of summarizing this deep view of Brouwer is
to say that he was trying to describe in a holistic way mathematics, arithmetic
and logic as being more or less the same – the science of
constructive truth – this unified discipline being governed by a Kantian-like
proof-regime.

The second historical step in this contemporary exploration of the semantics of proof is the step of realization.

Another attempt to define some semantics
of proofs, I believe, is *realization*, which was
initiated by Kleene. The original idea was that we may associate to any
intuitionist arithmetical formula – when it is true –
some integer number *n* which realizes the formula
in the sense that it encapsulates and recalls the process of its constructive
justification. The technical definition of *n*
realizes *A* [notation *n* **r** *A*],
for that reason, goes as follows:

(i) If *A* is
of the form *t**1**=t**2* and is
true (and therefore provable in HA) then any integer number realizes *A*.

(ii) If *A*
if of the form *B**C*, then *n* **r** *A*
if *n* codes the ordered pair (*j**1**(n), j**2**(n)*), and on one hand* j**1**(n)*** r** *B*,
on the other hand* j**2**(n)*** r** *C*.

(iii) If *A*
is of the form *B**C*, then *n* **r** *A*
if *n* codes the ordered pair (*j**1**(n), j**2**(n)*), and *j**2**(n)***r** *B* in
case* j**1**(n)*=0,** ***j**2**(n)***r** C** **in the alternative case.

(iv) If *A* is
of the form *B**C*, then *n* **r** *A* means
that for all integer *y* , if *y* **r** *B*
then *{x}(y)* exists and *{x}(y)* **r** C.

(v) If *A* is
of the form $*x B*, then *n* **r** *A*
if *n* codes the ordered pair (*j**1**(n), j**2**(n)*) and *j**2**(n)*** r** *B(j**1**(n))*.

(vi) If *A* is
of the form "*x B*, then *x* **r** *A*
means that for all integer *y*, *{x}(y)* exists and *{x}(y)* **r** *B*.

It is not difficult to see what this
definition takes up from BHK-explanation. Troelstra comments that ()
realizability is similar in spirit to (may be viewed as a variant of) the
BHK-explanation [13]. As a matter of fact, realizability interprets the construction
justifying *A* as an integer, and puts the
condition on some integer *n* to count as
constructive justification for *A*. For an atomic
basic formula of the type *t**1**=t**2*, nothing is asked from *n*, any
integer does the job: this means that the formula is taken as bearing in itself
already the justification that it deserves. In other cases an integer which
realizes *A* exhibits the further constructive
justification incorporated in a supposed proof of *A* in HA, insofar as it may be meta-mathematically proved that a
formula *A* is provable in HA exactly when it is
realizable. We may think that such an integer shows how to go from the basic
evidences (of formulae of the type 7+5=12) to the evidence of the complex
formula. The difference between realizability and BHK-explanation is that the
word construction is in some cases translated by the reference to some
recursive action: to the action of the recursive function coded by some
integer number on another integer number.

The semantic of proofs, in that case, is
addressed to proofs in HA. Some integer realizing *A* adds to such a proof the constructive evidence of how its truth
eventually comes from the truth of elementary finitary statements. For such
statements, the evidence would have to be conceived of as already given by the
statements, or incorporated in them.

So we meet again the problem of obtaining an integral semantic of proofs, picturing not only the way evidence gets transmitted by the logical operations involved in (the assertion) of the complex statement, but also the evidence incorporated in its elementary components.

But let us now come to the third step of this contemporary theoretical exploration of the semantics for proofs: Curry-Howards correspondence.

Let us recall first what Curry-Howards correspondence is. We may add to lambda-calculus the concept of type: we define types for terms and rules for assigning to each term its type. There are basic types (let us note them A, B, etc.), and we may form complex types with rules of following kind:

i) If *A* and *B* are types, so is *A**B*;

ii) If *A* and
*B* are types, so is *A**B*.

Type assignment to terms is supposed to
work in such a way that when *s* is of type *A**B* and *t* of type *A*, *st* is of type *B*; and when *s* is of type *B* and *x*, appearing free in *s*, is of type *A*, then the
lambda-abstraction (l*x*.*s*)
is of type *A**B*. These requirements simply express
that we understand lambda-calculus in a functional way, to the effect that the
product *st* means for us applying *s* to *t* and that we understand (l*x*.*s*) as the function assigning *s* to *x*. These rules also mean that the
assignment of some type to a term is supposed to reflect the complex functional
structure of the term: what kind of action the term may exert on terms given to
it as functional food.

In order to collaborate with the idea of
the Cartesian product type *A**B*, we
must suppose that some constants are at disposal in our lambda-calculus: let us
say that from the terms *s* and *t* we may form the term *s*,*t*, and from any
term *s* we may form the terms p1(*s*) and p2(*s*). And we add the straightforward reduction rules p1(*s*,*t*)*s* and p2(*s*,*t*)*t *to the general logic of the
reduction of terms.

We then define a way to assign some term of
the typed lambda-calculus to every proof in the intuitionist natural deduction
system. The deep insight is the formulae as types conception: we decide to
philosophically equate the formula with the class of its proofs, the class of
items through which the formula holds. If we are doing so, then the formula
becomes also describable as the *type* of its
proofs: it is what its proof share, have in common. When we are carrying some
natural deduction, some formulas are used as premises: they intervene without
any known justification. We may translate this by saying that they are
supported by a completely undetermined proof, from which we only know that it
is a proof of the concerned formula: in the new language, that it gets typed by
it. We then introduce the idea that at each step of the natural deduction
proof, any formula appearing at some node of the proof-tree will be accompanied
by some term, which will express how this formula has been derived following
the rules, in general from some invoked premises. We write now *t*:A, *t* being a term of our lambda-calculus,
and *A* being seen both as a type and as a formula
(because of our *formulae as types* philosophy),
intending to express at the same time that the type *A* may be assigned to *t* and that *t *incorporates the structure of a proof of *A*. Our rules entail that the two assertions say the same. We list
them here (the reader will remark that the rules refer to other complex types
formation schemes than the two ones we gave: our exposition does not claim to
be technically complete; a satisfactory account may be found for example in *Basic
Proof Theory*[14])

(i) If *s:A*
and *t:A*, then *s*,*t**:A**B*.

(ii) If *t:A**B*, then *p**1**(t):A*.

(iii) If *t:A**B*, then *p**2**(t):B*.

(iv) If *s:A**B* and *t:A*, then *st:B*.

(v) If *t:B*
is obtained after some path initiating with some premise introduction *x:A*, then *(**l**x.t):A**B*.

(vi) If *t:A(x)*, then *(**l**x.t):**"**xA(x)*.

(vii) If *s: **"**xA(x)*, then *st:A(t)*.

Rules (i), (ii), (iii) correspond to introduction and elimination rules for . Rules (iv) and (v) correspond to introduction and elimination rules for . Rules (vi) and (vii) correspond to introduction and elimination rules for ".

These rules, on one side, globally entail
that the term *t* such that *t:B* keeps the memory of how the proof of *B* goes from some premises which are represented by the free variables
appearing in *t* to *B*. So this term may be considered as a kind a code for the proof,
reflecting the integrality of its structure. On the other side, each rule may
also be read as expressing the assignment of its type to the term written on
the left of the symbol :. If indeed the type assignments given after the If
of the rule are valid, then the new type assignment given after the then of
the rule is also valid. As far as, at the beginning, the assignment of the type
of the variables associated with the premises are by definition correct, in the
name of the formulae as types interpretation, we may be recursively sure on
the whole that when *t* represents the proof of A,
A is the correct type for *t*.

But what does the Curry-Howards correspondence teach about what we called semantics of proofs?

First, this correspondence is, again, very
close to the BHK-explanation. We could paraphrase our rules in terms of the
BHK-explanation: for example, a proof of *A**B* has a code which is the term-conjunction of codes of *A* and *B*, and rules (iv) and (v) both
say that a proof of *A**B* is some function assigning a proof
of *B* to any supposed given proof of *A*. In general, Curry-Howards correspondence (CHC) seems to say in
two goes what BHK-explanation says in one.

Second, may we estimate that the term *t* associated with the proof of *B* shows
the evidence conveyed by this proof? That it brings some kind of intuition of
what *B* shows as its object? We have to answer in
a prudent way. A lambda-term makes some computation explicit, the language of
lambda-calculus is one of the available theoretical settings expressing the
general power of computation, as it is well known. So what the correspondence
associates to the proof is some computation. Let us take some very easy
example: *(A**(A**B))**B* is, for sure, a theorem of the
logical calculus for which CHC is defined. What kind of term gets associated to
this theorem? Let us apply the rules:

(1) If *x: A**(A**B)*, then *p**1**(x):A*.

(2) If *x: A**(A**B)*, then *p**2**(x):A**B*.

(3) If *p**1**(x):A* and *p**2**(x):A**B*, then *p**2**(x)** p**1**(x):B*

(4) Therefore *(**l**x.** p**2**(x)** p**1**(x)):
(A**(A**B))**B*.

We see that the term *(**l**x.** p**2**(x)** p**1**(x))* expresses the computation which produces a proof of *B* given a proof of *A**(A**B)*. So CHC identifies the construction which BHK-explanation
requires for having a proof of the implication which *(A**(A**B))**B* is. In our comment of BHK-explanation and of realizability, we
already stressed the problem of the heterogeneous character of evidence
underlying the elementary mathematical statements, in case what we prove is not
a logically universally valid formula: there has to be some basic evidence in
favor of the truth of these statements (like the *t**1**=t**2* in the context of Heytings arithmetic),
which Brouwer would identify as given by the construction of the mathematical
content of the formula; and there is on the other side the constructive path
of the tree-structure of the proof, which is already construed as some
computation in realizability (some recursive function encoded by some integer
number), and which is now again interpreted in such a computational way, the
computational content being this time encoded by some lambda-term rather.

So, on the whole, this work on the semantics of proofs discovers systematically computation as the evidence incorporated by proofs: when we deduce, we write the successive sentences of the proof as if we computed them from the preceding ones. To prove some formula is to exhibit the computation required by the morphology of the formula, and the evidence associated with the proof is the explicit encoding of this computation, as the proof elaborated it. What was anticipated in BHK-explanation under the name of construction seems to have been scientifically identified as computation, itself expressed by one of the contemporary available theoretical frameworks (recursive functions, lambda-calculus).

But if the proof is not a purely logical one, we still have the problem of the basic truths, whose evidence would have to be described in a different way, unless we suppose it to be encapsulated in the formulas telling the truths.

From our point of view, the real question
is that of the showing character of these semantics of proofs: do they add
something which leads to some kind of (unempirical, generalized) seeing, do
they bring some intuition, or do they only meet the computational as objective
processing, as we were discussing the point earlier in this paper? And the
question is now naturally two-folded: 1) may the CHC identification of the
computation underlying some logical validity be counted as providing
intuition? ; 2) can we and should we understand the certainty of
elementary arithmetic statements of the form *t**1**=t**2* in an intuitive way, or more precisely how can we see in that case
evidence as being added to the proof by some semantics of proof?

I will briefly try to answer these two questions, in two very different ways.

Dealing first with the second one, I will go back to the debate between Hegel and Kant, which appears, when we read it nowadays, as surprisingly modern.

The point is that the arithmetical judgment 7+5=12 is evaluated by Hegel as analytic, while Kant was citing it as an example of synthetic judgment. The case is interesting, if one remembers at the same time that Kantian evaluation of that judgment has been universally rejected by post-Kantian epistemology, mainly by the analytical one, but also by the neo-Kantian one.

Let us recall Kants analysis of the judgment: for him, the subject 7+5 is predicated in it from the property of being 12. But there is nothing in the concept of the subject, in the concept of the addition of 7 and of 5, that would enfold the being 12. If we want to be convinced of the truth of the judgment, we have to construct both concepts, and to intuitively state identity of our constructions, which entails intensional equality at the level of concepts, because of the generic value of concepts construction. Therefore the judgment is synthetic.

Post-Kantian epistemology, be it analytical or neo-Kantian again, objects that 7+5=12 is a purely logical consequence of the axioms of Peano arithmetic. For analytical original epistemology, this shows that 7+5=12 is to be seen as a logical truth – or at least PA½¾ 7+5=12 is – but to be honest, this logicist epistemology of mathematics assumes the more general claim that every part of mathematical knowledge is logical. For neo-Kantian epistemology, the possibility of logically deriving 7+5=12 proves that the supposed pure intuition of time is nothing else that disguised laws of understanding, the Kantian word for the agency of logic: there never was something like pure intuition of time, human reason never faces without any mediation its object and the truth about it, the object is always produced and determined at the same time by reason and its fundamentally logical path (even if the figure of logic, for neo-Kantianism, is not the Frege-Russells one, but rather some dynamical figure inspired by Hegel).

We should first point that the classical
objection has no strength for constructivist-minded contemporary epistemology.
To be sure, 7+5=12 may be proved inside PA, but the proof, applying as many
times as necessary the axiom *x*+*Sy*=*S*(*x*+*y*), and leading progressively from the writing of the proper name 7+5
to the writing of 12, is nothing else that what Kant called concepts
construction. *SSSSS*0, *SSSSSSS*0 and *SSSSSSSSSSSS*0 may perfectly
well be considered as the constructions of the concept 5, 7 and 12 in the
Kantian sense, insofar as they project and realize these concepts in some
unilinear discrete symbolic space, some version of the relevant pure intuition
of time. And the proof actually transforms in this space *SSSSS*0+*SSSSSSS*0 into *SSSSSSSSSSSS*0, which is properly the intuitive showing Kant had in mind.

But let us forget of that discussion and come back to Hegels point of view. It is well expressed in following quotations:

The 12
is therefore a result of 5 and 7 and of an operation which is already posited
and in its nature is an act completely external and devoid of any thought, so
that it can be performed even by a machine. Here there is not the slightest
trace of a transition to an *other; *it is
a mere continuation, that is, *repetition, *of the same operation that produced 5 and 7 [15].

If the problem is to add several numbers, then the solution is to add them; the proof shows that the solution is correct because the problem was to add, and addition has been carried out [16].

Hegel argues in two ways that the judgment is analytical: first, the judgment is not moving from the same to the other, to see 5+7 as 12 is to see 5 and 7 again as they arose; and secondly, the content of the judgment is only that the rule of addition was correctly followed when we passed from 7+5 to 12.

In a way, with these two remarks Hegel interprets correctly 7+5=12 as some finitary constructive truth, to speak with contemporary words. On one hand, the being 12 of 7+5 cannot be separated of the constructive definition of 5 and 7; on the other hand, the statement only expresses the legality of addition, which Peanos axioms enfold, but which may also be stated at the algorithmic level.

So we understand that Hegels disagreement with Kant rests on his computational approach of elementary arithmetic truths: they arise as results of algorithmic processes and do not refer to some special kind (pure) of intuition. Their debate merge with the contemporary issue that we just addressed in our description of technical proposals for semantics of proofs. And this debate, also, reactivates the discussion of our section Construction is process, not intuition . If one is committed to the computational interpretation of the semantic of proofs, then one thinks that algorithm as an objective process if what lies behind elementary statements as well as behind proof structure.

So what we really have to face again is a computationalist answer to both previously raised questions: yes, CHC gives the semantic for proofs because the operative content of proofs counts as evidence for them, and this semantics agrees with the nature of elementary arithmetical statements, which is also computational. As we already said, what was imprecisely alluded to as construction in the first step is now more scientifically apprehended as computation, be it coded as recursive function or as lambda-term. And no talk about intuition would be relevant.

As I have argued in the earlier section
concerning this computational approach of construction, it cannot account for
the foundational value of construction, and therefore, it does not teach us the
true status of formal proof. We may, for sure, consider the evidence for 7+5=12
as given by the particular application of the addition-algorithm, be it
supposed to be performed by the formal proof itself or outside of any
formalism. But this evidence counts as evidence only insofar as the sequence of
steps gets gathered as sequence of our acts or gestures, insofar as we envision
what we are doing while doing it, insofar as we accomplish some intuition with
and in our computation. The original idea of Brouwer was to name *constructions* these particular sequence of acts which, far from counting as
impersonal or mechanical steps, at the same time result in intuition, offer
intuitive content. Only in that guise can computation count as evidence. If and
when computation does not mean construction, it is the name of an universal
possible process and has no foundational value, it becomes more something like
a counterpart, in the constructive realm, of Cantorian mappings.

We may add that we ultimately need to have some overview of our computer programs texts, or of their anticipated working path, or of the correctness of some specification checker, in order to be confident in what our computers compute, and in the fact that they compute it well. At some level the constructive gestures have to be under the responsibility of some agent for whom they are at the same time laid down as intuition, if we want the whole system to enjoy rational approval from the part of scientific mind, to motivate confidence.

For that reason, we maintain that what we described as semantic of proofs has to be understood as offering technical tools for acting and enjoying the evidence which, added to the proof, makes it a completed mathematical proof in Kants sense. These tools are first generally referred to as constructions, then identified as recursive actions coded by some integer, then as term-reduction acts indicated by lambda-terms.

May be this final discussion will be happily illustrated by some example taken from recent research.

CHC-correspondence, as one knows, has been recently extended to classical logic. Following the line of thought suggested by Felleisen and Griffin, Michel Parigot designed in his 1992 paper[17] an extended calculus, the lambda-mu-calculus, which allows a new version of Curry-Howard correspondence, also working for classical logic. Since then, J.-L. Krivine has proposed an alternative way of presenting this new correspondence, in the language of realization. What he proposes is a theory of assertions of the form t realizes X, where t is a term of the lambda-mu calculus, and X a formula (of first order logic in one of his papers, of ZF in another one[18]). And we have for these assertions the properties that one hopes for any notion of realization (in short: theorems are realizable, and what is realizable is a theorem).

So this addition to traditional CH makes it possible to bestow some computational content to typically classical logical entailments. For example, it says which computation corresponds with the (proof of) the theorem XX in natural classical deduction. I must confess that until now, I dont fully understand and master, at least as I would like to do it, at the philosophical as well as at the technical level, this new strata of the correspondence. But it seems to me that the problem of this extension is that the computational counterpart of typically classical moves never becomes really intuitive, we dont understand it as mirroring the logical inferences, as some superimposed part of process leading to constructive results available for contemplation that would offer evidence for the classical proofs. I know very well that I might be wrong on that point, simply on the ground of my to narrow penetration of the new theories. But standing at the comprehension stage which is actually mine, I feel that this lack of intuitive content of the counterparts provided by extended CHC reflects the non-constructive character of classical logic, expresses the fact that CHC, applied to classical logic, does not add the evidence to the proof in the same way.

As I said from the very beginning, the aim of this paper was to advocate the idea that insights taken from the source of classical German philosophy could be helpful for one who wishes to write some really instructive philosophy of logic, trying to accompany contemporary developments but not submitted in advance to logic as always providing the only clear criterion and decision for everything. For one who things that philosophy of logic is not logic of logic, who believes that logic, like mathematics, calls for some really philosophical estimate.

If I am right, the price we have to pay for
that is to reconsider the quasi-political exclusion of continental tradition
which happened in the context of analytical philosophy in the beginning of the
20^{th} century, to be ready to examine its texts and thoughts without
evaluating them *a priori* as obsolete. May
international epistemology afford this price?

[1]. Which takes
place in the part called *Project* of his famous
book *Fact, Fiction, Forecast*.

[2]. It was in the context of the first big conference of the Vienna Circle in Paris.

[3]. Or may be, it coincides with that concept : any constructive class may be seen as the class of theorems derived for a corresponding inference system.

[4]. Cf. *Contradiction*, Dordrecht, Martinus Nijhoff Publishers, 1987,
Chapitre 3.

[5]. Cf. Incompleteness
and Inconsistency , *Mind*,
Vol. 111. 444 . Octobre 2002, 817-832.

[6]. II, 828-829.

[7]. Cf. *Critique of pure reason* A 730-731, B 758-759.

[8]. A734, B762.

[9]. I have at
least met the expression in Girards *Proof Theory and Logical Complexity* (Napoli, 1987, Bibliopolis, 87). Girard uses semantics of proofs
in order to qualify Heytings definition of an arithmetica proof along the
lines of BHK-explanation, and while stating that it appears as ()
closely connected with questions of normalization in natural deduction .
I also read it in Constables chapter Types in Logic, Mathematics and
Programming in the *Handbook of Proof Theory* (Elsevier, 1998, 683-786), namely p. 692.

[10]. Sometimes, Kreisel is also used to make the K speak.

[11]. Cf. Heyting, *Intuitionism, and
introduction*, 105-109.

[12]. Cf. Troelstra,A.,
Constructive Mathematics , in *Handbook of mathematical logic*, Elsevier, 1977, p. 978 :

This interpretation of the
logical constants presents a first example of the introduction of *abstract* concepts in constructive mathematics (proof,
construction) ; and it is our understanding of these concepts
(reflection on them) which enables us to see that the laws of intuitionistic
predicate logic are valid on that interpretation (whatever the *exact* extension of the concepts of proof and construction is, the
explanation is sufficiently clear fort this) .

[13]. *Loc. cit*., 988.

[14]. Cf. Troelstra, A. &
Schwichtenberg, H., 1996, 2000, *Basic Proof Theory*, Cambridge, Cambridge University Press, chapt. 1 and
2.

[15]. Cf. Hegel,
G.-W.-F., *Science of Logic, The Doctrine of the Notion,* 1715, [322].

[16]. Cf. *Ibid*., 1717, [323].

[17]. Cf. Parigot, M., 1992, lm-calculus : an Algorithmic Interpretation of Classical Natural Deduction , in Proceedings of International Conference on Logic Programming and Automated Deduction, volume 624 of Lecture Notes in Computer Science, Springer, 190-201.

[18]. Cf. Krivine, J.-L., Type lambda-calculus in Classical Zermelo-Fraenkel Set Theory , available on the Internet.