7

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, enter image description here

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.

To elaborate the problem a bit, consider the following question,

What is an axiom scheme?

In response to this one may reply (as has been given here) that

An axiom scheme is a collection of axioms all of which have the same form.

But then,

  1. How is it possible to have "a collection of axioms all of which have the same form"?

  2. How are we differentiating between the forms of two axioms?

  3. Are we then saying that the form of an axiom and the axiom itself are two different objects? What does it mean then to say that logic is formal?

  4. Why does an axiom have "form" (assuming that it is indeed a property of an axiom and not the collection of axioms) and in what sense exactly?

Disclaimer

  • I had some discussion with user21820 regarding this question and one can see our discussion here. However for some reasons I don't agree with his answers and although I didn't explicitly elaborated my reasons of disagreement with him in this post till now, I hope to do so very soon.

  • For a different and more mathematical version of the question see here.

Improve this question
5
  • 2
    If you wanted to build a chair from Ikea and you had the instructions in front of you, those instructions would let you build the chair using any of the parts the company manufactured to build that type of chair, not just the parts that came in your box (not including any ones that have defects of course). An axiom schema is not an axiom, it is a set of rules that show you how to build/how to recognize axioms. All of the different chairs that are built are axioms, the instructions are the schema that show you how to build them and how to recognize that they were built correctly.
    – Not_Here
    Aug 21, 2017 at 17:54
  • 4
    Axiom schema is a way to write higher order axioms without going beyond first order language. For instance, to for induction what we really want to say is that it should hold for "any property". But to do that we need to quantify over properties, and that requires second order languages with their complications. Instead, we introduce a list of first order axioms of the same "form": if P(1) and P(n)→P(n+1) then for all n, P(n). Here P is allowed to be replaced by any properly formed predicate, hence the induction "schema". This way the talk of "any properties" is technically avoided.
    – Conifold
    Aug 21, 2017 at 20:22
  • @Not_Here: "All of the different chairs that are built are axioms, the instructions are the schema that show you how to build them and how to recognize that they were built correctly." - if the instructions are the schema then wouldn't the instruction for a particular chair (as opposed to the chair itself) be an axiom?
    – user13627
    Aug 22, 2017 at 3:37
  • Example of instance of A1 from "formal arithmetic": 1=1 → . 1=0 → 1=1. We have to fix a specific formal language and write down a specific formula according to the syntax rules of that language.
    – Mauro ALLEGRANZA
    Aug 28, 2017 at 14:43
  • A different instance of the same schema regarding the same language will be: 1=0 → . 1=1 → 1=0. This is a different formula from the above one.
    – Mauro ALLEGRANZA
    Aug 28, 2017 at 14:51

2 Answers 2

Reset to default
2

From Wolfram's MathWorld entry on axiom schema:

An axiom schema is a sentential formula representing infinitely many axioms. These axioms are obtained by replacing variables in the schema by any formula.

Axioms are specific sentences in a formal language, they contain specific formulae, variables, and terms. Axiom schema are general sentences that show how to create specific axioms within a formal system. Schema generalize over all of the formulae, variables, and terms in the language. You go from a scheme to an axiom by substituting in specifics for the generalized place holders in the scheme. For example:

Scheme: If P and Q are formulae of our language then P -> Q is an axiom

Axiom: (A^A) -> A

Axiom: ~(B) -> A

Why and how does this work? Because, assuming that our language contains the propositions A and B and the connectives ^, ->, and ~, then A^A and ~B are as well, therefore we can substitute both of those in for the P and Q in our scheme to create an axiom.

You ask "what is the same logical form?" The same logical form in this example is the form of P -> Q with P and Q both being formulae. (A^A) is a formula and A is a formula therefore (A^A) -> A is of the same form as P -> Q with P and Q being formulae.

An example of two formulae that do not have the same form:

A v B

~A

