10:02:03	 From  Mark Lavrentyev : yes
10:05:09	 From  Mia Santomauro : yes
10:05:57	 From  Thomas Del Vecchio : yee
10:05:59	 From  Danielle Rozenblit : yeah
10:06:06	 From  Jordan Hartzell : yes!
10:07:38	 From  Gene Siriviboon : yes
10:08:11	 From  Ryan Greenblatt : There exists some number of primes
10:08:14	 From  Ryan Greenblatt : not zero
10:08:19	 From  Thomas Del Vecchio : That you can write any number as a product of primes?
10:08:25	 From  Danielle Rozenblit : ^
10:08:42	 From  Nastassia Goodson : ^
10:11:06	 From  Gene Siriviboon : Is it like a sequence of premises and conclusion
10:15:15	 From  Jordan Hartzell : does that mean apply “logic for systems” idea of a “proof” to the “social object proof” ?
10:15:52	 From  Jordan Hartzell : yes
10:18:09	 From  christopher : no
10:18:10	 From  William Schor : no
10:18:10	 From  Justin's iPhone : no
10:18:31	 From  christopher : That is a tautology
10:18:31	 From  Gene Siriviboon : Gor check symbol pa
10:18:38	 From  Gene Siriviboon : yes
10:21:00	 From  Gene Siriviboon : Wouldn’t it be like searching in an infinite tree of proof?
10:22:15	 From  christopher : ^I think that’s why it is undecidable
10:22:58	 From  christopher : I think you also want to try to prove the true case and the false case simultaneously
10:25:29	 From  Thomas Del Vecchio : Whenever x and y are both true, x must be true
10:25:41	 From  Danielle Rozenblit : Implies is only false where x and y is false and x is false
10:25:44	 From  Danielle Rozenblit : Which cant happen
10:25:58	 From  christopher : assume X and Y, and then prove X (and then use a natural deduction step to show that this prove the implies statement)
10:27:46	 From  Gene Siriviboon : Are those two always equivalent? Or is it just for classical logic.
10:27:55	 From  Gene Siriviboon : yes
10:28:50	 From  christopher : I think you need a deductive logic rule like implication introduction to show that turnstile is the same as implies
10:28:57	 From  christopher : Natural deduction ruler*
10:28:59	 From  christopher : rule**
10:31:48	 From  Mia Santomauro : not all operations commute?
10:31:50	 From  christopher : You don’t have a rule that shows that AND commutes
10:33:15	 From  Jordan Hartzell : what are e1 and e2 again? (sorry)
10:34:30	 From  Mark Lavrentyev : those are just the names for the rules
10:34:44	 From  Mark Lavrentyev : so /\E1 is read "and elimination 1"
10:34:53	 From  Ben Ryjikov : do you need to prove that E1 and E2 are valid rules before you perform this step
10:35:11	 From  Spencer Dellenbaugh : What is the little box below X?
10:36:17	 From  Max Heller :  quod erat demonstrandum, I think
10:36:36	 From  Mary Loukidi-Papanikoli : ^
10:37:16	 From  Nicholas Keirstead : “That which had to be shown”
10:38:16	 From  Mia Santomauro : A ^ B
10:38:24	 From  Mia Santomauro : woohoo
10:39:41	 From  Monica Roy : B?
10:39:42	 From  Daniel Kostovetsky : B
10:40:32	 From  Phunn Boonchouchouy : Do we have to memorize these rules?
10:40:53	 From  Daniel Kostovetsky : B or not A
10:40:59	 From  Gene Siriviboon : C and C => A => B?
10:41:04	 From  Thomas Del Vecchio : A |- B
10:41:31	 From  christopher : ->I would be that we have A on one line and B on another, so we conclude A => B
10:42:26	 From  christopher : But then you need 2 => to get one more, which means you can’t created them from nothing
10:42:41	 From  Jordan Hartzell : why does the fraction-y part have an implies on the right now instead of /\ for these proof rules ?
10:42:53	 From  christopher : That second point was in reference to another comment
10:42:56	 From  Mia Santomauro : I think its just shorthand in the names of the rules
10:43:42	 From  Jordan Hartzell : ah cool thanks
10:43:58	 From  christopher : we need a step type called “assuming” and then we can assume A and prove B, then the rule is to say that this proves A => B
10:45:53	 From  Thomas Del Vecchio : =>I
10:46:00	 From  christopher : Assume (X ^ Y)
10:46:07	 From  christopher : then try to prove (Y ^ X)
10:47:47	 From  Thomas Del Vecchio : Im a bit concerned about what this will look like with nested implications
10:47:47	 From  christopher : lol
10:48:12	 From  Matteo Lunghi : when will the lecture notes be posted?
10:48:16	 From  christopher : I think you just have sub assumptions @Thomas
10:48:18	 From  Nastassia Goodson : Will all of these rules be summarized somewhere?
10:48:28	 From  Mark Lavrentyev : they're posted already from last lecture
10:49:36	 From  Mia Santomauro : ^E1  and ^E2
10:50:22	 From  Gene Siriviboon : Do we need A => B ^ A => C => A=> (B^C)
10:51:54	 From  Ryan Greenblatt : Isn't this still a social object?
10:52:59	 From  christopher : I think you can prove that these rules are sound and complete using a pretty simple axiom system which is maybe easier to be confident about
10:53:15	 From  Jordan Hartzell : so the last step (applying implication introduction) gives us “and introduction”  ?
10:54:14	 From  Thomas Del Vecchio : Do we ned a single starting bubble with our assumption, or is it ok to just invoke assumption multiple times
10:54:24	 From  Husam Salhab : What’s the point of having two “and eliminations”? Can’t one be used in place of the other WLoG?
10:56:16	 From  Husam Salhab : Got it. Thanks