A confusion about axioms and models

[fresh_42]

But from a standard point of view, it seems rather absolute that group SO(2) is commutative and that SO(3) is not. So what exactly is the difference between the standard and this awkward point of view?

The part of the comparison to group theory was the one I had difficulties with, too.
Then rereading it, I interpreted it this way: the starting point was group theory alone, not group theory within ZFC.
Otherwise I had the same question.

 

[micromass]

But from a standard point of view, it seems rather absolute that group SO(2) is commutative and that SO(3) is not. So what exactly is the difference between the standard and this awkward point of view?

That`s the difference between set theory and group theory. In group theory, you can exhibit a very specific model. Then you can prove everything you want about that model. In set theory however, we can never describe a model at all. We can only go by the axioms.
Try to do group theory like this: you know you`re working in some group, meaning that the usual axioms are satisfied. But outside of this, you have no clue about the specifics of the group. You cannot construct groups other than the one you have now. That is the point of view with which we do set theory.

 

[micromass]

The part of the comparison to group theory was the one I had difficulties with, too.
Then rereading it, I interpreted it this way: the starting point was group theory alone, not group theory within ZFC.
Otherwise I had the same question.

I understand it`s difficult. But the analogy between set theory and group theory is a really really good one. It helped me significantly.
Your interpretation is correct by the way. You start only from one single group, for which you know the axioms are valid, and nothing else.

 

[Demystifier]

In set theory however, we can never describe a model at all.

Then why don't they tell us that in the textbooks?

But here is a more interesting question. What if I remove the axiom which claims existence of an infinite set? Would it be possible to explicitly describe a model for such a reduced ZFC?
Or even more interestingly, is it possible to remove some other axiom (while retaining infinite-set axiom), such that again a model can be described explicitly?

 

[micromass]

Then why don't they tell us that in the textbooks?

But here is a more interesting question. What if I remove the axiom which claims existence of an infinite set? Would it be possible to explicitly describe a model for such a reduced ZFC?

Depends on what you mean with describe, but I`d say yes. You can explicitely describe all the sets in such a universe.

Or even more interestingly, is it possible to remove some other axiom (while retaining infinite-set axiom), such that again a model can be described explicitly?

That seems much less likely.

 

[fresh_42]

Wiki states that Goedel's completeness theorem says: each syntactically consistent theory (set of closed formulas without contradiction) has a model. Shouldn't this apply to any reduced ZFC system as long as consistency can be proved?

 

[micromass]

Wiki states that Goedel's completeness theorem says: each syntactically consistent theory (set of closed formulas without contradiction) has a model. Shouldn't this apply to any reduced ZFC system as long as consistency can be proved?

But consistency can`t be proved. Otherwise, yes.

 

[Demystifier]

But consistency can`t be proved.

I know that one can't prove consistency of ZFC or consistency of Peano axioms. But consistency of a weaker system, such as Presburger arithmetic, can be proved
https://en.wikipedia.org/wiki/Presburger_arithmetic#Properties
I think this is what fresh_42 had in mind.

 

[fresh_42]

I thought it answers your question, at least to some extend as it supplies a sufficient condition.

Or even more interestingly, is it possible to remove some other axiom (while retaining infinite-set axiom), such that again a model can be described explicitly?

