Rule based proofs

Suppose we have a set of rules for constructing proofs for a system, and the rules could (in principle) be used to construct a proof of the validity of the system. And suppose that we have a proof-computational analogue of validity, as Gödel has. But we add one more thing: the system we are working with is a 'language', and our concept of a rule is grounded in the intelligibility of this language - so that we give an account of 'rule' in terms of some actual rules, and we we give an account of these recursively (or transcendentally) as I've indicated elsewhere in this blog. (We show that the failure of one of these to be a rule would be inconsistent with the intelligibility of the language.)

Would we then be trying to ground the intelligility of the language (it's capacity to test validity) in the intelligibility of the language (upon which the rules of demonstration ultimately rest)? And, if we were, why would this circularity produce a contradiction, rather than just be vacuous or invalid?

Maybe because these are the only two options - vacuous circularity or inconsistency. Although that's a bit vague and long-range.

Arithmetic is a good subject for this kind of investigation because of its capacity to model an indefinite range of rules and representations. It's because it can do this that it generates the incompleteness and inconsistency theorems.



The cycle I'm thinking of looks something like this:



(1) It is possible to state a rule, because we couldn't speak otherwise - it is a consequence of intelligibility

(2) Some of the rules we must be able to state are rules of logic and of arithmetic

(3) We can use these rules to specify a general theory of validity

(4) A demonstration of validity is, essentially, a demonstration of intelligibilty...

What happens as we go around this circle?

Maybe we discover that either (a) we stop meaning anything (we execute the recitations of a machine) or (b) the meanings change as we iterate.

(a) would be a result of being able to give a complete behavioural account of what was going on (which we could only do in a 'meta-language'). Once we've done this, we can't constrain the meaning of the behaviour we have described.

(b) means the rules change as well. To change the meaning of a rule is to change its consequences - what can be deduced from its truth. This means that we don't get a 'closed' system of proofs.

(This is all consistent with (i) the current conversation being the top of the meta-linguistic hierarchy and (ii) unspecifiable constraints on meaning, allowing developmental change - especially as we change meta-linguistic perspective.)

How could we say that the 'meanings' of the rules (Peano plus logic?)that Gödel employed changed?

Or is it the meaning of 'validity' which changes?

His computations might be 'meta-computations', since he - in some sense - demonstrates that they are 'in principle' executable, but does not execute them.

This is like saying that a rule we use applies outside of any possible scope of use. That it is 'universal', where this includes things we can't talk about as well as things we can.