A mini “Logic Toolbox”

Facts-List

Here I list some tools/facts from old M1090 classes I taught, which you can use in M2090 (and beyond) “off the shelf”, without proof.

The list is long, but hopefully useful. The axioms of arithmetic and set theory are at the end.

The following metatheorems are good for both Propositional (Ch. 3–4) and Predicate Calculus (Ch. 8–9):

1. Redundant True. Γ ⊢ A iff Γ ⊢ A ≡ true

“Redundant true” is very convenient. Make a habit of using it. But do be careful! “true” is a “meaningless symbol”,^{∗} not the truth value t (also pronounced “true”) of the metatheory.

2. Modus Ponens (MP). A, A ⇒ B ⊢ B

3. Cut Rule. A ∨ B, ¬A ∨ C ⊢ B ∨ C

4. Deduction Theorem. If Γ, A ⊢ B, then Γ ⊢ A ⇒ B

5. Proof by contradiction. Γ, ¬A ⊢ false iff Γ ⊢ A

6. Post’s Theorem. (Also called “tautology theorem”, or even “completeness of Propositional Calculus theorem”)

If ⊧_{taut} A, then ⊢ A.

Also: If B_{1}, …, B_{n} ⊧_{taut} A, then B_{1}, …, B_{n} ⊢ A

7. Proof by cases. A ⇒ B, C ⇒ D ⊢ A ∨ C ⇒ B ∨ D

Also the special case: A ⇒ B, C ⇒ B ⊢ A ∨ C ⇒ B

Recall that if A is a formula and x_{1}, … x_{n}, where n ≥ 0, are ANY variables (occurring or not occurring free in A, we don’t care) then (∀x_{1})(∀x_{2}) … (∀x_{n})A is called a “partial generalisation” of A. If n = 0, then the “prefix” (∀x_{1})(∀x_{2}) … (∀x_{n}) is empty.^{†} Thus A is one of the partial generalizations of A. Example: Consider x < y (where < is some nonlogical predicate of arity 2). Here I list some partial generalizations of that formula:

x < y (∀z)x < y (∀x)x < y (∀y)(∀x)x < y (∀x)(∀y)x < y (∀x)(∀x)(∀x)(∀x)x < y.

∗Yes, it is one (multiple character) symbol, just like the symbol “else” of a programming language like Pascal. As I mentioned in class, some people go out of their way to emphasise that true and false are just meaningless symbols—not “values”—and write instead ⊤ and ⊥ respectively. We will not use ⊤ and ⊥, but we must always remember that “Γ ⊢ A ≡ true” is not pronounced “A is true” but “Γ proves that A is equivalent to the formula true”.

†This is a standard convention: A sequence x_{1}, …, x_{n}, where n ≥ 0, is “x_{1}” if n = 1, “x_{1}, x_{2}, x_{3}” if n = 3, etc. It is empty by convention, if n = 0, the thinking being that we have stopped listing the sequence before we started. So, nothing is listed.

As far as we—i.e., this class—are concerned,

the following are the axioms for Ch.9 and 8—NOT the ones listed in G & S:

Any partial generalization of any formula in groups Ax1–Ax6 is an axiom for Predicate Calculus.

Groups Ax1–Ax6 contain:

Ax1. All tautologies.

Ax2. For every formula A, (∀x)A ⇒ A[x := t], for any term t.

Ax3. For every formula A and variable x not free in A, the formula A ⇒ (∀x)A.

Ax4. For every formulas A and B, (∀x)(A ⇒ B) ⇒ (∀x)A ⇒ (∀x)B.

Ax5. For each object variable x, the formula x = x.

Ax6. (Leibniz’s characterisation of equality—1st order version. “3.83”) For any formula A, any object variable x and any terms t, s, the formula t = s ⇒ (A[x := t] ≡ A[x := s]).

Primary rules of inference are Equanimity and PSL in both Ch.3 and Ch.9.

\frac{A ≡ B}{C[p := A] ≡ C[p := B]}, provided p is not in the scope of a quantifier.
(P SL)

Translations

(∃x)A translates to ¬(∀x)¬A

(∀x|A : B) translates to (∀x)(A ⇒ B) (Range trading with ∀)

(∃x|A : B) translates to (∃x)(A ∧ B) (Range trading with ∃)

