Exercise Sheet 1

Teacher: Gilles Dowek

Exercise 1

Consider a language with

• 3 sorts of terms:

  • point: $p$
  • line: $l$
  • and scalar: $s$

• 2 predicate symbols:

  • $=$ with arity $⟨s, s⟩$
  • $∈$ with arity $⟨p, l⟩$

• 2 function symbols:

  • $d$ (distance) with arity $⟨p, p, s⟩$
  • $b$ (bisector (false friend: “médiatrice” in French)) with arity $⟨p, p, l⟩$

Let

\[Γ \, ≝ \, \lbrace ∀x,y,z. (x ∈ b(y, z) ⇔ d(x, y) = d(x,z)), \\ ∀x,y,z. ((x=y ∧ y=z) ⇒ x=z) \rbrace\]

and

\[A \, ≝ \, ∀w, x, y, z. ((w ∈ b(x, y) ∧ w ∈ b(y, z)) ⇒ w ∈ b(x, z))\]

stating that if two bisectors of the triangle $xyz$ intersect at point $w$, then the three biscetors intersect at this point.

Write a proof of a sequent $Γ ⊢ A$.

$Γ, Δ ⊢ d(w,x) = d(w, y) ∧ d(w, y) = d(w, z) ⇒ d(w,x) = d(w, z) \mid \quad\text{ axiom}$
$\phantom{Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ d(w, x) = d(w, z)} \mid \quad\text{ axiom}$
$\phantom{Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ d(w, x) = d(w, z)} \mid Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ ∀w, x, z. d(w, x) = d(w, z) ⇔ w ∈ b(x, z) \quad\text{ ∀-elim}$
$\phantom{Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ d(w, x) = d(w, z)} \mid Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ d(w, x) = d(w, z) ⇔ w ∈ b(x, z) \quad\text{ ∧-elim}$
$Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ d(w, x) = d(w, z) \mid Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ d(w, x) = d(w, z) ⇒ w ∈ b(x, z)$	$⇒$-elim
$Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ w ∈ b(x, z)$	$⇒$-intro
$Γ ⊢ (w ∈ b(x, y) ∧ w ∈ b(y, z)) ⇒ w ∈ b(x, z)$	$∀$-intro*
$Γ ⊢ ∀w, x, y, z. ((w ∈ b(x, y) ∧ w ∈ b(y, z)) ⇒ w ∈ b(x, z))$

and

axiom $\phantom{Γ, Δ ⊢ ∀α, β, γ. α = β ∧ β = γ ⇒ α = γ } \qquad\qquad\qquad\qquad\mid$
$Γ, Δ ⊢ ∀α, β, γ. α = β ∧ β = γ ⇒ α = γ \quad \text{ ∀-elim*}\qquad\qquad\qquad \mid Γ, Δ ⊢ d(w,x) = d(w, y) ∧ d(w, y) = d(w, z)$
$Γ, Δ ⊢ d(w,x) = d(w, y) ∧ d(w, y) = d(w, z) ⇒ d(w,x) = d(w, z) \mid Γ, Δ ⊢ d(w,x) = d(w, y) ∧ d(w, y) = d(w, z)$
$Γ, w ∈ b(x, y) ∧ w ∈ b(y, z) ⊢ d(w, x) = d(w, z)$

and

$\phantom{Γ, Δ ⊢ d(w, x) = d(w, y)} \mid $ same proof as before
$Γ, Δ ⊢ d(w, x) = d(w, y) \mid Γ, Δ ⊢ d(w, y) = d(w, z)$
$Γ, Δ ⊢ d(w, x) = d(w, y) \mid Γ, Δ ⊢ d(w, y) = d(w, z)$	∧-intro
$Γ, Δ ⊢ d(w,x) = d(w, y) ∧ d(w, y) = d(w, z)$

and

$Γ, Δ ⊢ d(w, x) = d(w, y) \mid Γ, Δ ⊢ d(w, y) = d(w, z)$
$Γ, Δ ⊢ d(w, x) = d(w, y) \mid Γ, Δ ⊢ d(w, y) = d(w, z)$	∧-intro
$Γ, Δ ⊢ d(w,x) = d(w, y) ∧ d(w, y) = d(w, z)$

then for each of the sequents $Γ, Δ ⊢ d(w, x) = d(w, y)$ and $Γ, Δ ⊢ d(w, y) = d(w, z)$: $⇒$-elim with the premise $w ∈ b(x, y)$ (for the first), $∧$-elim, and axiom:

$Γ, Δ ⊢ w ∈ b(x, y) ⇔ d(w, x) = d(w, y) \; \mid \; \text{ axiom }$
$Γ, Δ ⊢ w ∈ b(x, y) ⇒ d(w, x) = d(w, y) \; \mid \; Γ, Δ ⊢ w ∈ b(x, y)$
$Γ, Δ ⊢ d(w, x) = d(w, y)$

Or, with modulo deduction: set this definition (rewrite rule) of the bisector:

\[x ∈ b(y, z) ⟶ d(x, y) = d(x, z)\]

Exercise 2

Weakening in ND: if $Γ ⊢ B$ is provable, then $Γ, A ⊢ B$ is provable

By induction on the structure of the proof. Beware of $∀$-intro though!

\[\cfrac{Γ ⊢ B}{Γ ⊢ ∀x. B}\text{ ∀-intro: only if } x ∉ fv(Γ)\]

So if we have $x ∉ fv(Γ, A)$, we can’t use the $∀$-intro, except by picking a fresh variable $y$ not appearing in $A$ (nor $Γ$):

\[\cfrac{Γ, A ⊢ B[x ← y]}{Γ, A ⊢ ∀y. B}\text{ ∀-intro: } y ∉ fv(Γ, A)\]

But we can circumvent all these explanations by saying: « modulo $α$-equivalence, we can assume without loss of generality that $x ∉ fv(Γ, A)$ »