Full threadcodelion·It is also possible to build a model of Presburger arithmetic extended with infinity. We did that a few years back, you can try it out online here - http://loris-5.d2.comp.nus.edu.sg/SLPAInf/View on HN