{'fraction_non_alphanumeric': 0.019536019536019536, 'fraction_numerical': 0.001221001221001221, 'mean_word_length': 4.985401459854015, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On the lengths of proofs in the propositional calculus (Preliminary Version)

One of the most important open questions in the field of computational complexity is the question of whether there is a polynomial time decision procedure for the classical propositional calculus.
 The purpose of the present paper is to study a question related to the complexity of decision procedures for the propositional calculus; namely, the complexity of proof systems for the propositional calculus. The fundamental issue here is whether there exists any proof system, and a polynomial p(n) such that every valid formula has a proof of length not exceeding p(n), where n is the length of the formula. Theorem 1 below helps establish the importance of this question. For the purposes of this theorem, we give the following definitions.