# On density of truth of the intuitionistic logic in one variable.

In this paper we focus on the intuitionistic propositional logic with one propositional variable. More precisely we consider the standard fragment {[right arrow], [disjunction], [perpendicular to]} of this logic and compute the proportion of tautologies among all formulas. It turns out that this proportion is different from the analog one in the classical logic case.

Keywords: density of truth, intuitionistic logic

1 Introduction

Intuitionistic logic is an important subsystem of the classical one. In intuitionisfic logic the effective interpretation and mechanical extraction of programs from proofs are allowed. The programming interpretation of intuitionisfic propositional logic by simply typed lambda-calculus is a significant part of interest of computer scientists. The intuitionisfic natural deductions are actually the same as simply [lambda] - terms (Curry-Howard isomorphism).

For any set of formulas A [subset] F we define its density, denoted by [mu](A), as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (1)

The length [parallel][alpha][parallel] of a formula a is defined in the standard way and [absolute value of B] means the cardinality of the set B. If A is the set of tautologies of a given logic, then [mu](A) is called the density of truth of this logic. Note that [mu](A) does not exists for some sets (or logics) A .

The density of truth, and other asymptotic properties of logics, appeared in literature. In the first place, the density was computed for various fragments of classical propositional logic (see (9), (13), (1) and (5)). The problem of equality between density of truth of classical and intuitionistic logic was raised by M. Moczurad, 7. Tyszkiewicz and M. Zaionc in (11). In the present paper we take this subject up.

In (11), the densities of truth for the purely implicational fragments of classical and intuitionistic logic, in a language with one variable, were computed. The densities appeared to be the same. The authors also conjectured, that even in a language with a larger than one number of variables, the densities of truth of implicational fragments of these logics are also equal. This conjecture was refuted by Kostrzycka in (6).

In (6), the conjecture was reformulated and it was posed that the densities of truth, for the appropriate fragments of classical and intuitionisfic logics are asymptotically equal if the number of variables tends to infinity. The modified conjecture was proved by Fournier, Gardy, Genitrini and Zaionc in (4). The authors applied there a very interesting estimation for the sets of tautologies and non-tautologies of the implicational fragments of classical and intuitionistic logics.

It is possible to extend the above mentioned result to the language with implication and negation. A new problem, however, appears. The implicational-negational fragment of classical logic is functionally complete which means that any formula can be translated into an implicational-negational one. This is no longer true for the intuitionisfic logic. It is known, for instance, that using n variables one can define, by means of implication or negation, only finitely many formulas (up to equivalence). Whereas, even in the case of one variable, the fragment {[right arrow], [disjunction], [logical not]} (which is equivalent to {[right arrow], [disjunction], [perpendicular to]}) of intuitionistic logic consists of infinitely many non-equivalent formulas. They may be exposed in the so-called Rieger-Nishimura lattice which will be given later on. In the present paper, we consider the fragment {[right arrow], [disjunction], [perpendicular to]} of intuitionistic logic, in a language with one variable p. The problem of computing the density of truth, for this fragment, is by no means more difficult than for any previously considered case, with finitely many non-equivalent formulas. All methods already used to compute the density, fail in the case of existing an infinite number of non-equivalent formulas. It is even not quite clear if the density ever exists. However, we give a positive answer to this question in the case of intuitionistic logic in one variable. We also provide some estimation of the density in the considered case.

2 Semantics for intuitionistic logic

Intuitionistic logic is a subsystem of the classical one. It can be defined by discarding, from a set of classical axioms, the law of excluded middle. Intuitionistic logic may be characterized by various types of semantics, see (10). There are considered, for instance, relational structures such as Kripke frames or Beth's tables, topological spaces or Heyting algebras. In our paper we focus on the algebraic characterization of the intuitionistic logic.

