# Is it possible to prove that propositional calculus is consistent using only its syntax?

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?