Vrftsjtryk

I've looked at the tableau proofs of many rules of inference (double-negation, disjunction is commutative, modus tollendo ponens, and others), and they all seem to use the so-called "or-elimination" (Disjunction Elimination) rule:

$$(Pvdash R), (Qvdash R), (P lor Q) vdash R$$

(If $Pimplies R$ and $Qimplies R$, and either $P$ or $Q$ (or both) are true, then $R$ must be true.)

It's often called the "proof by cases" rule, it makes sense, and I've seen the principle used in many mathematical proofs.

I'm trying to figure out how to logically prove this rule (using other rules of inference and/or replacement), however the proof offered is self-reliant! Is this an axiom?

(There's also the Constructive Dilemma rule, which looks like a more generalized version of Disjunction Elimination. Maybe the proof of D.E. depends on C.D.? or maybe C.D. is an extension of D.E.?)

I agree that the link you provide to the proof offered by Proof Wiki is "self-reliant", and seems, to me at least, to invoke the very rule in which we are interested. In a sense, it can be seen as a "model" proof exemplifying the general case of invocation of Disjunction Elimination, $lor mathcal E$.

So, yes, this can sort of be thought of as an "axiom": a basic rule of inference we take to be valid, and from which other rules of inference may be derived. It does rely on modus ponens, twice. But the principle that, if, given the truth of $p lor q$, and some conclusion $r$ follows from $p$, and the same conclusion $r$ follows from $q$, then we can conclude that $r$ is true.

It might be reassuring to note that the argument characterizing "Disjunction Elimination" can be expressed as follows:

$$(((P to Q) land (R to Q)) land (P lor R)) to Qtag{Tautology}$$

which proves to be tautologically (necessarily) true $(dagger)$, and so we have very good reason to accept the rule of inference as valid.

$(dagger)$: Exercise - Confirm, using a truth-table, that the given tautology is, in fact, tautologically true.

In a standardly set up natural deduction system, with an introduction and an elimination rule for each connective, the rules are independent: you can't in particular, show that the $lor$E rule follows from the other rules.

What you can do, however, as Gentzen noted, is to argue (outside the system) that the $lor$E rule is in harmony with the introduction rule $lor$I in the following sense: what the application of the elimination rule allows you to extract from a disjunction is no more than what you must have already been entitled to in order to assert the disjunction on the basis of $lor$I in the first place.

Roughly: Suppose, as fixed background, that we have a proof from $P$ to $R$ and a proof from $Q$ to $R$. If you now put into play the disjunction $P lor Q$, then this will canonically be on the basis that you are already entitled to $P$ (and hence, in the circumstances, to $R$) or you are already entitled to $Q$ (and hence, in the circumstances, to $R$). So we can infer $R$. As $lor$E says.

The rules of Disjunction Elimination and Constructive dilemma are interchangable.

You can proof Disjunction Elimination from Constructive Dilemma and

You can proof Constructive Dilemma from Disjunction Elimination.

So whichever you have you can prove the other.

Your second question is Disjunction Elimination an axiom?

In a strict logical sense axioms are formulas that are treated as self-evidently true.

Rules of inference are not formulas so in the strict sense they cannot be axioms.

But seeing in it in a more relaxed way , they are treated as self-evidently true so you could call it a metalogical axiom or something like it.

I use Polish notation. First check that CCprCCqrCApqr qualifies as a tautology. I'll leave that to you. Then invoke the completeness theorem (so, we're lucky on this one), and you have $vdash$CCprCCqrCApqr. The next part you might do without reading what I've written now. Anyways, I'll still do it.

Instead of writing conditional introduction, and elimination, I write C-in and C-out respectively in the proof analysis. The Greek letters help us keep track of scope (or the "domains" as Jaskowski might write). The whole thing can use scope in a natural deduction context since it comes as a rule of inference and not a theorem. Thus...

1 $alpha$$beta$ p hypothesis

.

.

.

2 $alpha$$beta$ r assumed conclusion (we're assuming the derivation from p to r)

3 $alpha$ Cpr 1-2 C-in

4 $alpha$$gamma$ q hypothesis

.

.

.

5 $alpha$$gamma$ r assumed conclusion (again, we're assuming the derivation from q to r)

6 $alpha$ Cqr 4-5 C-in

7 $alpha$ Apq assumption

8 $alpha$ CCprCCqrCApqr Theorem Introduction

9 $alpha$ CCqrCApqr 3, 8 C-out

10 $alpha$ CApqr 6, 9 C-out

11 $alpha$ r 10, 7 C-out

Thus, "[ (p $vdash$ r) , (q $vdash$ r) , Apq] $vdash$ r".

Notice also that I didn't use any conjunction connective explicitly or implicitly. For all we know, in such a system conjunction might not come as definable, or it might come as definable, but "((((P→Q)∧(R→Q))∧(P∨R))→Q)" won't qualify as a tautology. Or at the very least, if you use ((((P→Q)∧(R→Q))∧(P∨R))→Q) to validate this rule as permissible, you'll need to use a conjunction-out rule to validate this rule, and still use the tautology that I used. This derivation didn't require "((((P→Q)∧(R→Q))∧(P∨R))→Q)".

Also, the rule might come as better written:

[Apq, (p $vdash$ r) , (q $vdash$ r)] $vdash$ r,

because if we did that, then Apq would appear before anything else and this derivation becomes more apparent:

1 $alpha$ Apq assumption

2 $alpha$$beta$ p hypothesis

.

.

.

3 $alpha$$beta$ r conclusion (we're assuming the derivation from p to r)

4 $alpha$ Cpr 2-3 C-in

5 $alpha$$gamma$ q hypothesis

.

.

.

6 $alpha$$gamma$ r conclusion (we're assuming the derivation from q to r)

7 $alpha$ Cqr 5-6 C-in

8 $alpha$ CCprCCqrCApqr Theorem Introduction

9 $alpha$ CCqrCApqr 4, 8 C-out

10 $alpha$ CApqr 7, 9 C-out

11 $alpha$ r 1, 10 C-out