axiom schemas in Lean?

Stream: new members

[Chris M]

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]

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]

lol, I hope you're joking

[Andrew Ashworth]

have fun: https://github.com/leanprover-community/mathlib/tree/master/src/set_theory

[Chris M]

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

[Mario Carneiro]

@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]

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

[Kenny Lau]

can you evaluate a FOL formula?

[Mario Carneiro]

sure

[Mario Carneiro]

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

[Kenny Lau]

oh right, Prop is impredicative

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris M]

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?

[Kenny Lau]

yeah

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

Chris M said:

lol, I hope you're joking

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