One of the seminal goals of Explicit Constructive Logic (ECL) is to provide a constructive formulation of full higher order logic (Classical 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 introduced 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.
Full higher order logic can be an extremely powerful tool for knowledge
representation 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 [
Explicit Logical Constructivism: Syntactic Environment and Epistemological Basis We will now give a short synthesis of the epistemological basis of Explicit Constructive Logic: the style will be heuristic and intuitive.
We will use the logical connectives `a la Church [
- 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 comparison 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 [
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 [
The Uniform Logic introduced in [
As detailed later, Zω shares relevant specific features with Intuitionistic
Logic, since it does not prove both ℵ0 instances of excluded middle
principle 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 [
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
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 [
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 A ∧ B, Γ ` Δ ∧ −L Γ, Λ ` Δ, X, A ∧ B ∧ −R Γ ` Δ, A, B A, Γ ` Δ B, Λ ` X Γ ` Δ, A ∨ B ∨ −R A ∨ B, Γ, Λ ` Δ, X ∨ −L A, Γ ` Δ, B Γ ` Δ, A B, Λ ` X Γ ` Δ, A ⊃ B ⊃ −R A ⊃ B, Γ, Λ ` Δ, X ⊃ −L Γ ` Δ, A A, Γ ` Δ ¬A, Γ ` Δ ¬ − L Γ ` Δ, ¬A ¬ − R
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
∀xαA, Γ ` Δ ∀ − L Γ ` Δ, ∀xαA ∀ − R [bα/xα] A, Γ ` Δ Γ ` Δ, [tα/xα] A
∃xαA, Γ ` Δ ∃ − L Γ ` Δ, ∃xαA ∃ − R 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.
λ -rule:
Γ 0 ` Δ0 λ
Γ ` Δ
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.
[
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
` W 2 − R ` W 2 − L ` F F ` Cut Rules Γ ` Δ, B+ B+, Γ ` Δ Cut1 ` F F ` Cut2 Structural rules must fuΓlfi`l Δthe following constrain`ts: - 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 descendant of B+ and is a non-atomic formula. Moreover, at leaast 1 context set is non-empty.
- Cut2−formula F may be arbitrary.
Γ ` Δ Γ ` Δ, A+ W 1 − R
Γ ` Δ A+, Γ ` Δ
W 1 − L 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 constraints: - 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 λxiAo 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 quantified. 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 language;
- 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 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 [
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 ([
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 quantification, without chaotic or collapsing phenomena, is a main goal of our constructive 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ω.
A Normal Form Theorem (NFT) for a system V (see [
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 [
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¨odel number ([
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: 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, propositional 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 resulting 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ω
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:
G+ ∧ H+ ` G+ ∧ H+ ` G+ ∧ H+, ¬(G+ ∧ H+) ¬ − R
∨ −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 [
B+ ` B+ B+, ¬B+ ` ¬ − L
B`+¬∧(B¬+B+∧ ¬`B+)∧ −R ¬ − R 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 ≡ ⊥⊥`` B Rj of bottom 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 Theorem 6. Consider the following instance of non contradiction principle expressed 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 J 1 ≡⊥ ∧(B ∧ C) ` ⊥ and J 2 ≡⊥ ∧(B ∧ C) ` (B ∧ C): unfortunately, it is evident that the succedent of J 1 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 J 3 ≡⊥, B ∧ C ` ⊥ ∧(B ∧ C). J 3 can be the conclusion either of a ∧ − L or of a ∧−R. In the first case the possible premise is J 4 ≡ ⊥, B, C ` ⊥ ∧(B ∧C), in the second case the two possible premises, both necessarily Z∗ω-provable, are J 5 ≡⊥, B ∧ C ` ⊥ and J 6 ≡ ⊥, B ∧ C ` B ∧ C. However, the sucedent of J 5 can be only weakly introduced and the same problems observed for J 1 stop the examined possibility. Thus, we have to examine the possible provability of J 4. The possibility that J 4 is the conclusion of any ∧−R rule gives the same problems already noted for J 1 and J 5. We have then to suppose that the succedent of J 4 has been introduced in V only by a set of bottom rule occurrences, and that the ⊥ in the J 4-antecedent is the integral descendant of the premise formulas of such bottom rules. By Lemma 2, we delete such bottom rule occurrences and get a proof Z of the sequent J 7 ≡⊥, B, C ` where by construction B, C are the only integral ancestors of the auxiliary formulas of the ∧ − L with conclusion J 3 ≡⊥, B ∧ C ` ⊥ ∧(B ∧ C). But this is absurd, since both B and C in J 7 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 expressed by the sequent M : ` [> ∨ ∃xiB] ∨ ¬[> ∨ ∃xiB] 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
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. 4 It is not difficult to imagine that infinitely many sequents having a form similar to S are not Z∗ω−provable.