Perhaps you should be upset if you've been led to believe as a generalisation that "...we never can know that our axiom system is consistent", and that "...proofs are not like as I once used to believe: a certificate that a counterexample for a statement can not be found".
These beliefs may be understandable (even if not justifiable) in the case of a set-theoretical language such as ZF, which can have no finitary interpretation.
They are misleading in the case of a first-order language such as PA which, in a digitally communicating universe, would be of more consequence than ZF.
Misleading, because they reflect the subjective belief that Aristotle's particularisation holds over the structure N of the natural numbers; which is the postulation that from an assertion such as:
'It is not the case that, for any given x, P(x) does not hold in N',
usually denoted symbolically by '~(Ax)~P(x)', we may always validly infer that:
'There exists an unspecified x such that P(x) holds in N',
usually denoted symbolically by '(Ex)P(x)'.
However, as Brouwer had noted in a seminal 1908 doctoral dissertation, the presumption that Aristotle's particularisation holds over infinite domains such as that of the natural numbers does not lie (as self-evident) within a common human intuition; and such a presumption has no logical basis in the objective decidability and computability of number-theoretic relations and functions over the domain of the natural numbers.
Now, although Kurt Goedel's arguments in his seminal 1931 on undecidable arithmetical propositions avoid assuming that Aristotle's particularisation holds over N, Goedel found it necessary to assume that the Peano Arithmetic he was considering was omega-consistent.
Omega-consistency: PA is omega-consistent if, and only if, there is no PA formula [F(x)] such that [~(Ax) F(x)] is PA-provable and also that, for any PA-numeral [n], [F(n)] is PA-provable.
However, it is easily seen that PA is omega-consistent if, and only if, Aristotle's particularisation holds over N.
(Although J. Barkley Rosser claimed in a 1936 paper to prove the existence of undecidable arithmetical propositions without the assumption of omega-consistency, his argument appears to implicitly presume that Aristotle's particularisation holds over N.)
The assumption of omega-consistency has a history.
David Hilbert was one who firmly believed that an arithmetical proof is, indeed, a certificate that a counterexample for a true arithmetical statement can not be found.
Thus, as part of his program for giving mathematical reasoning a finitary foundation, Hilbert proposed an omega-Rule as a finitary means of extending a Peano Arithmetic to a possible completion (i.e. to logically showing that, given any arithmetical proposition, either the proposition or its negation is formally provable from the axioms and rules of inference of the extended Arithmetic).
Hilbert also believed that the standard interpretation of PA is sound, which implies that Aristotle's particularisation holds over N.
In a contemporary context, Hilbert's omega-rule can thus be expressed as:
Hilbert's omega-Rule: If it is proved that a formula [F(x)] of the first-order Peano Arithmetic PA interprets under the standard interpretation of PA as an arithmetical relation F(x) that is true for any given natural number n, then the PA formula [(Ax) F(x)] can be admitted as an initial formula (axiom) in PA.
Goedel's 1931 paper on formally undecidable arithmetical propositions can, not unreasonably, be seen as the outcome of a presumed attempt to validate Hilbert's omega-rule by his assumption of omega-consistency.
However, Goedel discovered a PA formula [R(x)] such that if PA is assumed omega-consistent, then both [(Ax)R(x)] and [~(Ax)R(x)] are not PA-provable (Goedel's First Incompleteness Theorem).
Further, assuming that Aristotle's particularisation holds over N, Goedel defined a number-theoretic relation Wid(PA) which holds in N if, and only if, PA is consistent.
Goedel then discovered (his Second Incompleteness Theorem) that, if PA is assumed consistent, and we assume that some PA formula [W] expresses Wid(PA) in PA, then [(Ax)R(x)] is PA-provable if [W] is PA-provable.
Ergo, if PA is omega-consistent, then we cannot express the assertion 'PA is consistent' in PA by a PA-provable formula.
Now the points to note are that:
PA is omega-consistent if, and only if, Aristotle's particularisation holds over the domain N of the natural numbers.
If the standard interpretation of PA is logically sound, then Aristotle's particularisation holds over N.
Aristotle's particularisation over N can be expressed in contemporary terms as:
From an assertion such as:
'It is not the case that, for any given x, any witness Witness_N of N can decide that P(x) does not hold in N',
usually denoted symbolically by '~(Ax)~P(x)', we may always validly infer that:
'There exists an unspecified x such that any witness Witness_N of N can decide that P(x) holds in N',
usually denoted symbolically by '(Ex)P(x)'.
The validity of Brouwer's objection follows since Aristotle's particularisation does not hold over N if we take the witness Witness_N as a Turing machine, and P(x) is a Halting-type of number-theoretic relation.
It follows that if PA is not omega-consistent, then we cannot conclude from Goedel's Incompleteness Theorems that Goedel's [~(Ax)R(x)] is unprovable in PA.
The significance of the above is that issues involving number-theoretic functions and relations containing quantification over N lie naturally within the domains of:
(a) First-order Peano Arithmetic PA, which attempts to capture in a formal language the objective essence of how a human intelligence intuitively reasons about number-theoretic predicates, and;
(b) Computability Theory, which attempts to capture in a formal language the objective essence of how a human intelligence intuitively computes number-theoretic functions.
Now Goedel had also shown in Theorem VII of his 1931 paper that every recursive relation can be expressed arithmetically.
This suggests that if we can, conversely, define a finitary interpretation of first-order PA over N as sought by Hilbert, then any number-theoretic problem can be expressed - and addressed - formally in PA and its solution, if any, interpreted finitarily over N.
Now, if [A(x1, x2, ..., xn)] is an atomic formula of PA then, for any given sequence of numerals [b1, b2, ..., bn], the PA formula [A(b1, b2, ..., bn)] is an atomic formula of the form [c=d], where [c] and [d] are atomic PA formulas that denote PA numerals. Since [c] and [d] are recursively defined formulas in the language of PA, it follows from a standard result that, if PA is consistent, then [c=d] is algorithmically computable as either true or false in N.
In other words, if PA is consistent, then [A(x1, x2, ..., xn)] is algorithmically decidable over N in the sense that there is a Turing machine TM_A that, for any given sequence of numerals [b1, b2, ..., bn], will accept the natural number m if, and only if, m is the Goedel number of the PA formula [A(b1, b2, ..., bn)], and halt with output 0 if [A(b1, b2, ..., bn)] interprets as true in N; and halt with output 1 if [A(b1, b2, ..., bn)] interprets as false in N.
Moreover, since Tarski has shown that the satisfaction and truth of the compound formulas of PA (i.e., the formulas involving the logical connectives and the quantifiers) under an interpretation of PA is definable inductively in terms of only the satisfaction (non-satisfaction) of the atomic formulas of PA, it follows that the satisfaction and/or truth of the formulas of PA under the usual interpretation of the PA symbols is algorithmically decidable.
This is clearly a finitary interpretation of PA over N.
So, if Aristotle's particularisation does not hold over N, and the standard interpretation of PA is not logically sound, then - instead of considering Hilbert's omega-rule - the question that one ought to consider is whether the above is a sound algorithmic interpretation of PA such that:
Algorithmic omega-Rule: If it is proved that the PA formula [F(x)] interprets as an arithmetical relation F(x) that is algorithmically decidable as true for any given natural number n, then the PA formula [(Ax)F(x)] can be admitted as an initial formula (axiom) in PA.
This question is far more amenable to finitary reasoning, and I argue that it can be answered affirmatively. See:
http://alixcomsi.com/27_Resolving_PvNP_Update.pdf
If so, it would confirm that your faith in the classical notion of a proof is not misplaced, and an arithmetical proof is, indeed, a certificate that a counterexample for a true arithmetical statement can not be found.