Revised syntax of the quantified formula

The syntax published in March turned out to be problematic in order to be compatible with the old syntax.  The reason is the different treatment of Exists “function”.  The second parameter if Exists, if supplied three parameters, are evaluated differently than what I treated in Eos. 3.1.

I switched to the old syntax in order to be compatible with the old system and moreover to compatible with the commonly used syntax of the language of the first-order predicate logic.

Notation commands

Notation commands are not easy to write correctly, as Tutorial on Notation on Mathematica 12.2 document explains. In my (short) experience, the easiest is to put all the Notation commands that you will use at the beginning of your notebook. Alternatively, create a notebook file, say EosNotations.nb under the Eos3.3 directory, put all your rotation commands, and read them by:


So the header of your file will be
<< “EosHeader.m”

g3 Version 1.2.9
Eos3.32 (March 18,2021) running under Mathematica 12.2.0 for Mac OS X x86 (64-bit) (February 2, 2021)

<< “EosNotations.nb”;

Start wrinting Orikoto program


Eos3.32 is the modification of Eos3.31 to cope with the upgrade of Mathematica from version 12.1 to version  12.2.0.  The reasons that Eos3.31 do not work come from the changes of implementation of the Notation package and the Exists function.  Especially, the change of Exists posed challenges.  I treat Exists differently than the way implemented in the new Mathematica 12.2.  I also used a different notation for existentially (and universally) quantified formulas.  The use of the Notation package realized my notation.  Since the Notation command with non-trivial external expression does not seem to work as it worked in Mathematica 12.1 and earlier versions.  It took me more time than I expected.


More geometric theorems

We added the following geometric constructions and theorems.  They are collected under the new title “Origami Geometry.”

Euler line

Simson’s theorem


Meneraus’s Theorem

Ceva’s Theorem

Steiner-Lehmus Theorem