https://mathshistory.st-andrews.ac.uk/Biographies/Poretsky/ 

Вот простые два теста на Котлине.

    Stream.of<String>().forAll {   it.isEmpty() } shouldBe true
    Stream.of<String>().forAll {  !it.isEmpty() } shouldBe true

Не очень понятно, как это непрофессионалы воспримут. Моим студентам требуются усилия обычно.

 So, if you think you call a function in your code, and this function returns current time, or a random number... IT'S NOT A FUNCTION. Your code is function of "random number", or "time".

So, if your code is written as something that retrieves this kind of data, to test your code, you should provide that data. Not just today, but try the time, like 10 years from now. As to "random", You provide the randomness. If your code cannot be fixed to behave as a function of those inputs, make your "random stream" or "time stream" not hard-coded, but substitutable. Mockable. And mock it in your tests. MAKE SURE that you don't provide just happy-path data. Provide anything. A sequence of 100 numbers 4 for random. Time that is 10 years from now. Or even 30 yeas from now.

Make sure that your tests don't depend on anything. Because test Must Be Reproducible.

All these things, I know, are obvious to some, and not obvious to others.

If you still have questions, ask. But don't argue. Because what I say is math. Unless you have another math (some people do), or another logic (there's plenty of them), please don't argue.

I'd be glad to see how all this changes if logic is e.g. linear. 

 

https://www.meetup.com/SF-Types-Theorems-and-Programming-Languages/events/270634414/ 

http://math.andrej.com/2008/02/02/the-hydra-game/

My question actually is this: can Goodstein sequence to be proven to stop in a lambda calculus? Naively, it should be.

And another question: can set theory be modeled in lambda? (Or should I reread Dana Scott's works?)

 def checkDistributivity(cat: Category): MatchResult[Any] = {

  val topos = new CategoryOfDiagrams(cat)
  import topos._
  val points = Ω.points

  val desc = s"Testing ${cat.name} distributivity laws"
  println(desc)
  
  for { pt1 ← points } {
    println(s"  at ${pt1.tag}")
    val p = predicateFor(pt1)

    for { pt2 ← points } {
      val q = predicateFor(pt2)
      val pAndQ = p ∧ q
      val pOrQ = p ∨ q

      for { pt3 ← points } {
        val r = predicateFor(pt3)
        // distributivity of conjunction over disjunction
        (p ∧ (q ∨ r)) === (pAndQ ∨ (p ∧ r))
        // distributivity of disjunction over conjunction
        (p ∨ (q ∧ r)) === (pOrQ ∧ (p ∨ r))
      }
    }
  }

  ok
}

Knowledge and wisdom, savoir et connaître, ведать и знать, etc. Not only in Indo-European languages, but in may others (e.g. yakut).

For decades I tried to figure out how come this dichotomy is so ubiquitous, although not explicitly recognized.

It turned out it's a part of epistemology. Kant wrote about it. Popper, Quine. And of course it's a part of Navya-Nyaya logic.

(Just reading about "Einstein-Bohr discussions", that's where I found it.)


 

 

Pocket Set Theory 

PST also verifies the:

• Continuum hypothesis. This follows from (5) and (6) above;
• Axiom of replacement. This is a consequence of (A4);
• Axiom of choice. Proof. The class Ord of all ordinals is well-ordered by definition. Ord and the class V of all sets are both proper classes, because of the Burali-Forti paradox and Cantor's paradox, respectively. Therefore there exists a bijection between V and Ord, which well-orders V. ∎

The well-foundedness of all sets is neither provable nor disprovable in PST.

Straßburger, "What is Logic, What is Proof" 

John Baez writes in his tweets (go ahead and look up, or, better, subscribe to his amazing tweets).

Do you know what "continuum hypothesis" is? It's about whether there is an intermediate size set between a countable (ℵ₀), for example, natural numbers, and 2^countable (ℵ₁). It's been proven over 50 years ago that neither the existence nor the non-existence follows from the axioms of Zermelo-Fraenkel. So, when mathematicians say that they base their absolutely strict and correct theorems on set theory (I don't believe them), we can always ask - which one?

Now the things got more serious.

Suppose you are a serious "machine learning data scientist", and you want to base your tea-leaves guesses on a solid math. That is, figure out the theory behind taking billions of pictures of cats and dogs and detecting cats on them (my former colleagues was focusing on figuring out whether he has a cat or a mouse, and figured that if the fur is uniform gray, the "algorithm" says it's a mouse. Do you have a Russian Blue?)

So, what we do, while "detecting", is a kind of data compression. It's closer to something like mapping, 2^N -> N.

Now, surprise. The feasibility of this operation, in general settings, is equivalent to having a finite number of intermediate sizes between ℵ₀ and ℵ₁.

Details are here: https://www.nature.com/articles/s42256-018-0002-3

Learnability can be undecidable

"The mathematical foundations of machine learning play a key role in the development of the field. They improve our understanding and provide tools for designing new learning paradigms. The advantages of mathematics, however, sometimes come with a cost. Gödel and Cohen showed, in a nutshell, that not everything is provable. Here we show that machine learning shares this fate. We describe simple scenarios where learnability cannot be proved nor refuted using the standard axioms of mathematics. Our proof is based on the fact the continuum hypothesis cannot be proved nor refuted. We show that, in some cases, a solution to the ‘estimating the maximum’ problem is equivalent to the continuum hypothesis. The main idea is to prove an equivalence between learnability and compression."