@MaliceVidrine Because people are sometimes busy. =)

@user709833 It's common to see confusion (even on Math SE) regarding meta-logical issues, and (usually) it is because they read some unclear exposition. The thing you must understand first before everything else is that a formal system is something that you can write a program to verify or refute the validity of any proof (given as a character string) over that system.

With this in mind, you can then look at FOL (first-order logic) and think carefully to convince yourself that, if you have a program that halts on every input string and outputs "yes" iff it is an axiom, then you can write a proof verifier program for the FOL system with those axioms.

What I've just said is in complete generality and applies to every possible practical formal system, whether it is Hilbert-style or Fitch-style or some new style in the future that we don't know about yet. Yes, the proof verifier program will be different for each particular system, but the underlying idea behind formal systems is completely identical.

I feel that there is a regrettable dearth of explanations of this that is accessible to the lay person. All you need is to understand rudimentary programming, and in fact it is necessary to understand programming if one wants to fully grasp certain parts of logic such as the incompleteness theorems.

If you know programming, I strongly encourage you to first figure out for yourself roughly how one might write a proof verifier program for say Fitch-style FOL, of which a specific variant can be found at ProofMood. Unfortunately, the English version has been recently taken down temporarily so you might have to wait to try it.

After you understand what goes into such concrete formal systems, then it is trivial to explain what axioms and schemas are. I've already stated above that an FOL system must come with a proof verifier program, which of course must not only know the deductive rules for your chosen flavour of FOL, but must also know the axioms for the specific system (such as PA, ACA, ZC, ZFC, NBG, ...). There is no mention of schemas, because there is no actual need for them.

But in the past, before logicians acquired a proper understanding of computation, when they wished to write down an axiomatization of some structure, they literally wrote down one axiom at a time. Hence for them to express the induction schema (which comprise infinitely many axioms, one for each sentence about a parameter from N) they gave the syntactic form that all such axioms must have.

But even historically, the term "schema" has not been precise, because it includes much more than a sentence with some placeholders! For example, even ZFC's specification schema includes axioms with arbitrarily many free variables.

Nevertheless, I hope it is clear to you that whatever people call an axiom schema is not an axiom. Informally, it is the form of some axioms. Formally, it is just a set of some axioms, but if we define "schema" as "set of axiom" then the term "schema" becomes redundant... And I doubt there is a rigorous way to define "schema" that will correspond to exactly what logicians will use it for in the future.

@user21820 I am still a little confused though if only because I feel like I can write a program for just about anything I want

@user709833 That's why I never use the term "schema" when teaching basic logic, because it seems more confusing to try and explain the vague ways people use the term than to just not use it.

When people say a schema is infinitely many axioms I get sort of confused by that because if I have the axiom x = y iff S(x) = S(y), to me that also seems kind of infinite because I can pick infinitely many natural numbers for either x or y

so I don't understand the difference between "an axiom with infinitely many inputs" and "an axiom schema with infinitely many axioms you can make"

@user709833 In PA you do not have natural numbers. There are only two constant-symbols in PA, namely 0 and 1.

I was reading a book called Analysis Volume I (by Terrence Tao) where he uses PA to derive the natural number laws and build up to integers, rationals, reals etc

Moreover, even if you have many constant-symbols, one for each 'real' natural number, there is still only one axiom "∀x,y ( S(x)=S(y) ⇒ x=y )".

@user709833 Terence Tao is unfortunately too imprecise when it comes to foundations of mathematics.

are you referring to something like how we're really only saying things like S(S(S(0))) instead of 3

@user709833 No I don't; I was just being precise because you were talking specifically about PA, which in all modern expositions is defined to have only two constant-symbols. That's why I then said that it does not matter even if you have infinitely many constant-symbols.

> there is still only one axiom "∀x,y ( S(x)=S(y) ⇒ x=y )".

is a "schema" something where we can write infinitely many axioms where each one literally looks different?

Vaguely, yes. But I emphasize that I cannot give a rigorous definition of "schema" because there is none. The only meaningful distinction I know is that people only use that term to describe infinitely many axioms of some kind.

why does PA only have 0 and 1? minimal number of constant symbols to describe the basic axioms?

@user709833 Yes, in my preferred axiomatization.

In the one you seem to be using, you only need 0. I forgot about that when I made my earlier remark.

right, yeah, I think tao only relies on 0 at first but then says we can just define S(0) = 1, S(1) = 2, S(2) = 3, etc

That's fine.

when you say PA only uses 0 and 1, is this part of the "signature"?

that is another word I've seen a lot

or the "language"?

Yes. The language/signature of an FOL system (typically called theory) is the specification of the function/predicate-symbols available.

Function-symbols include constant-symbols.

is a theory just a set of axioms/schemas?

