Meaning and proof

The meaning of a statement is not one of its proofs, because there might be others.  Not all of its proofs because we might not know all of these. And a proof consists in turn of statements which must in turn have meaning leading to an infinite regress.  If the statements of a proof do not have meaning, how can it be a proof ? And  proofs also contains relations between statements. For a proof is not just a bag of statements.  Then what are these relations and what is their meaning ?  

Axioms have meaning, but they are accepted as not needing proof. Proofs depend on there being axioms. So proofs are not meaning. 

Who could deny that Gödel's sentence still has meaning in PA without it having a proof ?

Do we need a proof that a certain thing is a proof ? Do proofs themselves have meaning and does this meaning not have to be in turn a proof ? And if it does not, then  meaning is not proof. And if proofs do not have meaning how can they constitute the meaning of a statement ?

A term as a mere string has no meaning, cannot be a meaning, and is not a proof. To interpret this string as a proof, that is, as a term in the $\lambda$-calculus, as an algorithm, we need theory. We cannot invoke proofs-as-terms without dependence on the meaning of mathematical statements. We just pushed the whole matter upstairs as we can ask meaningful questions about the theory of terms which in turn require proof.

Proof-theoretic semantics is false and untenable. Meaning is constituted by meaning-constructions applied to primitive meanings but the total meaning is seized as a whole. Proofs themselves have meaning which can be grasped as a whole. Linear logic, intuitionistic logic and classical logic show a profound convergence and inter-relatedness which counts as a devastating argument against logical pluralism rather than for it. Incompleteness does not imply lack of categoricity.

Nor are the meanings of connectives and quantifiers given by rules. Rules in which they appear ? Rules in in which they exclusively appear ? And what if there is more than one rule, is the meaning  the whole collection or is the whole meaning in each part  or is the meaning fragmented into the various rules so each rule only gives the partial meaning of the connective ? What about equivalent systems of rules ? Why are the rules accepted in the first place if not because their are judged to conform to the meaning of the connective ? And what is a rule in general but a partial recursive functions on sequences of strings. These can be given through Boolean circuits and other models of recursion. So we just pushed back the problem to studying the meaning of recursion theory. And what about embeddings into higher-order logic which allows connectives to be expressed in terms of a fewer number of connectives.  Is the meaning then dissolved ?

Let us look at the natural deduction rule for $\&$ (the same argument applies for the sequence calculus).  Suppose we wanted to teach somebody this rule, that we wanted to describe this rule.  Can we do so without using the word 'and' ? Indeed, can we describe anything or teach anybody how to do anything without the concepts mediated by the basic connectives (and specially intuitionistic connectives) as well as universals (senses, intensions, meanings, abstract ideas), that is, quantifiers not reducible to extensional, possibly infinitary disjunctions or conjunctions ? 

And how do we recognize the equivalence between different types of deductive system involving the 'same' connective ? We already need logic to describe and know the relationship between rule systems. Why do we accept that the cartesian product corresponds to conjunction and the disjoint union to disjunction (considered from the point of view of category theory) ?  Product and coproduct are presented differently than deduction or sequent rules. Yet we recognize the same concept and idea.