Useful facts from Predicate Calculus (proved in class—you may use them without proof):

We know that SLCS, WLUS (as well as GS-Leibniz “8.12(a)” and “8.12(b)”) are derived rules. These are the following (I am using “GS”-notation for 8.12(a–b)):

Same as PSL, without the condition: A ≡ B ⊢ C[p := A] ≡ C[p := B]  (SLCS)
if ⊢ A ≡ B, then ⊢ C[p \ A] ≡ C[p \ B]  (W LUS)
if ⊢ A ≡ B, then ⊢ ( ∗ x|C[p := A] : D) ≡ ( ∗ x|C[p := B] : D)  (8.12(a))
if ⊢ D ⇒ (A ≡ B), then ⊢ ( ∗ x|D : C[p := A]) ≡ ( ∗ x|D : C[p := B])  (8.12(b))

where in 8.12(a–b) “∗” stands everywhere for the symbol “∀”, or the symbol “∃”.

▶ More “rules” and (meta)theorems. (Only the “∀-versions” are listed. This should help you remember the “∃-versions” that were also covered in the M1090 class.):

(i) ⊢ A ≡ (∀x)A, provided x is not free in A

⊢ A ≡ (∃x)A, provided x is not free in A

(ii) Dummy renaming.

If z does not occur in (∀x)A as either free or bound, then ⊢ (∀x)A ≡ (∀z)(A[x := z])

If z does not occur in (∃x)A as either free or bound, then ⊢ (∃x)A ≡ (∃z)(A[x := z])

(iii) ∀ over ∘ distribution, where ∘ is “∨” or “⇒”.

⊢ A ∘ (∀x)B ≡ (∀x)(A ∘ B), provided x is not free in A

∃ over ∧ distribution

⊢ A ∧ (∃x)B ≡ (∃x)(A ∧ B), provided x is not free in A

(iv) ∀ over ∧ distribution.

⊢ (∀x)A ∧ (∀x)B ≡ (∀x)(A ∧ B)

∃ over ∨ distribution.

⊢ (∃x)A ∨ (∃x)B ≡ (∃x)(A ∨ B)

(v) ∀ commutativity (symmetry).

⊢ (∀x)(∀y)A ≡ (∀y)(∀x)A

∃ commutativity (symmetry).

⊢ (∃x)(∃y)A ≡ (∃y)(∃x)A

(vi) Specialization. Follows from Ax2 and MP. (∀x)A ⊢ A[x := t], for any term t.

(vii) Generalization. If Γ ⊢ A and if, moreover, the formulas in Γ have no free x occurrences, then also Γ ⊢ (∀x)A.

(viii) ∀ Monotonicity. If Γ ⊢ A ⇒ B so that the formulas in Γ have no free x occurrences, then we can infer

Γ ⊢ (∀x)A ⇒ (∀x)B

∃ Monotonicity. If Γ ⊢ A ⇒ B so that the formulas in Γ have no free x occurrences, then we can infer

Γ ⊢ (∃x)A ⇒ (∃x)B

(ix) ∀ Introduction; a special case of ∀ Monotonicity that uses (i) above. If Γ ⊢ A ⇒ B so that neither the formulas in Γ nor A have any free x occurrences, then we can infer

Γ ⊢ A ⇒ (∀x)B

∃ Introduction; a special case of ∃ Monotonicity that uses (i) above. If Γ ⊢ A ⇒ B so that neither the formulas in Γ nor B have any free x occurrences, then we can infer

Γ ⊢ (∃x)A ⇒ B

(x) Super-WLUS or sWLUS. If Γ ⊢ A ≡ B so that the formulas in Γ have no free variables, then we can infer

Γ ⊢ C[p \ A] ≡ C[p \ B]

where C is any formula and p is a Boolean variable.

(xi) (Equals-for-equals in terms) For any terms t, s, t′ and variable x,

⊢ t = t′ ⇒ s[x := t] = s[x := t′]

(xii) Finally, the Auxiliary Variable (“witness”) Metatheorem. If Γ ⊢ (∃x)A, and if y is a variable that does not occur as either free or bound variable in any of A or B or the formulas of Γ, then

Γ, A[x := y] ⊢ B implies Γ ⊢ B

Semantics facts

