Talk:Axiom schema

From Wikipedia, the free encyclopedia

I think this entry needs to reference the inference rule of Uniform Substitution (which doesn't yet have an entry). Uniform subsitution, in sketch: given wff X, in which variable y is free, and another wff Y, we can create a new wff X\[y/Y\] in which every occurrence of y is replaced with Y. 'Uniform' indicates that every y has been replaced with the same wff. The inference rule of Uniform Substitution is: if X is a theorem, and Y a wff, then X\[y/y\] is also a theorem. If Uniform Substitution exists as a given or derivable inference rule in a deductive system, then a great many axiom schemata can be dispensed with (though, given how general the definition in this entry is, not necessarily all). Thoughts?

I have just rewritten this entry, unintentionally doing so without implementing your suggestion. I have no quarrel with what you say, but I do find it very hard to be very precise about substitution rules. I wrote the substitution rules in Laws of Form. I have read that even Alonzo Church himself had trouble getting substitution right in his early formulations of the predicate calculus.132.181.160.42 05:33, 8 August 2006 (UTC)