Theorem:
  1 + 1 = 2
Proof:
  Without loss of generality,
  we may assume that 1+1=3.
  Therefore by contradiction 1+1=2.

^ Informal proof:
   it's an argument to convince people
   that your proposition is a theorem

** Inference rules **

   Premises   
  ____________ (rule name)
   Conclusion

"If I have proofs of the premises,
 then I can invoke (rule name) to
 obtain a proof of the conclusion"

  ⊢   a *judgement*, entailment

  S ⊢ X  "S entails X"

  From the (set of) premises S,
  there is a proof of the proposition X

 _____________________________ (assumption)
 {it's raining} ⊢ it's raining

 _________ (asssumption) _________ (assumption)
 {A,B} ⊢ B               {A,B} ⊢ A
 _________________________ (conjI)
  {A, B} ⊢ B ∧ A
 ________________________ (conjE)
 {A ∧ B} ⊢ B ∧ A
 _________________________ (impl)
 {} ⊢ A ∧ B → B ∧ A

 A → B   is a formula

 {A} ⊢ B  is a truth claim
  this means "I have a *proof* of B from {A}"


 Trusted computing base (TCB):
 - what are the assumptions that
   are beyond the scope of my proof?


  

  map f []     = []
  map f (x:xs) = f x : map f xs

  map size ["hello","world!"] = (syntactic sugar for)
  map size ("hello":"world!":[]) = (by equation 2 above)
  (size "hello"):map size ("world!":[]) =  (by equation 2 above)
  (size "hello"):size "world!":[] =
  [5,6]
                           
  ∃x. (P(x) ⇒ ∀x. P(x))

  ∃x.        there exists an x, such that...
    (P(x)    ...if P(x) holds,
     ⇒          then
     ∀x.        for all x, it is the case that
      P(x)         P(x) holds
    )
  
  ^ the birthday paradox

  There exists a person such that,
    if it is that person's birthday today,
    then it is everybody's birthday today.


 A ⇒ (B ⇒ C)

 is logically equivalent to

 (A ∧ B) ⇒ C

 if A *and* B, then C

 A ⇒ B ⇒ C  does *not* connote in any way that B follows from A
 it just means that
   "the fact that (B follows from C) follows from A"


 f(x) = x + 1   <-- a function that returns its argument + 1

 equivalently, we could write:

 f = λx. x + 1

 instead of writing

   f(2)

  we could write

   (λx. x + 1)(2) = 2 + 1 = 3

.. so lambdas are a way to define *anonymous* functions
   we can define functions with arguments,
   but without naming the functions themselves