Difference(s) between an axiom scheme and an axiom The basic question which motivated me to write this post is the following,

What is(are) the difference(s) between an axiom scheme and an axiom?

In Margaris's book First Order Mathematical Logic we have the following, 
However, the difference between an axiom and an axiom scheme is not clearly stated there in the sense that in the book it is not clearly specified exactly what is(are) the property (or properties)  that help us to distinguish between an axiom and an axiom scheme.
Question

What is an axiom scheme? Is an axiom scheme different from one of its instances? If so, then in what sense exactly? 


Disclaimer


*

*I had some discussion with user21820 regarding this question and one can see our discussion here.

*For a different and more philosophical version of the question see here.
 A: An axiom scheme is simply (but see below) a set - usually infinite, otherwise there's not really much of a point - of axioms. This is different from an axiom, in general, since axioms are sentences in some formal language, and "saying infinitely many things at once" might not be something that language lets us do. Specifically, given a set of sentences $\Sigma$, there may be no single sentence $\varphi$ in our specific formal language which implies every single sentence in $\Sigma$. (Note that we can of course say "Every thing in $\Sigma$ is true" in English, but there's no reason this sequence of words has to have a corresponding sentence in the specific formal language we're working in.)
OK, my first sentence isn't totally honest. Usually we think of an axiom scheme not as just some arbitrary set of sentences, but rather some set of sentences following some pattern. But this isn't relevant to your sub-question of how schemes are different from individual axioms; rather, it just says that some kinds of sets of sentences are nicer than others and deserve special names.

EDIT: Reading your linked posts, it's clear that you're actually interested in my second paragraph above - the one that I didn't elaborate on. So this answer is, I'm sure, very unsatisfying. I don't have time at the moment to elaborate, but I will do so this evening if no one posts a more on-point answer in the meantime. The ultra-short version is: the phrase "of the same form," or "following some pattern," is not formal, and "axiom scheme" is not a formal term; however, it is a useful informal term, and in fact it is easy to formalize (although there is not, in my opinion, any "best" formalization or reason why such should exist).
A: I'll expand on my responses to his question in the logic chat-room. =)

An axiom scheme is a collection of axioms. That is pretty much all there is to it, since we do not generally precisely delineate what is not an axiom scheme. For a concrete example, all the basic properties of arithmetic are captured by a finite collection of axioms called PA− (which are listed out in this article)‌​, but it turns out that the induction axiom schema can never be captured by a finite collection of axioms.
Of course, we never need an axiom schema when it consists of finitely many axioms, since we can just conjunct them all together into one axiom. The word "schema" can be thought of as meaning "template", namely a prescribed general format for some collection of axioms.
The law of excluded middle (LEM) can be treated as either a deductive rule or an axiom schema (one axiom "$P∨¬P$" for each sentence $P$). Same with all those propositional axiom schemas you have in the picture. In that presentation you have a Hilbert-style system (where there is only one deductive rule, modus ponens) and so all the laws/rules will be axioms, and you have infinitely many of them. Naturally you would classify them into a few schemas, one for each kind of law/rule. They are described via schemas, since you cannot write all of the axioms down.
If instead you had a natural deduction system, you could capture these via deductive rules instead of axioms. You cannot write down every instance of application of these deductive rules, but you can write down the rule itself.

