--- Day changed Fri Jun 30 2017
Nik05hey mietek, i had some other things to and started again with the 3rd lecture of clnstructive logic. Had some problems understandkng what he meant with verifications and "may be used". i think i understand it now30/06 21:16
Nik05to do*30/06 21:16
mietekgood :)30/06 21:16
Nik05sometimes it good to take a break30/06 21:16
mietekyes30/06 21:16
mietekalso, verifications are related to sequent calculus30/06 21:17
mietekI’m not sure if Frank says that30/06 21:17
Nik05oke30/06 21:17
Nik05How is this theory he is explaining called?30/06 21:18
Nik05theory of verifications?30/06 21:18
mietekI’m not sure if it has a name30/06 21:18
Nik05thank you, im going to finish the lecthre and reread his book about this30/06 21:20
Nik05thanj you very much for reccomending me this30/06 21:21
mietekI’m glad you’re enjoying it30/06 21:21
Nik05mietek he is talking about sequent calculus now, and how it is similar to his verifications30/06 21:49
mietekah cool30/06 21:49
Nik05and he is talking about |- and => like everyone knows what it means...30/06 21:51
Nik05where is |- coming from? Hilbert?30/06 21:52
mietekif I recall correctly, |- is actually the only symbol from Frege’s Begriffsschrift that we continue to use30/06 21:57
mietekso that’s 189330/06 21:57
mietekNik05: did you read the PDF?30/06 21:58
mietekA Tutorial on the Curry-Howard Correspondence30/06 21:58
mietekhttp://purelytheoretical.com/papers/ATCHC.pdf30/06 21:58
mietekpage 3 explains implication (⇒)30/06 21:58
dolioOh.30/06 21:58
dolioI was thinking |- for natural deduction and => for sequents.30/06 21:59
mietekpage 6 explains syntactic entailment (⊢)30/06 21:59
mietekoh, dolio is probably right, in the context of those lectures30/06 21:59
mietekso then it’s ⟹30/06 22:00
mietekand I don’t have a good name for it30/06 22:00
mietekhttps://en.wikipedia.org/wiki/Turnstile_(symbol)30/06 22:01
mietekNik05: look at the proof theory interpretation30/06 22:02
mietekand if I haven’t told you to read http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf already, it’s great30/06 22:03
mietekit gives a historical perspective, and explains a little how natural deduction and sequent calculus are related, although it doesn’t go into detail on the latter30/06 22:04
mietekhttps://www.amazon.com/Logic-Proof-Computation-Mark-Tarver/dp/178456127430/06 22:04
mietekthis guy is all about sequent calculus30/06 22:04
mietekI can’t recommend this book, because I haven’t read it, but I intend to30/06 22:04
mietekNik05: ask augur about sequent calculus stuff30/06 22:09
mietekaugur: Nik05 is following your guide to learn TT30/06 22:09
mietekaugur: currently watching Pfenning videos30/06 22:09
Nik05oke30/06 22:15
Nik05|- is the turnstile or something30/06 22:16
Nik05sorry my client missing some text30/06 22:18
Nik05Running irssi in screem via ssh on android. it is not that great30/06 22:19
Nik05im just understanding that there are different logic calculi30/06 22:22
Nik05will put those links into my mietek's recommendations list ;)30/06 22:23
mietekNik05: I was saying that you’re actually following augur’s guide, so he’s really the guy to thank30/06 22:25
Nik05thank you augur :)30/06 22:30
Nik05mietek and related to agda, would i be able to implement natural deduction, IPC, sequentient calculus in agda?30/06 22:33
mietekyes30/06 22:33
auguroh? cool :)30/06 22:35
augur⊢ is indeed called turnstile30/06 22:35
Nik05and what kind of logic is agda based on?30/06 22:49
mietekNik05: loosely, the Calculus of Constructions30/06 22:56
mietekwith extras30/06 22:56
Nik05thank you30/06 23:33

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!