# New hilbert system and theorem [closed]

Let we have following axioms and modus ponens : $$(A1):(B ⇒ (C ⇒B ))$$ $$(A2):((B ⇒ (C ⇒D )) ⇒ ((B ⇒C ) ⇒ (B ⇒D )))$$ $$(A3):( ( B ⇒C) ⇒(¬C ) ⇒ (¬B ))$$

now can we prove following theorem ?

$\vdash _{H^,}$(((¬C ) ⇒ (¬B )) ⇒( B ⇒C ))

I can prove transitive law in this system.

No. Your axioms are intuitionistically valid and modus ponens preserves intuitionistic validity, but $((\neg C)\implies(\neg B))\implies (B\implies C)$ is not inuitionistically valid.
• I'm not sure what sort of truth table you have in mind for intuitionistic logic. But here's a Kripke model counterexample. The underlying partially ordered set (sometimes called a Kripke frame) consists of two elements $0$ and $1$, with $0<1$. The formula $C$ is true at $1$ and false at $0$, while $B$ is true at both $0$ and $1$. Then $(neg C)\implies(\neg B)$ is true at both $0$ and $1$ because $\neg C$ is false at both. But $B\implies C$ is true only at $1$, not at $0$. – Andreas Blass Nov 21 '15 at 22:33
• If you prefer a Heyting-algebra model, take the model to be a linearly ordered 3-element set, let the value of $B$ be the top element ("true") and let the value of $C$ be the middle element. – Andreas Blass Nov 21 '15 at 22:34