Questions about TPIL

Stream: new members

[ccn]

Marcus Rossel said:

ccn said:

Does it mean pretty much that this is a "template" where if you give two propositions, you get a proof of modeus_ponens for those specific Props p and q ?

I'm not sure if thinking about them as "templates" is really helpful.
The parameters p and q are just "normal" parameters, too. The only difference is that all the other parameters (after the comma) are allowed to reference p and q.
Perhaps this example motivates this better:

array is a type of fixed length arrays (like a list, but with an additional parameter in the type that constrains the size of the array):

#check array --  ℕ → Type u → Type u
#check array 10 int -- Type u

-- for comparison:
#check list --  Type u → Type u
#check list nat -- Type u

Let's say you define a function that returns the last item in a given array of integers of length 10:

def array.last (a : array 10 int) : int :=
  a.read 9

Obviously it would would be nice to write this function more generically for all lengths. So we add a parameter n for the length:

def array.last (n : nat) (a : array n int) : int :=
  a.read (n-1) -- this wouldn't actually work exactly like this, but for the example it's ok

This is now a dependent function, as the type of a depends on the value n.

#check array.last -- Π (n : ℕ), array n int → int

But as you can see n is still just a regular parameter. In fact, we use it in the body of the function.

Your explanation helps, thanks!

[ccn]

I'm working on the propositions now:

4.1. The Universal Quantifier

Notice that if α is any type, we can represent a unary predicate p on α as an object of type α → Prop.
In that case, given x : α, p x denotes the assertion that p holds of x.
Similarly, an object r : α → α → Prop denotes a binary relation on α: given x y : α, r x y denotes the assertion that x is related to y.

I just want to make sure "the assertion that p holds of x" is not the same as a proof of that assertion right? (because it has type Prop)

[Henrik Böving]

If you have something of type Prop it is itself a type that represents some mathematical proposition such as that p holds for x, so p x : Prop if you have an element of that type so h : p x you have a proof that p x holds.

[ccn]

Since p x is always of type Prop isn't this the same thing as ∀ x : α, Prop which would be the same as Π x : α, Prop which is just the type α → Prop

image.png

(let me know if I understand it incorrectly)

[Reid Barton]

Assuming you are talking about the thing in the red box, then no. You cannot replace something by its type.

[ccn]

Reid Barton said:

Assuming you are talking about the thing in the red box, then no. You cannot replace something by its type.

Ok, what's in the red box is the type of functions that take in an element of type alpha, and output a proof of p x then?

[Reid Barton]

Yes, exactly (where x was the element that was passed in).

[ccn]

The idea is as follows. If j is not 0, then Π x : α, β is an element of Sort
(max i j). In other words, the type of dependent functions from α to β “lives”
in the universe whose index is the maximum of i and j. Suppose, however, that β
is of Sort 0, that is, an element of Prop. In that case, Π x : α, β is an
element of Sort 0 as well, no matter which type universe α lives in. In other
words, if β is a proposition depending on α, then ∀ x : α, β is again a
proposition. This reflects the interpretation of Prop as the type of
propositions rather than data, and it is what makes Prop impredicative.

The term “predicative” stems from foundational developments around the turn of
the twentieth century, when logicians such as Poincaré and Russell blamed
set-theoretic paradoxes on the “vicious circles” that arise when we define a
property by quantifying over a collection that includes the very property being
defined. Notice that if α is any type, we can form the type α → Prop of all
predicates on α (the “power type of α”). The impredicativity of Prop means that
we can form propositions that quantify over α → Prop. In particular, we can
define predicates on α by quantifying over all predicates on α, which is exactly
the type of circularity that was once considered problematic.

Can someone share an example of

“vicious circles” that arise when we define a
property by quantifying over a collection that includes the very property being
defined

[Bryan Gin-ge Chen]

You could start here: https://en.wikipedia.org/wiki/Barber_paradox

[ccn]

Bryan, Is this implying that there is no such thing as order/time in mathematics? Before he shaves himself it's true, after he shaves himself it's false, at no point in time was there a moment when he was the be barber and wasn't the barber?

[Arthur Paulino]

At the moment he touches the blades on his skin he explodes :rofl:

But he should have exploded even before that, because he shaves everyone who don't shave themselves

[Henrik Böving]

You can certainly formalize time in a variant of logic called temporal logic but the logical statements made about the barber and his activities are simply inconsistent.

[Parivash]

Hi,
How we can get openAI API key for using gptf tactics?

[Alex J. Best]

Hi @Parivash you should ask this in the #lean-gptf stream instead, or search there for existing answers

[Parivash]

Actually, I sent email and asked them, but didn't receive answer up to now !

[Alex J. Best]

See https://leanprover.zulipchat.com/#narrow/stream/274007-lean-gptf/topic/OpenAI.20gpt-f.20key/near/256739969, I think you will have better luck posting in that thread and being patient

[Parivash]

thank you Alex!