0
$\begingroup$

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?

$\endgroup$

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.