[PL13] Soundness and completeness

Module: Predicate logic

Quote of the page

Blind commitment to a theory is not an intellectual virtue: it is an intellectual crime.

- Lakatos

Popular pages

§1. Metalogic

Our MPL natural deduction system is sound. You can verify this for yourself, by examining each of the rules to ensure that the rules only permit you to write down well-formed wffs which are entailed by their dependencies. That the system as a whole is sound means:

For any MPL wff φ, if ⊢ φ, then ⊨ φ,

and

For any MPL wff φ, and list of MPL wffs X, if X ⊢ φ then X ⊨ φ.

The system is also good for a further reason; it is complete. That the system is complete means:

For any MPL wff φ, if ⊨ φ then ⊢ φ.

and

For any MPL wff φ, and list of MPL wffs X, if X ⊨ φ then X ⊢ φ.

We won't prove the completeness of our MPL system in this introductory course. But it is useful to know that the system is complete. In SL you can use the truth table method to determine whether or not a particular SL wff is valid. But in MPL you cannot rely on the truth table method to determine whether or not an MPL wff is valid. You need some other method. Since the natural deduction is system for MPL is complete, if an MPL wff is valid, there is a derivation of the wff using the system.

When we are carrying out derivations using the rules of MPL, we are working "within" the system. But when we describe and try to show whether MPL is sound and complete, we are using not just MPL, but also English, to talk about the system. The study of the these higher-level properties of a system of logic is known as "metalogic".

Show that "∀x(Fx→Fx)" is valid in two different ways.

"∀x(Fx→Fx)" is true under every interpretation. So "∀x(Fx→Fx)" is valid. "∀x(Fx→Fx)" is derivable using MPL natural deduction:

1	1. Fa		A
	2. (Fa→Fa)	1,→I 
	3. ∀x(Fx→Fx)	2,∀I

Since "∀x(Fx→Fx)" is derivable with no dependencies, and the system is sound, "∀x(Fx→Fx)" is valid.

Suppose you try to find a derivation of a certain MPL wff, but you do not succeed in finding a derivation. Does it follow that that wff is not valid?

Show the following:

∀xHx ⊢ Ha
∀xHx, (Hc → ∃xGx) ⊢ ∃xGx
∀x(Hx→Mx), ∀xHx ⊢ ∀xMx
Ha ⊢ ∃yHy
(Ab → Dc) ⊢ (Ab → ∃xDx)
∃x(Fx & Gx) ⊢ ∃xFx
∀x(Fx→∀yGy) ⊢ ∀x∀y(Fx→Gy)
∀x(Px→Qx), ∀x(Qx→Px) ⊢ ∀x(Px↔Qx)
∃x~Px ⊢ ~∀xPx
(∃xPx→∀x(Qx→Rx)), (Pa&Qa) ⊢ Ra
(∀x(Px→Qx)→∃x(Rx&Sx)), (∀x(Px→Sx)&∀x(Sx→Qx)) ⊢ ∃xSx
(∀x(Px&~Qx)→∃xRx), ~∃x(Qx∨Rx) ⊢ ~∀xPx
(∃x~Px→∀x~Qx), (∃x~Px→∃xQx), ∀x(Px→Rx) ⊢ ∀xRx
~∃x(Px∨Qx), (∃xRx→∃xPx), (∃xSx→∃xQx) ⊢ ~∃x(Rx∨Sx)

a. ∀xHx ⊢ Ha

1 	1)∀xHx 		A
1 	2) Ha 		1 ∀E

b. ∀xHx, (Hc → ∃xGx) ⊢ ∃xGx

1	1) ∀xHx		A
2	2) (Hc→∃xGx)	A
1 	3) Hc		1 ∀E
1, 2	4) ∃xGx		2, 3 →E

c. ∀x(Hx→Mx), ∀xHx ⊢ ∀xMx

1	1) ∀x(Hx→Mx)	A
2	2) ∀xHx		A
1	3) (Ha→Ma)	1 ∀E
2 	4) Ha		2 ∀E
1, 2 	5) Ma		3, 4 →E
1, 2	6) ∀xMx		5 ∀I

d. Ha ⊢ ∃yHy

1 	1) Ha 		A
2 	2) ∃yHy 		1 ∃I

e. (Ab → Dc) ⊢ (Ab → ∃xDx)

1	1) (Ab→Dc)	A
2	2) Ab		A
1, 2 	3) Dc		1, 2 →E 
1, 2 	4) ∃xDx		3 ∃I
1	5) (Ab→∃xDx)	2, 4 →I

