/sci/ - Science & Math » Thread #10855536

18KiB, 291x49, 2019-08-01-220300_291x49_scrot.png

View Same Google iqdb SauceNAO

Anonymous Thu 01 Aug 21:03:23 2019 No.10855536 View Reply Original Report

Quoted By: >>10855739 >>10856799 >>10856835

how?

Anonymous

View Same Google iqdb SauceNAO applbla.jpg, 260KiB, 1280x1792

Anonymous Thu 01 Aug 2019 21:17:11 No.10855575 Report

Quoted By: >>10855578

The proof term is

$\lambda x.\, \langle x, \mathrm{refl_x} \rangle$

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

Anonymous

Anonymous Thu 01 Aug 2019 21:19:36 No.10855578 Report

Quoted By: >>10855595

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

Anonymous

View Same Google iqdb SauceNAO tech.gif, 983KiB, 384x288

Anonymous Thu 01 Aug 2019 21:20:05 No.10855580 Report

Quoted By:

The proof term is

$\lambda A. \lambda x. \langle x, \mathrm{refl_x} \rangle \ : \ \Pi_{x:A} \Sigma_{y:A} Id_A(x, y)$

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

Anonymous

View Same Google iqdb SauceNAO tech.gif, 983KiB, 384x288

Anonymous Thu 01 Aug 2019 21:25:51 No.10855595 Report

Quoted By: >>10855613

>>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,
$\lambda A. \lambda x. \langle x, \mathrm{refl_x} \rangle \ : \ \Pi_{x:A} \Sigma_{y:A} Id_A(x, y)$

Anonymous

View Same Google iqdb SauceNAO believe.jpg, 12KiB, 288x175

Anonymous Thu 01 Aug 2019 21:28:55 No.10855604 Report

Quoted By:

(Nevermind the A, I also left out a $\Pi_{A: \mathrm {Type}}$ )

Anonymous

Anonymous Thu 01 Aug 2019 21:33:00 No.10855613 Report

Quoted By: >>10855642

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

Anonymous

View Same Google iqdb SauceNAO del.png, 50KiB, 877x513

Anonymous Thu 01 Aug 2019 21:42:00 No.10855642 Report

Quoted By: >>10855653

>>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

View Same Google iqdb SauceNAO 2019-08-01-224534_677x588_scrot.png, 69KiB, 677x588

Anonymous Thu 01 Aug 2019 21:46:15 No.10855653 Report

Quoted By: >>10855671 >>10855719 >>10855726

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

Anonymous

View Same Google iqdb SauceNAO First_order_natural_deduction.png, 34KiB, 685x873

Anonymous Thu 01 Aug 2019 21:53:02 No.10855671 Report

Quoted By: >>10855684 >>10855719 >>10855726

>>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

Anonymous Thu 01 Aug 2019 21:58:49 No.10855684 Report

Quoted By: >>10855703

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

Anonymous

View Same Google iqdb SauceNAO giphy.gif, 2MiB, 480x270

Anonymous Thu 01 Aug 2019 22:05:15 No.10855703 Report

Quoted By: >>10855709

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

Your OP pic says
$(\forall x)(\exists y)(x=y)$
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 $\exists I$ and then build up $(\forall x)(\exists y)(x=y)$ assuming $(\forall x) (x=x)$

Give it a shot.

Anonymous

Anonymous Thu 01 Aug 2019 22:08:47 No.10855709 Report

Quoted By: >>10855719 >>10855726

>>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

Anonymous Thu 01 Aug 2019 22:14:31 No.10855719 Report

Quoted By:

>>10855709
To formally make this step you need the $\exist /$ -rule, i.e. the rule to introduce an $\exist$ . 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 $\exist a$ (and then forget information and turn it $\exist y$ . 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

Anonymous Thu 01 Aug 2019 22:16:18 No.10855726 Report

Quoted By: >>10855748

>>10855709
To formally make this step you need the $\exists I$ rule, i.e. the rule to introduce an $\exists$ . 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 $\exists a$ (and then forget information and turn it $\exists y$ . 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

Anonymous Thu 01 Aug 2019 22:20:41 No.10855739 Report

Quoted By:

>>10855536
suppose y = x
qed

Anonymous

Anonymous Thu 01 Aug 2019 22:24:17 No.10855748 Report

Quoted By: >>10855761

>>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

View Same Google iqdb SauceNAO murphy_eddie_the_nutty_professor (...).jpg, 148KiB, 400x500

Anonymous Thu 01 Aug 2019 22:29:41 No.10855761 Report

Quoted By:

>>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. $(\forall x) (x=x)$ (refl)
2. $a=a$ (a particular via 1.)
3. $b=a$ (introduce b)
4. $a=b$ (flip 3)
5. $(\exists y) a=y$ (via exists introduction, what above I called weakening)
6. $(\forall x) (\exists y) x=y$ (via forall introduction aka generalization)

pic related is your neighbor

Anonymous

Anonymous Fri 02 Aug 2019 08:06:36 No.10856799 Report

Quoted By:

>>10855536
lazy

Anonymous

Anonymous Fri 02 Aug 2019 08:27:50 No.10856835 Report

Quoted By:

>>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)

Capcode	All Only User Posts Only Moderator Posts Only Admin Posts Only Developer Posts
Show Posts	All Only With Images Only Without Images
Deleted Posts	All Only Deleted Posts Only Non-Deleted Posts
Ghost Posts	All Only Ghost Posts Only Non-Ghost Posts
Post Type	All Only Sticky Threads Only Opening Posts Only Reply Posts
Results	All Grouped By Threads
Order	Latest Posts First Oldest Posts First

Your latest searches