Zulip Chat Archive

Stream: new members

Topic: axiom schemas in Lean?


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Chris M (Apr 12 2020 at 04:54):

lol, I hope you're joking

view this post on Zulip Andrew Ashworth (Apr 12 2020 at 05:06):

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

view this post on Zulip Chris M (Apr 12 2020 at 05:14):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:30):

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

view this post on Zulip Kenny Lau (Apr 12 2020 at 05:39):

can you evaluate a FOL formula?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:39):

sure

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 12 2020 at 05:41):

oh right, Prop is impredicative

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:42):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 05:43):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 12 2020 at 05:44):

yeah

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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