Finitary consistency of a free arithmetic
A free variant FA of Peano arithmetic is proved consistent by using finite (outer domain) models. FA is weaker than standard arithmetic in two senses. First, one cannot prove that the successor, addition, and multiplication functions are always defined. Second, one cannot prove \(\sim s(t)=0.\) However, one can prove both of the above for closed terms.
scientific article; zbMATH DE number 3867320