These formulae obviously do not have the same form, one of them is a disjunction between two formulae and one of them is the negation of one formula. In the above example of our axiom scheme we state that there are infinitely many axioms of the same form, ones that have the form of an implication, P -> Q. Obviously A v B and ~A are not the same form as P -> Q.

Yes, the form of an axiom and the axiom itself are different. Again, this is because with an axiom we are substituting in specifics. That is what is meant by "Let P, Q and S by any formulas" in the text you quoted, in those schema P, Q, and S are not actual formulae, they are dummy variables that we are using as placeholders. To get a real axiom you substitute in actual examples from the language. (A -> B), (B -> A), (A -> A) all have the same form and they are obviously not the same axiom, they are examples of substituting in different particulars. I can understand how this can be confusing if P is actually in the language but that's why the author clarifies with "let them by any", they are not saying only, P -> Q is an axiom, they are saying there is an infinite list of all formulae of the form P -> Q, e.g., again, (A -> B), (B -> A), etc.

From Wikipedia's article Logical form:

The logical form of a sentence (or proposition or statement or truthbearer) or set of sentences is the form obtained by abstracting from the subject matter of its content terms or by regarding the content terms as mere placeholders or blanks on a form. In an ideal logical language, the logical form can be determined from syntax alone; formal languages used in formal sciences are examples of such languages.

The logical form of an axiom is its syntax. P -> Q is the specified syntax that we are looking for, in our example. So, any formulae that has the syntax of P -> Q where P and Q are both formulae, is of that same logical form.

Improve this answer
16
  • As just a note now because I don't have to time to add more yet, Conifold brought up a point that I was going to point out as well and use ZFC as an example, so that will come soon, and additionally I'll explain why "A scheme is an infinite set of axioms" and "a scheme is instructions on how to create an infinite set of axioms" both mean the same thing, and why the former is strictly more correct but the latter makes more sense when you consider what the definition of scheme is, but again they both mean the same thing. Hopefully that point isn't confusing as it currently is written.
    – Not_Here
    Aug 21, 2017 at 20:54
  • A small caveat: An axiom can be an instance of several axiom schemes. For instance, you could have axiom schemes P → ⊤ and ⊥ → Q, and the axiom ⊥ → ⊤ is an instance of both.
    – Uwe
    Aug 21, 2017 at 21:44
  • @Uwe sure but I don't see how that is a caveat to what I wrote, the OP asked what the difference between an axiom and an axiom scheme is. Of course there are different instructions for how to make the same thing.
    – Not_Here
    Aug 21, 2017 at 22:04
  • 3
    I disagree with this answer. Nearly every axiom schema in well-known first-order theories (PA, ACA, ZF[C], ...) are not simply templates where you can substitute sentences into placeholders. Take a look at Replacement in ZF for example... pinging @user170039 as well. =)
    – user21820
    Aug 24, 2017 at 6:48
  • 1
    In particular, it is incorrect for Wolfram Mathworld to say that "An axiom schema is a sentential formula representing infinitely many axioms." as it simply does not hold for actual mathematical usage of the term "axiom schema".
    – user21820
    Aug 24, 2017 at 6:50
1

You say that this text does not explicitly say what could help us distinguish between axiom and axiom scheme; however, I do think this text has given the formal difference between axiom and axiom scheme, at least as they are used in this context:

"Each axiom scheme provides infinitely many axioms, which we call instances of the axiom scheme".

Though this may appear circular, the formal difference is given in the above quote, through their respective definitions in relation to each other:

  • an axiom scheme in this context is what provides (gives the formula for) infinitely many axioms
  • axioms in this context is the term we give to specific instances of a given axiom scheme

I hope this is of some help

Improve this answer
1
  • You can also have axioms that are singular and do not instantiate a scheme. Most axioms are of that form. But some, like the principle of induction in first order arithmetic, need infinitely many instances -- in that case we need one for each integer because a single axiom to explain the action taking place would have to be either second-order or infinitely long.
    – user9166
    Aug 24, 2017 at 21:26

You must log in to answer this question.