März 2022 Archiv

Logicalidarity.

  • 2022-03-09

The Board of the Dutch Association for Logic and Philosophy of the Exact Sciences (VvL) unconditionally condemns the military aggression by Russia in Ukraine. We stand up against the blatant attack of the Russian government against a sovereign state, against democracy and against innocent people. In these difficult times we express our full solidarity and support to our Ukrainian colleagues.

Het bestuur van de Vereniging voor Logica en Wijsbegeerte van de Exacte Wetenschappen (VvL) veroordeelt de militaire agressie van Rusland in Oekraïne onvoorwaardelijk. Wij staan op tegen de brute aanval van de Russische regering op een soevereine staat, op de democratie en op onschuldige mensen. In deze moeilijke tijden betuigen we onze volledige solidariteit en steun aan onze Oekraïense collega's.

VvL: Statement on the War in Ukraine / Verklaring met betrekking tot oorlog in Oekraïne

Strange strangeness.

  • 2022-03-08

Strange world, strange symbols.

Fake Spring.

  • 2022-03-07

Sonnig, aber irgendwie funktioniert es noch nicht ganz.

Back ups, not downs.

  • 2022-03-04

It's just so much easier to live in the past.

Leanorris.

  • 2022-03-03

Hey! I heard that Lean thinks 1/0 = 0. Is that true?

Yes. So do Coq and Agda and many other theorem provers.

[...]

But doesn’t that lead to confusion?

It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work.

Xena: Division by zero in type theory: a FAQ