Definition 1 A Heyting algebra is a pair (B, [less than or equal to]) where B is a non-empty set and [less than or equal to] is a lattice ordering on B with the least element [perpendicular to] and the pseudo-complement a [right arrow] b := max{c : c [conjunction] a [less than or equal to] b} for each a, b [member of] B.

The greatest element is defined as T = [perpendicular to] [right arrow] [perpendicular to] and [logical not] a = a [right arrow] [perpendicular to] is the complement of the element a. A valuation from the set V ar of propositional variables to a (B, [less than or equal to]) is a function h : V ar [right arrow] B. The valuation extends to all formulas in {[right arrow], [conjunction], [disjunction], [perpendicular to]} as a homomorphism.

Formula [alpha] is valid in (B, [less than or equal to]) if h([alpha]) = T for each valuation h. Formula a is an intuitionistic tautology if it is valid in any Heyting algebra. For example, the law of excluded middle could be falsified in the following algebra, see Figure 1.

[FIGURE 1 OMITTED]

3 Generating functions

In our paper we deal with sequences of numbers of formulas. We consider different classes of formulas (e.g. class of tautologies) and count number of formulas with the established length. To determine limits of such sequences we use generating functions. An exhaustive presentation of this method can be found, for instance, in (2) and (12). We take advantage of the Drmota-Lalley-Woods theorem; see (2), Thm. 8.13, p.71. Suppose we have two generating functions [f.sub.A] and [f.sub.F] representing, respectively, formulas from the class A and all formulas. Suppose they have the same dominant singularity [rho] and there are suitable constants [[alpha].sub.1], [[alpha].sub.2], [[beta].sub.1], [[beta].sub.2] such that:

[f.sub.A](z) = [[alpha].sub.1] - [[beta].sub.1] [square root of 1- z/[rho]] + O(1 - z/[rho]), [f.sub.F](z) = [[alpha].sub.2] - [[beta].sub.2] [square root of 1- z/[rho]] + O(1 - z/[rho]), (2)

Then the density of the class A is given by:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (3)

4 Intuitionistic logic in one variable

In this section we consider the fragment {[right arrow], [disjunction], [perpendicular to]} of intuitionisfic logic, in a propositional language with one variable p. Let

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

In the set of all formulas F we introduce an equivalence relation [equivalent to] in the standard way:

Definition 2 [psi] [equivalent to] [psi] if both [psi] [right arrow] [psi] and [psi] [right arrow] [psi] are intuitionistic tautologies.

Every formula from our language F falls into one of the equivalence classes [A.sup.m] = [[[[alpha].sup.m].sub.[equivalent to]]]. Therefore, up to this equivalence relation on the classes of formulas A', the quotient algebra rises to the so-called Rieger--Nishimura lattice R, which is a single-generated free Heyting algebra (see Figure 2).

The above algebra is a nice example of a finitely generated free algebra, which is infinite. Let us stress, that [A.sup.[omega]] is the class of intuitionisfic tautologies in the considered language. Our purpose is to compute the density [mu] ([INT.sup.{[right arrow], [disjunction] [perpendicular to]}.sub.{p}]) = [mu]([A.sup.[omega]]) if it exists. This is directly related to computing (and proving the existence) the density of the class [A.sup.m] for each m [greater than or equal to] 0. There are infinitely many classes, so the methods which are effective in the cases of finite algebras (and logics) must be now modified.

The length of a formula is defined as follows:

Definition 3

[parallel]p[parallel] = 1, [parallel][perpendicular to][parallel] = 1, [parallel][phi][right arrow][psi][parallel] = [parallel][phi][parallel] + [parallel][psi][parallel], [parallel][phi][disjunction][psi][parallel] = [parallel][phi][parallel] + [parallel][psi][parallel]

[FIGURE 2 OMITTED]

By [F.sub.n] we mean the set of formulas of the length n and, by [absolute value of [F.sub.n]], the cardinality of [F.sub.n]. We will also consider some subclasses of [F.sub.n], For any B [subset] F, we take [B.sub.n] = B [intersection] [F.sub.n] and, by [absolute value of [B.sub.n]], we denote the cardinality of the class [B.sub.n],

