Process journal of learning by Attila Vajda

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