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.

| cite | improve this answer | |
  • $\begingroup$ What is definition of ''inuitionistically valid'',what is mean? $\endgroup$ – amir bahadory Nov 21 '15 at 21:11
  • $\begingroup$ There are several equivalent definitions of intuitionistic validity. One is deducibility in a certain formal system that you can surely find by googling. Another is truth in all Kripke models. Another is truth in all topological models. Another is having value 1 in all interpretations in Heyting algebras. See en.wikipedia.org/wiki/Intuitionistic_logic for details. $\endgroup$ – Andreas Blass Nov 21 '15 at 21:29
  • $\begingroup$ Thanks, excuseme ,why''((¬C)⟹=>(¬B))=>⟹(B=>⟹C) ''is not inuitionistically valid?,with truth table it has ''1 ''in every place. $\endgroup$ – amir bahadory Nov 21 '15 at 21:48
  • $\begingroup$ 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$. $\endgroup$ – Andreas Blass Nov 21 '15 at 22:33
  • $\begingroup$ 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. $\endgroup$ – Andreas Blass Nov 21 '15 at 22:34

Not the answer you're looking for? Browse other questions tagged or ask your own question.