Intuitionistic vs. Classical Tautologies, Quantitative Comparison

We consider propositional formulas built on implication. The size of a formula is the number of occurrences of variables in it. We assume that two formulas which differ only in the naming of variables are identical. For every n ∈ N, there is a finite number of different formulas of size n. For every n we consider the proportion between the number of intuitionistic tautologies of size n compared with the number of classical tautologies of size n. We prove that the limit of that fraction is 1 when n tends to infinity1 .

• Type: Conference
• Year: 2007
• Where: TYPES
• Authors: Antoine Genitrini, Jakub Kozik, Marek Zaionc
• Keywords: Formal Methods, Formulas, Propositional Formulas, TYPES 2007, finite Number