$P \to Q \equiv \neg P \vee Q$

Question

Most of the textbook that I had went through proves the given equivalence using truth table. But is there any way of proving $P \to Q \equiv \neg P \vee Q$ without truth table?

Answer 1

$(1)\quad$ Prove: $(P\rightarrow Q)\rightarrow(\neg P\vee Q)$ and $(\neg P\vee Q)\rightarrow (P\rightarrow Q)$

$(2)\quad$ Assume $P\rightarrow Q$ and assume $P$, then $Q$

$(3)\quad$ and therefor $\neg P\vee Q$

$(4)\quad$ if $\neg P$ then also $\neg P\vee Q$.

$(5)\quad$ Reversed, assume $\neg P\vee Q$. If $Q$ then $P\rightarrow Q$.

$(6)\quad$ And if $\,\neg P$ then also $P\rightarrow Q$.

$\therefore$ $(P\rightarrow Q)\equiv(\neg P\vee Q)$

---

$(1)\quad ((f\rightarrow g) \wedge (g\rightarrow f))\equiv (f\equiv g)$

$(2)\quad ((f\rightarrow g)\wedge f)\rightarrow g$

$(3)\quad f\rightarrow (f\vee g)$

$(4)\quad f\rightarrow (f\vee g)$

$(5)\quad g\rightarrow (f\rightarrow g)$

$(6)\quad \neg f\rightarrow (f\rightarrow g)$

Answer 2

I use Polish/Lukasiewicz notation. The axioms of the system are 1. CaCba. and 2. CCaCbcCCabCac.

