How to create a FirstOrder.Language?

Stream: mathlib4

[C7X]

I want to create a FirstOrder.Language for the language of set theory, with one relation symbol for \in (and if necessary another relation symbol for =). I have the following idea, but I think I need to replace ZFSet with a type that has only ZFSet as a member. If I do this will it give me the first-order language I intend? If so, how do I do this?

import Mathlib

def FOST : FirstOrder.Language := {
  Functions := (fun _ ↦ PEmpty),
  Relations := (fun n ↦
    if n = 2 then ZFSet.Mem else PEmpty)
}

[C7X]

I think I have solved this, by looking at how it was done in the Flypitch project's zfc.leanand mathlib4's FirstOrder.Language.presburger. For future readers, here's my example:

import Mathlib

inductive FOSTRel : ℕ → Type
| mem : FOSTRel 2

def FOST : FirstOrder.Language := {
  Functions := (fun _ ↦ PEmpty),
  Relations := FOSTRel
}

[James E Hanson]

C7X said:

I think I have solved this, by looking at how it was done in the Flypitch project's zfc.leanand mathlib4's FirstOrder.Language.presburger. For future readers, here's my example:

import Mathlib

inductive FOSTRel : ℕ → Type
| mem : FOSTRel 2

def FOST : FirstOrder.Language := {
  Functions := (fun _ ↦ PEmpty),
  Relations := FOSTRel
}

Looking back at my recent attempt to do L (which did not go much beyond writing the definition down), I think you're going to want these instances eventually.

import Mathlib

inductive FOSTRel : ℕ → Type
| mem : FOSTRel 2
  deriving DecidableEq

def FOST : FirstOrder.Language := {
  Functions := (fun _ ↦ PEmpty),
  Relations := FOSTRel
}
  deriving FirstOrder.Language.IsRelational

[C7X]

Oh wow, I was trying to define L with this too, thanks for the advice!

[James E Hanson]

You're also maybe going to want a type class for languages that extend FOST and a term-forming function for the in-relation.

I can DM you what I did if you want.

[C7X]

Sure, that would be great!

[James E Hanson]

Also, if I recall correctly, the Flypitch project's paper mentioned the idea of maybe eventually doing L, so maybe @Floris van Doorn would have some relevant suggestions.

[James E Hanson]

Anyway, I kind of suspect that while the definition in terms of first-order definability is very easy to write down, the more common definition in terms of rudimentary functions or the Gödel operations are maybe going to be easier to work with in Lean.

[James E Hanson]

But maybe not. The existing Mathlib implementation of downward Löwenheim–Skolem may end up saving a lot of time if and when you get to condensation.

[Dexin Zhang]

That's nice! I feel inductive is usually better than if in defining FO symbols, since it 1. gives names for symbols 2. Allows you to do match or cases on variables of type Functions n or Relations n

[Dexin Zhang]

I'm also trying to define L recently. Flypitch uses an extended language that includes function symbols for empty sets, powersets, etc, which is good in defining formulas like "x is a function" or the axiom of choice. But it's hard to give interpretations when I want to say "every ZFSet has a structure of set theory" since arbitrary sets are not closed under these functions.

[Dexin Zhang]

Meanwhile, it's natural to use a language that contains purely one symbol of membership (and the equality), but it then seems harder to define the axioms of ZFC in this language. I find #26644 has a very nice idea on addressing this, it defines Class formulas that are predicates over all sets, but also allows one to use it as if using a term (and such formula is only meaningful if the Class is actually a set).

[C7X]

Great!

2. Allows you to do match or cases on variables of type Functions n or Relations n

I don't understand this yet, so I will guess that it comes up when I've done more work with FirstOrder (so far I just started).

Class formulas

I'll also have to look at how notations like ∀' work here, if they allow brief definition of formal formulas. Thanks for the pointer!

[Violeta Hernández]

(Oh, hi C7X! Glad to finally see you around here)

[C7X]

(Hi!)