f. ∃x(Fx & Gx) ⊢ ∃xFx

1 	1) ∃x(Fx&Gx)		A
2 	2) (Fa&Ga)		A
2 	3) Fa			2 &E
2 	4) ∃xFx 			3 ∃I
1	5) ∃xFx			1, 2, 4 ∃E

g. ∀x(Fx→∀yGy) ⊢ ∀x∀y(Fx→Gy)

1	1) ∀x(Fx→∀yGy) 		A
1	2) (Fa→∀yGy)		1∀E
3	3) Fa			A
1, 3 	4) ∀yGy			2, 3 →E
1, 3 	5) Gb			4 ∀E
1	6) (Fa→Gb)		3, 5 →I
1	7) ∀y(Fa→Gy)		6 ∀I
1	8) ∀x∀y(Fx→Gy)		7 ∀I

h. ∀x(Px→Qx), ∀x(Qx→Px) ⊢ ∀x(Px↔Qx)

1	1) ∀x(Px→Qx) 		A
2	2) ∀x(Qx→Px)		A
1	3) (Pa→Qa)		1 ∀E
2 	4) (Qa→Pa)		2 ∀E
1, 2 	5) ((Pa→Qa)&(Qa→Pa))	3, 4 &I
1, 2	6) (Pa↔Qa)		5 ↔I
1, 2	7) ∀x(Px↔Qx)		6 ∀I

i. ∃x~Px ⊢ ~∀xPx

1 	1) ∃x~Px 	A
2	2) ∀xPx		A
3	3) ~Pa		A
2	4) Pa		2 ∀E
5 	5) ~(Qb&~Qb)	A
2, 3 	6) (Pa&~Pa) 	3, 4 &I
2, 3 	7) (Qb&~Qb)	5, 6 ~E
1, 2 	8) (Qb&~Qb)	1, 3, 7 ∃E
1	9) ~∀xPx	2, 8 ~I

j. (∃xPx→∀x(Qx→Rx)), (Pa&Qa) ⊢ Ra

1 	1) (∃xPx→∀x(Qx→Rx))	A
2	2) (Pa&Qa)		A
2	3) Pa			2 &E
2 	4) ∃xPx			3 ∃I
1, 2	5) ∀x(Qx→Rx)		1, 4 →E			
2 	6) Qa			2 &E
1, 2	7) (Qa→Ra) 		5 ∀E
1, 2	8) Ra			6, 7 →E

k. (∀x(Px→Qx)→∃x(Rx&Sx)), (∀x(Px→Sx)&∀x(Sx→Qx)) ⊢ ∃xSx

1	1) (∀x(Px→Qx)→∃x(Rx&Sx)) 	A
2	2) (∀x(Px→Sx)&∀x(Sx→Qx)) 	A
2	3) ∀x(Px→Sx) 			2 &E
2	4) ∀x(Sx→Qx)			2 &E
5	5) Pa				A
2 	6) (Pa→Sa)			3 ∀E
2, 5 	7) Sa				5, 6 →E
2 	8) (Sa→Qa)			4 ∀E
2, 5 	9) Qa				7, 8 →E
2	10) (Pa→Qa) 			5, 9 →I
2 	11) ∀x(Px→Qx)			10 ∀I
1, 2	12) ∃x(Rx&Sx)			1, 11 →E
13	13) (Rb&Sb) 			A
13 	14) Sb				13 &E
13 	15) ∃xSx				14 ∃I
1, 2 	16) ∃xSx				12, 13, 15 ∃E

l. (∀x(Px&~Qx)→∃xRx), ~∃x(Qx∨Rx) ⊢ ~∀xPx

1	1) (∀x(Px&~Qx)→∃xRx)		A
2	2) ~∃x(QxvRx) 			A
3	3) ∀xPx 			A 
4	4) Qa 				A
4	5) (QavRa)			4 vI
4	6) ∃x(QxvRx)			5 ∃I		
2, 4	7)(∃x(QxvRx)&~∃x(QxvRx))		2, 6 &I
2	8) ~Qa				4, 7 ~I
3	9) Pa				3 ∀E
2, 3	10) (Pa&~Qa)			8, 9 &I
2, 3	11) ∀x(Px&~Qx)			10 ∀I
1, 2, 3	12) ∃xRx				1, 11 →E
13	13) Rb				A
13	14) (QbvRb)			13 vI
13	15) ∃x(QxvRx)			14 ∃I
1, 2, 3	16) ∃x(QxvRx)			12, 13, 15 ∃E
1, 2, 3	17) (∃x(QxvRx)&~∃x(QxvRx))	2, 16 &I
1, 2	18) ~∀xPx 			3, 17 ~I

