I'm not sure how to prove these basic theorems in propositional calculus. Instead of using the standard axioms, we're supposed to use:

  1. Deduction Theorem (if $\Phi, \alpha \vdash \beta$ then $\Phi \vdash \alpha \to \beta$),
  2. Reductio (if $\Phi, \alpha \vdash \, $, then $\Phi \vdash \lnot \alpha$),
  3. Cut Rule (if $\Phi \vdash \alpha$ and $\Psi, \alpha \vdash \beta$ then $\Phi \cup \Psi \vdash \beta$),
  4. Inconsistency Effect (if $\Phi \vdash \, $, then $\Phi \vdash \beta$ for every formula $\beta$), and
  5. the Principle of Indirect Proof (if $\Phi, \lnot \alpha \vdash \, $, then $\Phi \vdash \alpha$),

as all the axioms can be deduced using these theorems.

I don't really know how to start the proofs without using the axioms:

i) prove that $\lnot(\alpha \to \beta) ⊢ \alpha$

ii) prove that $\lnot\alpha \vdash \alpha \to \beta$

Any suggestions on how to start these proofs or any insight at all would be greatly appreciated!



closed as off-topic by Andrés E. Caicedo, Namaste, GNUSupporter 8964民主女神 地下教會, Sahiba Arora, jkabrg Feb 5 '18 at 21:02

This question appears to be off-topic. The users who voted to close gave this specific reason:

  • "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – Andrés E. Caicedo, Namaste, GNUSupporter 8964民主女神 地下教會, Sahiba Arora, jkabrg
If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ Is $\neg$ just a symbol in your system, or is $\neg a$ e.g. shorthand for $a \to \bot$? $\endgroup$ – Patrick Stevens Feb 4 '18 at 21:23
  • $\begingroup$ Negation is a symbol in the system. The system is built using negation and implication. $\endgroup$ – DiscipleOfKant Feb 4 '18 at 21:36
  • $\begingroup$ What does it mean "Reductio"? $\endgroup$ – Taroccoesbrocco Feb 4 '18 at 21:48
  • 1
    $\begingroup$ What is the Cut Rule? $\endgroup$ – Bram28 Feb 4 '18 at 22:00
  • 1
    $\begingroup$ All of the rules you've listed are of the form "if $\Phi\vdash \Psi$ then..." This means you have no way of starting a chain of logic (more technically called a "derivation"). I suspect, at least, a rule like "$\Phi,a\vdash a$ always holds" is also intended to be in the set of rules you're allowed to use. $\endgroup$ – Derek Elkins Feb 5 '18 at 4:32

Now that we have the source of your problem, we can help you...

See: Moshe Machover, Set Theory, Logic and Their Limitations Cambridge UP (1996), page 116-on for the definitions and some results about propositional calculus.

Definition 8.1.

A set of two formulas $\{ \alpha, \lnot \alpha \}$, one of which is the negation of the other, is called a contradictory pair.

A set $\Phi$ of formulas is said to be [propositionally] inconsistent - in symbols: "$\Phi \vdash_0$" - if both members of some contradictory pair are propositionally deducible from $\Phi$.

We have to note some results: Problem 8.12 [page 126]: $\alpha \vdash_0 \lnot \lnot \alpha$, for all $\alpha$, and Lemma 8.14: $\lnot \lnot \alpha \vdash_0 \alpha$, for all $\alpha$.

At this point of the book, the proof system regarding $\vdash_0$, based on $\lnot$ and $\to$ and the five axioms of page 117 plus modus ponens, has been enlarged with addiotnal (derived) rules:

Theorem 7.2: Deduction Theorem.

Theorem 6.13: Cut Rule: If $\Phi \vdash_0 \delta_i$ for each $i = 1, 2,\ldots, k$ and $\Psi \cup \{ \delta_0, \ldots, \delta_k \} \vdash_0 \alpha$, then $\Phi \cup \Psi \vdash_0 \alpha$.

Inconsistency Effect: If $\Phi \vdash_0$, then $\Phi \vdash_0 \beta$, for every formula $\beta$.

Reductio: If $\Phi, \alpha\vdash_0$, then $\Phi \vdash_0 \lnot \alpha$.

Indirect proof: If $\Phi \lnot \alpha \vdash_0 $, then $\Phi \vdash_0 \alpha$.

Now we have: Problem 8.19 [page 128]:

