The logically implies concept in first-order logic

[Fredrik]

The "logically implies" concept in first-order logic

I've been reading about first-order logic (in Enderton, and in Rautenberg) and I've gotten to the point where (I think) I understand what it means for a set of formulas to "logically imply" another formula. I'm a bit confused by one thing though...the absence of words like "axiom" and "theorem". Isn't this stuff supposed to be the definition of what a theorem is?

Also, I'd like some clarification on the terms "model theory" and "proof theory". This "logically implies" stuff is presented shortly after the concept of a "model", and uses it in the definition. And I feel that this has to be the stuff that defines what's considered a proof. So this stuff I'm reading...should I think of this as the intersection of model theory and proof theory, or do those terms mean something I still don't get?

 

[Hurkyl]

There are a lot of kinds of implication. For example,

There is the logical connective (P implies Q), which is the same thing as "not P or Q".
There is syntactic entailment -- that a given proposition can be proven from a set of premises.
There is semantic entailment -- that any set-theoretic interpretation of the language that satisfying the set of premises also satisfies the proposition.

The cool theorem is that in first-order logic, the difference doesn't really matter. We can prove (P implies Q) if and only if Q can be proven from the premise P. Furthermore, syntactic entailment and semantic entailment turn out to be the same relation.


Axioms are to theories like spanning sets are to vector spaces: a convenient way to present a theory. Axiomness is not a property of the statements themselves, but what is an axiom is a property of the presentation (i.e. the axiomatization) of the theory.

In this setting, I'm used to the word "theorem" simply meaning an element of a theory.

 

[Fredrik]

There is the logical connective (P implies Q), which is the same thing as "not P or Q".
There is syntactic entailment -- that a given proposition can be proven from a set of premises.
There is semantic entailment -- that any set-theoretic interpretation of the language that satisfying the set of premises also satisfies the proposition.

The cool theorem is that in first-order logic, the difference doesn't really matter. We can prove (P implies Q) if and only if Q can be proven from the premise P. Furthermore, syntactic entailment and semantic entailment turn out to be the same relation.

Cool. I didn't know about that theorem.

In this setting, I'm used to the word "theorem" simply meaning an element of a theory.

How do you define "theory"? Is it the set of all formulas that are logically implied by a given set of formulas? This would make sense, because then we can call the members of the given set of formulas "axioms", and the theory is defined by its axioms. If "theory" is defined in some other way, e.g. as the set of formulas of a given language, things get a bit weird.

 

[Hurkyl]

Is it the set of all formulas that are logically implied by a given set of formulas?

Almost -- I would define it as a "deductively closed set of formulas". i.e. if P can be proven from the set of formulas, then P is already in the set.


An axiomatization of a theory is a generating set: a set of formulas whose deductive closure is the theory of interest. i.e. every formula of the theory can be proven from the set of axioms.

Of course, every theory has an axiomatization. For example, the trivial one: take every theorem as an axiom.

 

[Fredrik]

Almost -- I would define it as a "deductively closed set of formulas". i.e. if P can be proven from the set of formulas, then P is already in the set.

But the set of all formulas is a special case of that, so we might as well take that to be the "theory", and then we can change the axioms (of e.g. "group theory") without changing the theory.

 

[Hurkyl]

But the set of all formulas is a special case of that, so we might as well take that to be the "theory"

Yes it is; that is the inconsistent theory. (For a given language, there is only one inconsistent theory)

However, the inconsistent theory is rather uninteresting. A complete theory is somewhat more interesting: for any formula P, either P or (not P) is a theorem.

However, completeness is not always desirable. e.g. One of the reasons Group Theory is useful is precisely because it not complete -- it has interpretations in a wide variety of distinct mathematical contexts.

we can change the axioms (of e.g. "group theory") without changing the theory.

Yep! I'm not sure if the standard choice of axioms has any merit beyond pedagogy and tradition. I know that there is some interest in alternative axiomatizations for group theory -- e.g. http://www.mcs.anl.gov/uploads/cels/papers/P901.pdf -- I don't know the application, though.

 

[Fredrik]

Yes it is; that is the inconsistent theory. (For a given language, there is only one inconsistent theory)

OK, that makes sense.

Hm...your choice of words (here and in your previous post) suggests that each set of formulas with the property you mentioned is a "theory". What does this mean specifically for "group theory"? What does that term refer to? Is each of those theories a group theory, or is "group theory" the set of all such theories?

 

[Hurkyl]

Ah, a gotcha in natural language.

"Group theory" is the branch of mathematics that studies the properties of groups, relationships between different groups, operations one can perform with groups, et cetera.

Then, there is theory in the language generated by the symbols $(1, \{\}^{-1}, \cdot)$ (of arity 0,1,2 respectively) that is generated by the group axioms. When it was worth giving it a specific name, I've seen this called "the theory of a group". It consists of those propositions that are true for all groups, and no others.

 

[Hurkyl]

Incidentally, if you use typed logic, you get other interesting things like "the theory of two groups and a homomorphism between them" whose language consists of two types G and H, two of each of $(1, \{\}^{-1}, \cdot)$ with the obvious domains and codomains, and one symbol f of type G --> H. The theorems of this theory are generated by the group axioms applied to G and H, and the group homomorphism axioms applied to f.

 

[yossell]

