I A confusion about axioms and models

[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

 

[microsansfil]

looks like a true syntactic statement to me. Am I missing something?

How do you establish the proposal truth table (in the language of arithmetic) ?

\forall x \forall y \forall z \forall n (n \, &gt; \, 2 \,\Rightarrow \, (x^n \, +\, y^n \, \neq \, z^n))

(This is the great Fermat theorem, proved by A. Wiles, a few years ago.)

Patrick

 

[WWGD]

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.

.

I think you're right, I don't know where I got this name from. My bad.

 

[atyy]

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

Would you accept rephrasing this question as: Can a version of the Löwenheim-Skolem Theorem be formally proved within ZFC (in which case a machine should be able to prove the LST which is about the relationship between syntax and semantics)?

Kunen http://logic.wikischolars.columbia.edu/file/view/Kunen,+K.+(1980).+Set+Theory.pdf p143 Appendix 3 talks about formalizing model theory in ZF.

With a little googling, I found https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf which seems to describe a mechanized proof of Goedel's incompleteness theorem, including the semantic version (ie. in which the Goedel statement is true). The underlying programme seems to be something called Isabelle https://isabelle.in.tum.de/overview.html, which seems to be an implementation of higher-order logic.

With even more googling I found http://www.concrete-semantics.org.

 

[Demystifier]

Another non-technical and very illuminating text on related issues
http://lesswrong.com/lw/93q/completeness_incompleteness_and_what_it_all_means/

 

[A. Neumaier]

Thank you all, but my questions are still not answered explicitly and I am still confused. So let me rephrase my questions.
- The additional statements which define a model uniquely, are they axioms or not?

Note that the notion of axioms is relative to a concept. There are axioms for set theory, for projective geometry, for group theory, for natural numbers, etc., and all of them are different and mean different things.

In modern mathematics, the statements one assumes as the basis of a mathematical theory are called the axioms for that theory. Everyone making a new theory or a variation of an old one can choose the axioms. Even for the same disciplines. Thus an axiom is something very relative - except among those who agreed on a particular axiom system for their discipline.

Different books on group theory start with different but equivalent axiom systems. This means that each axiom in one of the books but not the other is derivable as a theorem in the latter, and conversely. If you add to the axiom for groups the additional axiom of commutativity, the resulting axiom system defines a different concept than a group, namely that of an abelian group. This is typical for the Bourbaki approach to mathematics.

Different books on set theory start with axioms that are not necessarily equivalent. This indicates that there are several flavors of such a theory with a slightly different meaning, all covering in their intersection a lot of common ground. For example, you can do set theory in ZF (Zermelo-Frankel), ZFC (ZF with the axiom of choice), or ZFGC (ZF+global choice, Bourbaki's starting point). The three theories are not equivalent, but every axiom in ZF is also an axiom of ZFC, which has as additional axiom the ''axiom of choice'', which is not an axiom of ZF. ZFGC has a stronger form of this axiom, the existence of a choice operator that selects a distinguished choice from each nonempty set. These axiom systems define different (inequivalent) set theories. (For simplicity I only discuss these thee; there are also axioms for set theory that differ essentially from ZF!)

As a consequence, every theorem of ZF is a theorem of ZFC and of ZFGC, and every theorem of ZFC is one of ZFGC - with proper inclusion in each case. Correspondingly, every model of ZFGC is a model of ZFC and of ZF, and every model of ZFC is a model of ZF; again with proper inclusions.

Models are never unique; they can be unique only up to isomorphism (relabeling of the objects in it). Even that is possible only in second-order logic, and then only for special concepts such as the natural number or the real numbers. Or for extremely specific objects such as the cyclic group of order 5 or the monster. But in the latter cases one talks of characterizing properties rather than axioms...

 

[Demystifier]

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 .

Consider the following string:
"Logic is tricky."
This string has some meaning to me, and probably to you to. But does it have the same meaning to me as it does to you? Probably not exactly the same. And to someone who does not speak english, it dos not have any meaning at all. Does it mean that meaning only exists in the human mind?