I A confusion about axioms and models

[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?