\subsection{Classical Negation}

It is a basic fact of classical propositional logic that connectives
are inter-definable; more precisely, given a sufficiently expressive
set of operators, the latter provide by definition the missing ones;
this is an immediate consequence of their truth-value semantics.  It
is therefore customary and economically convenient to assume as
primitive only this basis and define the others operators in terms of
the former.  In almost every definition negation is taken as
primitive, paired either with conjunction, disjunction or implication;
even those more succinct presentations based on a singleton connective
as {\em nand} retain an implicit flavor of negation.
% The same remark applies 
% to a notion of negation defined via a propositional constant for 
% falsehood. This provably goes back to Kolmogorov and it is 
% motivated by what Girard \ref{Gir91} likes to call the Heyting 
% semantics.  

There is yet another way to address negation which is peculiar to 
classical negation and is related to the transformational approach we 
are interested in.  This is known as {\em negation normal form} and it 
is used for example in Tait's concise proof of cut-elimination for 
classical logic.  For every atomic predicate symbol $p$ we 
also have a symbol denoting the opposite, say $\ol{p}$.  Then, with 
the essential usage of double negation elimination and De Morgan' s 
laws, negation is \emph{defined} as follows:

\[
\neg p =_{def} \ol{p} \quad\quad \neg \ol{p} =_{def} p \quad\quad 
\neg \neg p =_{def} p \]
\[
\neg (A \And B) =_{def} \neg A \Or \neg B \quad\quad \neg (A \Or B) 
=_{def} \neg 
A \And \neg B
\]

Thus, as far as the classical propositional structure is concerned, 
negation can be achieved by renaming. Consistency is then achieved by 
adding axioms that specifies that is it inconsistent to hold both $p$ 
and $\ol{p}$, namely $p \Bimp \neg \ol{p}$ an  $\neg p \Bimp  \ol{p}$.
Of course, this does not carry immediately over to computational
logic.

\smallskip
For accident or necessity (though now we lean for the former)
Horn logic imposed itself as {\em the} format in logic programming.
Though it truns out to be Turing-complete and therefore as expressive
as any other programming language, its lack of an explicit negation operator has been hailed
as a major drawback.
Rather than extending the syntax in an ad hoc way or introducing
dubious operators as \NF
a  possibility to be attempted is to
investigate how far we can go by renaming to Horn format. 
The limits of this approach are investigated in Chapter \ref{ch:hornelim}.

Informally, the reasons why this is feasible is that classical and 
intuitionistic logic coincide as far as the Horn format is concerned. 
%Several straightforward proof-theoretical arguments are known 
%\cite{??}.
 This entails that classical equivalences  
preserve the intended operational semantic of the source program. Once
we go beyond Horn logic the intuitionistic (or `search-like')
interpretation becomes crucial to ensure the existence of what is
commonly agreed as a reasonable interpreter for a \lp language.
Our endavour can be paraphrased as the search for a notion of negation
normal form for a significantly fragment of (\ho) intuitionistic logic
which is compatible with a \lp interpretation.

It must be remarked that the issue of negation and constructivism has
been considered by many problematic. The key point lies in the Heyting
semantics of $\neg A$ seen as a short ... of $A\Imp\bot$; many have
expressed doubts to the epistemological status of a construction which
yields the absurdum. A discussion can be found in Wansig's monograph
\cite{Wansig93}. Already in its textbook \cite{Heyting56} cites Griss'
negation-less mathematics. The most well-known approach is Nelson's
\emph{strong negation}:
\begin{metanote}
Insert some from sn.tex
\end{metanote}
\medskip

As we will  argue in Chapter \ref{ch:lfelim}, the interaction between
strong negation and implication is  inadequate to support the
operational interpretation on uniform proofs.

%%%%%%
\subsection{Failure (in a Logical Framework)}

Discussion on whether complementation is to be performed only on 
decision procedures or also on possibly non-terminating programs, 
r.e. predicates (like demo). What is the failure set of demo? 

Let us mention here the basic issue of \emph{proof-terms}:
s8such a framework must deliver evidence of what a proof is of a
certain judgment. The most popular way, since the Automath project
\cite{DeBruijn80} is to to see derivations as lambda terms inhabiting
theorems seen as types. It is not clear how to represent, in a
faithful fashion how to associate a proof-terms to a `derivation' by
negation-as-failure. This is not a mere notational problem.
























