/sci/ - Science & Math

[Anonymous No.10855536]

how?

[Anonymous No.10855575]

The proof term is

[math] \lambda x.\, \langle x, \mathrm{refl_x} \rangle [/math]

i.e. for each x take y:=x, assuming reflectivity of equality.

[Anonymous No.10855578]

>>10855575
What? What's lambda? What are the angle brackets? Where do we use the empty set part? I don't get it

[Anonymous No.10855580]

The proof term is

[math] \lambda A. \lambda x. \langle x, \mathrm{refl_x} \rangle \ : \ \Pi_{x:A} \Sigma_{y:A} Id_A(x, y) [/math]

i.e. for each x take y:=x, assuming reflectivity of equality.

[Anonymous No.10855595]

>>10855578
Nevermind the formal syntax if you don't know it.
The point is that for each x, you have that x=x. The truth of x=x follos from the definition of equality (it's an axiom that equality is reflective).
The empty set just says that you don't need any assumptions.

The notation comes from reading the claim constructively via
https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation

Forall x gets translated into wanting an explicit map from x (and that's what the lambda is, it just binds x) and Exists says you need an explicit term (y is x here) together with a proof of the proposition (and refl generally comes with equality wherever it's implemented - refl is the incarnation of the axiom). See also
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
In full,
[math] \lambda A. \lambda x. \langle x, \mathrm{refl_x} \rangle \ : \ \Pi_{x:A} \Sigma_{y:A} Id_A(x, y) [/math]

[Anonymous No.10855604]

(Nevermind the A, I also left out a [math] \Pi_{A: \mathrm {Type}} [/math])

[Anonymous No.10855613]

>>10855595
I wish I understood what you're talking about? Is there no retard way to show what it's asked?

[Anonymous No.10855642]

>>10855613
I gave you both.

"For all x, the let y be x, and then reflectivity of equality tells us x=y, which reduces to x=x, is true."

Look at pic related: We need a proof of the [existence] [forall] x, and that proof of forall is an assignment and the proof of existence is a pair.
So given x, the pair holding y:=x and the (here, effectively via axiom) proof of x=y is the proof of
"Forall x, there exists a y such that x=y"

[Anonymous No.10855653]

>>10855642
I think my class just uses very different format? This is what a solution looks like in a practical

[Anonymous No.10855671]

>>10855653
It's the same rules
(pic related taken from
https://en.wikipedia.org/wiki/Natural_deduction#First_and_higher-order_extensions
)
except that my calculus is "proof relevant" (the proofs are mathematical objects in themselves and you state proof and propositions) while the one in your pic just forms the propositions.

In any case, do you logically understand why your theorem is evident?
PS the pic you posted has not \exists introduction, so with that alone you naturally won't get far in building up your proposition.
State your sheet with \exist introduction and then try to build it up assuming x=x and that you can set y:=x.

[Anonymous No.10855684]

>>10855671
I'm too dumb for this shit man, but thanks for trying anon

[Anonymous No.10855703]

>>10855684
Do you understand, in natural language words, the expression you try to proof?

Your OP pic says
[math] (\forall x)(\exists y)(x=y) [/math]
In words, "For any x, there is an y, such that x is y"?
Is this clear to you and is it clear why it's true?
For example,
"Let x by your left eye. Then there is some thing which we may label y, such that y is your left eye"
It's true because you may set "y" to "your left eye". And this works for anything.

Now what you need to do is to find out your rule for what will probably be denotes by [math] \exists I [/math] and then build up [math] (\forall x)(\exists y)(x=y) [/math] assuming [math] (\forall x) (x=x) [/math]

Give it a shot.

[Anonymous No.10855709]

>>10855703
That's what I've been trying man. I used the identity that for all x, x =x, but i don't understand how to use this notation to claim that for any x, x = y for a particular y cause y can take the x value

[Anonymous No.10855719]

>>10855709
To formally make this step you need the [math] \exist / [/math]-rule, i.e. the rule to introduce an [math] \exist [/math]. If you must solve your problem, then somewhere in your notes or texts this will be stated for your deduction calculus.
In my sheet >>10855671 from the natural deduction- or lambda calculus, this amounts to introduce a pair <,> but in your case it will just be a statement about how to insert [math] \exist a [/math] (and then forget information and turn it [math] \exist y [/math]. Where "a" is a particular and not bound, like in your pic >>10855653. But this is just my guess how it will go). I don't know, look it up in your notes.

[Anonymous No.10855726]

>>10855709
To formally make this step you need the [math]\exists I [/math] rule, i.e. the rule to introduce an [math]\exists [/math]. If you must solve your problem, then somewhere in your notes or texts this will be stated for your deduction calculus.
In my sheet >>10855671 from the natural deduction- or lambda calculus, this amounts to introduce a pair <,> but in your case it will just be a statement about how to insert [math] \exists a [/math] (and then forget information and turn it [math]\exists y [/math]. Where "a" is a particular and not bound, like in your pic >>10855653. But this is just my guess how it will go). I don't know, look it up in your notes.

[Anonymous No.10855739]

>>10855536
suppose y = x
qed

[Anonymous No.10855748]

>>10855726
Right, yeah I've been going through notes for something like this but haven't found it yet. Thanks anon, at least I think I'm on the right track now

[Anonymous No.10855761]

>>10855748
Just googled "Existential introduction for Hilbert calculus" and found the answer with 4 upvotes here
https://mathoverflow.net/questions/116671/existential-instantiation-in-hilbert-style-deduction-systems
saying that if
B(a) |-> S
for a particular, then the introduction weakens it as
(exists y) B(y) |-> S

Example:
If your mom gets banged by your neighbor means you'll soon have a new sister, then there is someone such that if he bangs your mom, you'll soon have a new sister.
The second sentence being weaker, as there's less info on who does the banging.

From this, I presume the proof will eventually look something along those lines:

1. [math] (\forall x) (x=x) [/math] (refl)
2. [math] a=a [/math] (a particular via 1.)
3. [math] b=a [/math] (introduce b)
4. [math] a=b [/math] (flip 3)
5. [math] (\exists y) a=y [/math] (via exists introduction, what above I called weakening)
6. [math] (\forall x) (\exists y) x=y [/math] (via forall introduction aka generalization)

pic related is your neighbor

[Anonymous No.10856799]

>>10855536
lazy

[Anonymous No.10856835]

>>10855536
by the definition of an equivalence relation, it has to be reflexive, symmetric, and transitive
reflexivity means that any element is equal to itself, so, the element y can be based on x (just pick x to be your y)