Let us consider Gentzen's propositional calculus with only one axiom: $$ \phi \vdash \phi $$

and 12 rules of inference.

As far as I know this PC is consistent, i.e. not all of their expressions (sequents) are provable. In the book I read (russian edition only, I suppose) there is a proof of this fact. But it uses an interpretation of PC: $$ f_X : \phi \to x,\qquad x\in \mathcal{P}(X), $$ where $X$ is some set. For example, $$ f_X(\neg\phi) = X\setminus f_X(\phi) $$ Then it is proven that the sequent $\phi\wedge\neg\phi$ is not provable: $$ f_X(\vdash\phi\wedge\neg\phi) = f_X(\phi) \cap X\setminus f_X(\phi) = \emptyset = X $$ which is false since $X$ is not empty.

I have a question here. In the above proof we used ''additional structure'' $f_X$ which is not part of calculus - its semantics. Question: how to prove the consistency of PC using only its syntax?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.