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.