# Are PA and ZFC examples of logical systems?

Wikipedia says

A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to sentences of the formal language.

When we talk about PA or ZFC, are these logical systems, or are they merely formal systems?

-
They are first-order theories. –  André Nicolas Feb 7 '13 at 0:39

PA and ZFC are first-order theories. That means that they are additional axioms for the first-order logic. In other words, by PA we mean the first-order logic (FOL) plus the axioms of these theories. The syntax and semantics comes from first-order logic. The first-order logic is nice enough that we don't need to define a new logical system every time, we can just change the non-logical axioms and the rest of the system remains as it was. The syntax and semantics of first-order logic extend naturally to cover any first-order theory. If you want to emphasize the resulting logical system we should write FOL+PA or FOL+ZFC.

Generally don't let these terms confuse you, some people try to generalize these terms so particular systems they study become part of the definition. These generalization can be confusing for people who are not working in logic or related areas. If you ask 10 logicians what is a formal system and what is a logic you may hear 10 different answers.

For a non-logician who is not interested in these generality the things are simple. The main point of logic is language. That is what separates it from the rest of mathematics in a sense. A logician doesn't study mathematical objects on themselves but their relation with the language.

We have a language, we use it to express fact about some mathematical objects. We call the meaningful expressions in the language formulas.

For example we may want to talk about groups, and use the language of groups. We may talk about natural numbers, we can use the language of arithmetic.

Next, we define a relation between a class of structures and formulas $M \vDash \varphi$ which says that the formula $\varphi$ is true in the structure $M$. This is called the satisfiability relation. The relation has to satisfy some basic properties, e.g. it should normally respect the structure of the formula, i.e. if $p$ and $q$ are true $p \land q$ has to be true. This is model theory. See Tarski's definition of truth for more information.

We can use this relation to define a relation between formulas: $T\vDash \varphi$: in any structure $M$ (in the class of structures that we are considering) if the formulas in $T$ are true in $M$, $\varphi$ is also true in $M$.

Now we want to reason about those objects directly without referring to structures. This brings us to proof theory. We have a relation between formulas again: $T \vdash \varphi$ which means that there is a proof of $\varphi$ from assumptions in $T$. This is called the provability relation. We normally want to at least be able to decide if a given sequence of formulas (or more generally a string of symbols) $\pi$ is a proof of $T \vdash \varphi$. You may see people write $\pi : T \vdash \varphi$.

We can now talk about the relation between proof theory and model theory: soundness and completeness. A system is sound and complete if the relations $\vdash$ and $\vDash$ match, i.e. $T\vdash \varphi$ iff $T\vDash \varphi$.

For language of arithmetic and theories in it like PA we normally have an intended structure in mind: the standard model of natural number $\mathbb{N}$. An arithmetic theory like PA is sound and/or complete if the proof theoretic relation $\vdash$ matches the model theoretic relation $\vDash$ for the intended class of structures which in this case is $\mathbb{N}$.

So there are two parts: model theoretic and proof theoretic.

For these theories and their proof theory we can create a matching model theory by using Henkin's construction for example. This is essentially Godel's comepleteness theorem for first-order logic. If you consider all first-order structures that are models of a theory (i.e. all first-order structures that the theory is true in them) we have soundness and completeness. (It is not really interesting, it is just taking the equivalence classes of the free-algebra of the provability relations.)

Similarly starting from a first-order structure like $\mathbb{N}$ we can make a sound and complete first-order theory for it: take all true formulas in $\mathbb{N}$ as your theory. However this is again not interesting.

What we want is a theory that we can work with (e.g. we can algorithmically check if a formula is an axiom in the theory) and have soundness and completeness with respect to the class of structure we were interested in. And this is not always possible, e.g. by Godel's incompleteness theorem there is no such theory for $\mathbb{N}$. Same is true for the "standard" model of set theory, the set theory universe $\mathbb{V}$ (whatever it is).

-
In any event, neither PA nor ZFC can be said to be "sound", right? Soundness is a property of logical systems, and not of formal systems, nor of theories. True? Because neither PA nor ZFC are associated with any particular semantics. –  goblin Feb 7 '13 at 2:42
@user18921, no, they can be considered logical systems. They have semantics. –  Kaveh Feb 7 '13 at 4:07
So theyre sometimes theorys and sometimes logical systems? –  goblin Feb 7 '13 at 4:39
@user18921, yes, the symbols PA and ZFC are used for both theories (i.e. a set of formulas) and also for the theories plus first-order logic. Normally it is clear from context which one is intended and it doesn't cause confusion. Some people write PA+FOL and ZFC+FOL but it is very very uncommon. –  Kaveh Feb 7 '13 at 4:44
Okay just read your addendum, cleared a few things up for me. –  goblin Feb 7 '13 at 4:46

First-order PA and ZFC are first-order theories. That term has a clear technical meaning. Traditional PA with induction over all subsets is a second-order theory.

-

When I talk about a logical system in the way that

A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation

I understand that a logic $\mathcal{L}$ is a pair $(L,\models)$, where $L$ is a function, and the domain of $L$ is the class of all the signatures. But the signature of $ZFC$ has just a member, $\in$. So, there is no sense in talk in the $ZFC$ as a logic.

-