today I explored succ in Lean4
Aujourd’hui j’ai exploré #
la nature de succ dans Lean."
I learnt it was possible #
to have more than two truth values because for example to have more than two truth values
x<½, x∈ℝ [0, ¼) vrai (½, ¾) et partiellement vrai! (¾, 1] faux
I was very happy for this example, because how could you possibly have more than two truth values? this seems to connect to fuzzy logic, and truth values living on a continuum of shades which I learnt about reading Art of Logic by Eugenia Cheng
I started doing the #
Lean4 tutorials, the Natural Number Game, while collaburating with computer agent, asking questions about analogies of patterns in Lean4, classical logic and Topos theory
- Previous: foundations, s
- Next: ajourdhui