The Co rule is {C$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$.

The Ail rule is $\alpha$ $\vdash$ A$\alpha$$\beta$.

The Ci rule allows us to move from {$\gamma$, $\alpha$} $\vdash$ $\beta$ to $\gamma$ $\vdash$ C$\alpha$$\beta$, where "$\gamma$" indicates a set of hypotheses, axioms, or assumptions, and $\alpha$ consists of the last hypothesis made.

The No rule is {CN$\alpha$$\beta$, CN$\alpha$N$\beta$} $\vdash$ $\alpha$ (there is no Ni rule at the basis of the system).

The Air rule is $\alpha$ $\vdash$ A$\beta$$\alpha$.

The Ao rule is {A$\alpha$$\beta$, C$\alpha$$\gamma$, C$\beta$$\gamma$} $\vdash$ $\gamma$.

The Ei rule is {C$\alpha$$\beta$, C$\beta$$\alpha$} $\vdash$ E$\alpha$$\beta$.

hypothesis         1 | Cpq
hypothesis         2 || NANpq
hypothesis         3 ||| Np
3 Ail              4 ||| ANpq
3-4 Ci             5 || CNpANpq
axiom CaCba        6 || CNANpqCNpNANpq
6, 2 Co            7 || CNpNANpq
5, 7 No            8 || p
8, 1 Co            9 || q
9 Air              10 || ANpq
2-10 Ci            11 | CNANpqANpq
hypothesis         12 || NANpq
12-12 Ci           13 | CNANpqNANpq
11, 13 No          14 | ANpq
Ci 1-14            15 CCpqANpq
hypothesis         16 | ANpq
hypothesis         17 || p
hypothesis         18 ||| Np
axiom CaCba        20 ||| CpCNqp
axiom CaCba        21 ||| CNpCNqNp
20, 17 Co          22 ||| CNqp
21, 18 Co          23 ||| CNqNp
22, 23 No          24 ||| q
Ci 18-24           25 || CNpq
hypothesis         26 ||| q
Ci 26-26           27 || Cqq
16, 25, 27 Ao      28 || q
17-28 Ci           29 | Cpq
16-29 Ci           30 CANpqCpq
15, 30 Ei          31 ECpqANpq

Lehs seems to have challenged me to prove this axiomatically. The definition of a formula is:

1. All lower case letters of the Latin alphabet are formulas.
2. If $\alpha$ is a formula, then N$\alpha$ is a formula.
3. If $\alpha$ and $\beta$ are formulas, then C$\alpha$$\beta$ and A$\alpha$$\beta$ are formulas.
4. Nothing else for this answer is a formula.

The axioms of the system are:

Recursive Variable Prefixing: CpCqp

Conditional Distribution: CCpCqrCCpqCpr

Negation Out: CCNpNqCCNpqp

Alternation In Left: CpApq

Alternation In Right: CpAqp

Alternation Out: CApqCCprCCqrr

Equivalence In: CCpqCCqpEpq

The only primitive rules of inference are uniform substitution and C-detachment {C$\alpha$$\beta$, $\alpha$} $\vdash$ $\beta$. This makes condensed detachment into a derivable rule of inference as J. A. Kalman demonstrated.

A proof is a finite sequence of formulas in which each step of the proof is either an axiom, or derived from preceding steps in the proof by uniform substitution, C-detachment, or condensed detachment. D$\alpha$.$\beta$ indicates an application of condensed detachment with $\alpha$ as the premise having the form C$\gamma$$\delta$ (the "major premise"), and $\beta$ having the form $\gamma$ (the "minor premise") yielding the formula $\delta$. I proved this by hand. I don't know how to get an automated theorem prover to prove something like this from scratch. Robert Veroff's notes on proofs in intuitionistic logic might have useful suggestions for automating such a proof, and the method of proof sketches might have useful suggestions here (see [8] in the previous link). This theorem can't get proved in intuitionist logic. Veroff's paper on Proof Sketches might have utility here for finding an automated proof, and it references OTTER.

axiom       1 CpCqp.
axiom       2 CCpCqrCCpqCpr.
axiom       3 CCNpqCCNpNqp.
axiom       4 CpApq.
axiom       5 CpAqp.
axiom       6 CApqCCprCCqrr.
axiom       7 CCpqCCqpEpq.
D2.1        8 CCpqCCpp.
D8.1        9 Cpp.  
D1.1        10 CpCqCrq.
D1.3        11 CpCCNqrCCNqNrq.
D2.10       12 CCpqCpCrq.
D12.11      13 CpCqCCNrsCCNrNsr.
D1.4        14 CpCqAqr.
D12.14      15 CpCqCrArs.
D1.2        16 CpCCqCrsCCqrCqs.
D2.16       17 CCpCqCrsCpCCqrCqs.
D17.13      18 CpCCqCNrsCqCCNrNsr.
D2.18       19 CCpCqCNrsCpCqCCNrNsr.
D19.15      20 CpCqCCNrNANrsr.
D17.20      21 CpCCqCNrNANrsCqr.
D2.21       22 CCpCqCNrNANrsCpCqr.
D22.10      23 CpCNANqrq.
D17.1       24 CCpqCCrpCrq.
D2.24       25 CCCpqCrpCCpqCrq.
D25.23      26 CCpqCNANprq.
D1.5        27 CpCqArq.
D1.27       28 CpCqCrAsr.
D17.28      29 CpCCqrCqAsr.
D2.29       30 CCpCqrCpCqAsr.

%

D30.26      31 CCpqCNANprAsq.
D2.11       32 CCpCNqrCpCCNqNrq.
D32.31      33 CCpqCCNANprNAsqANpr.
D2.33       34 CCCpqCNANprNAsqCCpqANpr.
D1.9        35 CpCqq.
D34.35      36 CCpqANpq.
D1.10       37 CpCqCrCsr.
D1.17       38 CpCCqCrCstCqCCrsCrt.
D2.38       39 CCpCqCrCstCpCqCCrsCrt.
D17.37      40 CpCCqrCqCsr.
D2.40       41 CCpCqrCpCqCsr.
D41.10      42 CpCqCrCsq.
D1.11       43 CpCqCCNrsCCNrNsr.
D1.43       44 CpCqCrCCNstCCNsNts.
D39.44      45 CpCqCCrCNstCrCCNsNts.
D17.45      46 CpCCqCrCNstCqCrCCNsNts.
D2.46       47 CCpCqCrCNstCpCqCrCCNsNts.
D47.42      48 CpCqCrCCNsNqs.
D39.48      49 CpCqCCrCNsNqCrs.
D17.49      50 CpCCqCrCNsNqCqCrs.
D2.50       51 CCpCqCrCNsNqCpCqCrs.
D51.37      52 CpCqCNqr.
D1.6        53 CpCAqrCCqsCCrss.
D1.53       54 CpCqCArsCCrtCCstt.
D17.54      55 CpCCqArsCqCCrtCCstt.
D2.55       56 CCpCqArsCpCqCCrtCCstt.
D56.1       57 CApqCrCCpsCCqss.
D17.57      58 CApqCCrCpsCrCCqss.
D2.58       59 CCApqCrCpsCApqCrCCqss.
D59.52      60 CANpqCpCCqrr.

%

D1.9        61 CpCqq.
D1.61       62 CpCqCrr.
D17.60      63 CANpqCCpCqrCpr.
D2.63       64 CCANpqCpCqrCANpqCpr.
D64.62      65 CANpqCpq.
D7.36       66 CCANpqCpqECpqANpq.
D66.65      67 ECpqANpq.

Answer 3

In many formal systems you don't have both $\to$ and $\lor$, rather one of them is defined. For example, in Hilbert-style systems it is popular to have $\to$ as a primitive and define $\lor$ essentially using the equivalence you note, while in the sequent calculus we usually have $\lor$ and define $\to$ using your equivalence. In such systems there is no need to prove this equivalence, since it is true by definition.

Other systems, such as natural deduction, do contain both $\to$ and $\lor$ as primitive notions. It is then an easy exercise to prove your equivalence given the axioms of the system. If you're curious, you can look up natural deduction and give it a shot yourself.

Answer 4

Here's another approach adapted from Arthur Prior's Formal Logic p. 65-66.

First formation rules:

1. All lower case letters of the Latin alphabet are formulas.
2. If x is a formula, then $\delta$x is a formula.
3. If x is a formula, then Nx is a formula.
4. If x and y are formulas, then C x y is a formula (spaces can get ignored or inserted freely).

Let "0" stand for falsity, and "1" for truth. We have the following matrix for implication "C", disjunction (or equivalently alternation) "A", and negation "N".

C | 0  1|  A| 0  1|  N
----------------------
0 | 1  1|  0| 0  1|  1
1*| 0  1|  1| 1  1|  0

This gives us the equations C00 =1, C01=1, C10=0, C11=1, A00=0, A01=1, A10=1, A11=1, N0=1, N1=0.

$\delta$ stands for a functioral variable. Paraphrasing Prior, where x is a formula, $\delta$x stands for any truth-function into which $\delta$ enters as argument. $\delta$a stands for any truth-function of b, such as Nb, Abb, Aab, CNba, CCbcCCabCac. $\delta$b can also stand for b itself. Substitution for $\delta$ occurs by putting the argument of $\delta$ into the position where an " ' " symbol appears. The notation x/y indicates that x is to get substituted with y for all instances of x in the formula in which x appears. For example, the substitution instruction $\delta$/C ' ' in $\delta$r yields Crr. $\delta$/C ' A ' p in C $\delta$r $\delta$p yields C CrArp CpApp. The substitution $\delta$/' in say C $\delta$p $\delta$1 just has us dropping $\delta$ yielding Cp1. $\delta$/A ' C ' ' in C $\delta$p A $\delta$q $\delta$ Na yields C ApCpp A AqCqq CNaANaNa.

Note that the valuation function "v", v(C x y)=C v(x) v(y). Also, for the valuation function v($\delta$x)=$\delta$v(x).

Now it turns out that the following is a meta-theorem.

Meta-Theorem 1: If v(x)=v(y), then v(C $\delta$x $\delta$y)=1. In other words, if x=y, then C $\delta$x $\delta$y follows.

Demonstration: Suppose v(x)=v(y). Since v(C00)=1, and v(C11)=1, it follows that for all p, v(Cpp)=1. Substituting p/$\delta$x in Cpp we then obtain that v(C $\delta$x $\delta$x)=1. Since v(C x y)=C v(x) v(y), it then follows that C v($\delta$x) v($\delta$x)=1. Since v($\delta$x)=$\delta$v(x), it then follows that C $\delta$v(x) $\delta$v(x)=1. By the initial supposition, we then obtain that C $\delta$v(x) $\delta$ v(y)=1. Since v($\delta$x)=$\delta$v(x) we then obtain that

C v($\delta$x) v($\delta$y)=1. From v(C x y)=C v(x) v(y) we thus obtain that v(C $\delta$x $\delta$y)=1. Therefore, if v(x)=v(y), then v(C $\delta$x $\delta$y)=1.

The upshot here comes as that an equation like Cxy=z gives us C $\delta$z $\delta$Cxy. The suggested formulas from the above equations immediately following the table along with the axioms "C $\delta$0 C $\delta$1 $\delta$p" and "1", and "C Cpq C Cqp Epq" give us an axiom set here.

Let the notation 1 x/y * C 2-3 indicate that in formula 1 x gets substituted with y. This matches the formula which starts with C has 2 as its next part, and 3 as its last part. We then detach formula 3. The notation 4 x/y C 5-C 6-7 indicates that 4 matches the formula C5-C6-7. Since we already have formulas 5 and 6, we thus detach formula 7.

To see how the plan of writing the deduction proceeds, I'll write out the following calculation:

                         |-C C00 AN00=C 1 AN00=C 1 A10=C 1 1=1
            |-C C0q AN0q-|
            |            |-C C01 AN01=C 1 AN01=C 1 A11=C 1 1=1
 C Cpq ANpq-|
            |            |-C C10 AN10=C 0 AN10=C 0 A00=C 0 0=1
            |-C C1q AN1q-|
                         |-C C11 AN11=C 1 AN11=C 1 A01=C 1 1=1.

Now, to write out a deduction, we can basically move left to right here. From 1, we'll deduce C11. Then from C11 we'll deduce C 1 A10. Then C 1 AN00. Then C C00 AN00. Once we get C C01 AN01, then since we have C C00 AN00, we can get C C0q AN0q. But, I'll skip some steps here which gives us a simpler proof. Here goes:

1 1.

2 C δ1 δC00.

3 C δ1 δC01.

4 C δ0 δC10.

5 C δ1 δC11.

6 C δ0 δA00.

7 C δ1 δA01.

8 C δ1 δA10.

9 C δ1 δA11.

10 C δ1 δN0.

11 C δ0 δN1.

12 C Cpq C Cqp Epq.

13 C δ0 C δ1 δp. (this is not an axiom or theorem in intuitionistic logic).

2 δ/' * C1-14

14 C00.

3 δ/' * C1-15

15 C01.

13 δ/C0' * C14-C15-16

16 C0p.

5 δ/' * C1-17

17 C11.

13 δ/C'1 * C15-C17-18

18 Cp1.

18 p/C00 * 19

19 C C00 1.

8 δ/C C00 ' * C19-20

20 C C00 A10.

10 δ/C C00 A'0 * 20-21

21 C C00 AN00.

18 p/C01 * 22

22 C C01 1.

9 δ/CC01' * C22-23

23 C C01 A11.

10 δ/C C01 A'1 * C23-24

24 C C01 AN01.

13 δ/ C C0' AN0', p/q * C21-C24-25 

25 C C0q AN0q.

16 p/AN10 * 26

26 C 0 AN10.

4 δ/C ' AN10 * C26-27

27 C C10 AN10.

18 p/C11 * 28

28 C C11 1.

7 δ/C C11 ' * C28-29

29 C C11 A01.

11 δ/C C11 A'1 * C29-30

30 C C11 AN11.

13 δ/C C1' AN1', p/q *C27-C30-31

31 C C1q AN1q.

14 δ/C C'q AN'q * C25-C31-32

32 C Cpq ANpq.

18 p/AN00 * 33

33 C AN00 1.

2 δ/C AN00 ' * C33-34

34 C AN00 C00.

18 p/AN01 * 35

35 C AN01 1.

3 δ/C AN01 ' * C35-36

36 C AN01 C01.

13 δ /C AN0' C0', p/q * C34-C36-37

37 C AN0q C0q.

6 δ/C'0 * C14-38

38 C A00 0.

11 δ/C A'0 0 * C38-39

39 C AN10 0.

4 δ/C AN10 ' * C39-40

40 C AN10 C10.

18 p/AN11 * 41

41 C AN11 1.

5 δ/C AN11 ' * C41-42

42 C AN11 C11.

13 δ/C AN1' C1', p/q * C40-C42-43

43 C AN1q C1q.

37 δ/C AN'q C'q * C37-C43-44

44 C ANpq Cpq.

 12 p/Cpq, q/ANpq * C32-C44-45

45 E Cpq ANpq.