Propositional Calculus  Predicate Calculus
(Boolean Soundness) ⊢ A implies ⊧_{taut} A  ⊢ A does NOT imply ⊧_{taut} A
(Post) ⊧_{taut} A implies ⊢ A  However, (Ax1) ⊧_{taut} A implies ⊢ A

(Pred. Calc. Soundness) ⊢ A implies ⊧ A (Gödel Completeness) ⊧ A implies ⊢ A CAUTION! The above facts/tools are only a fraction of what one should

have seen in M1090. They are very important and very useful, and that is why I list them for your easy reference here.

You can still use without proof ALL the things one sees in M1090, such as “one-point-rule”, “deMorgan’s laws”, etc. Subject to the follow-

ing constraints:

(1) AXIOMS for predicate calculus are those listed here, NOT those listed in Ch.8–9 in G & S. Happily, the latter are theorems for us, and can be used. But \underline{don’t} quote them as axioms!

(2) Forget all the “facts” in Ch.8 involving “∗”, UNLESS you interpret “∗” exclusively as one of ∃ or ∀. NO OTHER INTERPRETATIONS (e.g., “+, ∪, ∩”) of “∗” lead to FACTS OF PURE LOGIC (because +, ∪, etc. are non logical symbols and one needs nonlogical axioms before discussing them!)

Peano Arithmetic Axioms

These are the universal closures of the following formulas ((Ind) is a schema):

(S)1. ¬0 = Sx

(S)2. Sx = Sy ⇒ x = y (“1-1ness of S”)

(+)1. x + 0 = x

(+)2. x + Sy = S(x + y)

(·)1. x · 0 = 0

(·)2. x · Sy = x · y + x

(<)1. ¬x < 0

(<)2. x < Sy ≡ x < y ∨ x = y

(<)3. x < y ∨ x = y ∨ y < x

And the Induction Schema, one axiom for each formula A:

(Ind)  A[x := 0] ∧ (∀x)(A ⇒ A[x := Sx]) ⇒ A

CVI (Course-of-Values Induction) is a derived schema, the following

(CVI)  (∀x)((∀z < x)A[z] ⇒ A[x]) ⇒ (∀x)A[x]

(Ind) is applied by proving A[0] (Basis) and then A[Sx] (or informally written A[x + 1]—this is the goto step) by assuming A[x] (the I.H.).

(CVI) is applied by assuming (∀z < x)A[z] (I.H.) and then proving A[x] (goto). It is important to do the “boundary cases” (Basis cases) during this step. These are cases that are not helped by the I.H.

Set Theory

First off, for any set-type variable S formula A and typeless variable x (i.e., of type set or atom), S = {x|A[x]} is short for (∀x)(x ∈ S ≡ A[x]). From this we get the provable principle of ∈-elimination:

ST ⊢ t ∈ {x|A} ≡ A[x := t], for any term t

Formally, “{x|A} is a set” is captured by (∃y)y = {x|A} where y is of type set. Using the above convention we can eliminate “{…}” and write

(∃y)(∀x)(x ∈ y ≡ A)

The axioms of set theory that we covered are the universal closures of the formulas that express the following statements.^{‡} Note that, deliberately, I have not introduced three important axioms that I consider “non-elementary”: The axiom of choice, the axiom of replacement, and the axiom of infinity. These three do not appear below.

Axiom1. \underline{Extensionality}: For all variables S, T of type set, and all typeless

variables x,

(∀x)(x ∈ S ≡ x ∈ T) ⇒ S = T

Axiom2. \underline{Empty Set}: \{x|false\} is a set denoted by ∅

Axiom3. \underline{Atoms contain no members}: If x is of type atom and y is typeless, then we have ¬(∃y)y ∈ x

Axiom4. \underline{Subsets}: Any subset of a set is a set.

Axiom5. \underline{Pair}: For any sets or atoms x and y, \{x, y\} is a set

Axiom6. \underline{Union}: For any sets S and T their union is a set. For any family of sets F, its union ⋃ F is a set

Axiom7. \underline{Foundation}: It is impossible to have an infinite descending chain

… ∈ a′′′ ∈ a′′ ∈ a ∈ a

Axiom8. \underline{Power Set}: For any set S, \{x|x ⊆ S\} is a set

‡OK, some are already formulas