Asymptotic density as a method of expressing quantitative relations in intuitionistic logic
Grzegorz Soza · Jagiellonian University Repository (Jagiellonian University) · 2002
A b s t r a c t.Our efforts in this work are mainly directed towards the statistical properties of tautologies and non-tautologies in intuitionistic logic (which is equivalent to research in typed lambda calculus because of the Curry-Howard isomorphism, see [1]).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 (the "length" of a type) 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 (defined precisely there) that a random onevariable formula is valid in intuitionistic logic (with implication only) is exactly 1, while by the linear definition of the length of a type (as discussed in [2] and [3]) this probability is equal to 1 2 + √ 5 10 .In Section 3 we shall be concerned with formulas their corresponding types consist of more than one ground type.We define a subset