=Paper=
{{Paper
|id=None
|storemode=property
|title=Explicit Constructive Logic ECL: a New Representation of Construction and Selection of Logical Information by an Epistemic Agent
|pdfUrl=https://ceur-ws.org/Vol-1068/paper-l10.pdf
|volume=Vol-1068
|dblpUrl=https://dblp.org/rec/conf/cilc/GentiliniM13
}}
==Explicit Constructive Logic ECL: a New Representation of Construction and Selection of Logical Information by an Epistemic Agent==
https://ceur-ws.org/Vol-1068/paper-l10.pdf
Explicit Constructive Logic ECL: a New
Representation of Construction and Selection of
Logical Information by an Epistemic Agent
Paolo Gentilini1 and Maurizio Martelli2
1
DIMA, University of Genoa , Via Dodecaneso 35, 16146 Genova, and
IMATI-CNR, via de Marini 6, 16149 Genova, Italy
2
DIBRIS, University of Genoa, Via Dodecaneso 35, 16146 Genova, Italy
Abstract. One of the seminal goals of Explicit Constructive Logic (ECL)
is to provide a constructive formulation of full higher order logic (Clas-
sical Type Theory LKω ) that can be seen as a foundation for knowledge
representation. Moreover, the development of this work has produced
the basis of a new approach to constructivism in Logic.ECL is intro-
duced as a sub-system Zω of LKω . Also the first order case Z1 and
the propositional case ZP of ECL are examined. A comparison between
ECL’s constructivism and the corresponding features of Intuitionistic
Logic, and Constructive Paraconsistent Logic is proposed.
Keywords: Constructivism in Logic, Higher Order Logic, Intuitionistic
and Constructive Paraconsistent Logic
1 Introduction
Full higher order logic can be an extremely powerful tool for knowledge represen-
tation if some of its features could be simplified and controlled. A constructive
formulation of it is the goal of Explicit Constructive Logic (ECL) and will be
presented in this paper. We will start from the sequent version LKω of Classical
Type Theory as presented in [7] where the Church formalism is used and logical
connectives are expressed as typed formulas.For the extensive definitions of the
syntax of typed language and the basic notions of proof-theory (sequents, rules,
proof-trees and so on) see [7] Sections 2 and 3. To realize the foundational prin-
ciples of the ECL inference we will define the systems Zω and Z∗ω ,(included in
LKω ), that, even maintaining a very high expressive power, show strong con-
structivity properties and could admit a new organization of proofs (through
a Normal Form Theorem). Zω could be also seen as a generalization, at the
theoretical level, of the features of Higher Order Uniform Logic, introduced in
[8] to express Higher Order Logic Programming. Indeed, in both cases the very
specific behaviour of proofs is that the principal formula in the conclusion of a
logical rule can be deduced only if some constraints on the introductions of the
auxiliary formulas in the rule premise(s) are respected. We will also examine
the first order case Z1 and the propositional case ZP of ECL. The real novelty
148 Paolo Gentilini and Maurizio Martelli
of any proposed new logical framework must arise clearly at the propositional
level, and this is the case for Intuitionistic Logic and Paraconsistent Logic. The
Church formalism is maintained also for the first order case and the proposi-
tional case, since it is very convenient for a deep analysis of logical connectives.
A parallel and a comparison between ECL and Intuitionistic Logic and Para-
consistent Logic as different kinds of constructive logics will be often proposed
in this paper. The constructivity of Intuitionistic Logic [10] doesn’t need expla-
nations. As to the constructivity of Paraconsistent Logic we consider only a well
delimited area of paraconsistency, given by the Logics of Formal Inconsistency
(LFI) and the included C-system family, introduced in [2]. The formal notion
of constructive paraconsistent logic is introduced in [6].
2 Explicit Logical Constructivism: Syntactic Environment
and Epistemological Basis
We will now give a short synthesis of the epistemological basis of Explicit Con-
structive Logic: the style will be heuristic and intuitive.
We will use the logical connectives à la Church [3]:
¬o→o , ∧o→(o→o) , ∨o→(o→o) , ⊃o→(o→o) , ∀(α→o)→o , ∃(α→o)→o , ⊥o , >o
where the type subscript is in general omitted in writing formulas. We call
judgments of the epistemic subject the compound logical formulas: we want to
convey the idea that logical information is provided by compound propositions
and is introduced by the subject starting from elementary data, expressed by
atomic formulas. The elementary data reflect the elementary facts that take
place inside a fixed empirical world that is assumed as reference for construct-
ing knowledge. The difference in the logical and epistemic role between atomic
formulas and compound formulas is so relevant, that we introduce for it specific
meta-symbols: thus, latin capital letters A, B, C, ... will indicate arbitrary for-
mulas, whereas latin capital letters with the + superscript A+ , B + , C + , ... will
indicate arbitrary atomic formulas. We recall that logical connectives are not
atomic formulas. A formula is atomic if the outermost symbol is not a logical
connective. A formula is an atom if it has not proper Church sub-term. In partic-
ular, the o-typed logical connectives, i.e. the logical constants ⊥o , >o are atoms
but not atomic formulas. The first expresses the judgement which is always ac-
ceptable (for which no criticism is possible) so that the sequent ` > is always
provable; the latter expresses the judgement which is always refutable (for which
no corroboration is possible) so that the sequent ⊥ ` is always provable. (see also
[7], Sec. 2 and 3). A further technical remark is that in this paper we will always
use the sequent version of the considered logical systems. Other foundational
assumptions are the following. In the demonstration (argumentation) produced
by the epistemic subject, judgments are not received from the external world :
they must be explicitly constructed alongside the demonstration itself. Only ele-
mentary data are necessarily provided by the external world. Therefore, logical
Explicit Constructive Logic ECL 149
information has to be always reconstructed by the epistemic subject and never
merely acquired; differently, elementary data are merely acquired. Simmetrically,
judgements, alongside a demonstration, cannot be eliminated without an explicit
logical motivation: this must have the form of another explicit judgment of the
espistemic subject, that is by applying a logical rule. The eliminating rules, in a
context where the cut rule in strictly bounded and anyway eliminable (as it hap-
pens in the main logical calculi) are the so called Comprehension rules (Comp
rules) in [7], i.e ∀ − L and ∃ − R. An exhaustive discussion of the elimination
power of Comp Rules is given in [7] Section 3. Thus, the full higher order system
Zω for ECL Logic that we are going to define, is a subsystem of LKω where:
- only atomic formulas occur in the logical axioms;
- weakening rules are admitted only to introduce atomic formulas, i.e. weak-
ening cannot introduce logical information;
- cut rule is admitted only with atomic cut formulas, i.e. cut cannot eliminate
logical information;
- each logical rule is always thought as occurring in some proof P, and have
constraints on its auxiliary formulas that take into account their introduction in
the whole proof-segment above the premise(s) of the rule occurrence in P. That
is, they are global and not local constraints. The underlying idea is that the
construction of a judgment introducing new logical information must be based
only on previously produced logical information which has been itself acceptably
constructed.
We note that the restrictions on weakening and cut rules immediately follow
from the epistemic assumptions mentioned above. The constraints on the logical
rules will be presented and discussed in detail in the next Sections. Moreover, the
constructivity properties we assign to Zω are also justified through the compari-
son with those logics that in the literature are already considered as constructive
(Intuitionistic Logic, Paraconsistent Logic, Uniform Logic).
The constructivism of Intuitionistic Logic LJ is well known. We recall that,
from a merely technical point of view, it is characterized by the refutation of
the excluded middle (or tertium non datur ) principle, syntactically expressed by
the schema A ∨ ¬A and , collaterally, also by the refutation of the left double
negation principle, expressed by the schema ¬¬A ⊃ A. The standard sequent
version LJ is characterized by the following condition: each sequent in a proof has
the empty set or a singleton as succedent. However, this is not strictly necessary:
in the sequent version of Maehara [9] p. 52, such condition is replaced by local
contraints on three logical rules, among which, centrally, the negation rule on
the right ¬ − R. Even if intuitionism has many peculiar constructive features,
that cannot be reduced to the mere refutation of tertium non datur, it is a fact
that LJ plus ` A ∨ ¬A ≡ classical LK.
The constructivism of Paraconsistent Logic has been only recently defined
in a formal way, and the set of paraconsistent logics to which the notion can be
applied must be clearly delimited. We consider here the system CI examined
in [6]. Paraconsistent Logic arises form the refutation of the classical (syntactic)
principle ex contraditione quodlibet that can be expressed by the LK-provable
150 Paolo Gentilini and Maurizio Martelli
sequent schema A∧¬A ` which is classically equivalent to the non contradiction
principle ` ¬(A ∧ ¬A). CI and the various systems in the C-system family do
not prove contradictions, but can support axioms of the form B ∧ ¬B without
trivializing, i.e. without proving the empty sequent “ ` ”. Even if the refutation
of ex contradictione quodlibet could seem today a position which is naturally
constructive, in [6] a formal definition of constructive paraconsistent logic is
given, also employing the introduction of antisimmetry connections between C-
system paraconsistency and intuitionistic logic.
The Uniform Logic introduced in [8], that we indicate here with LUω , is
a sub-system of Higher Order Intuitionistic Logic LJω where a particular con-
straint is added for the application of logical rules inside a proof-tree. Essen-
tially, if a logical rule occurrence R has the auxiliary formula(s) in the premise
succedent(s), then it (they) must be the principal formula(s) of the logical rule
occurrence(s) immediately above R in the branch. Uniform Logic specifies the
intuitionism constructivity in the direction of computation: indeed, it expresses
abstract logic programming languages. Moreover, as to the main discussion of
this paper, it must be remarked that the rule-constraint mentioned above is a
first example of global, i.e. referred to the context of the rule-occurrence in the
proof, and not local constraint.
As detailed later, Zω shares relevant specific features with Intuitionistic
Logic, since it does not prove both ℵ0 instances of excluded middle princi-
ple A ∨ ¬A and ℵ0 instances of left double negation principle ¬¬A ⊃ A. It could
be called also a pseudo-intuitionistic system (such notion is formally introduced
in [6]).
Zω shares relevant specific features with Paraconsistent Logic, since it does
not prove ℵ0 instances of non contradiction principle ¬(A ∧ ¬A) and can be
extended by ℵ0 contradictions without trivializing. It could be called also a
paraconsistent system.
Zω shares some properties with Uniform Logic. In fact it does not hold, (in
general, for Zω proof trees), the possibility of any permutation of the order of
propositional rules in a proof branch without changing the end-sequent, even in
those cases where classical logic would admit such a permutation.
We also point out that ECL has a strong expression power. Indeed, besides
the Zω -proof capabilities allowed by the higher order, the following properties
also hold for Z1 and ZP:
Zω proves ℵ0 arbitratrily complex instances of excluded middle principle A ∨
¬A that LJω does not prove;
Zω proves ℵ0 arbitratrily complex instances of non contradiction principle
¬(A ∧ ¬A) that CIω does not prove.
3 The Systems Zω , Z1, ZP for Explicit Constructive
Logic (ECL)
In the sequel we briefly call bottom and top the formulas ⊥ and >, recalling that
they are not atomic formulas. Moreover, if Zω proves the sequent ` B we say that
Explicit Constructive Logic ECL 151
B is a theorem of Zω , if Zω proves the sequent E ` we say that E is a refuted by
Zω . The language of Zω is that of LKω (see [7] Sec. 2) with the exclusion of all
the equality symbol =o→(o→o) that would express the equality relation between
o-typed formulas, since such relation is not considered by ECL. For the notions
concerning general proof theory, the analysis of proofs as well as the notions of
ancestor, descendant, auxiliary formula, principal formula and so on, we refer to
[7] Section 2 and 6.
The sequent system Zω is the following:
(In a sequent Ω, ∆, Γ , Π, Θ, ... will be used as meta-expressions for finite
and possibly empty sets of o-typed formulas, A, B, C, D, ...for arbitrary isolated
formulas in a sequent, A+ , B + , C + , D+ , ... for arbitrary atomic isolated formulas.
The writing Ω, ∆ denotes Ω ∪ ∆ )
Axioms
Logical axioms A+ ` A+ with the following constraint:
+
if the atomic A is a β-redex, possible repeated application of the λ-rule
does not produce any β-contractum F which is a descendant of A+ and is a
non-atomic formula.
Top axiom `>
Bottom axiom ⊥`
Rules
Strong Logical Rules:
Propositional rules:
A, B, Γ ` ∆ Γ ` ∆, A Λ ` X, B
∧ −L ∧ −R
A ∧ B, Γ ` ∆ Γ, Λ ` ∆, X, A ∧ B
Γ ` ∆, A, B A, Γ ` ∆ B, Λ ` X
∨ −R ∨ −L
Γ ` ∆, A ∨ B A ∨ B, Γ, Λ ` ∆, X
A, Γ ` ∆, B Γ ` ∆, A B, Λ ` X
⊃ −R ⊃ −L
Γ ` ∆, A ⊃ B A ⊃ B, Γ, Λ ` ∆, X
Γ ` ∆, A A, Γ ` ∆
¬−L ¬−R
¬A, Γ ` ∆ Γ ` ∆, ¬A
It can be noted that the forms of ∧ − L and ∨ − R are not the standard
one. This is a specific requirement of the Explicit Constructive Logic that will
be discussed in the next Sections.
Quantifier rules:
[tα /xα ] A, Γ ` ∆ Γ ` ∆, [bα /xα ] A
∀−L ∀−R
∀xα A, Γ ` ∆ Γ ` ∆, ∀xα A
[bα /xα ] A, Γ ` ∆ Γ ` ∆, [tα /xα ] A
∃−L ∃−R
∃xα A, Γ ` ∆ Γ ` ∆, ∃xα A
where: in ∀−L, ∃−R, tα is an arbitrary term and in the corresponding ∀xα A,
∃xα A, tα may still occur, that is tα may be not fully quantified in ∀xα A, ∃xα A;
on the other hand, in ∀ − R, ∃ − L, the free variable bα occurring in [bα /xα ] A
is uniformly replaced in ∀xα A, ∃xα A by the bound variable xα having the same
index, and bα does not occur in Γ, ∆. bα is the proper variable or eigenvariable
of the rule.
Γ 0 ` ∆0
λ -rule: λ
Γ `∆
152 Paolo Gentilini and Maurizio Martelli
where the sets Γ and Γ 0 and the sets ∆ and ∆0 differ only in that zero
or 1 formula in them is replaced by some formula to which it is β-reducible.
Note that the rule is defined so that the β-reduction may work either upwards
or downwards. We observe that differently from the more usual version (see e.g.
[8], [4]) it is imposed here that λ-rule works on 1 auxiliary formula only, and not
simultaneously on any arbitrary set of auxiliary formulas. This option is more
coherent with the ECL perspective and with the inclusion of the rule among the
strong logical rules, where the control of all the origins of the auxiliary formulas
of the rule -occurrence in the above standing proof-segment is required. Finally,
the inclusion of λ-rule among strong logical rules is due to the possibility that a
rule occurrence R in a proof P of Zω may β−reduce a β-redex to a non-atomic
formula D arbitrarily complex, with a main logical connective (the outermost
symbol of D) that can be seen as introduced by R.
Strong logical rules must fulfil the following constraints:
- If R is a 1 premise strong logical rule then each occurrence of R in a
Zω -proof P is such that at least 1 auxiliary formula has at least 1 uppermost
ancestor introduced by an axiom.
- If R is a 2 premise strong logical rule, having i.e. two auxiliary formulas,
then each occurrence of R in a Zω -proof P is such that each auxiliary formula
has at least 1 uppermost ancestor introduced by an axiom.
- If R is a λ-rule then each R- occurrence in a proof P in Zω is such that
its auxiliary formula has at least 1 uppermost ancestor introduced by an axiom.
Weak Logical Rules
⊥ `
bottom rule
⊥ ` A
where A is an arbitrary formula without sub-formulas of the form ∀xo (xo ),
∃xo (xo ).
` >
top rule:
B ` >
where B is san arbitrary formula without sub-formulas of the form ∀xo (xo ),
∃xo (xo ).
Structural Rules
Γ `∆ Γ `∆
Wakening rules: +
W1 − R +
W1 − L
Γ ` ∆, A A ,Γ ` ∆
` `
W2 − R W2 − L
` F F `
+ +
Γ ` ∆, B B ,Γ ` ∆ `F F `
Cut Rules Cut1 Cut2
Γ `∆ `
Structural rules must fulfil the following constraints:
- Each W1 -principal formula is atomic, and in any W 1-rule at least 1 set
of the contex is non-empty.
- Each W 2- principal formula may be arbitrary.
- Cut1-formula B + is atomic, such that if it is a β-redex, possible repeated
application of the λ-rule does not produce any β-contractum G which is a de-
scendant of B + and is a non-atomic formula. Moreover, at leaast 1 context set
is non-empty.
- Cut2−formula F may be arbitrary.
Explicit Constructive Logic ECL 153
3.1 The First Order System Z1 of ECL
The language of Z1 is defined as follows:
The well formed expressions of Z1 are Church-terms with the following con-
straints:
- variables are only of type i;
- λ-abstractions are only over variables of type i and on formulas of type o,
i.e. have only the form λxi Ao with type i → o;
- quantifiers occur only with type (i → o) → o , i.e. with the forms ∃(i→o)→o
∀(i→o)→o ;
- if τ is a type occurrence in any Z1-espression, no occurrences of the type o
in τ precede any occurrence of the type i in τ ;
- non-logical constants of Z1 are only of a type τ such that:
either in τ the type o does not occur, or the type o has at most one occurrence
as tail of τ ; τ has a condensed writing of the form: i → i → i → ... → u, where
u is a primitive type.
Deduction apparatus of Z1:
It is identical to Zω deduction apparatus, with the constraint that rules are
restricted to sequents of Z1-formulas, so that only i-typed terms can be quanti-
fied. The λ-rule could be useful but is not strictly necessary for the expressivity
of the system. Thus, we denote Z1λ the version including λ-rule, Z1 the λ-rule
free version.
3.2 The Propositional Calculus ZP of ECL
The language of ZP is obtained from Z1 with the following restrictions:
-quantifiers, variables, λ-abstraction expressions, do not occur in the lan-
guage;
- the only non logical constants are o-typed atoms, also called propositional
letters.
The deduction apparatus is obtained from that of Z1 by deleting quantifier
rules.
3.3 Immediate Properties and Definitions of Zω , Z1, ZP
In this Section we will focus mainly on the most powerful and expressive
system, which is Zω ; however, many definitions and properties naturally extend
to Z1 and ZP.
Remark 1. Weak logical rules are also imposed by the necessity to give a suitable
proof power to ECL systems. For example, in LKω , the axiom ⊥ ` makes
superfluous a rule of the form
⊥ `
⊥, U ` V
U, V arbitrary sets, due to constraint free weakening rules of LKω . In ECL
systems, such approach would not be conceivable.
Definition 1. Let P be a proof tree in Zω . Then we say that the occurrence of
the formula A in P is strongly introduced if it is integral descendant of an axiom
formula or it is integral descendant of the principal formula of a strong logical
rule. We say that the occurrence of the formula A in P is weakly introduced if
154 Paolo Gentilini and Maurizio Martelli
it is integral descendant of the principal formula of a weak logical rule or of a
weakening formula.
For the definition of integral descendant of a formula occurrence in a proof
see [7] Def. 6.5.ii p. 750. Intuitively the integral descendant B of the formula
occurence F in a proof branch is such that B and F are occurrences of the same
formula, i.e. B ≡ F, connected by a proof-path where F (or B) is never an
auxiliary formula of any rule.
Definition 2. Among the strong logical rules we call major (strong) logical rules
those where all auxiliary formulas must be strongly introduced, minor (strong)
logical rules those where at least 1 auxiliary formula may be weakly introduced.
Corollary 1. {∨ − L, ∧ − R, ⊃ −L, ¬ − R, ¬ − L, ∀ − L, ∀ − R, ∃ − L, ∃ − R,
λ − rule} is the set of major logical rules in Zω , {∨ − R, ∧ − L, ⊃ −R} is the
set of minor logical rules in Zω .
Definition 3. Let P be a proof tree in Zω . Then we say that a sequent S
occurring in P is strongly proven in P if each formula of S is strongly introduced
in P. We say that S is weakly proven in P otherwise.
Caveat: the same S may be strongly proven in a proof P and, simultaneously,
weakly proven in a different proof Q. In ECL logic the proof-context of a sequent
or of a formula has a substantial role, and this is coherent with the fact that
the constraints on the application of a logical rule in ECL are always global and
not local. We also mention these two evident facts: Zω is consistent, since it is
a LKω subsystem; moreover, if P is a Zω -proof, it cannot have an end-sequent
where all formulas are weakly introduced.
4 General Epistemological and Logical Justifications
for Axioms and Rules of Zω , Z1, ZP, and Further
Properties of Connectives and Rules in ECL
4.1 The Formulas Bottom and Top
o-typed logical constants ⊥ and > standardly occur in the Church presentation
of Type Theories ([7], [8], [4]). In the Explicit Constructive Logic ECL > ex-
presses the judgment that the subject thinks as always acceptable, beyond any
possible confutation, and ⊥ expresses the judgment that the subject thinks as
always refutable, beyond any possible corroboration. That’s why, in general, we
can state: if B is a Zω -theorem different from >, then it is not provable in Zω
the sentence (> ⊃ B) ∧ (B ⊃ >) (or B ←→ >), and if E is a Zω -refuted dif-
ferent from ⊥, then it is not provable in Zω the sentence (⊥⊃ E) ∧ (E ⊃⊥) (or
E ←→⊥). In particular, as to the conjunctions that would give the mentioned
Zω -logical equivalences, it is not provable, in general, in the first case the con-
junct > ⊃ B and in the second case the conjunct E ⊃⊥ . Remarkable exceptions
may exist. For example > ∧ > is a theorem and > ⊃ > ∧ > is provable. However,
Explicit Constructive Logic ECL 155
for each atomic A+ , A+ ∨ ¬A+ is a theorem but > ⊃ A+ ∨ ¬A+ is not provable.
For example, for each atomic B + , ⊥ ∧B + is a refuted and ⊥ ∧B + ⊃⊥ is prov-
able. However, for each atomic B + , B + ∧ ¬B + is a refuted but B + ∧ ¬B + ⊃⊥
is not provable. These examples suggest that explicit constructivity includes a
criticism to classical implication. Moreover, the usual systems of classical, in-
tuitionistic and paraconsistent logics lack such fine separation capability: all of
them make top particles equivalent to theorems, and bottom particles equivalent
to refuted sentences.
4.2 The Weak Logical Rules
Let’s comment on and justify the weak logical rules, i.e. the top rule and the
bottom rule. They are logical since they realize through an information trans-
formation process the presumed logical content of the logical connectives top and
bottom. Note that, in the foundational perspective of ECL, without such rules,
the presence in the system of the mentioned o-typed logical connectives would
be not motivated and they should be excluded from the language. On the other
side, they are the only rules through which not explicitly constructed logical
information can be introduced in the argumentative discourse. Indeed, they rep-
resent a very constrained and regulated way to partially have that information
introduction power of the standard weakening rule. This is also why they are
called weak, and their principal formulas are qualified as weakly introduced. This
causes inferential limitations. If ⊥` C and D ` > are the conclusions of any
bottom rule and top rule respectively, we cannot apply to them a ⊃ −L rule and
infer C ⊃ D, ⊥ ` > , since both the auxiliary formulas are weakly introduced.
As a matter of fact ⊥ ` ⊥ and > ` > are not logical axioms, they are con-
clusions of weak logical rules, so that one of the two cedents ([1] p. 10) is always
weakly introduced. Nevertheless, the contribution of weak logical rules to ECL
inference is substantial; otherwise the information sources of ECL proofs would
be too poor. In addition, their weakly introduced principal formula can anyway
contribute to infer strongly introduced formulas: from D ` >, we can infer `
D ⊃ > that is a strongly introduced formula, as the principal formula of a ⊃ −R
must be. We shall prove in Section 6 that weak logical rules must only occur as
the initial rule in a branch: in addition, their principal formula has not auxiliary
formula, so that it has no predecessor. This justifies the requirement that for-
mulas ∀xo (xo ), ∃yo (yo ) do not occur as sub-formulas of the principal formula of
any weak logical rule. In a Zω −proof, ∀xo (xo ), ∃yo (yo ) mark elimination judg-
ments about previously produced logical information. Then, their occurrence is
meaningless in an initial (uppermost) formula of the proof tree.
4.3 The Exclusion of Equational Logic EQω from Zω
In LKω and LJω , Equational Higher Order Logic EQω can be fully included
in the system and works together with the logical part. For the EQω -axioms
see [7], Sec. 2.4. What must be clearly emphasized is that in the higher order
context and inside the Church formalism EQω becomes extremely powerful and
mixes itself with the logical connectives’ deduction action. This is clear if we
consider that each theorem B of LKω and LJω can be provably constricted
to the atomic formula B =o >, and that the equality predicate on type o can
156 Paolo Gentilini and Maurizio Martelli
be provably identified with the logical equivalence between propositions, i.e., in
the ECL perspective, between judgments. From the standpoint of ECL, aiming
to obtain a very fine characterization of logical connectives through a construc-
tive approach, this is not admissible. Equational Logic is explicitly excluded from
ECL. More generally, we point out that, in the context of explicit construc-
tivism, is also inadmissible the confusion between the equality relation =o and
the logical implication ⊃ or double-implication ←→. We think that the equality
relation can be only defined a priori in a platonic universe. In a knowledge repre-
sentation setting, we are not able to imagine an epistemic subject that, inside an
empirical world and through an effective process can establish that two objects
are equal, with the same meaning owned by the statement “these two Euclidean
triangles are equal” affirmed inside a platonic universe. On the contrary, if we
consider the epistemic subject that formulates judgments on the world, the im-
plication or double-implication relation must be established by a construction
which increases the complexity of the judgment through the logical rules, starting
from elementary data. Observe that in Zω theorems that are atomic formulas do
not exist (with the minor exception of possible β-redexes, which are a bit arti-
ficial form both for possible judgments and for possible data), coherently with
the principle that elementary data cannot be judgments. Differently, Equational
Logic EQω produces a multitude of atomic theorems, most of them having a
substantial and non-artificial information content, such as, for example, the as-
sertion B =o F ∧ ¬F , establishing that the arbitrarily complex formula B is
logically equivalent to a contradiction.
4.4 The Strong Logical Rules
The originality of the proposed logic is mainly expressed in these rules. In fact,
the constraints involving these rules are not local, i.e. they do not operate on the
occurrence of the specific rule R in a proof, but are conditions concerning the
whole proof P in which the rule occurs: to apply R it is necessary, in general, to
examine all the introductions of the uppermost ancestors of the auxiliary formu-
las of R in the proof segment of P standing above the R -premise(s). We deem
that relevant innovations in Logic could be obtained by changing the praxis of
imposing only local constraints on a single rule. This lightly changes the usual
notion of performing a proof, and could produce innovative results and situa-
tions, perhaps more than the introduction of new connectives and new rules. By
recalling the Definitions of Section 3, the distinction between strongly introduced
formula in a proof P and weakly introduced formula in a proof P should result
natural. Axioms are the choices of the epistemic subject, on which it decides to
found its reasoning. Weakening and weak logical rules are auxiliary tools, useful
to introduce information. On the other hand, a proof without at least one ax-
iom occurrence cannot exist, while infinite proofs may exist without weakening
or weak rule occurrences. It must be emphasized that the minor strong logical
rules ∨−R , ∧ − L are differently presented w.r.t. the usual standard presenta-
tion, that is both the auxiliary formulas must occur as isolated in the premise.
This reflects two crucial requirements. First, if this would not be the case, the
introduction of one of the maximal disjunct (conjunct) of the principal formula
Explicit Constructive Logic ECL 157
would be an arbitrary hidden weakening. Furthermore, since we need to con-
straint all the uppermost ancestors of both the auxiliary formulas in the whole
proof-segment above, both the formulas must explicitly occur in the premise.
4.5 The Structures of Weakening and Cut in Zω
The constraints on the weakening rule, i.e. the imposition on principal formulas
to be atomic, should be quite clear. It is at the basis of Explicit Constructive
Logic: only elementary data can be used without having been constructed. A first
non trivial fact follows immediately, thus clarifying the differences from LKω
and LJω : if X ` Y is Zω -provable, its over-sequents U ` V with X ⊂ U and
Y ⊂ V , are, in general, not Zω -provable. A motivation of the presence of two
rules W 1 and W 2 is due: while W1 is immediately understandable, less obvious
is the necessity of W 2, i.e. of arbitrary weakenings on the empty sequent. The
reason arises from the fact that Zω is supposed to be possibly extended to vari-
ous (countably many) axiomatized theories Tj ’s. Some of them are expected to
be absolutely inconsistent, and we usually identify this situation with the prov-
ability of the empty sequent. But this does not work in the ECL-framework,
since from the empty sequent, Zω -rules minus W 2, in general, cannot derive all
formulas of the language as theorems. Therefore, W 2 is added. The motivations
of Cut2 are also linked to the ones of W 2: if a Zω -based theory T has any non
atomic theorem and any non atomic refuted that are identical, i.e. T proves
both B ` and ` B, Zω -rules minus Cut2, in general, cannot derive the empty
sequent. Thus, Cut2 is added. We consider now the substantial restrictions that
are imposed to the cut rule. They reflect the requirements already considered
about the introduction and the elimination of logical information by a reasoning
epistemic subject: logical information is not eliminated by a material deletion,
but only by a logical transformation. The selection of logical information is a
thinking act, requires elaboration, then it must involve logical rules. Thus, cut
at most deletes atomic formulas, i.e. elementary data. On the other hand, the pe-
culiar structure of the cut rule cannot become a clandestine arbitrary weakening,
and this is obtained by imposing the same context for the two premises.
5 Possible New Effective Applicability of ECL-based
Higher Order Logic
It is well known that, in full Higher Order Logic, the unbounded quantification
on o-typed formulas, or on formulas of arbitrary types where o-typed formulas
occur as Church-subterms, makes it extremely difficult to establish any useful
link between the formulas occurring in the root of a cut-free proof-tree P and
the formulas occurring in the overstanding sequents alongside the branches of P.
To find how to exploit the information and proof power of higher order quan-
tification, without chaotic or collapsing phenomena, is a main goal of our con-
structive view of higher order logic. The envisaged road is the following:
to suitably and lightly normalize higher order quantification by a set of
constraints allowing a Normal Form Theorem for the proofs of an adequately
expressive sub-system of LKω .
158 Paolo Gentilini and Maurizio Martelli
A Normal Form Theorem (NFT) for a system V (see [1] or for example [5]
where a NFT for Arithmetic is proposed) is characterized by:
i ) an effective description of the transformation of a V-proof into a V-proof
tree with the same root, partitioned in blocks such that each block includes only
homogeneous rules or axioms;
ii ) a set of effective procedures such that given a root sequent L, the following
reasonable estimates about the features of a possible proof Q of L in V can be
produced:
an estimate of the possible V-rule instance set occurring in Q
an estimate of the possible V-axiom instance set occurring in Q
an estimate of the length and the width of Q
an estimate of the formula (or term) set occurring in Q.
It is quite clear that an efficient Normal Form Theorem for an adequate and
non redundant LKω sub-system can give a new basis for higher order automated
deduction and knowledge representation. We believe that:
the very strong and peculiar ECL constructivity of the system Zω allows
us to state those normative constraints on its quantification power that can
generate an adequately expressive subsystem Z∗ω that admits a Normal Form
Theorem. We present now a first hint of the system Z∗ω that should exemplify
how further constructive conditions imposed on the quantification judgements of
the epistemic subject may lead to a Normal Form Theorem. As a basic feature of
Z∗ω we introduce the notion of Zω −proof with the witness property. We previously
recall that the language includes, for each type γ, ℵ0 free variables (atoms) bjγ ,
univocally individuated by their index j ∈ N, and ℵ0 bound variables (atoms)
yγi , univocally individuated by their index i ∈ N (see [7] Section 2.2). In the
following definition, the most relevant point is b):
Definition 4. A Zω −proof P has the witness property if the following condi-
tions hold:
a) Each time o-typed formulas/terms Boj , j = 1, ..., m, m ≥ 1 occur in P as
the auxiliary formula E of a Comp rule, or are included in it as sub-terms, then
the bound variable zo in the corresponding principal formula Qzo (zo ), Q ∈ {∀, ∃}
has as index the gödel number ([7] Section 2.5) of their sequence.
b) Any auxiliary formula of a Comp rule in P may have o-typed sub-terms
only if the quantification is over the type o.
c) In P isolated formulas of the form ao , bo , i.e. free variables of type o which
occur as isolated formulas in a sequent, cannot be auxiliary formulas of quantifier
rules.
Proposition 1. The property “to be a proof with the witness property of the
system Zω ” is a recursive relation, it can be expressed by a recursive predicate
inside Primitive Recursive Arithmetic PRA and is a decidable property.
Proof. The Definition above describes exactly effective conditions to get a
Zω − proof with the witness property.
Only as one of the possible example of the effective control on proofs allowed
by the witness property we mention these results:
Explicit Constructive Logic ECL 159
Proposition 2. a) Let P be a proof in Zω with the witness property. If in P a
formula of the form Qzo (zo ), Q ∈ {∀, ∃} is introduced, then in the root at least
one formula of the form Hzo (zo ), H ∈ {∀, ∃} occurs.
b) Let P be a proof in Zω with the witness property. Let us suppose that
quantified formulas over the type o do not occur in the P-root. Then each atom
of type o occurring in P occurs also in the root of P.
Definition 5. The weakly normalized system Z∗ω is so defined: a) Axioms, propo-
sitional rules, structural rules of Z∗ω are the same as that of Zω and with the
same constraints; b) Quantifier rules of Z∗ω have the same constraints as the ones
of Zω , and moreover are applied in a proof-tree in a way such that the result-
ing proof has the witness property, i.e. it fulfils all the conditions stated in the
previous Definition of the witness property. c) The λ-rule is omitted from the
deduction aparatus.
Therefore, in Z∗ω all proofs have the witness property. Thus, even if the higher
order quantification power is not dramatically bounded at all, some interesting
links between the formulas occurring in the root and the rule instances and
formulas occurring in the above proof-segments are at disposal. We will see such
links at work in particular in Section 7.
6 Elementary Proof-theory and Expressivity of Zω
Proposition 3. Zω admits cut-elimination.
Proof. The proof is straightforward. Indeed, Cut1-formulas can be only atomic.
Then they can be introduced in any Zω −proof only by weakenings or by logical
axioms. This makes the proof-reductions to get cut-elimination very easy. As
to Cut2 the set of Cut2-occurrences in the Zω −proofs is empty, due to the
consistency of Zω .
In the sequel we assume to work only with cut-free Zω −proofs. Moreover, by
coherence with ECL setting, we will consider only the equality free versions of
type theories LKω LJω , that so have the full cut elimination property. The next
results could seem to have obvious proofs. This would be a misunderstanding,
since in ECL the form of the logical rules is essentially standard, but their
application conditions are not standard at all. For example, if F is not atomic,
then F ` F is not a Zω −logical axioms, and, in general, nobody can easily assert
or deny that it must be a Zω −theorem.
Proposition 4. Zω proves ℵ0 instances both of the excluded middle principle
B ∨ ¬B and of the left double negation principle ¬¬B ⊃ B that Intuitionistic
Higher Order Logic LJω does not prove.
Proof. Let G+ , H + different non logical constants of type o. It is easy to see
that Zω proves the sequent G+ ∧ H + ` G+ ∧ H + with all the formulas strongly
introduced in the proof. Then we produce in Zω the following proof segment:
160 Paolo Gentilini and Maurizio Martelli
G+ ∧ H + ` G+ ∧ H +
¬−R
` G+ ∧ H + , ¬(G+ ∧ H + )
∨ −R
` (G+ ∧ H + ) ∨ ¬(G+ ∧ H + )
where all the rules have strongly introduced auxiliary formulas. Differently, by
applying the cut-elimination property of LJω it is evident that LJω cannot prove
the same end-sequent without breaking the local constraints of each LJω −rule,
imposing at most one formula in each succedent. Analogous considerations hold
for the sequent ` ¬¬H + ⊃ H + . Moreover, the thesis can be easily extends to
arbitrarily complex instances of the mentioned principles.
Proposition 5. Zω proves ℵ0 instances of the non contradiction principle ¬(A∧
¬A) that equality free paraconsistent type theory CIω , extending the system CI,
cannot prove.
Proof. Let B + be an atomic formula. It is wellknown that CIω does not prove
` ¬(B + ∧ ¬B + ) (for the details on CI see [6]). The following proof can be
produced in Zω :
B+ ` B+
¬−L
B + , ¬B + `
∧ −R
B + ∧ ¬B + ` ¬−R
` ¬(B + ∧ ¬B + )
where all the auxiliary formulas of the rules are strongly introduced.
In the following, we simply state some lemmas without proofs:
Lemma 1. The weak logical rules top rule and bottom rule can be only initial
rules in a proof branch, i.e. they always occur as the uppermost rules of the
branch.
Lemma 2. Let Q be a proof in Zω with root X ` Y,B where B is the integral
⊥`
descendant of the principal formulas of a set W ≡ Rj of bottom
⊥` B
rules in Q. Then we can replace each element of W in Q with the axiom ⊥`
obtaining a proof P of X ` Y in Zω .
Lemma 3. Analogous to the last Lemma, by replacing “bottom rule” with “top
rule” and the formula bottom ⊥ with the formula top >.
7 What ECL does not want to prove: Z∗ω , Z1, ZP as
paraconsistent and pseudo-intuitionistic systems
A very remarkable property of ECL is that without imposing any local constraint
on negation rules of its systems, it nevertheless shows simultaneously a relevant
and interesting intuitionistic and paraconsistent behaviour of its proofs. We will
use now the weakly normalized system Z∗ω (Definition 5) that is a convenient
setting of our epistemic consideration. We have the following results3 :
3
in the sequel the superscript (.)+ in atomic formulas will be omitted
Explicit Constructive Logic ECL 161
Theorem 6. Consider the following instance of non contradiction principle ex-
pressed by the sequent S: ` ¬[(⊥ ∧(B ∧ C)) ∧ ¬(⊥ ∧(B ∧ C))] where B and C
are different o-typed non logical constants. Then S is not Z∗ω −provable. Since
S belongs also to propositional and first order languages the same holds for Z1
and ZP.
Proof. Suppose ad absurdum that S is the root of a proof Q of Z∗ω . If the root
formula B is also the integral descendant of the principal formula of a set of of
bottom rule occcurences in Q, by Lemma 2 we delete such rules and get a proof
Q’ where the root formula B is never introduced by a bottom rule occurrence:
indeed, we exclude that the root of Q’ could result the empty sequent, by the
absolute consistency of Z∗ω . Therefore, by properties of Z∗ω , the end rule of Q’
must be a ¬ − L rule having the sequent M ≡ (⊥ ∧(B ∧ C)) ∧ ¬(⊥ ∧(B ∧ C)) `
as premise, and let H be its root formula. In M top formulas do not occur: then,
by Proposition 2 (item b)), in Q’ neither top formulas nor top rules can occur.
Thus, neither H nor H sub-formulas can be integral descendant of principal
formulas of top rule occurrences in Q’. H must be so the conclusion of a ∧ − L
rule, with premise K ≡ (⊥ ∧(B ∧ C)), ¬(⊥ ∧(B ∧ C)) ` . By analogous reasons
K is the conclusion of a ¬ − R rule with premise N ≡ (⊥ ∧(B ∧ C)) `
(⊥ ∧(B ∧ C)). Let D be the succedent of N . We have to examine the possibility
that D has been introduced by bottom rules in Q’. We have two possible cases.
The first one is that D is exclusively the integral descendant of principal formulas
of bottom rule occurrences in Q’. By Lemma 2 we delete them, and get G ≡
⊥ ∧(B ∧ C) ` as the root of a Z∗ω -proof W. Since top rules do not exist in W,
the premise of G in W must be ⊥, B ∧ C `, that necessarily has ⊥, B, C ` as
premise: this is absurd, since being both B and C obviously weakly introduced,
they cannot be auxiliary formulas of a ∧ − L rule. The second case is that D is
not only the integral descendant of principal formulas of bottom rule occurrences
so that, having deleted these by Lemma 2, we obtain a proof V of the sequent
L ≡ ⊥ ∧(B ∧ C) ` ⊥ ∧(B ∧ C) where no cedent is the integral descendant of
principal formulas of weak logical rule occurrences. L must be the conclusion of
a strong logical rule. Indeed, suppose that the end rule of V is any ∧ − R rule.
Then its premises, that are both necessarily Z∗ω -provable, are J1 ≡⊥ ∧(B ∧ C) `
⊥ and J2 ≡⊥ ∧(B ∧C) ` (B ∧C): unfortunately, it is evident that the succedent
of J1 cannot be strongly introduced, so that the ∧ − R constraint would not be
respected. We must so assume that the end rule of V is any ∧ − L rule, with
premise J3 ≡⊥, B ∧ C ` ⊥ ∧(B ∧ C). J3 can be the conclusion either of a ∧ − L
or of a ∧−R. In the first case the possible premise is J4 ≡ ⊥, B, C ` ⊥ ∧(B ∧C),
in the second case the two possible premises, both necessarily Z∗ω -provable, are
J5 ≡⊥, B ∧ C ` ⊥ and J6 ≡ ⊥, B ∧ C ` B ∧ C. However, the sucedent of J5
can be only weakly introduced and the same problems observed for J1 stop the
examined possibility. Thus, we have to examine the possible provability of J4.
The possibility that J4 is the conclusion of any ∧−R rule gives the same problems
already noted for J1 and J5. We have then to suppose that the succedent of
J4 has been introduced in V only by a set of bottom rule occurrences, and that
the ⊥ in the J4-antecedent is the integral descendant of the premise formulas
162 Paolo Gentilini and Maurizio Martelli
of such bottom rules. By Lemma 2, we delete such bottom rule occurrences and
get a proof Z of the sequent J7 ≡⊥, B, C ` where by construction B, C are the
only integral ancestors of the auxiliary formulas of the ∧ − L with conclusion
J3 ≡⊥, B ∧ C ` ⊥ ∧(B ∧ C). But this is absurd, since both B and C in J7 would
be only introduced by weakenings in V, i.e. both are weakly introduced, and the
∧ − L constraints would not be respected4 .
Theorem 7. Consider the following instance of excluded middle principle ex-
pressed by the sequent M : ` [> ∨ ∃xi B] ∨ ¬[> ∨ ∃xi B] with B o-typed non logical
constant. Then M is not Z∗ω −provable. Since M belongs also to the first order
language the same holds for Z1.
8 Conclusions
The introduction of the ECL logic and the first results regarding its relations
with intuitionistic and paraconsistent logics are the main topics of the paper.
We stressed the higher order setting since we believe that it is a relevant issue
to find ways to make HOL a foundational setting for knowledge representation
(constructive and with controlled use of instantiations). The future work will be
devoted to further analyze the characteristics of ECL. As some considerations
already present in the paper suggest the constructivity of ECL is not related to
the “not rules” but to some peculiarities of the implication and of the possible
proofs that can be accepted. These properties should be relevant for the use of
ECL as the foundation logic of both Logic Programming and Theorem Proving.
References
1. S.R. Buss (Ed.), Handbook of Proof Theory, Elsevier, Amsterdam, 1998.
2. W. A. Carnielli, M. E. Coniglio, J. Marcos, ‘Logics of formal inconsistency’ in
Handbook of Philosophical Logic, D. Gabbay, F. Guenthner (Eds.), 2nd ed., volume
14, Kluwer, Dordrecht, 2005.
3. A. Church, ‘A Formulation of Simple Theory of Types’, Journal of Symbolic Logic,
5, 1940, 56-68.
4. M. De Marco, J. Lipton, ‘Completeness and Cut-elimination in the Intuitionistic
Theory of Types’, Journal of Logic and Computation, 15, 2005, 821-854.
5. P. Forcheri, P. Gentilini , M.T. Molfino, ’Informational Logic in knowledge repre-
sentation and automated deduction’, AI COMMUNICATIONS, vol. 12,1999, 185-
208.
6. P. Gentilini, ‘Proof Theory and Mathematical Meaning of Paraconsistent C-
Systems’, Journal of Applied Logic, vol. 9, 3, 2011, 171-202.
7. P. Gentilini, M. Martelli, ‘Abstract Deduction and Inferential Models for Type
Theory’, Information and Computation, vol. 208, Issue 7, July 2010, 737-77.
8. D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, ‘Uniform Proofs as a Founda-
tion for Logic Programming’. Annals of Pure and Applied Logic 51, 1991, 125-157.
9. G. Takeuti, Proof Theory, North-Holland, Amsterdam, 1987.
10. A.S. Troelstra, D. van Dalen, Constructivism in Mathematics, Vol.1, Elsevier, 1988.
4
It is not difficult to imagine that infinitely many sequents having a form similar to
S are not Z∗ω −provable.