Also, I'd like some clarification on the terms "model theory" and "proof theory". This "logically implies" stuff is presented shortly after the concept of a "model", and uses it in the definition. And I feel that this has to be the stuff that defines what's considered a proof. So this stuff I'm reading...should I think of this as the intersection of model theory and proof theory, or do those terms mean something I still don't get?

I may have misread the puzzlement here but:

logical implication *can* be defined without using the notion of a proof, and it looks as though that's what they're doing in the book you mention.
It's defined instead in terms of models: T |= s iff, in every model where T is true, s is true. Of course, `s is true in Model M' also has to be defined for the sentences of the formal Langauge under investigation and its Models - but this can be done purely formally.

Proof theory presents a notion of implication by giving a set of rules that allow you to move from one sentence to another, the sequence of sentences forming a proof. Normally these rules are given in a very explicit way: E.g. if in the sequence, you have written P & Q then you are allowed to write P as the next bit of the sequence; if in the sequence P appears and P -> Q appears, then you are allowed to write Q as the next bit of the sequence; you can write P -> (Q -> P) at any point (i.e. this formula is an axiom). No mention of truth is made at all. Rather, a notion of a permissible sequence of formula is defined. So, the definitions are independent of each other.

Extensionally, though, the two definitions may be equivalent.

There are many different definitions of the proof theoretic notion of implication - it's easy to make up different rules and different axioms and play different games. Many logic books introduce different proof systems. But they're usually all extensionally equivalent: they don't differ about which sequences are permissible.

However, there are non-classical logics where the rules or axioms are weakened. E.g. in Intuitionistic logic, P v ¬P is NOT a theorem.

In the first order case, as Hurkyl said, it is possible to define a proof system which has the following features: if T logically implies s (logical implication in the *model theoretically* defined sense), then we can construct a proof of s from T. This is completeness. Also: if we can construct a proof of s from T, then T logically implies s (logical implication again in the model theoretic sense).

In higher order case, any proof theoretically definable notion of implication turns out to be inadequate - each system we give, if it's consistent (as it should be) then there are implications of the theory it misses out.

 

[Fredrik]

logical implication *can* be defined without using the notion of a proof, and it looks as though that's what they're doing in the book you mention.
It's defined instead in terms of models: T |= s iff, in every model where T is true, s is true. Of course, `s is true in Model M' also has to be defined for the sentences of the formal Langauge under investigation and its Models - but this can be done purely formally.

Proof theory presents a notion of implication by giving a set of rules that allow you to move from one sentence to another, the sequence of sentences forming a proof. Normally these rules are given in a very explicit way: E.g. if in the sequence, you have written P & Q then you are allowed to write P as the next bit of the sequence; if in the sequence P appears and P -> Q appears, then you are allowed to write Q as the next bit of the sequence; you can write P -> (Q -> P) at any point (i.e. this formula is an axiom). No mention of truth is made at all. Rather, a notion of a permissible sequence of formula is defined. So, the definitions are independent of each other.

That's the sort of answer I was looking for. What you're saying about "rules that allow you to move from one sentence to another" is what I expected from mathematical logic, but when I came across this notion of "logically implies", I started to think that maybe that's what a proof is. So you did clear things up for me. I appreciate that.

In the first order case, as Hurkyl said, it is possible to define a proof system which has the following features: if T logically implies s (logical implication in the *model theoretically* defined sense), then we can construct a proof of s from T. This is completeness. Also: if we can construct a proof of s from T, then T logically implies s (logical implication again in the model theoretic sense).

In higher order case, any proof theoretically definable notion of implication turns out to be inadequate - each system we give, if it's consistent (as it should be) then there are implications of the theory it misses out.

This is great stuff too. I didn't know that you need to consider higher orders for this to be an issue.

 

[JSuarez]

This is great stuff too. I didn't know that you need to consider higher orders for this to be an issue.

If I didn't misread "higher-order" (I take it to mean second, or higher, order logic), you don't. Almost any extension of first-order logic that is sufficiently expressive to be able to model even weak systems of arithmetic is incomplete in this sense; there are true sentences (or logical implications) that are unprovable in the system. That's one of the reasons why some authors introduce the semantic side (logical implication, or consequence), before provability; the latter is, in general, weaker.

 

[Landau]

Somewhat off-topic:

logical implication *can* be defined without using the notion of a proof (...)
It's defined instead in terms of models: T |= s iff, in every model where T is true, s is true.

Yeah, this is what I learned in model theory. What troubled me, is that a lot of this stuff seemed circular reasoning to me: all these kind of definitions use the English words "if" and "then" themselves. In fact, it is done twice here: in the definition of definition (we define 'blah' by saying " 'blah' iff 'other blah'", but iff already is an implication), and implicitly in the part "in every model where T is true, s is true", which actually says "for every model: if T is true in it, then s is true in it".

I asked my teacher about it, and got some answer about the difference between semantics and syntax, but didn't really appreciate it then.

 

[JSuarez]

What troubled me, is that a lot of this stuff seemed circular reasoning to me: all these kind of definitions use the English words "if" and "then" themselves.

This is the metalanguage/object language distinction; it means that, when you say something like:

"for every model: if T is true in it, then s is true in it".

The "if" and "then" are in the metalanguage, the language you use to state properties of the objects you are studying; the implications and other logical connectives are in the object language, the language we use to represent them.

By the way, it doesn't have to do with the distinction between syntax and semantics: this is a different problem altogether.