You can say so. The theory comes with a language and a set of axioms, and that's it. Out of laziness, people sometimes don't bother stating the language when others can guess it... Also, as I mentioned before, in the past people didn't know programming so they had no way to express an infinite set of axioms except via what they called schemas.

For an example, the induction schema for PA is called a schema because it describes infinitely many axioms. It turns out (a difficult and non-trivial fact) that there is no single axiom in the language of PA that can capture all the induction axioms (i.e. instances of the induction schema). So there is usefulness for the notion of "schemas" if one doesn't know any programming.

If you look at the link I gave you, PA− is the system that has a bunch of axioms for 'basic facts about N', and PA is simply PA− plus induction.

PA− has finitely many axioms, and is preferred in the logic community when talking about foundational systems for arithmetic, because it is in some sense a better structural axiomatization than if you take the successor-based PA and remove induction...

In structural terms, PA− is the axiomatization of discrete ordered semirings, so you should find all the axioms look familiar except axioms 13,14,15, which catch the "discrete" and "semi" part.

does our usual mathematics rely on the first or second order system?

like say you write a proof of some random number theory or calculus concept and partway in you have a line that uses a(b + c) = ab + ac and I go "huh that's kinda peculiar, what is the proof that that works"

what would you resort to?

the second order peano axioms or the first order PA system?

@user709833 All modern mathematics can be expressed in an FOL system, and it is especially convenient to use many-sorted FOL such as the one I gave in this post. Any formal system based on higher-order logic can be easily translated into a many-sorted FOL system.

@user709833 Note that Peano's original axiomatization with the second-order induction axiom is useless for actual mathematics, because it quantifies over all sets, but Peano never did give any axiomatization for precisely what sets can be constructed, so the induction axiom becomes useless.

It turns out that almost every number theoretic fact can be proven in (first-order) PA, and there is no need to go to higher-order, but the price you pay is that you need to encode some stuff via Godel encoding. If you are not familiar with that, basically the issue is that you cannot obviously deal with arbitrary-length tuples in PA, so you need to devise some tricks that work in PA. But you can only observe from outside PA that those tricks actually capture tuples!

is second-order logic required at all for establishing the reals? @user21820

Based on what I said above, it is fair to say that PA cannot capture most number theory. That said, there are many systems of second-order arithmetic. One called ACA0 is conservative over PA (every arithmetical sentence is proven by ACA0 iff it is proven by PA). So although ACA0 proves some sentences that are not arithmetical (because they are about second-order objects), it does not prove any extra arithmetical sentences that PA does not. And the key point: ACA0 has finitely many axioms!

So ACA0 is a finitely axiomatized FOL system (with two sorts) that can capture most number theory, because we can more transparently encode a tuple as a set of pairs (i,k) where i is the index and k is the term.

ACA0 basically has all the axioms of PA− for N, plus a second-order induction axiom, plus an 'arithmetical comprehension axiom' (hence its name) that says that you can construct any subset of N { x : Q(x) } where Q is an arithmetical property (roughly speaking Q quantifies over only N).

@user709833 So to answer your specific question here, I would say that the right system to work in for number theory is at least ACA0, though it is better to have a little more, such as a function-symbol for exponentiation, and native function sorts rather than just encoding everything as sets.

Sorry I am confused, before you said "It turns out that almost every number theoretic fact can be proven in (first-order) PA" and then you said "It is fair to say that PA cannot capture most number theory"

Oh I forgot to say that while ACA0 is usually defined with the 'comprehension axiom' being a schema (one for each arithmetical property), it turns out that you can replace that by finitely many axioms.

@user709833 Because it can be proven after you have encoded the statement you want to prove via Godel encoding. However, you cannot convince anyone that you have proven what you originally wanted to prove without going outside PA and looking at what the encoding is doing.

It's not so easy to explain briefly what Godel coding is if you're not familiar with it, but I can point you to references if you are interested.

Anyway to be precise, for elementary number theory would probably be a good idea to have at least the language (0,1,+,·,<,^) and the axioms of PA− plus basic facts about ^ (i.e. all those you learnt in high-school) plus full induction plus ACA0's comprehension schema. For example Fermat's little theorem would be ∀p∈N ( Prime(p) ⇒ ∀k∈N ∃d∈N ( k^p = k+d·p ) ), where Prime(p) :≡ p ≠ 1 ∧ ∀x,y∈N ( p = x·y ⇒ x = 1 ∨ y = 1 ).

The easiest proof of this goes via proving existence of inverses mod p and using it to show that { a·k : a∈[1..p−1] } = [1..p−1], and so their products are equal, and then using inverses again to eliminate the product of [1..p−1] to get the desired result.

You can see that we would like to construct these sets, as well as their products (which can be easily done using a tuple of partial products).