[ironborn123]

There are weaker formal systems like Presburger arithmetic (peano without multiplication) and Skolem arithmetic (peano without addition) that have been proven to be complete and consistent. Tarski also showed that there are formal systems for real numbers (hence also geometry) which have the same properties. (although the real numbers include integers, the integers alone have a lot more structure and so Tarski's result does not imply Peano)

There are also extensions to these (eg. presburger extended to multiplication by constants) that are also known to be complete and consistent.

These systems do not require any social compact. Any theorems proven through them are absolute truth, although the the range of statements that these systems can express is limited.

One may require a social compact for Peano, ZFC, and such other powerful formal systems.

That the software implementations like Coq and Lean are bug free may also require a social compact, if the nature of being bug free cannot be formally proved, although it seems determining this should be an easier problem.