Prove: (i) $\lnot \alpha \vdash_0 \alpha \to \beta$; (iv) $\lnot (\alpha \to \beta) \vdash_0 \alpha$.

We assume to use, in addition to modus ponens, also the derived rules above, as well as the already available results.

For (i):

1) $\vdash_0 \lnot \alpha \to (\alpha \to \beta)$ --- Axiom scheme iv

2) $\lnot \alpha$ --- premise

3) $\alpha \to \beta$ --- from 1) and 2) by mp.

According to Definition 6.8 [page 117], the above is a propositional deduction of $\alpha \to \beta$ from the set of formulas $\Phi= \{ \lnot \alpha \}$ and we can write (according to Definition 6.9): $\lnot \alpha \vdash_0 \alpha \to \beta$.

For (iv):

1) $\lnot (\alpha \to \beta)$ --- premise

2) $\lnot \alpha$ --- premise

3) $\alpha \to \beta$ --- from 2) and previous result (Problem 8.19 (i)).

Up to now we have:

$\lnot (\alpha \to \beta), \lnot \alpha \vdash_0 (\alpha \to \beta)$

and obviously:

$\lnot (\alpha \to \beta), \lnot \alpha \vdash_0 \lnot (\alpha \to \beta)$.

This means: $\lnot (\alpha \to \beta), \lnot \alpha \vdash_0$.

Finally, we apply Reductio to get:

4) $\lnot (\alpha \to \beta) \vdash_0 \lnot \lnot \alpha$,

followed by Lemma 8.14: $\lnot \lnot \alpha \vdash_0 \alpha$, to conclude:

$\lnot (\alpha \to \beta) \vdash_0 \alpha$.

Note. How to prove (i) with MP, DT and Inconsistency (without axioms)?

1) $\alpha$ --- premise

2) $\lnot \alpha$ --- premise

Form 1) and 2) we have: $\Phi= \{ \alpha, \lnot \alpha \} \vdash_0$.

Thus, we can apply Inconsistency to get:

3) $\lnot \alpha, \alpha \vdash^* \beta$,

concluding, by DT, with:

$\lnot \alpha \vdash^* \alpha \to \beta$.

Having proved $\lnot \alpha \vdash^* \alpha \to \beta$, we can use it in the proof of (iv) above (line 3)) to get:

$\lnot (\alpha \to \beta) \vdash^* \alpha$.

  • $\begingroup$ Superb! Your answer completely clarifies the context of the question in the OP. In my answer I followed what the questioner said in a comment "we should no longer use the axioms". Moreover, I used a formulation of the cut rule that does not correspond to the one used in the book. I think I will delete my answer. $\endgroup$ – Taroccoesbrocco Feb 5 '18 at 8:27
  • $\begingroup$ @Taroccoesbrocco - why delete it ? The result is fine also for Machover's system as long as you use Machover's result: Example 6.11: $\vdash_0 \alpha \to \alpha$ (instead of calling it "Axiom"). $\endgroup$ – Mauro ALLEGRANZA Feb 5 '18 at 8:40

As correctly suggested by Derek Elkins in his comment, I strongly conjecture that your system should have an axiom rule of the form $\alpha \vdash \alpha$ (or $\Phi, \alpha \vdash \alpha$) for every formula $\alpha$. I do not know the exact formulation of the cut rule in your system, anyway it should be equivalent to the formulation of the cut rule I used in my derivations.

First, I answer your question (ii). The following is a derivation of $\lnot A \vdash A \to B$ in your system.

  1. $\lnot A \vdash \lnot A$ -- axiom
  2. $A \vdash A$ -- axiom
  3. $\lnot A, A \vdash \ $ -- cut rule (modus ponens) of 1. and 2.
  4. $\lnot A, A \vdash B$ -- inconsistency effect (ex falso quodlibet) from 3.
  5. $\lnot A \vdash A \to B$ -- deduction theorem from 4.

Concerning your question (i), the following is a derivation of $\lnot(A \to B) \vdash A$ in your system. It uses my answer to your question (ii).

  1. $\lnot (A \to B) \vdash \lnot (A \to B)$ -- axiom.
  2. $\lnot A \vdash A \to B$ -- see derivation above, question (ii)
  3. $\lnot (A \to B), \lnot A \vdash \ $ -- cut rule (modus ponens) of 1. and 2.
  4. $\lnot (A \to B) \vdash A$ -- (principle of indirect proof (reductio ad absurdum) from 3.

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