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
Andrew Ashworth (Apr 12 2020 at 05:06):
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?
Mario Carneiro (Apr 12 2020 at 05:39):
Mario Carneiro (Apr 12 2020 at 05:40):
not computably, but you can define a function from
(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
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?
Kenny Lau (Apr 12 2020 at 05:44):
Mario Carneiro (Apr 12 2020 at 05:44):
The quantifier would range over
formula, and then you would replace
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
Last updated: May 08 2021 at 19:11 UTC