Propositional consistency proofs (Q1177033)

Let \(\text{Con}_{\text{ZF}(n)}\) be the statement that there is no ZF- proof of a contradiction using at most \(n\) symbols. Then, of course, \(\forall n \text{Con}_{\text{ZF}(n)}\) is not provable in ZF; but \(\text{Con}_{\text{ZF}(n)}\) is for each numeral \(n\), and, indeed, within a polnomial of \(n\) steps. The author presents similar results in propositional calculi. A choice of (propositional) connectives and (a finite number of) axiom schemes, together with modus ponens as the only rule of inference constitute a Frege system. (Of course, completeness is required.) Of any two such systems \(\mathcal F\) and \(\mathcal G\), the autor (i) produces a polnomial \(p(n)\) such that \(\mathcal F\) proves \(\text{Con}_{\mathcal G}(n)\) within \(p(n)\) symbols, and (ii) presents a new proof of a result of Reckhow that \(\mathcal F\) and \(\mathcal G\) \(p\)-simulate each other (i.e. a proof of \(\mathcal F\) is translatable in \(\mathcal G\) within polynomial growth rate, and vice versa). Let \(e{\mathcal F}\) be the extension of \(\mathcal F\) by addition of the rule that allows the derivation of \(p\leftrightarrow\varphi\) where \(p\) is a new variable which has not been used yet and does not appear in \(\varphi\) or in the last line of the proof. The last result is: (iii) \(\mathcal F\) \(p\)-simulates \(e{\mathcal F}\) iff \(\mathcal F\) proves \(\text{Con}_{e{\mathcal F}}(n)\) with a polynomial bound of \(n\). To code meta-mathematical notions into propositional languages, and within polynomial bounds at that, requires much skill and elaborate work: hence the length of the paper. Indeed, for instance, the natural definition of a formula being depth \(k\) subformula of another grows faster than any polynomial of \(k\), and so the author devises a new definition that is polynomially bounded. With good explanations and examples, he makes the flow of thought clear.