Lemma 4 The generating function f for the numbers [absolute value of [F.sub.n]] is the following:

f(z) = 1 - [square root of 1 - 16z] / 4 (4)

Proof. The number [absolute value of [F.sub.n]] of formulas from [F.sub.n] is given by the recursion:

[absolute value of [F.sub.0]] = 0, [absolute value of [F.sub.1]] = 2, [absolute value of [F.sub.n]] = 2[n-1.summation over (i=1)] [absolute value of [F.sub.i]][absolute value of [F.sub.n-i]] (5)

Hence the function f has to fulfil the equation: f(z) = 2[f.sup.2](z) + 2z. With the boundary condition: f(0) = 0 we obtain (4).

5 Quotient algebras

In this section we give a practical approach to the problem of computing the density of truth in the case of infinite Rieger-Nishimura lattice.

It can be immediately seen from the definition that the density [mu] is finitely additive. So, if A and B are disjoined classes of formulas such that [mu](A) and [mu](B) exist, then [mu](A [union] B) exists as well and

[mu](A [union] B) = [mu](A) + [mu](B). (6)

Unfortunately, the density [mu] is not countably additive. We only have the following inequality:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (7)

In the case of Rieger--Nishimura lattice R, we have [[union].sup.[infinity].sub.i=0] [A.sub.i] [union] [A.sup.[omega]] = F and hence we get [mu][[union].sup.[infinity].sub.i=0] [A.sub.i] [union] [A.sup.[omega]] = 1. In this section we show that [mu]([A.sub.i]) exists for any i [member of] N. In Section 9 we prove the existence of [mu]([A.sub.[omega]]). Before we are able to do it, we consider finite quotient algebras obtained from the Rieger--Nishimura lattice R.

Definition 5 Let (B, [less than or equal to]) be a Heyting algebra. A nonempty set D [subset] B is a filter if. 1) a [conjunction] b [member of] D, for any a, b [member of] D; 2) if a [member of] D and a [less than or equal to] c, then c [member of] D.

By [[A.sup.2n-1]) we mean a filter in the algebra R generated by the element [A.sup.2n-1]. Formally, [[A.sup.2n-1]) = {[alpha] [member of] F : [[alpha].sup.2n-1] [right arrow] [alpha] [member of] [A.sup.[omega]]}, n [greater than or equal to] 1.

We consider a sequence of quotient algebras obtained from the algebra R by division by the filters: [[A.sup.2n-1]) for n [greater than or equal to] 2. Every such algebra consists of 2n elements, so we will denote it as [AL.sub.2n]. We have:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], ...

[FIGURE 3 OMITTED]

Let us notice that the filters [[A.sup.2n-1]), n [greater than or equal to] 2 form the following decreasing sequence:

[[A.sup.3]) [contains] [[A.sup.5]) [contains] ... [contains] [[A.sup.2n-1]) [contains] .... [contains] [[A.sup.[omega]]) (8)

Theorem 6 The density [mu]([A.sup.k]) exists for any k [member of] N.

