Home MATH 318 Wednesday, October 19, 2011

Wednesday, October 19, 2011 CC-BY-NC
A long proof and more on signatures

Maintainer: admin

1Proving properties of function composition

1.1Composing two injective functions

Continued from last class.

$$\forall x \forall y (fx = fy \to x = y),\, \forall x \forall y(gx = gy \to x = y) \vdash \forall x \forall y(gfx = gfy \to x = y)$$

Sequent Justification/rule
(1) $\forall x \forall y (gx = gy \to x = y) \vdash gfx = gfy \to fx = fy$ $\forall$-elimination twice1
(2) $gfx = gfy \to fx = fy, \, gfx = gfy \vdash fx = fy$ Tautology
(3) $\forall x \forall y (gx = gy \to x = y),\, gfx = gfy \vdash fx = fy$ Transitivity using (1), (2)
(4) $\forall x \forall y(fx = fy \to x = y) \vdash fx = fy \to x = y$ $\forall$-elimination twice
(5) $\forall x \forall y(fx = fy \to x = y),\,fy = fy \vdash x = y$ Deduction from (4)
(6) $\forall x\forall y(fx = fy \to x = y),\,\forall x \forall y(gx = gy \to x=y),\, gfx = gfy \vdash x = y$ Transitivity using (3), (5)
(7) $\forall x \forall y(fx = fy \to x = y),\,\forall x \forall y(gx = gy \to x = y) \vdash gfx = gfy \to x = y$ Deduction from (6)
(8) $\forall x \forall y(fx = fy \to x = y),\,\forall x \forall y(gx = gy \to x = y) \vdash \forall x \forall y (gfx = gfy \to x = y)$ $\forall$-introduction from (7), twice

1.2Composing two surjective functions

$$\forall x \exists y (fy=x),\, \forall x \exists y (gy = x) \vdash \forall x \exists y(gfy = x)$$

So when you compose two surjective functions, the result is surjective. Note that although $\forall y \exists x (fx=y)$ is more obviously

Sequent Justification/rule
(1) $\forall x \exists (gy = x) \vdash \exists y(gy = x)$ $\forall$-elimination
(2) $\exists y (gy=x) \vdash \exists z (gz=x)$ Change of bound variable
(3) $\forall x \exists y (fy=x) \vdash \exists y (fy=z)$ $\forall$-elimination
(4) $fy=z \vdash gfy=gz$ Substitution
(5) $\vdash \forall x \forall y \forall z ((x = y \land y=z) \to x=z)$ Logical axiom
(6) $\forall x \forall y \forall z ((x =y \land y = z ) \to x =z) \vdash (gfy = gz \land gz = x) \to gfy=x$ Change of bound variable
(7) $\forall u \forall v \forall w ((u = v \land v = w) \to u = w) \vdash (gfy = gz \land gz = x) \to gfy = x$ $\forall$-elimination three times
(8) $\vdash (gfy = gz \land gz=x) \to gfy = x$ Transitivity (twice) using (5), (6) and (7)
(9) $gfy = gz \land gz = x \vdash gfy = x$ Deduction from (8)
(10) $gfy = gz \land gz = x \vdash \exists y (gfy = x)$ $\exists$-introduction from (9)
(11) $gfy = gz,\,gz=x \vdash gfy = gz \land gz = x$ Tautology
(12) $fy = z,\,gz=x \vdash \exists y (gfy = x)$ Transitivity (twice) using (4), (10) and (11)
(13) $\exists y (fy = z),\,gz=x \vdash \exists y (gfy = x)$ $\exists$-elimination using (12)
(14) $\forall x \exists y (fy=x),\,gz=x \vdash \exists y (gfy=x)$ Transitivity using (3) and (13)
(15) $\forall x \exists y (fy=x),\,\exists z(gz=x) \vdash \exists y (gfy = x)$ $\exists$-elimination from (14)
(16) $\forall x \exists y(fy=x),\,\forall x \exists y (gy=x) \vdash \exists y (gfy=x)$ Transitivity using (12) and (15)
(17) $\forall x \exists y (fy=x),\, \forall x \exists y(gy =x) \vdash \forall x \exists y (gfy=x)$ $\forall$-introduction from (16)

2Structures in predicate calculus

Fix a signature $\Sigma$. A $\Sigma$-structure (model, interpretation, context etc) $\mathcal{M}$ consists of a non-empty set $M$ and for each contant symbol, an element $C^{\mathcal{M}} \in M$ (so each constant symbol is associated with a given element of the structure). For each $n$-ary function symbol $f$, a function $f^{\mathcal{M}}: M^n \to M$, and for each predicate symbol, same idea etc.

Given a $\Sigma$-structure $\mathcal{M}$, a formula $\varphi(x_1, ... x_n)$ and a tuple $(a_1, ... a_n) \in M^n$, define when $M \models \varphi (\bar a)$ ("$\varphi$ is true of $\bar a$ in the structure $M$).

(I'm missing notes for this)

  1. There is also a change of bound variable done during the $\forall$-elimination (so $x$ becomes $fx$ and $y$ becomes $fy$), which is valid in this quasi-formal proofonly?. ↩