## Stream: new members

### Topic: axiom schemas in Lean?

#### Chris M (Apr 12 2020 at 04:46):

In set theory, we have the axiom schema of specification: Let ϕ(u, p) be a formula. Then there is an axiom ∀X ∀p ∃Y ∀u (u ∈ Y ↔ u ∈ X ∧ ϕ(u, p)).

It seems like in CoIC we can formalize this as: ∀(φ : Set → Set → Prop) , ∀X, ∀p, ∃S, (∀u, u ε S ↔ u ε X ∧ φ u p), where I'm interpreting ε as $\in$. However, it seems to me that strictly speaking, this is stronger than the axiom schema as used in set theory, since φ : Set → Set → Prop does not have to correspond to any first-order formula. It could be a binary property that cannot be represented in (first-order) logic.

How do we more faithfully represent axiom schemas in Lean?

#### Kenny Lau (Apr 12 2020 at 04:53):

first formalize a theory of FOL (first order languages), then build a model of ZFC, and then verify that the model satisfies the axioms

#### Chris M (Apr 12 2020 at 04:54):

lol, I hope you're joking

#### Chris M (Apr 12 2020 at 05:14):

Isn't there a simple way that one can formalize axiom schema's in Lean?

#### Mario Carneiro (Apr 12 2020 at 05:28):

@Chris M What you described is the way we represent schemas. Yes, this is a second order formulation, and it's not exactly equivalent, but it is the version that plays well with everything else. The quantifier ranges over all formulas that can be described in lean, which is more important for formalization in lean. This is strictly more than the set of formulas that can be described in FOL, because Lean is has access to higher order quantifiers, and if you want to capture all and only the first order formulas you have to define what a first order formula is, which requires a definition of FOL as kenny said.

#### Mario Carneiro (Apr 12 2020 at 05:30):

you don't have to build a model of ZFC though

#### Kenny Lau (Apr 12 2020 at 05:39):

can you evaluate a FOL formula?

sure

#### Mario Carneiro (Apr 12 2020 at 05:40):

not computably, but you can define a function from formula to (nat -> Prop) -> Prop or something like that

#### Kenny Lau (Apr 12 2020 at 05:41):

oh right, Prop is impredicative

#### Mario Carneiro (Apr 12 2020 at 05:41):

Impredicativity isn't needed here, i.e. you could do the same in Type if the model also lives in Type

#### Mario Carneiro (Apr 12 2020 at 05:42):

actually the type of the eval should be formula -> (nat -> A) -> Prop

#### Mario Carneiro (Apr 12 2020 at 05:43):

where the function is providing elements of the model A for every free variable

#### Chris M (Apr 12 2020 at 05:44):

When you say "define what a FOL formula is", does that mean you can no longer use the ∀(φ : Set → Set → Prop) approach, because a formula is now no longer a function to Prop, but a normal structure like any other structure we'd want to formalize?

yeah

#### Mario Carneiro (Apr 12 2020 at 05:44):

The quantifier would range over formula, and then you would replace phi with eval2 phi : Set -> Set -> Prop

#### Mario Carneiro (Apr 12 2020 at 05:45):

You can restrict attention to two variable formulas, or set variables out of range to a default value

#### Mario Carneiro (Apr 12 2020 at 05:46):

If you use a quantifier ∀(φ : Set → Set → Prop), then it's a higher order quantifier so you get those "indescribable" formulas

#### Reid Barton (Apr 12 2020 at 12:49):

Chris M said:

lol, I hope you're joking

https://github.com/flypitch/flypitch/

Last updated: May 08 2021 at 19:11 UTC