Expressing the size of structures in FOL

Stream: new members

[Alexandre Rademaker]

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]

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

[Alexandre Rademaker]

you mean, define formula as an inductive type?

[Mario Carneiro]

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

[Kenny Lau]

just read flypitch

[Alexandre Rademaker]

What is that?

[Alexandre Rademaker]

You are probably taking about https://flypitch.github.io/about/, right? My point is really much simpler. I am reacting to a student question on a want to procure FOL formulas from templates in Lean