𝟭
/
𝟘𝟠·
I've added ‘comprehensions’ which support set and sequence expressions such as { _^3 ⋮ 1⋯2026} and ⟨ ⦗str _⦘ ⋮ x y z ⟩, where the variable ‘_’ (displayed as ◒ in
┊
logical contexts, to satisfy my aesthic preferences) which is evaluated for each of the elements to the right of the ‘⋮’ symbol. I use ‘⋯’ as an inclusive, integer
╰
range operator, so ⟨1⋯3⟩ is the tuple ⟨1 2 3⟩. It meshes well with my implementation of sets of integers expressed as intervals.
╭
𝟚𝟛·
I've added support for the Cartesian Product, represented by ‘×’ in Unicode (U+D7). What I call “tuple constrained quantification” (∀⟨x y⟩∈Z×Z) is accepted in
┊
⟪Sapphire⟫ as well as set exponentiation by an integer (Z^4 ▶ Z×Z×Z×Z) ({1⋯3}^3 ▶ {1⋯3}×{1⋯3}×{1⋯3}). Finite expressions can be evaluated in calculator fashion (⟨1 2
𝔻
┊
3⟩∈{1⋯3}^3 ▶ ✔) (∀⟨a b⟩∈{1⋯3}^2 a>3 ⇒ a+b>4 ▶ ✔) and can also be symbolically manipulated by ⟪Ag⟫, aka “The Silver Solver”. I've updated my Sudoku rules to use these
𝕖
┊
new features
𝕔
┊
┊
𝟘𝟞·
I now have a somewhat general "pigeonhole solver" which, given a set of equations of the form x_i¬=x_j and for each x_i, one equation of the form x_i∈{c_j c_(j+1)
┊
c_(j+2) ... c_(j+k)}. This can directly be solved with a search, but I've been trying to avoid that in my pretense toward symbolic manipulation. In the end, I'm not
╰
sure my approach is all that different than a search - if I can write my approach up in a sensible form, I'll post a doc someplace and hope to learn more.
𝟳
/
𝟘𝟚·
This page is a rough (perhaps embarrassingly so) version of a solution to the first puzzle in Raymond M. Smullyan's Satan, Cantor and Infinity
𝟲
/
𝟛𝟘·
I'm generalizing the way I validate proof steps so inference rules match if any formulae with an equivalent (Sapphire specific) normal form would have matched.