Proof. The idea of the proof is to take some finite quotient algebra [AL.sub.2n] such that 2n > k - 3 and show that the appropriate system of 2n equations fulfils the assumptions of the Drmota-Lalley-Woods theorem. Formally, the proof should proceed by induction but we present here only the basic step. Let us consider the algebra [AL.sub.4]. The operations {[right arrow], [disjunction]} in the algebra are given by the following truth-tables:
```Table 1.

[right arrow] [A.sup.0] [A.sup.1][union]
[A.sup.4]

[A.sup.0] [[A.sup.3]) [[A.sup.3])
[A.sup.1][union] [A.sup.2] [[A.sup.3])
[A.sup.4]
[A.sup.2] [A.sup.1][union] [A.sup.1][union]
[A.sup.4] [A.sup.4]
[[A.sup.3]) [A.sup.0] [A.sup.1][union]
[A.sup.4]

[right arrow] [A.sup.2] [[A.sup.3])

[A.sup.0] [A.sup.3]) [[A.sup.3])
[A.sup.1][union] [A.sup.2] [[A.sup.3])
[A.sup.4]
[A.sup.2] [A.sup.3]) [[A.sup.3])
[A.sup.3]) [A.sup.2] [[A.sup.3])

V [A.sup.0] [A.sup.1][union]
[A.sup.4]
[A.sup.0] [A.sup.0] [A.sup.1][union]
[A.sup.4]
[A.sup.1][union] [A.sup.1][union] [A.sup.1][union]
[A.sup.4] [A.sup.4] [A.sup.4]
[A.sup.2] [A.sup.2] [[A.sup.3])
[[A.sup.3]) [[A.sup.3]) [[A.sup.3])

V [A.sup.2] [[A.sup.3])

[A.sup.0] [A.sup.2] [[A.sup.3])

[A.sup.1][union] [[A.sup.3]) [[A.sup.3])
[A.sup.4]
[A.sup.2] [[A.sup.3]) [[A.sup.3])
[[A.sup.3]) [[A.sup.3]) [[A.sup.3])
```

The appropriate generating functions [f.sub.0], [f.sub.1] + [f.sub.4], [f.sub.2], [f.sub.[3)] for the classes [A.sup.0], [A.sup.1] [union] [A.sup.4], [A.sup.2], [[A.sup.3]) fulfil the following system of equations:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (9)

From the Drmota-Lalley-Woods theorem we conclude that all the functions have the same dominant singularity. Actually, it is the same singularity as the one of the function f. Hence [z.sup.0] = 1/16 is the common singularity and the densities of the classes [A.sup.0], [A.sup.1] [union] [A.sup.4], [A.sup.2], [[A.sup.3]) exist.

Analogous situation holds for the algebra [AL.sub.2n] for any n > N. All involved functions have the same dominant singularity [z.sup.0] = 1/16. Hence densities of all classes of formulas from [AL.sub.2n] exist. Among these classes we have the class of true formulas in [AL.sub.2n], which is denoted as [[A.sup.2n-1]).

From Theorem 6 and inclusions (8) it follows that:

Corollary 7 The density [mu]([[A.sup.2n-1])) exists for any n [member of] N and the following inequalities hold:

[mu]([[A.sup.3])) [greater than or equal to] [mu]([[A.sup.5])) [greater than or equal to] ... [greater than or equal to] [mu]([[A.sup.2n-1])) [greater than or equal to] ... (10)

6 Calculation of the basic generating functions

In this section we calculate the generating functions for the classes: [A.sup.0], [A.sup.1] [union] [A.sup.4], [A.sup.2], [[A.sup.3]). To solve the system of equations (9) we use strictly algebraical methods, i.e. division by filters. The method is presented with all details in (7) and (8). Roughly speaking, we take two filters: [[A.sup.2]) and [[A.sup.1]), and two quotient algebras: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], which are two-element algebras. In the first one we have classes: [[A.sup.2]) and [A.sup.0] [union] [A.sup.1] [union] [A.sup.4], in the second one: [[A.sup.1]) and [A.sup.0][union] [A.sup.2].

