>>16835705
You can define logic in a fragment of arithmetic (e.g. the bounded arithmetic).

It is possible to write a computer program which checks if a proof is correct without reference of a set theory.