{"action":"created","issue":{"url":"https://api.github.com/repos/nomeata/incredible/issues/71","labels_url":"https://api.github.com/repos/nomeata/incredible/issues/71/labels{/name}","comments_url":"https://api.github.com/repos/nomeata/incredible/issues/71/comments","events_url":"https://api.github.com/repos/nomeata/incredible/issues/71/events","html_url":"https://github.com/nomeata/incredible/issues/71","id":121943866,"number":71,"title":"I don't quite understand the rules for quantification","user":{"login":"michaelgwelch","id":826112,"avatar_url":"https://avatars.githubusercontent.com/u/826112?v=3","gravatar_id":"","url":"https://api.github.com/users/michaelgwelch","html_url":"https://github.com/michaelgwelch","followers_url":"https://api.github.com/users/michaelgwelch/followers","following_url":"https://api.github.com/users/michaelgwelch/following{/other_user}","gists_url":"https://api.github.com/users/michaelgwelch/gists{/gist_id}","starred_url":"https://api.github.com/users/michaelgwelch/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/michaelgwelch/subscriptions","organizations_url":"https://api.github.com/users/michaelgwelch/orgs","repos_url":"https://api.github.com/users/michaelgwelch/repos","events_url":"https://api.github.com/users/michaelgwelch/events{/privacy}","received_events_url":"https://api.github.com/users/michaelgwelch/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/nomeata/incredible/labels/question","name":"question","color":"cc317c"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-12-13T21:09:07Z","updated_at":"2015-12-13T21:49:21Z","closed_at":null,"body":"I was able to complete all of the proofs involving quantification except for one. I find I don't quite understand a few things. (If these could be clarified in the info box that'd be great)\r\n\r\n1. The difference between a `c` and a `y` in the rules that introduce universal and existential quantifiers respectively. Obviously the `c` must somehow capture the fact that this value was completely arbitrary and therefore if `P(c)` is true then it must be true for all values.\r\n\r\n2. How does one \"generate\" a `c` or I guess I should say a `P(c)` so that you may prove a universal. None of the rules produce a `P(c)` only a `P(y)` and I'm assuming there's a difference. (Hmm, not quite right. I see one of the existential rules let's you assume a `P(c_v)` (where v is a subscript) within the context of the block. So I guess that's a hint for me.\r\n\r\n3. I've been able to complete all of the proofs involving quantification except for the last one. I've tried many different approaches. The image below captures one approach I took which I really didn't think was going to work. But even though I didn't think I was on the right track, I found it interesting that if you look at the image you can see that it appears (incorrectly) that I'm really close. The output of the -> elimination  block is an `A`. The desired conclusion for the -> introduction block is `A`. So it would appear that I could just hook those two up and be done. However if I actually connect these two, then it is revealed that I have some unification errors. Why are there no errors prior to connecting them?\r\n<img width=\"924\" alt=\"almostproved\" src=\"https://cloud.githubusercontent.com/assets/826112/11769355/cbac3786-a1aa-11e5-9160-16134747c819.png\">\r\n\r\nThe errors become apparent when I make the connection.\r\n\r\n<img width=\"919\" alt=\"nopenotgoingtowork\" src=\"https://cloud.githubusercontent.com/assets/826112/11769381/9a8071e4-a1ab-11e5-809e-a4cb232788fb.png\">\r\n\r\nBy the way, I'd appreciate a hint on this one. Been struggling for 2 days now and while on paper this proof seems trivial, I can't \"solve the puzzle\" using the tool."},"comment":{"url":"https://api.github.com/repos/nomeata/incredible/issues/comments/164301251","html_url":"https://github.com/nomeata/incredible/issues/71#issuecomment-164301251","issue_url":"https://api.github.com/repos/nomeata/incredible/issues/71","id":164301251,"user":{"login":"nomeata","id":148037,"avatar_url":"https://avatars.githubusercontent.com/u/148037?v=3","gravatar_id":"","url":"https://api.github.com/users/nomeata","html_url":"https://github.com/nomeata","followers_url":"https://api.github.com/users/nomeata/followers","following_url":"https://api.github.com/users/nomeata/following{/other_user}","gists_url":"https://api.github.com/users/nomeata/gists{/gist_id}","starred_url":"https://api.github.com/users/nomeata/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nomeata/subscriptions","organizations_url":"https://api.github.com/users/nomeata/orgs","repos_url":"https://api.github.com/users/nomeata/repos","events_url":"https://api.github.com/users/nomeata/events{/privacy}","received_events_url":"https://api.github.com/users/nomeata/received_events","type":"User","site_admin":false},"created_at":"2015-12-13T21:49:21Z","updated_at":"2015-12-13T21:49:21Z","body":"Indeed the quantification mechanism is not very well documented, and also not presented in the UI as good as I’d like it to be.\r\n\r\n1. `c` are constants, e.g. they only unify with themselves. `y` are free variables: They will unify, if needed. So if you connect `P(y)` with `P(f(c))`, this works (and `y` becomes `f(c)`), but connecting `P(c)` with `P(c₂)` will not work.\r\n\r\n2. To prove `∀x.P(x)`, you will have to prove `P(c)` for some arbitrary `c`; that’s what the ∀-introduction block is for. The subscript indices the block that introduced a certain constant (`c₂`) or free variable (`y₂`).\r\n\r\n3. This proof will not work without the TND block, as it is a theorem only in classical logic. In your dead end proof attempt, the problem is that you may use `c₅`, the “arbitrary constant” of the ∀-intro-block, only in the part of the proof that enters that block, but nothing “to the right of it”. In a partial proof, the system cannot always know what wil end up to the right of it. You can see that `c₅` may not occur there because the free variable is written as `y₃`, and not `y₃(c₃)` (read: `y₃` is any expression and may depend on c₃). If you have seen more standard rule inference: This corresponds to the “`c` free in the context” requirement of the ∀-introduction-rule.\r\n\r\nUsing TND should get you further. Here a hint: Make sure you use the ∃-intro-block inside the case analysis block, once above and once below the line. Do _not_ just put it once at the very end, directly connected to the conclusion."}}