# Zulip Chat Archive

## Stream: maths

### Topic: I don't understand forall in flypitch

#### Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:01):

I'm reading flypitch, and in the definition of `preformula`

, we have:

```
inductive preformula : ℕ → Type u
...
| all (f : preformula 0) : preformula 0
```

I must be missing something -- don't we need to specify which variable we're quantifying over? How do we distinguish `forall x, x < y`

from `forall y, x < y`

?

#### Johan Commelin (Jul 29 2020 at 07:04):

I guess it uses de Bruijn indices, and so `f`

contains the info

#### Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:09):

I see, so the `x < y`

in `forall x, x < y`

is *different* from the `x < y`

in `forall y, x < y`

.

#### Johan Commelin (Jul 29 2020 at 07:10):

Yup (that's my guess)

#### Kenny Lau (Jul 29 2020 at 07:19):

```
/- preterm L l is a partially applied term. if applied to n terms, it becomes a term.
* Every element of preterm L 0 is a well-formed term.
* We use this encoding to avoid mutual or nested inductive types, since those are not too convenient to work with in Lean. -/
inductive preterm : ℕ → Type u
| var {} : ∀ (k : ℕ), preterm 0
| func : ∀ {l : ℕ} (f : L.functions l), preterm l
| app : ∀ {l : ℕ} (t : preterm (l + 1)) (s : preterm 0), preterm l
export preterm
@[reducible] def term := preterm L 0
/- preformula l is a partially applied formula. if applied to n terms, it becomes a formula.
* We only have implication as binary connective. Since we use classical logic, we can define
the other connectives from implication and falsum.
* Similarly, universal quantification is our only quantifier.
* We could make `falsum` and `equal` into elements of rel. However, if we do that, then we cannot make the interpretation of them in a model definitionally what we want.
-/
variable (L)
inductive preformula : ℕ → Type u
| falsum {} : preformula 0
| equal (t₁ t₂ : term L) : preformula 0
| rel {l : ℕ} (R : L.relations l) : preformula l
| apprel {l : ℕ} (f : preformula (l + 1)) (t : term L) : preformula l
| imp (f₁ f₂ : preformula 0) : preformula 0
| all (f : preformula 0) : preformula 0
export preformula
@[reducible] def formula := preformula L 0
```

#### Kenny Lau (Jul 29 2020 at 07:21):

so presumably $\forall x, x < y$ is `all (apprel (apprel (rel ()) (var 0)) (var 1))`

and $\forall y, x < y$ is with `0`

and `1`

swapped

#### Kenny Lau (Jul 29 2020 at 07:22):

more evidence is:

```
/- subst_term t s n substitutes s for (&n) and reduces the level of all variables above n by 1 -/
def subst_term : ∀ {l}, preterm L l → term L → ℕ → preterm L l
| _ &k s n := subst_realize var (s ↑ n) n k
| _ (func f) s n := func f
| _ (app t₁ t₂) s n := app (subst_term t₁ s n) (subst_term t₂ s n)
@[simp] def subst_formula : ∀ {l}, preformula L l → term L → ℕ → preformula L l
| _ falsum s n := falsum
| _ (t₁ ≃ t₂) s n := subst_term t₁ s n ≃ subst_term t₂ s n
| _ (rel R) s n := rel R
| _ (apprel f t) s n := apprel (subst_formula f s n) (subst_term t s n)
| _ (f₁ ⟹ f₂) s n := subst_formula f₁ s n ⟹ subst_formula f₂ s n
| _ (∀' f) s n := ∀' subst_formula f s (n+1)
```

#### Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:31):

Right -- so we always quantify over `var 0`

.

So if we want to say `forall z, x < y`

, we'd write the same thing with `0`

and `1`

replaced with `1`

and `2`

, etc.

#### Kenny Lau (Jul 29 2020 at 07:32):

you would actually need to look at how a formula is interpreted, but the file is too big and causes performance issues for my humble chrome browser so I'm afraid I can't help you with that

#### Abhimanyu Pallavi Sudhir (Jul 29 2020 at 07:33):

ok, thanks

#### Mario Carneiro (Jul 29 2020 at 07:52):

@Abhimanyu Pallavi Sudhir The answer to your question is yes

#### Mario Carneiro (Jul 29 2020 at 07:53):

@Kenny Lau I don't think formula interpretation comes into it? He's just talking about writing formulae

#### Kenny Lau (Jul 29 2020 at 07:54):

well to know what formula a term of `pre_formula 0`

represents, one needs to look at the code where they define interpretation of a `pre_formula 0`

#### Kenny Lau (Jul 29 2020 at 07:54):

```
/- realization of formulas -/
@[simp] def realize_formula {S : Structure L} : ∀{l}, (ℕ → S) → preformula L l → dvector S l → Prop
| _ v falsum xs := false
| _ v (t₁ ≃ t₂) xs := realize_term v t₁ xs = realize_term v t₂ xs
| _ v (rel R) xs := S.rel_map R xs
| _ v (apprel f t) xs := realize_formula v f $ realize_term v t ([])::xs
| _ v (f₁ ⟹ f₂) xs := realize_formula v f₁ xs → realize_formula v f₂ xs
| _ v (∀' f) xs := ∀(x : S), realize_formula (v [x // 0]) f xs
```

Last updated: May 06 2021 at 18:20 UTC