## Stream: new members

### Topic: Expressing the size of structures in FOL

#### Alexandre Rademaker (Sep 10 2020 at 02:54):

In FOL we can express that a structure must have a size n for a given n. A template for produce such a sentence can be easily defined using n variables. Can we define a function in Lean to produce such sentence given a n?

#### Mario Carneiro (Sep 10 2020 at 03:27):

Yes, but you need a definition of what a formula is to start with

#### Alexandre Rademaker (Sep 10 2020 at 03:32):

you mean, define formula as an inductive type?

#### Mario Carneiro (Sep 10 2020 at 03:39):

Yes. Something like this:

import data.list.defs

inductive fmla
| true : fmla
| eq : ℕ → ℕ → fmla
| not : fmla → fmla
| and : fmla → fmla → fmla
| all : fmla → fmla

def fmla.conj : list fmla → fmla := list.foldl fmla.and fmla.true

def at_least_n (n : ℕ) : fmla :=
fmla.all^[n] $fmla.conj$ do
j ← list.range n,
i ← list.range j,
[(fmla.eq i j).not]

#reduce at_least_n 3