From Semantics to Consistency Proofs and Back

Abstract

The current article endorses two main thesis. First we claim that the starting point in a consistency proof of a formal system is a semantic notion. This thesis is supported by an analysis of the stages in which a consistency proof goes through once that already in the initial stage an attribute for formulas must be specified on a interpretative basis. In order to move one stage forward at a time, a consistency proof must give an additional information corresponding to the system. We corroborate the thesis with case studies of three systems by which their constructive consistency proofs are analysed. Each study is restricted to constructive proofs since in the model-theoretic case the thesis is trivial. We analyse first-order logic, arithmetic without induction, also known as Robinson’s arithmetic, and arithmetic with induction or Peano’s. Then, we consider the relation between consistency and truth in Peano arithmetic in light of the case study. In regard to this we can formulate our second thesis: there is a conception of arithmetic truth in which no commitment with consistency must be taken for granted. The motivation for this thesis is the limitation for achieving constructive consistency proofs presented in the article.