Note: This question is not a duplicate of the suggested link. That link explains the schema system is great detail -- and is a great reference, and better than I have seen elsewhere. However, it does not address propositional variable systems, or the differences between them. Further, the fact that they also require substitution rules is glossed over.
This may appear to be trivial. But, some authors make a big deal over formalizing a logical system using schema vs using propositional variables. The claim is generally that using propositional variables requires a substitution rule.
Yet, if we have $A \lor B$ as an axiom in a schema system, first each of the A, B represents some wff composed of propositional variables and / or object expressions. And, inside of a proof, instances of that axiom such as $(X \land Y) \lor (U \land V)$ are allowed "instances" of that schema axiom.
So, where is the real difference? There are substitution rules somewhere in both types of systems. They may be explicit, part of the proof rules, etc. Worse, the schema systems are more complex because they require two types of variables and must, therefore, have two distinct substitution rules (one to substitute schema wffs for a schema variable, and one to substitute a propositional variable wff for a schema variable). Another claim is that the substitution rules in a propositional system are more complex, yet those in a schema system have to deal with exactly the same circumstances and two types of variables.
As I see it, a propositional name may be variable, fixed, or constant. They are variable in the statement of an axiom, rule, or theorem. They are fixed within the context of a proof. And they are constant if they are a logical constant, a global constant introduced via definition, or a local constant whose scope is restricted to a specific proof, and which is introduced by a definition. A propositional logical system may or may not have global constants. This is very similar to object names which may be variable, bound (and limited to a specific scope), or constant.
Additionally, in a logical system where there are multiple object types and expressions, you may have a situation where those propositional variables could then be replaced by different object expressions as well, and object variables which may be replaced by appropriate object expressions.
This distinction between schema systems and propositional variable systems appears to be a tempest in a teacup. Completely meaningless, and a pointless waste of time.
Of course, I probably have no idea of what I am talking about. So what is the "real" difference, or is there really one? Where are the real benefits? Does anybody actually bother to formalize any of that when defining a logical system?
Thanks. I am interested in what other people think about this.
Edit: A link to a different question was suggested as a possible answer. This link did touch upon the subject, and does clarify one point. Namely that in a schema system, the schema variables represent arbitrary propositions, but that proposition variables represent specific "atomic" propositions. This may reduce the number of substitution rules required in a schema system from two to one, but otherwise there is no difference. Really, in a propositional system, all propositions are "atomic" because we don't know, or care, what they represent. So adding an extra variable type for that doesn't really buy you anything except extra complexity.
Thank you to whomever suggested the link, because that did clarify one point about the schema propositional variables always being atomic.