# Proof complexity and lower bounds

One way to prove NP$\neq$ coNP is to show that for every propositional proof system $f$ computable in polynomial time, there exists a family of tautologies for which $f$ requires super polynomial proof lengths (w.r.t the length of tautology being proven). Results like that of Haken and Ajtai fix a propositional proof system and prove that a certain family (PHP in this case) requires super polynomial length proofs.

My Question: Are there results which do not fix a proof system and show, possibly very weak, but non-trivial lower bounds on proof length? For Example: Are there results showing that for every propositional proof system, there exists a family of tautologies which requires superlinear proof lengths?

Recall that we don't even know if SAT $\notin$ DTime(O(n)) so we also don't know if SAT$\notin$ coNTime(O(n)) which is equivalent to your question TAUT $\notin$ NTime(O(n)) and follows from a positive answer to your question.
{"ft_lang_label":"__label__en","ft_lang_prob":0.9093886,"math_prob":0.97732407,"size":717,"snap":"2022-40-2023-06","text_gpt3_token_len":155,"char_repetition_ratio":0.13464236,"word_repetition_ratio":0.054054055,"special_character_ratio":0.19246861,"punctuation_ratio":0.091603056,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99698627,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-09-30T22:25:27Z\",\"WARC-Record-ID\":\"<urn:uuid:baab0023-934c-4216-8343-9cea9b7c2d3d>\",\"Content-Length\":\"224460\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:9effdf9e-4909-42f5-9a0e-eaa167c48ce5>\",\"WARC-Concurrent-To\":\"<urn:uuid:abb48b6f-07ef-4e5b-bbca-66fd9064bbac>\",\"WARC-IP-Address\":\"151.101.65.69\",\"WARC-Target-URI\":\"https://cstheory.stackexchange.com/questions/20408/proof-complexity-and-lower-bounds\",\"WARC-Payload-Digest\":\"sha1:6QP565TAXA3G6KQ3PSQYE6B7RNDOIS7L\",\"WARC-Block-Digest\":\"sha1:OTASUI3MFQ75I4A4LGUHDORQF6ZMN7XQ\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030335504.37_warc_CC-MAIN-20220930212504-20221001002504-00080.warc.gz\"}"}