(To be honest: I haven't thought about whether every reduction of ZFC cannot be proven consistent.)

 

[atyy]

http://www.columbia.edu/~hg17/nonstandard-02-16-04-cls.pdf
[PLAIN]http://lesswrong.com/lw/g0i/standard_and_nonstandard_numbers/[/PLAIN]
http://lesswrong.com/lw/g0i/standard_and_nonstandard_numbers/

 

[atyy]

@micromass, if higher-order theory is necessary for unique definition of mathematical models, then why most textbooks on logic say almost nothing about higher-order logic and claim that first-order logic is sufficient for most of mathematics?

First order logic has the Goedel "Completeness" Theorem, which second order logic does not. The notion of "Completeness" in the "Completeness Theorem" is not the same as that in the "Incompleteness Theorem". Mathematicians have much worse terminology than physicists :P

https://en.wikipedia.org/wiki/Gödel's_completeness_theorem

 

[Samy_A]

Mathematicians have much worse terminology than physicists :P

Now that I have seen how mathematicians use the term "axiom", I have (with great sadness) to somewhat agree.

 

[atyy]

Now that I have seen how mathematicians use the term "axiom", I have (with great sadness) to somewhat agree.

They justify it with computer science https://en.wikipedia.org/wiki/Operator_overloading

 

[stevendaryl]

Suppose that I have a set of axioms in first-order logic. And suppose that I have several inequivalent models for this set of axioms. And suppose that I want to choose one specific model. To choose it, I need to make some additional claims which specify my model uniquely.

My question is the following: What kind of claims these additional claims are? Are they some additional axioms? Or are they claims which are not classified as axioms? If they are not classified as axioms, what property do they have/lack so that they cannot be classified as axioms?

If the question looks too abstract, let me consider an example. Suppose that I start from axioms of group theory. There are many different groups satisfying these axioms. So I choose some specific group, say SO(3), defined by some claims which define that group. Are these claims also axioms? If not, then what property do they have/lack so that they cannot be called axioms?

Could it be that my confusion stems from the fact that the word "axiom" in logic has more narrow meaning than the word "axiom" in the rest of mathematics?

I spent a fair amount of time pretending to do mathematical logic, and I think I can answer this question.

The difference between a theory and a model is that a theory is a collection of mathematical statements, while a model is a mathematical object. Of course, to reason about a mathematical object, you need a characterization of that object, and that requires statements, too. But usually, what in mathematical logic is considered a "model" is some specification of a mathematical structure in a way that is believed to uniquely characterize that structure (or sometimes, up to isomorphism).

Coming up with a model is often along the lines of a construction--a concrete recipe for building that object. Of course, the recipe often involves steps that cannot be carried out by a human being, but would require some kind of godlike being that can do infinitely many things in a finite amount of time.

Maybe it's best to see an example:

To axiomatize the natural numbers, you might give the following (Peano axioms): (I'll use x' to mean the next number after x)

1. x+0 = x
2. x+y' = (x+y)'
3. x*0 = 0
4. x*y' = (x*y) + x
5. 0 $\neq$ x'
6. x' = y' $\Rightarrow$ x=y

There's actually an induction schema, too, but I'll skip that for now.

I think it's obvious that the interpretation of the domain as the natural numbers $0, 1, 2, ...$, and the interpretation of x' as x+1, and the interpretation of "+" as ordinary addition, and "*" as ordinary multiplication works. But the question is, do those axioms uniquely specify a mathematical structure? The answer is no. To see this, you can see that the axioms don't rule out "hyperfinite" objects that are infinitely far removed from 0. More concretely, let's add a new constant symbol, $\infty$, and add the (infinitely many) axioms:

$\infty \neq 0$
$\infty \neq 0'$
$\infty \neq 0''$
$\infty \neq 0'''$
etc.

(Having an infinite number of axioms might seem like cheating, but when they follow a simple pattern, as they usually do with axiom schema's, an infinite number of axioms is no harder to use in theorem-proving from than a finite number)

It's clear that this new theory is not about the (finite) natural numbers, since it has an object, $\infty$, that is not anyone of the natural numbers. But the original set of axioms didn't rule out the possibility of such an object, so the original axioms didn't uniquely characterize the natural numbers, either.

It turns out that you can't possibly uniquely characterize the natural numbers using only first-order language. That is, using only statements involving +, *, 0, x', etc., you can't axiomatize the truths about the natural numbers.

But we can (allowing godlike operations) construct a model of the natural numbers. Roughly speaking:

Let $A$ be any set, and let $f: A \rightarrow A$ be any unary function on $A$ that is one-to-one, but not onto. Let $Z$ be any element of $A$ that is not in the image of $f$. If $A'$ is a subset of $A$, call it "closed" if $Z$ is in $A'$ and whenever $x$ is in $A'$, so is $f(x)$. Finally, we define $N =$ the set of all $x$ that are in every closed subset of $A$.

Then $N$ is a model of the natural numbers. It was definitely not obtained by adding more axioms to the Peano axioms. The language used to "construct" N doesn't even mention the original axioms.

A model is definitely not a collection of axioms. It's a mathematical object.

 

[microsansfil]

The difference between a theory and a model is that a theory is a collection of mathematical statements, while a model is a mathematical object.

IMHO, we can also claim : A theory is a set of mathematical formula provable from a set of chosen axioms and the logic used (here first-order logic). Thus It is also a mathematical object. A mathematical syntactic object. A model is use to give a semantic (e.g. an interpretation ) to the theory. The model theory is the semantic of the formal discourse.

For example from the group axioms (syntax) https://proofwiki.org/wiki/Definition:Group_Axioms we can built models (semantic) that we call group which is a "concrete realization" of the axioms. There are many different groups satisfying the group axioms, and they come in all shapes and sizes.

The Gödel's[/PLAIN] completeness theorem give a relationship between theory and model.

Patrick
https://en.wikipedia.org/wiki/First-order_logic

 

[WWGD]

A model is definitely not a collection of axioms. It's a mathematical object.

A model is a semantic object, a theory is syntactic. A model for a theory maps the theory into a world where each of the sentences of the theory are
satisfied according to Tarski's satisfiability criterion.

 

[zhangvict]

I am not sure if the OP's specific question is resolved, but I think I can answer it.

The OP is asking given a theory T, with a collection of nonisomorphic models, how to specify a subset of the models. I am unsure how much model theory does the OP know, and whether they have in mind are additional assumptions I missed. What I know below is from undergraduate model theory, so there may be more to it.

The first thing to check is whether T is complete. A complete theory is one which derives every sentence or it's negation. If T is not a complete theory, then there is some sentence σ of first order logic that is independent of T, which is to say that both T∪{σ} and T∪{~σ} are consistent, and by completeness have models. Then simply adding σ to you set of axioms will remove all models of T∪{~σ}, and you have specified a subset of the models of T.

An example of this is when T is the group axioms and σ is the sentence asserting commutative. This parses down from all groups to abelian groups

It is however, possible for T to be complete, yet have nonisomorphic models. In fact, it is a theorem of model theory that if T has an infnite model, it has models of arbitrarily large infinite cardinalities. An easy way to specify a subset of models would be to specify a cardinality, since models of different sizes can never be isomorphic. This specification will not be first order in general unless you specify a finite cardinality. In the previous example this may mean requiring your groups to have 3 elements, which would give you the cyclic group of order 3, or countable etc.

An example of a complete theory with nonisomorphic models is the theory of dense linear orders without endpoints. It has only one model in countable infinity, i.e. ℚ, and it is a theorem that if a theory has only one isomorphism class in some uncountable cardnality, then it must be complete. Several nonisomorphic dense linear orders without endpoints in cardinality continuum include ℝ and (a copy of ℝ followed by a copy of ℚ)

As an aside, In model theory, theories with only one model in cardinality λ are called λ-categorical. Categoricity is an important concept in model theory, as with completeness. There are other important concepts the OP may be interested in, including "stability" which roughly means that there are not too many elements that could exist but don't. An example of an unstability is in dense linear orders, because in the model ℚ there are only countable many elements, but you can describe uncountably many real numbers by dedekind cuts using only the language of order and parameters from ℚ.

Going back to the OP's question again, in general whatever mathematical property you want to add to a theory T to restrict the models, it will likely be first order, but in the language of sets rather than your original language. For example the property of being noetherian in a ring is not first order in the language of algebra, but you can formula it in terms of sets.

EDIT: Thinking of the OP's example of SO(3), you can never find first order axioms such that the only model is SO(3), because SO(3) is an infinite model, and you can build models of arbitrarily large cardinalities that satisfy the same first order sentences (and your axioms) as SO(3) by ultrapowers, or the compactness theorem etc.

I spent a fair amount of time pretending to do mathematical logic, and I think I can answer this question.
A model is definitely not a collection of axioms. It's a mathematical object.

BTW this is true, but the completeness theorem constructs models by taking equivalence classes of strings of symbols. When I think about the completeness theorem, models in some sense literally become quotients of infinite lists of sentences, and this gives me weird philosophical thoughts about the nature of language, reality, etc.

 

[Demystifier]

an infinite number of axioms is no harder to use in theorem-proving from than a finite number

Perhaps it's not harder for a human, but what if we want a machine to prove the theorems?

 

[Demystifier]

A model is a semantic object, a theory is syntactic.

Both semantic and syntax are expressed as a collection of claims. Can a machine distinguish between semantics and syntax?

 

[stevendaryl]

Perhaps it's not harder for a human, but what if we want a machine to prove the theorems?

Well, theorem-proving is a tremendously complicated thing that potentially would require artificial intelligence to do a really good job. But proof-checking is pretty straight-forward: A proof is a sequence of claims, and each claim must either be an axiom, or must follow from previous claims by the rules of inference. Such a sequence is a proof of the last claim. So as long as there is an algorithm to determine whether a claim is an axiom, then you can do proof checking.

If you don't care about efficiency, and have trillions of years to wait, then a proof checker can be turned into a theorem prover, by just generating all possible sequences of claims and checking each sequence to see if it's a proof, and if so, then you've got a proof of the last claim.

 

[Demystifier]

@stevendaryl I was asking about theorems (to be proved by a machine) which follow from an infinite number of axioms. And I am not interested in efficiency, only if it is possible in principle.

I think that machine can make such theorems only if they are reformulated as a finite number of axioms, which may require second-order logic.

 

[stevendaryl]

@stevendaryl I was asking about theorems (to be proved by a machine) which follow from an infinite number of axioms. And I am not interested in efficiency, only if it is possible in principle.

I think that machine can make such theorems only if they are reformulated as a finite number of axioms, which may require second-order logic.

As I said, the only requirement is that an axiom be recognizable as an axiom. That is, there has to be an algorithm that, given an arbitrary statement in the language, will eventually halt in an accepting state if that statement is an axiom. (It's actually not required that it be able to reject a claim as definitely not an axiom).

I suppose in some sense, it might be true that every theory with an infinite number of axioms can be recast as a theory with a finite number of axioms, if you allow higher-order constructs, but there is no need to do that.

 

[stevendaryl]

As I said, the only requirement is that an axiom be recognizable as an axiom. That is, there has to be an algorithm that, given an arbitrary statement in the language, will eventually halt in an accepting state if that statement is an axiom. (It's actually not required that it be able to reject a claim as definitely not an axiom).

I suppose in some sense, it might be true that every theory with an infinite number of axioms can be recast as a theory with a finite number of axioms, if you allow higher-order constructs, but there is no need to do that.

I should point out that proofs are finite objects, so even if there are infinitely many axioms, any given proof only uses finitely many axioms.

 

[stevendaryl]

Both semantic and syntax are expressed as a collection of claims. Can a machine distinguish between semantics and syntax?

No, it's all syntax. Perhaps this is a way to explain it that might make sense.

I believe that there is a sense in which model theory is equivalent to a relative interpretation. Relative interpretation is maybe easier to explain than model theory.

So you start with some theory that you think you understand--say arithmetic, or set theory. This theory has certain function symbols, relation symbols, and constants. It has certain axioms. Actually, it's simpler to just have relation symbols.

Now, you have a second theory in a different language. It has different relation symbols and different axioms.

So to interpret the second theory in the first is pretty straightforward:

• For every n-ary relation symbol $R$ in the new theory, you come up with a formula with free variables $\Phi(x_1, x_2, ..., x_n)$ in the old theory.
• You come up with a unary formula $U(x)$ in the old theory (the interpretation being that x is an element of the "universe" of the new theory)
• Given those two choices, you can map every statement of the new theory to a statement of the old theory. Just replace the relation symbols by the appropriate formulas, and replace quantifies by relativized quantifiers: $\forall x \psi(x) \Rightarrow \forall x (U(x) \rightarrow {\tilde{\psi}(x))}$ and $\exists x \psi(x) \Rightarrow \exists x (U(x) \& \tilde{\psi}(x))$

Then you prove the translation of each axiom of the new theory, using the axioms of the old theory. If you can do that, then you've interpreted the new theory in the old theory.

Typically, the base theory that you start with is either set theory, or something less powerful like arithmetic or second-order arithmetic.

 

[WWGD]

Both semantic and syntax are expressed as a collection of claims. Can a machine distinguish between semantics and syntax?

I don't know if this helps, but semantic statements can be assigned truth values, syntactic ones cannot.

 

[Demystifier]

I don't know if this helps, but semantic statements can be assigned truth values, syntactic ones cannot.

I'm not sure about that. For example
$$x\wedge y\rightarrow x$$
looks like a true syntactic statement to me. Am I missing something?

 

[WWGD]

I'm not sure about that. For example
$$x\wedge y\rightarrow x$$
looks like a true syntactic statement to me. Am I missing something?

But this is a string without meaning until you assign a specific one to it. I think you are assuming the standard meaning of "x and y implies x" , but there are many other possible meanings/models to be assigned to the string .

 

[stevendaryl]

But this is a string without meaning until you assign a specific one to it. I think you are assuming the standard meaning of "x and y implies x" , but there are many other possible meanings/models to be assigned to the string .

Yes, but usually when people are doing model theory, certain things are kept fixed (not necessarily, but usually). It's usually assumed that logical operators mean the usual thing, and that equality means the usual thing. The only parts of the theory that are unspecified are the interpretations of constant symbols, relation symbols and function symbols.

 

[WWGD]

Yes, but usually when people are doing model theory, certain things are kept fixed (not necessarily, but usually). It's usually assumed that logical operators mean the usual thing, and that equality means the usual thing. The only parts of the theory that are unspecified are the interpretations of constant symbols, relation symbols and function symbols.

You're right, but then this is a consensual meaning, where the semantics are assumed, but it has no intrinsic meaning and the statement cannot be said to be intrinsically true or false without the assumed meaning.

 

[john baez]

My question is the following: What kind of claims these additional claims are? Are they some additional axioms? Or are they claims which are not classified as axioms? If they are not classified as axioms, what property do they have/lack so that they cannot be classified as axioms?

You can narrow down the collection of models of a theory in first-order logic by adding extra axioms to that theory. In some cases you may need to add infinitely many axioms to get a unique model. For example, if you start with Peano arithmetic or Zermelo-Frenkel set theory, there is no way to add finitely many axioms and get a theory with exactly one model. You can however do it with infinitely many.

Could it be that my confusion stems from the fact that the word "axiom" in logic has more narrow meaning than the word "axiom" in the rest of mathematics?

Even in logic, an "axiom" is just a statement in a collection of statements. You prove theorems starting from this collection of statements.

 

[WWGD]

You can narrow down the collection of models of a theory in first-order logic by adding extra axioms to that theory. In some cases you may need to add infinitely many axioms to get a unique model. For example, if you start with Peano arithmetic or Zermelo-Frenkel set theory, there is no way to add finitely many axioms and get a theory with exactly one model. You can however do it with infinitely many.
Even in logic, an "axiom" is just a statement in a collection of statements. You prove theorems starting from this collection of statements.

But don't you also have non-logical axioms that tell you how you can put theorems together (Together with MP)?

 

[john baez]

But don't you also have non-logical axioms that tell you how you can put theorems together (Together with MP)?

I don't know what MP is, and I don't know what you mean by "put theorems together". All I know is that what I'm saying is true, if we're talking about any the most common approaches to first-order-logic. In these approaches you have a fixed set of "deduction rules" for proving new statements from old one. Then, a "theory" consists of an arbitrarily chosen set of statements called "axioms"; from these you can use the deduction rules to get other statements, called "theorems".

 

[WWGD]

I don't know what MP is, and I don't know what you mean by "put theorems together". All I know is that what I'm saying is true, if we're talking about any the most common approaches to first-order-logic. In these approaches you have a fixed set of "deduction rules" for proving new statements from old one. Then, a "theory" consists of an arbitrarily chosen set of statements called "axioms"; from these you can use the deduction rules to get other statements, called "theorems".

Sorry, MP is Modus Ponens: P and $P \rightarrow Q$ imply Q. I think the deduction rules are the non-logical axioms.

 

[john baez]

Sorry, MP is Modus Ponens: P and $P \rightarrow Q$ imply Q.

Okay. Modus ponens is one of the most famous of deduction rules, and in one popular approach to first-order logic it's the only one: you don't really need any more. There's another approach, going back to Gentzen, that takes lots of lots of the axioms about logic and replace them with lots of deduction rules.

I think the deduction rules are the non-logical axioms.

That doesn't sound right to me: axioms are the statements we start with in a given theory, while deduction rules are ways to get new statements from old ones.

People usually say that axioms like $not(not(P)) \rightarrow P$ are logical axioms (since they help us understand the logical connectives like "not"), while axioms like the axioms for a group are non-logical axioms.

 

[microsansfil]

Can a machine distinguish between semantics and syntax?

What do you mean by "machine" ? With a computer we can execute algorithm to do parsing or syntactic analysis, but also
to do semantic analysis (compilers).

Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs

an example to show the difference

Syntax
F = ∀x ∀y (p(x,y) → ∃ z ( p(x,z) ∧ p(z,y) ) a closed formula in first order logic that i re-write F :∀x ∀y ( G ) with G is the implication.

Semantic
- Interpretation I1 in the domain D1 which is the set of real number and p is <
if p(x,y) is false, G is true
if p(x,y) is true, then x<y. with z =( x+y)/2. then, p( x,z) is true and p( z,y) also
Thus F is satisfiable and I1 is a model for F.

- Interpretation I2 in the domain D2 which is the set of natural number
If p(x,y) is false, G is true
if p(x,y) is true, then x<y. It doesn't exit natural number between x et y thenceforth x et y are consecutive. G can be false.
Thus F is not valid

The formula F is undecidable in the theory of total order, while it is a theorem in the dense order.

Outside the mathematics (when used in physics for example) you only see syntax but inside the mathematics the difference makes sense, that is why there is a model theory which is different from the proof theory

Patrick