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)$ »

Leave a comment