m. (∃x~Px→∀x~Qx), (∃x~Px→∃xQx), ∀x(Px→Rx) ⊢ ∀xRx

1		1) (∃x~Px→∀x~Qx)	A
2		2) (∃x~Px→∃xQx)		A
3		3) ∀x(Px→Rx)		A
4		4) ~Pc			A
4 		5) ∃x~Px			4 ∃I
1, 4 		6) ∀x~Qx		1, 5 →E
2, 4 		7) ∃xQx			2, 5 →E
8		8) Qa			A
9		9) ~(Sb&~Sb)		A
1, 4 		10) ~Qa			6 ∀E
1, 4, 8 	11) (Qa&~Qa)		8, 10 &I
1, 4, 8 	12) (Sb&~Sb) 		9, 11 ~E
1, 2, 4 	13) (Sb&~Sb)		7, 8, 12 ∃E
1, 2		14) Pc			4, 13 ~E
3		15) (Pc→Rc)		3∀E
1, 2, 3 	16) Rc			14, 15 →E
1, 2, 3		17) ∀xRx		16 ∀I

n. ~∃x(Px∨Qx), (∃xRx→∃xPx), (∃xSx→∃xQx) ⊢ ~∃x(Rx∨Sx)

1		1) ~∃x(PxvQx)			A
2		2) (∃xRx→∃xPx)			A
3		3) (∃xSx→∃xQx)			A
4		4) ∃x(RxvSx)			A
5		5) Ra				A
5 		6) ∃xRx				5 ∃I
2, 5 		7) ∃xPx				2, 6 →E
8		8) Pb				A
8		9) (PbvQb)			8 vI
8		10) ∃x(PxvQx)			9∃I
2, 5		11) ∃x(PxvQx)			7,8,10 ∃E
1, 2, 5		12) (∃x(PxvQx)&~∃x(PxvQx))	1, 11 &I
1, 2		13) ~Ra				5, 12 ~I
14		14) Sa				A
14		15) ∃xSx				14 ∃I
3, 14 		16) ∃xQx				3, 15 →E
17		17) Qa				A
17		18) (PavQa)			17 vI
17		19) ∃x(PxvQx)			18 ∃I
3, 14 		20) ∃x(PxvQx)			16, 17, 19 ∃E
1, 3, 14	21) (∃x(PxvQx)&~∃x(PxvQx)) 	1, 20 &I
1, 3		22) ~Sa				14, 21 ~I
23		23) (RavSa)			A
24		24) ~(Tb&~Tb)			A
1, 2, 23	25) Sa				13, 23 vE
1 ,2, 3, 23	26) (Sa&~Sa)			22, 25 &I
1, 2, 3, 23	27) (Tb&~Tb)			24, 26 ~E
1, 2, 3, 4 	28) (Tb&~Tb)			4, 23, 27 ∃E
1, 2, 3		29) ~∃x(RxvSx)			4, 28 ~I

§2. A final word

MPL is a subset of what is known as first-order predicate logic. In MPL, our predicates are all "one-place" predicates which can be combined with only one variable or name. In standard predicate logic, we can have "two-place" or "multi-place" predicates, e.g. Pxy, Qabc. This allows for a system with higher expressive power. So for example, we can use Lbc to mean "b loves c", and then prove "something loves something", which we cannot do in MPL.

A bit of history and metalogic: It was the mathematician and logician Kurt Gödel who first succeeded in proving the completeness of predicate logic in 1929. His proof is known as Gödel's completeness theorem.

But there is also another famous proof he has made, which is Gödel's incompleteness theorem! Roughly, what it says is that in any consistent formal system of logic that is powerful enough to include basic arithmetic, there will be valid wff that cannot be proven (these are systems more powerful than MPL). Think for a moment: it doesn't matter how powerful your mathematical rules are. There will always be true theorems that CANNOT be proven, and it is not because you are not smart enough! This is one of the most amazing and important results in modern logic and the foundations of mathematics.

We have come to the end of the tutorials on formal logic. There is a lot more you can learn from here onwards. The next step would be to study first-order predicate logic in full. Afterwards, you can start learning about second-order logic, which include quantifying over properties. In addition, you can study the connections between set theory and logic, and see how they help us formalize arithmetic and other branches of mathematics. Furthermore, there are lots of interesting connections between computation and logic. There are also all sorts of systems of so-called non-classical logic which you can learn about. Have fun!

previous tutorial