Abstract

Our efforts in this work are mainly directed towards the statistical properties of tautologies and non-tautologies in intuitionistic logic. This article is a part of my master's thesis, which I defended at the Computer Science Department of Jagiellonian University in 2000. The inspiration for the thesis were the scientific works of the supervisor of my thesis dr hab. Marek Zaionc. In his [2] and [3] he dealt with typed lambda calculus considered over a finite number of ground types. His aim was to study the properties of types according to their length, defined as the number of occurrences of ground type variables in a type.The goal here is quite similar, though we start from a different definition of the length of a type. In this work the complexity measure function is defined as the height of its constructing tree. As we show the statistical behaviour of the type depends vitaly on the definition of its length. In Section 2 we prove that the asymptotic probability that a random one-variable formula is valid in intuitionistic logic is exactly 1, while by the linear definition of the length of a type this probability is equal to ${{1}\over{2}}+{{\sqrt{5}}\over{10}}$.In Section 3 we shall be concerned with formulas their corresponding types consist of more than one ground type. We define a subset of tautologies. Then we show that for each number k of ground type variables, and for each number $ n>1$, the ratio of types corresponding to this class of length n to all types of the same length n expressed as a fraction is always positive and at the same time bounded by ${1}\over{k}$. We show also that the similarly defined ratio of all types representing tautologies to all types expressed as a fraction is greater than ${1}\over{k} $, which implies that we have noticeably more tautologies than simple tautologies. However, it does not give us precise information about all tautologies. Later on in Section 3 we shall be occupied with a subset of non-tautologies whose asymptotic density is positive by the linear definition of the length of a type, and moreover, this density tends to 1 as k tends to infinity. We show that by our double exponential definition of the length of a type this density equals 0.In the last chapter we state some conjectures, which seem to hold but are not contained in this work.