By "prescribed general format" we mean a rule of generating the axioms. Note that an axiom may very well belong to multiple schemas, but typically we like no redundancy and hence axiomatic theories that we define mostly do not employ 'overlapping' schemas. Note also that an axiom schema is certainly not an axiom. An axiom schema can sometimes be represented by a syntactic template (as in your picture), which is just a symbolic string that can be interpreted to denote the schema itself, but the schema should not be treated as any of its instances, just as $\mathbb{N}$ cannot be treated as any of its members.
Finally, we definitely use "axiom schema" only for recursively enumerable collections of axioms, but it seems that in practice we use it only for collections that can be decided by primitive recursive functions; we view schemas as referring to lists that can be easily verified syntactically.
As a related example see this usage of "theorem schema" with the same kind of meaning I have described above; since that list of recursion theorems is the collection of all sentences of the form "$WO(A,<) ∧ ∀f\ ∃!y\ (γ(f,y)) ⇒ ∃F\ ( Func(F,A) ∧ ∀t ∈ A\ ( γ( F ↾ A_{<t} , F(t) ) ) )$" where $γ$ is a 2-parameter sentence over ZFC and $A,<$ are free variables and $WO(A,<)$ expands to a sentence stating that $A$ is well-ordered under $<$ and $Func(F,A)$ expands to a sentence stating that $F$ is a function with domain $A$.
A: Sequent logics have axioms and inferences.  These are mechanically different things.  $\dfrac{P \to Q,~P}{Q}$ is an inference, where as $\lnot \exists y ~:~ y + 1 = 0$ is an axiom.  
Even though $P \to Q \to P$ looks like an axiom, it isn't (see caveat below).  It is the inference $\dfrac{P \text{ is Prop},~Q \text{ is Prop}}{P \to Q \to P}$, where $P$ and $Q$ are just placeholders for any arbitrary propositional expression.  $\vdash (A \to B) \to (C \land D) \to (A \to B)$ is a valid instance of the inference A1.  If $P \to Q \to P$ was an axiom, then it wouldn't affect the provability of $(A \to B) \to (C \land D) \to (A \to B)$ for the same reason that the axiom "all squares have 4 sides" can't be instantiated as "all triangles have 4 sides".  Axioms mean exactly what they say and nothing else.
But it looks a lot like an axiom.  Also, every proof only uses a finite number of instances of (for example) A1.  Suppose a proof uses 70 instances of A1.  You could say it is uses 1 inference, or you could say it is uses 70 different axioms and doesn't use the inference.  Both would be correct.  Thus the term "axiom-schema".  As far as why you would ever want to look at things that way:  consider the principle of mathematical induction:
$$\forall P() ~:~ \bigg(P(0) \land (P(k) \to P(k + 1)) \vdash \forall n~:~ P(n)\bigg)$$
This can be treated as a rule of inference, or as 1 second order axiom, or as finite number of first order axioms for any given proof, or as a countably infinite number of axioms in general.  All of those ways of looking at induction are correct.  So it is often called an "axiom-schema" to reference how it spans the ideas of inferences and sets of axioms.  Furthermore, many results of first order logic (without restrictions to finite sets of expressions) will apply to this despite it also being a second order axiom since it could also be described as infinitely many first order axioms.
Caveat:  It is possible to introduce an inference known as something like "universal propositional substitution" (UPS), which basically says "If P is proven, and A is a propositional variable and B is any proposition, then all instances of A can be replaced by B to create a new proven expression P[B/A]".  If you have UPS then A1 etc can be treated as axioms, and some logicians like Jaśkowski did that instead of having axiom-schemas.  The pros and cons of using UPS instead of axiom schemas are probably for another question though.
A: Axiom schemes are conceptually (usually infinite) collections of axioms. However, since it's critical that checking a putative proof is decidable, this collection needs to be describable via a finite algorithm. So in general an axiom scheme is an algorithmic description of a collection of axioms. (You can weaken things a bit more, but at that point it's questionable whether the term "axiom scheme" would be appropriate. It's rare that anything close to the full flexibility of computation is used.)
All that said, A1-A6 don't look like an algorithm.  In this case, axiom schemes in the question can be viewed as templates for use in a matching algorithm. This can be formalized quite literally. The axiom schemes are written in the same formal language as formulas except they add the possibility for meta-variables, i.e. the $P$, $Q$, $S$, $t$ and $v$. Sentences in this extended language are simply not formulas in the original language (unless they have no meta-variables). 
There's a fairly straightforward algorithm to take a formula and an axiom scheme and find instantiations for the meta-variables that make the instantiated axiom scheme match the formula. This is syntactic matching, though A5 (and to a lesser extent A6) actually would require higher-order matching (which is decidable but not so straightforward) if we wanted to handle it solely through matching. For A6, you can just do normal, first-order matching then check the side-condition afterwards, but this will happen automatically with higher-order matching.
The algorithm for simply checking whether some given instantiation for the meta-variables is correct is much simpler, basically syntactic substitution and syntactic equality. That is, I give the algorithm a formula and ask it whether it's an instance of, say, A1 with some specific formulas provided for $P$ and $Q$, and it returns either true or false as appropriate. Using Haskell's algebraic data type notation, it would be a function like:
data AxiomInfo
  = Axiom1 { p :: Formula, q :: Formula }
  | Axiom2 { p :: Formula, q :: Formula, s :: Formula }
  | Axiom3 { p :: Formula, q :: Formula }
  | Axiom4 { p :: Formula, q :: Formula, v :: Variable }
  | Axiom5 { p :: Formula, t :: Term, v :: Variable }
  | Axiom6 { p :: Formula, v :: Variable }

check :: AxiomInfo -> Formula -> Bool

where Formula, Term, and Variable are data types representing formulas, terms, and variables respectively. In other words, check takes a data type (AxiomInfo) which specifies which axiom scheme you want to check and what values you want to use for the meta-variables (which vary depending on the axiom scheme). You can view it as a number $i\in\{1,\dots,6\}$ and a substitution $\theta$ which calculates $\phi = A_i\theta$ where $\phi$ is the formula and $A_i$ corresponds to the relevant axiom scheme. A matching function is then a function like match :: Formula -> List AxiomInfo with the guarantee that for each AxiomInfo returned, running check against it and the formula provided to match will return True, and that this is true for no other AxiomInfos not in the list returned by match. (This doesn't quite work due to A5 which, naively, can have an infinite number of matches as any term $t$ will do if $v$ does not occur in $P$. We could use a special symbol to represent this case, or we could split A5 into two cases: one that requires $v$ to occur in $P$ and one that disallows $v$ to occur in $P$.)
A decidable algorithm like check leads to an algorithm for checking the correctness of a proof if a proof is represented as a tree of uses of modus ponens and applications of axiom schemes.
