Zulip Chat Archive

Stream: new members

Topic: Questions about TPIL


ccn (Jan 13 2022 at 16:43):

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 (Jan 13 2022 at 16:44):

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 (Jan 13 2022 at 16:46):

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 (Jan 13 2022 at 16:53):

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 (Jan 13 2022 at 17:14):

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

ccn (Jan 13 2022 at 17:21):

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 (Jan 13 2022 at 17:22):

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

ccn (Jan 13 2022 at 17:29):

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 (Jan 13 2022 at 17:36):

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

ccn (Jan 13 2022 at 19:28):

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 (Jan 13 2022 at 19:34):

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 (Jan 13 2022 at 19:35):

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 (Feb 05 2022 at 16:12):

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

Alex J. Best (Feb 05 2022 at 16:18):

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

Parivash (Feb 05 2022 at 16:34):

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

Alex J. Best (Feb 05 2022 at 16:46):

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 (Feb 05 2022 at 16:55):

thank you Alex!


Last updated: Dec 20 2023 at 11:08 UTC