# Prove P v ~P using most basic rules?

Is there a way to prove `P v ~P` in basic inference rules?

I can't think of where to start because nothing applies to this. I was thinking about usinig Conditional proof, but I don't know what should I assume.

Here's a list of the rules I can use: pastebin.com/5Fbp8f85

One thing I think I should add is that, my prof. told us we can use (line 23 to line 26) to discharge the assumption.

• What rules of inference do you allow? It's pretty important. – Niel de Beaudrap Sep 29 '13 at 21:58
• @NieldeBeaudrap - The conjunction/disjunction/condition/negation elimination and introduction, conditional proof, thanks – Derek 朕會功夫 Sep 29 '13 at 22:08
• Could you be more formal? There are many ways of spelling out connective introduction and elimination rules, and your "conditional proof" rules might well make these things trivial. – Paul Ross Sep 29 '13 at 22:15
• @PaulRoss - Here's a list of the rules I can use: pastebin.com/5Fbp8f85 – Derek 朕會功夫 Sep 29 '13 at 22:20
• @Derek朕會功夫 You should add all that information, the link and the comment of your prof, to your original question, since it's relevant and the question can't be answered appropriately without it. – iphigenie Sep 29 '13 at 22:38

If you take `A -> B` to be a material conditional, such that `A -> B iff ~A v B` is a prior definition rule MC, then a very simple proof might go something like this:

`A->A` (established in the subproof below:)

1. `A` (suppose for a conditional)
2. `A` (by reiteration)
3. `A->A` (by conditional proof

`~A v A` (by MC)

But the actual details of your logic system will make a massive difference to whether this kind of proof will work.

E: Now that we do have the specifics of the system, you could do it like this:

`~A -> ~A` (by subproof below)

1. `~A` (suppose for conditional)
2. `~A -> ~A` (by conditional introduction, discharging supposition 1.)

`A v ~A` (by the equivalent MC rule, lines 12-15)

• Note that the rules of inference specified do not allow conditional introduction. – Niel de Beaudrap Sep 29 '13 at 22:31
• Yes, since the rules specified don't appear to actually include anything like a "conditional proof rule", this proposed proof won't work. There's hints of something you might do by, say, doing the same thing with `~A` to show `~A->~A`, but I guess without some means of introducing conditionals or otherwise discharging assumptions, this system isn't going to prove any theorems at all. E: Now that we know the conditional introduction can be used to discharge assumptions, I think the modified version would work. – Paul Ross Sep 29 '13 at 22:34
• Typo: "A v ¬ B" in the first line should be "¬ A v B". – Hunan Rostomyan Sep 30 '13 at 0:00
• You're quite right! Duly amended. – Paul Ross Sep 30 '13 at 8:41

I'd also like to point out that the system you're working with as presented is radically unstable.

`(~C)->A` (by the following subproof)

1. `A` (suppose for the conditional)
2. `(~C)->A` (by the conditional introduction rule, lines 24-27, discharging assumption 1.)

`(~C)->(~A)` (by the following subproof)

1. `(~A)` (suppose for the conditional)
2. `(~C)->(~A)` (by the conditional introduction rule, lines 24-27, discharging assumption 1.)

`~~C` (by lines 35-39, supposed to represent a contradiction)

`C` (By double negation elimination lines 41-43)

In effect, any arbitrary sentence is a theorem of the system you've proposed. Something doesn't seem right there.

To fix it, you probably need to amend the rule about conditional introduction to be in some sense Relevantly restricted. That is, rather than

`A`

`B->A`

you could use an argument skeleton type rule like this:

`[A]`

`...`

`B`

`A -> B`

The idea here is that you can discharge `A` in this inference, but you need to ensure that the `...` here is itself a permissable deductive inference from `A` to `B`. This would let you keep the cases like `A v ~A` without the arbitrariness involved in the current rule.

Here is the question:

Is there a way to prove P v ~P in basic inference rules?

Assume ~P.

Consider lines 23-26:

```A
----
B -> A
```

Based on this rule, anything implies ~P. Therefore, ~P -> ~P.

It is permitted at this point to discharge the assumption made above based on this comment:

One thing I think I should add is that, my prof. told us we can use (line 23 to line 26) to discharge the assumption.

Consider lines 11-14:

```(~A -> B)
---------
(A v B)
```

This allows us to obtain the desired result P v ~P.