Let us consider the second algebra [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and let [f.sup.*.sub.0] := [f.sup.0] + [f.sup.2]. We can draw an appropriate truth table for the operations: [right arrow], V and obtain a suitable equation for the function [f.sup.*.sub.0]. It is: [f.sup.*.sub.0] = [f.sub.[1)] x [f.sup.*.sub.0] + [([f.sup.*.sub.0]).sup.2] + z. Also: [f.sub.[j)] = f - [f.sup.*.sub.0]. Hence after simplification we get: [f.sup.*.sub.0] = z / 1 - f.

Analogously, we obtain the generating function [f.sup.**.sub.0] for the class [A.sup.0] [union] [A.sup.1] [union] [A.sup.4] in the algebra [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. It is: [f.sup.**.sub.0] = 2z / 1 - f. Hence [f.sup.**.sub.0] = 2[f.sup.**.sub.0]. Having the functions [f.sup.*.sub.0] and [f.sup.**.sub.0] we can determine the generating functions for the classes from algebra [AL.sub.4].

Lemma 8 The generating function [f.sub.0] for the class [A.sup.0] is the following:

[f.sub.0](z) = 1 / 4 (1 + 3[f.sup.*] - f - [square root of [(1 + 3[f.sup.*] - f)sup.2] - 8z), (11)

where f is defined by (4) and [f.sup.*] = z / 1 - f.

Proof. In the first equation from (9) we put: [f.sub.[3)] = f - [f.sup.*.sub.0] - [f.sup.**.sub.0] + [f.sup.0] and [f.sup.**.sub.0] = 2[f.sup.*.sub.0]. Then we obtain an equation with the one unknown function [f.sub.0].

[f.sub.0](z) = [f(z) - 3[f.sup.*.sub.0](z) + [f.sub.0](z)] x [f.sub.0](z) + [[[f.sub.0](z)].sup.2] + z. (12)

It is a quadratic equation and after solving it with the condition [f.sub.0](0) = 0 we obtain (11).

Having the function [f.sub.0] we obtain the other generating functions from [AL.sub.4].

([f.sub.1] + [f.sub.4]) = 2[f.sup.*] - [f.sub.0], [f.sub.2] = [f.sup.*] - [f.sub.0], [f.sub.[3)] = f - [f.sub.0] - ([f.sub.1] + [f.sub.4]) - [f.sub.2] (13)

We expand the functions f, [f.sub.0], ([f.sub.1] + [f.sub.4]), [f.sub.2] and [f.sub.[3)] in a neighborhood of [z.sub.0] = 1/16 and, by use of the transfer lemma, we obtain:

Lemma 9 The densities of the classes of formulas from the algebra [AL.sub.4] are the following:

[mu]([A.sup.0]) [approximately equal to] 0.069, [mu]([A.sup.1] [union] [A.sup.4]) [approximately equal to] 0.153, [mu]([A.sup.2]) [approximately equal to], [mu]([[A.sup.3])) [approximately equal to] 0.736

Analogously, we determine the generating functions for the classes from algebra [AL.sub.6]. Obviously, the functions [f.sub.0] and [f.sub.2] are already given. Using again division by filters, we are able to solve the appropriate system of six equations. It is not difficult to define the functions [f.sub.1], [f.sub.4], ([f.sub.3] + [f.sub.6]), [f.sub.[5)] explicitly, expand them around [z.sub.0] = 1/16, use the transfer lemma and obtain:

Lemma 10 The densities of the classes from the algebra [AL.sub.6] are the following:

[mu]([A.sup.1]) [approximately equal to] 0.1315, [mu]([A.sup.3] [union] [A.sup.6]) [approximately equal to] 0.0244, [mu]([A.sup.4]) [approximately equal to] 0.02164, [mu]([[A.sup.5])) [approximately equal to] 0.71099,

7 Upper bound of the density of INT

In this section we estimate the density of [INT.sup.{[right arrow], [disjunction],[perpendicular to]}.sub.{p} by densities of the filters [[A.sup.2k-1]). Let us consider the algebra [AL.sub.2k]; see Figure 4.

[FIGURE 4 OMITTED]

Directly from the diagram of [AL.sub.2k] we can read out how formulas from the class [[L.sup.2k-1]) are obtained. They arise as implications from [A.sup.0] to any other class, and from [A.sup.1] to any other class, with the exception of [A.sup.0] and [A.sup.2], and so on. They also arise as disjunctions between formulas from [A.sup.2k-4] [union] [A.sup.2k-3] [union] [A.sub.2k] and [A.sub.2k-2], and from [[A.sub.2k-1]) and any other class. To write it precisely, we introduce the following abbreviation: [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for [??] [member of] {[right arrow], V}. Hence we have:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (14)

Of course, the sum written above as '...' is finite in the case of finite algebra [AL.sub.2k]. After simplification, the above formula may by transformed into the following one:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Note that all generating functions, related to the algebra [AL.sub.2n], are involved in the above equation. It is possible to determine the functions [f.sub.[2n-1)] explicitly, for any n [member of] N. We skip all details, the same methods as in (7) and (8) should be used here. Let us add that the growing index n involves increase of the number of nested square roots in the formula defining [f.sub.[2n-1)]. It is not difficult to compute the density of the class of valid formulas for the next two algebras: [AL.sub.8] and [AL.sub.10]. They are as follows: [mu]([[A.sup.7])) [approximately equal to] 0.709016 and [mu]([[A.sup.9])) [approximately equal to] 0.709011. From the inequality (10) we get:

Observation 11 If the density of [mu]([A.sup.[omega]) exists then [mu]([A.sup.[omega]) < 0.709011 .

8 Lower bound of the density of INT

Let us consider the algebra R. As we see in Figure 1, the formulas from the class ([A.sup.[omega]) are either implications or some special disjunctions. In these disjunctions at least one formula comes from ([A.sup.[omega]). Hence, analogously as in the previous section, we may write down the set of intuitionisfic tautologies ([A.sup.[omega]) as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (15)

Observation 12 Let ([c.sub.n]), ([d.sub.n]) and ([e.sub.n]) be three sequences of natural numbers, such that [c.sub.n] [greater than or equal to] [d.sub.n] for all n [member of] N. Suppose two new sequences are defined recursively as follows:

[x.sub.n] = [c.sub.n] + [n-1.summation over (i=1)] [e.sub.i] x [x.sub.n-i], [y.sub.n] = [d.sub.n] + [n-1.summation over (i=1)] [e.sub.i] x [y.sub.n-i],

Then [x.sub.n] [less than or equal to] [y.sub.n] for any n [member of] N.

We will consider subset of [A.sup.[omega]]. We just omit the infinite part in the formula (15), which is written as '...'. The omitted sets consists of formulas which are implications. The new set is denoted as [B.sup.5] and the superscript 5 is due to the fact that all intuitionistically valid implications, with the predecessor in [A.sup.n], for n > 5, do not appear in [B.sup.5].

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (16)

On the basis of Observation 12 we conclude that [absolute value of [B.sup.5.sub.n]] [less than or equal to] [absolute value of [A.sup.[omega].sub.n]] for any n [member of] N. The generating function [g.sub.5], for [absolute value of [B.sup.5.sub.n]] is the following:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (17)

The function [g.sub.5] is obtained from the generating functions for classes of formulas from [AL.sub.8]. So, [z.sub.0] = 1/16 is its dominant singularity and its density exists.

Lemma 13 The density of the class [B.sup.5] exists and [micro]([B.sup.5]) [approximately equal to] 0.7068.

From Lemma 13 and Observations 11 and 12 we obtain a quite tight estimation of the density of truth of intuitionistic tautologies.

Theorem 14 If the density of the class [A.sup.[omega]] exists, then it is estimated as follows:

0.7068 [less than or equal to] [mu]([A.sup.[omega]]) [less than or equal] 0.709011 (18)

9 Existence of the density

In this section we prove that the density of truth [mu]([A.sup.[omega]]) exists. We define two sequences of sets (and numbers) approximating the set [A.sup.[omega]] (and [absolute value of [A.sup.[omega].sub.n]]). Let us consider the sequence ([B.sup.2k.sub.n]) of smaller than [A.sup.[omega].sub.n] sets defined analogously as the set [B.sup.5.sub.n] in the previous section:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (19)

The formula (19) defines the cardinalities of subsets of some set [B.sup.2k], with k [greater than or equal to] 2, which is a proper subset of [A.sup.[omega]]. Hence on the basis of Observation 12 and inclusions (8) we get the following inclusions:

[B.sup.4] [subset] [B.sup.6] [subset] ... [subset] [A.sup.[omega]] [subset] ... [subset] [[A.sup.5]) [subset] [[A.sup.3]). (20)

Let us consider the sequence of compartments [[mu]([B.sup.2k]), [mu]([[A.sup.2k-1]))], for k [greater than or equal to] 2, and show that their 'lengths' tend to 0.

Lemma 15

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (21)

Proof. We consider the numbers [absolute value of [[A.sup.2k-1]).sub.n]] - [absolute value of [B.sup.2k.sub.n]]. From (14) and (19) we obtain:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (22)

The numbers [[summation].sup.n-1.sub.i=1] p[absolute value of [A.sup.2k-1.sub.i]] x [absolute value of [[A.sup.2k-1]) .sub.n-i]] are non-negative, so on the base of Observation 12 we may consider larger numbers [absolute value of [C.sup.k.sub.n]]:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (23)

The numbers [absolute value of [C.sup.k.sub.n]] characterize the set [C.sup.k] consisting of formulas being disjunctions between formulas from [A.sup.2k-2] and [A.sup.2k-4] [union] [A.sup.2k-3] [union] [A.sup.2k], and implications from [A.sup.2k] to [A.sup.2k-3] [union] [A.sup.2k-1] [union] [A.sup.2k+2], and disjunctions between formulas from [C.sup.k] and formulas from F.

From the above we obtain formulas defining the generating functions [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] for the numbers [absolute value of [C.sup.k.sub.n]]:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (24)

The function [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] is defined by functions with dominant singularity at [z.sub.0] = 1/16 (see proof of Theorem 6). So, it has the same dominant singularity. The density of the class [C.sup.k] can be computed as follows:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (25)

We show that the values of [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] tend to 0 when k tends to infinity. For simplicity, we introduce a new symbol [h.sub.k] := [f.sub.2k] x ([f.sub.2k-3] + [f.sub.2k-1] + [f.sub.2k+2]) + 2[f.sub.2k-2] x ([f.sub.2k-4] + [f.sub.2k-3] + [f.sub.2k]). Then, from (25), we have:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (26)

The values of f(1/16) and f'(1/16) exist and are constant. To prove that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (27)

we prove that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (28)

It is straightforward to observe that (28) yields (27). From Theorem 6 it follows that [mu]([A.sup.k]) exists for each k [member of] N. By (7), the series [[summation].sup.[infinity].sub.k=0] [mu] ([A.sup.k]) is convergent and hence [lim.sub.k[right arrow][infinity]] [mu] ([A.sup.k]) = 0. So, from the transfer lemma (we know that the functions [f.sub.k] have the same dominant singularity) we obtain:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (29)

Similarly, let us consider the series [[summation].sup.[infinity].sub.k=0] [f.sub.k] (1/16). This series is bounded by f (1/16) = 1/2 and the values [f.sub.k] (1/16) are non-negative [sup.(i)], so it also must be convergent. Hence:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] (30)

By Theorem 14 and Lemma 15 we get:

Theorem 16 The density of the class [A.sup.[omega]] exists and is about 70%.

Let us compare the above result with the one we can get for the classical logic:

Observation 17 The algebra [AL.sub.4] is the Lindenbaum algebra of the classical logic {[right arrow], [disjunction], [perpendicular to]} in one variable. Hence

[mu](CL.sup.{[right arrow], [disjunction], [perpendicular to]}.sub.{p}) = [mu]([[A.sup.3])) [approximately equal to] 0.736 (31)

By Theorem 14 and Observation 17 we immediately have:

Theorem 18 The relative density of intuitionistic tautologies among classical ones in the language {[right arrow], [disjunction], [perpendicular to], p} is more than 96%.

We conjecture that the density of truth for [INT.sup.{[right arrow], [disjunction], [perpendicular to]}.sub.m] exists for any m [greater than or equal to] 1, where m is the number of variables occurring in the language. The following problem appears:

Problem 1 Whether, or not, the logics [INT.sup.{[right arrow], [disjunction], [perpendicular to]}.sub.m] and [CL.sup.{[right arrow], [disjunction], [perpendicular to]}.sub.m] are asymptotically identical.

It seems to be important to work out a new and effective method for calculation (or estimation) the density of truth in the case of logics with infinite number of non-equivalent formulas. Any semantical approach to this question usually involves extremely complicated calculations. More promising seem to be syntactical approaches where one can analyze shapes of binary trees. However, these methods also need some refinement as, for instance, formulas from {[right arrow], [disjunction]} have not been yet investigated as binary trees.

References

[1] B. Chauvin B., Flajolet P., Gardy D., Gittenberger B. AndOr trees revisited, Combinatorics, Probability and Computing, 13(4-5), July-September 2004, pp 475-497.

[2] Flajolet P. and Sedgewick R. Analitic combinatorics: functional equations, rational and algebraic functions, INRIA, Number 4103, 2001.

[3] Flajolet P. and Odlyzko A. M. Singularity analysis of generating functions, SIAM J. on Discrete Math., 3(2), 1990, pp 216-240.

[4] Fournier H., Gardy D., Genitrini A., Zaionc M. Classical and intuitionistic logic are asymptotically identical,Lecture Notes in Computer Science 4646, pp. 177-193.

[5] Gardy D. and Woods A.R. And/or tree probabilities of Boolean functions, Discrete Mathematics and Theoretical Computer Science, 2005, pp 139-146.

[6] Kostrzycka Z. On the density of implicational parts of intuitionistic and classical logics, Journal of Applied Non-Classical Logics, Vol. 13, Number 3, 2003, pp 295-325.

[7] Kostrzycka Z. and Zaionc M. Statistics of intuitionistic versus classical logics, Studia Logica, Vol. 76, Number 3, 2004, pp 307-328.

[8] Kostrzycka Z. and Zaionc M. Asymptotic densities in logic and type theory, Studia Logica, Vol. 88, 2008, pp 385-403.

[9] Lefmann H., Savicky P. Some typical properties of large and/or boolean formulas, Random Structures and Algorithms, 10, 1997, pp 337-351.

[10] Mints G. A Short Introduction to Intuitionistic Logic. The University Series in Mathematics, Kluwer Academic/Plenum Publishers, Stanford 2000.

[11] Moczurad M., Tyszkiewicz J., Zaionc M. Statistical properties of simple types, Mathematical Structures in Computer Science, vol 10, 2000, pp 575-594.

[12] Wilf H.S. Generatingfunctionology. Second edition. Academic Press, Boston 1994.

[13] Woods A.R. Coloring Rules for Finite Trees, and Probabilities of Monadic Second Order Sentences, Random Structures Algorithms 10, (4), 1997, 453-485.

(i) It could be justified as follows: for each i [member of] N, [f.sub.i](1/16) [greater than or equal to] 0 because [f.sub.i](z) = [[summation].sup.[infinity].sub.n=0] [a.sub.in][z.sup.n] and the series is convergent at [z.sub.0] = 1/16 and then the sum [[summation].sup.[infinity].sub.n=0] [a.sub.in][(1/16).sup.n] is also non-negative.

Zofia Kostrzycka

University of Technology

Luboszycka 3, 45-036 Opole, Poland

E-mail z.kostrzycka@po.opo1e.pl