Free variables

Stream: new members

[Guillaume Dubach]

What is the correct syntax to create (or speak of) a proposition with a free variable ? Say I want to call my variable (x : Nat), consider a proposition where x is free such as x = 2 (btw, this would not have type Prop, so what type would it be ?), and evaluate this at a particular integer, e.g. at 3, to get 3 = 2 : Prop?

[Kevin Buzzard]

This isn't related to the above discussion and would be better off in a new thread in #new members .

[Guillaume Dubach]

Sorry about this !

[Notification Bot]

2 messages were moved here from #lean4 > Lean 4 variable command discussion by Kyle Miller.

[Kyle Miller]

(I moved these messages to a new topic and didn't realize @Guillaume Dubach already create a new one, so then I merged them. Kevin's message is irrelevant in this new context. Sorry if any of this causes confusion!)

[Kyle Miller]

I think you're looking for the type Nat -> Prop. You write functions like fun x => x = 2 to create things of this type.

[Guillaume Dubach]

No, Nat -> Prop will not do, it's not the same thing. In Nat -> Prop you can change the proposition completely, the image of 2 and the image of 3 do not need to be related in any way...

[Guillaume Dubach]

For instance: there are uncountably many things of type Nat -> Prop, right ? But there should be countably many well-built propositions with a free variable...

[Kyle Miller]

fun x => x = 2 is the proposition with a free variable x

[Kyle Miller]

If p := fun x => x = 2, then p 3 is 3 = 2 : Prop.

[Guillaume Dubach]

Sure, I agree that what I am talking about can be seen as a particular case of Nat -> Prop. But so is the function that would associate x = 2 to even numbers and x = 3 to odd numbers, and this example is not just a given proposition with a free variable.

Edit: of course it is, as Kevin's example below shows; and anything I actually write could be turned into a Nat -> Prop the same way, but my point was that I am interested in the (countably many) propositions that can be written, then evaluated at any particular n.

[Kyle Miller]

This is fine if you just want a single such proposition with a free variable, but if you want to quantify over propositions with a single free variable (and you only want the ones that come from a syntactic one) I think you have to create your own type that represents propositions and give a Prop interpretation of them.

[Kyle Miller]

What's your goal here?

[Guillaume Dubach]

Yes, I would like to quantify over such propositions, exactly !

[Reid Barton]

Guillaume Dubach said:

For instance: there are uncountably many things of type Nat -> Prop, right ? But there should be countably many well-built propositions with a free variable...

This is mixing the semantic and syntactic levels.

[Kevin Buzzard]

I am confused about what your question is. A proposition with a free variable is the same thing as a family of propositions is the same thing as a function from Nat to Prop. Note that this is unrelated to the Lean variable command, which does something else :-)

[Kevin Buzzard]

The even/odd example is just the proposition P(x)=if x is even then x=2 else x=3 (def P : ℕ → Prop := fun x ↦ if x % 2 = 0 then x = 2 else x = 3)

[Kyle Miller]

Guillaume Dubach said:

Yes, I would like to quantify over such propositions, exactly !

What are you trying to do by quantifying over propositions though? The details matter. In Lean we're generally happy with quantifying over Nat -> Prop as propositions-with-a-free-variable.

[Guillaume Dubach]

I would like to see why Richard's paradox is wrong: I know why it is wrong in usual terms, I would be curious to see what prevents to write it in lean. Just curiosity.

[Kyle Miller]

I don't know anything about Richard's paradox. Does that mean you're wanting to do inductive arguments on the syntactic structure of a proposition?

[Guillaume Dubach]

@Reid Barton Could you perhaps explain a bit more ?

[Kevin Buzzard]

Richard's paradox just appears to be the statement that the power set of the naturals is uncountable.

[Reid Barton]

Whatever argument you have in mind to conclude that there are only countably many "propositions with a free variable" applies with equal force to conclude that there are also only countably many "things of type Nat -> Bool".

[Reid Barton]

So, we may as well forget about "propositions with a free variable".

[Kyle Miller]

The Lean version of the paradox I guess is that there are only countably many functions Nat -> Prop that we can actually write down in Lean, but we can prove that Nat -> Prop is uncountable. (That's defeq to what Kevin said :smile:)

[Reid Barton]

What is going on with Nat -> Bool? The trick is that we're conflating syntactic presentations of functions with the actual/internal functions themselves.

[Guillaume Dubach]

I see! Well, that answers my question I guess. Thanks!

[Guillaume Dubach]

But just to be sure: could we speak of a (countable) type whose elements would be exactly such syntactic presentations with one variable being free ? This by itself doesn't seem to be problematic ?

[Kyle Miller]

I imagine you could make a subtype of docs#Lean.Expr (the type that represents Lean expressions themselves) of well-typed expressions with a single bvar that's bvar 0 (where the type checker assumes bvar 0 has some given type, like Nat)

[Kyle Miller]

This would cover everything that you could actually enter into Lean

[Guillaume Dubach]

@Kyle Miller Thank you very much, I think this is exactly what I was looking for.

[Guillaume Dubach]

As this is built inductively, I guess one can write a proof in Lean that it is countable?

[Niels Voss]

I might be wrong but I think Lean.Expr was designed for usage in meta-code, not usage in proofs. You won't be able to find a function usable outside meta-code which converts Expr to terms. It still might be interesting to see what you can prove about Expr but Expr is just an inductive type and won't let you prove anything new about terms.
I think you can prove Expr is countable but it won't be that easy because Expr is made out of a bunch of other types you also have to prove are countable, including Lean.Name and Lean.MData.

[Chris Hughes]

You could also use the ModelTheory folder. I think Formula Unit or something might be what you're looking for. It's a first order formula with one free variable, but you'll have to define a first order language first to use that.