Is $(\phi\implies \psi) \iff ((\phi\land \psi)\lor \neg \phi) $ in the following hilbert calculus without contraposition or reductio ad absurdum? If so, how would I go about proving it, and if not, how would I prove that it is not derivable?

Inference Rules: Modus Ponens


$\phi \implies (\psi \implies \phi)$

$(\phi \implies (\chi \implies \psi)) \implies ((\phi \implies \chi) \implies (\phi \implies \psi))$

$(\phi \land \psi)\implies\phi; (\phi \land \psi) \implies \psi $

$\phi \implies (\psi \implies (\phi \land \psi)) $

$\phi \implies (\phi \lor \psi); \psi \implies (\phi \lor \psi) $

$(\phi \implies \psi) \implies ((\chi \implies \psi) \implies ((\phi \lor \chi) \implies \psi)) $

Biimplication is defined as usual.

$\phi\iff\neg\neg\phi $

$\neg (\phi \land \psi) \iff (\neg \phi \lor \neg \psi) $

$\neg (\phi \lor \psi) \iff (\neg \phi \land \neg \psi) $

$\phi \lor \neg \phi $

Here is my current attempt at proving one side of the conditional

  • 1
    $\begingroup$ The formula in the title of your question is not the same as the one in the body. As regards your question, finding proofs for this kind of thing in a Hilbert calculus is usually fairly tedious and IMO the best way is to see if you can transform the Hilbert calculus into a more tractable sequent calculus and then work in the sequent calculus (this typically involves proving the deduction theorem). Proving that a formula is not provable usually involves building models. $\endgroup$
    – Rob Arthan
    Dec 8, 2023 at 21:18
  • $\begingroup$ @RobArthan I fixed the title. I'm not familiar with sequent calculi, do you know a resource about them that would help? $\endgroup$
    – The Sea
    Dec 8, 2023 at 21:21
  • $\begingroup$ Well you could have a look at the Wikipedia page on sequent calculi, but if you don't know about them already, it might be a big detour. Can you say a bit more about the context: is this a course problem or are you working from a textbook? $\endgroup$
    – Rob Arthan
    Dec 8, 2023 at 21:32
  • $\begingroup$ @RobArthan I'm working through a logic textbook, but this isn't from the textbook; I've been messing around with axioms trying to see the effects of removing various ones or adding ones to see how it effects what is derivable in the logic, but I've been at this for a day and I have no idea how to proceed. $\endgroup$
    – The Sea
    Dec 8, 2023 at 21:37
  • 1
    $\begingroup$ @PW_246 so it turned out the other side of the biconditional is not provable in a stronger system that this logic happens to be a substructural logic of, meaning it's not provable in this system. $\endgroup$
    – The Sea
    Jan 18 at 0:49

1 Answer 1


The following tables satisfy the above axioms:


{1, 2} are the designated values.

Counterexample at 2, 3. ((ϕ ∧ ψ) ∨ ¬ϕ) is designated there but (ϕ⟹ψ) is not. Therefore the other side of the biconditional is not provable in this logic. □


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .