1

Consider the classical propositional calculus system (Hilbert system) with three axiom shemes: (1) $A \to (B \to A)$, (2) $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$, (3) $(\neg A \to \neg B) \to (B \to A)$. And you can use modus ponens.

Now we add a new axiom scheme: $(\neg A \to B) \to (A \to \neg B)$.

Sure this is not always true. But how to (formally, in the sense of propositional calculus) prove adding this results an inconsistent system? I.e., you can deduce $A$ and $\neg A$ for some wf.

For simplicity, you can use the deduction theorem and the hypothetical syllogism. I need a formal proof obeying the rules of the propositional calculus.

PinkRabbit
  • 798

2 Answers2

1

Axiom scheme 1 with $\lnot B$ replacing $B:$ $$ A \to (\lnot B \to A). $$ New axiom scheme with letters $A,B$ interchanged: $$(\lnot B \to A) \to (B \to \lnot A).$$ Modus ponens on last two lines: $$A \to (B \to \lnot A).$$ Axiom scheme 3 with $C=\lnot A$ and modus ponens applied to this: $$ (A \to B) \to (A \to \lnot A).$$ In this replace $B$ by $A$: $$(A \to A) \to (A \to \lnot A)$$ At this point I need to invoke $A \to A.$ [I did not get that from Hilbert's axioms, but surely it must follow from them] If I can do that, next apply modus ponens and get to: $$A \to \lnot A.$$ This is a contradiction, since it implies every proposition is false, for example we could replace $A$ here by the entire axiom scheme 1, call that $U,$ then modus ponens, and arrive at a proof that $U$ and $\lnot U$ both hold.

coffeemath
  • 7,403
  • 1
    Great, thanks! Though I found that all $B$'s can be replaced by $A$. Just as the other answer. – PinkRabbit Mar 23 '23 at 07:00
  • Seems more complicated than my earlier proof, using unnecessary schemes. Where does my own proof need more, please? – Laska Mar 23 '23 at 07:01
  • @Laska Initially thought your proof odd by starting with the informal sentence "Suppose we know something A". However that can be circumvented by simply letting A stand for one of the axioms. Since in a proof one can always put an axiom as a line of the proof, all works fine. – coffeemath Mar 23 '23 at 07:09
  • Formality has its place but can be opaque in explanation and lead to inelegant approach. Obv formal & informal approaches complement one another – Laska Mar 23 '23 at 08:46
0

I’m not familiar with Hilbert systems, so apologies for imprecisions.

Suppose we know something:

$A$

Then under your axiom scheme (1) we can legitimately derive:

$\neg A \to A$

Now we apply your new naughty axiom scheme to deduce:

$A \to \neg A$

And since we already know $A$, we can apply modus ponens to this, inferring:

$\neg A$

which is inconsistent with $A$.

Laska
  • 1,317
  • 1
    Thank you! Your answer is simpler, but finally we need to let $A$ to be an axiom which is naturally a theorem. – PinkRabbit Mar 23 '23 at 07:01
  • Thanks - yes I was wondering where $A$ comes from. Because if there’s no facts there’s no contradiction. I wondered if an axiom scheme can be used as a theorem? But I guess yea – Laska Mar 23 '23 at 07:02