Are formal systems of first order logic incomplete?

[T S Bailey]

Godels Incompleteness Theorem states that for any formal system with finitely recursive axioms we can construct a Godel sentence G that is unprovable within that system but is none the less true. Does this still apply to formal systems which, instead of creating Godel numbers for arithmetical formulas, created them for first order logic operations? Is first order logic inconsistent or incomplete?

 

[andrewkirk]

The key criterion is whether the system contains the basic rules of Robinson Arithmetic, which is Peano Arithmetic without the axiom schema of induction. If it contains those rules, or rules that have equivalent effect, the system cannot be both consistent and complete. There is no need for the rules to say anything about Godel numbers, as they can be constructed out of basic first order logic together with the axioms of Robinson Arithmetic.

Does this still apply to formal systems which, instead of creating Godel numbers for arithmetical formulas, created them for first order logic operations?

Godel numbers are constructed for all logical formulas (wffs), not just arithmetical formulas. Arithmetical formulas are just wffs that contain the extra symbols '0', 'S', '+', '##\times##' and '<'.

Is first order logic inconsistent or incomplete?

First order logic is a Language, not a Theory. Godel's theorem is about a Theory in a Language. It has no application to a Langauge if no Theory is specified.

 

[aikismos]

Um, please help me to understand this better @andrewkirk

You say first order logic is just a language, not a theory, but according to (https://en.wikipedia.org/wiki/First-order_logic):

"First-order logic is a formal system (https://en.wikipedia.org/wiki/Formal_system)"

And according to that article, a formal system has

1. A finite set of symbols (i.e. the alphabet), that can be used for constructing formulas (i.e. finite strings of symbols).
2. A grammar, which tells how well-formed formulas (abbreviated wff) are constructed out of the symbols in the alphabet. It is usually required that there be a decision procedure for deciding whether a formula is well formed or not.
3. A set of axioms or axiom schemata: each axiom must be a wff.
4. A set of inference rules.

Number three says that a set of axioms exists. That would seem to suggest to me what you have called Theory. What am I missing?

 

[andrewkirk]

Number three says that a set of axioms exists. That would seem to suggest to me what you have called Theory. What am I missing?

In logic we make the distinction between 'logical' and 'non-logical' axioms. The former are considered part of the language whereas the latter are part of a Theory.

The logical axioms, together with the rules of inference, determine how one can go about deducing things in any theory in that language.
The non-logical axioms are specific to a theory. For example the set of nonlogical axioms for Euclidean Geometry is different to the set of nonlogical axioms for Robinson Arithmetic. which is different to the set of nonlogical axioms for Zermelo-Frankel Set Theory.

There is no fundamental distinction between the natures of the two types of axioms. It just provides a clearer basis for stating theorems and so on if we make this division between the two types of axioms.

An example may help. Here are some logical axioms, taken from the Hilbert System and Natural Deduction (two different logical languages for 1st order logic)

##x=x##
##(F\to G)\to(\neg F\to\neg G)##
##\neg\neg F\leftrightarrow F##

And here are some non-logical axioms:

##\forall x\neg(Sx=0)## (from Robinson Arithmetic. No natural number satisfies n+1=0)
##\exists E(\forall x\neg(x\in E))## (From Zermelo Frankel Set Theory. There exists an empty set)

 

[aikismos]

So what you're saying is that by drawing a distinction between purely logical versus logicoarithmetical axioms, it's possible to distinguish between the reasoning system (whose arguments are valid or invalid by form) versus the qualitative and quantitative meaning added to the system in establishing not only formal truth but pragmatic truth established by the utility and accuracy of premises and conclusions? Would that be a fair characterization? So in a way, a mathematical formal system exists as a distinct entity from the logical formal system which undergirds it?

 

[andrewkirk]

Broadly, yes, but I'd be reluctant to use the word 'meaning' in there because there's a whole extra topic area in logic of Semantics, which is about the relationships between Theories (which are regarded as just collections of strings of symbols) and Models - which are supposed to be the 'actual mathematical entities about which the strings of symbols in a Theory are interpreted as being propositions. The relationships are called Interpretations.

So in logic, when people want to talk about meaning, they usually use the terminology of Semantics. The wiki article on it is not bad. The Stanford article goes into more depth and history.

So in a way, a mathematical formal system exists as a distinct entity from the logical formal system which undergirds it?

Yes. The mathematical system, like the collection of numbers or of geometrical objects is generally regarded as a model that is associated with, but not identical to, the formal logical Theory that is used to talk about it.

 

[Hornbein]

In logic we make the distinction between 'logical' and 'non-logical' axioms. The former are considered part of the language whereas the latter are part of a Theory.

The logical axioms, together with the rules of inference, determine how one can go about deducing things in any theory in that language.
The non-logical axioms are specific to a theory. For example the set of nonlogical axioms for Euclidean Geometry is different to the set of nonlogical axioms for Robinson Arithmetic. which is different to the set of nonlogical axioms for Zermelo-Frankel Set Theory.

There is no fundamental distinction between the natures of the two types of axioms. It just provides a clearer basis for stating theorems and so on if we make this division between the two types of axioms.

An example may help. Here are some logical axioms, taken from the Hilbert System and Natural Deduction (two different logical languages for 1st order logic)

##x=x##
##(F\to G)\to(\neg F\to\neg G)##
##\neg\neg F\leftrightarrow F##

And here are some non-logical axioms:

##\forall x\neg(Sx=0)## (from Robinson Arithmetic. No natural number satisfies n+1=0)
##\exists E(\forall x\neg(x\in E))## (From Zermelo Frankel Set Theory. There exists an empty set)

Don't you mean
##(F\to G)\to(\neg G\to\neg F)##
?

 

[aikismos]

Good catch on the contrapositive. :D

 

[andrewkirk]

Don't you mean
##(F\to G)\to(\neg G\to\neg F)##
?

Yes, d'oh!

I'm glad to have gotten one of my mistakes out of the way so early in the day.

 

[Hornbein]

Yes, d'oh!

I'm glad to have gotten one of my mistakes out of the way so early in the day.

I thought maybe it was one of those non-logical axioms.

 

[T S Bailey]

Is there a way to construct a formal system F such that one of the derivable theorems is Godels Incompleteness Theorem? When a human mathematician says that the Godel sentence for a Theory is true that must mean that it is true in some system, even if we call that system a language, ie prepositional logic, first order logic etc. Is there any way that a Turing machine could be programmed with, instead of the theory-dependent non-logical axioms, only logical axioms and derive (algorithmically) the same argument Godel thought up?

 

[andrewkirk]

Is there a way to construct a formal system F such that one of the derivable theorems is Godels Incompleteness Theorem?

Not only is it possible but, IIRC, it has been done, and thereby allowed the Godel theorem to be proven by a computerised theorem-proving algorithm.

The logical system in which the theorem is written and proven must be strictly larger than the systems to which the theorem applies. Hence the theorem does not apply to the system in which the theorem is written. To prove the theorem for that larger system, we need to create an even larger system, and so on ad infinitum.

The inability of the larger system to prove the Godel Theorem about itself is what saves the whole thing from collapsing in paradox.

 

[T S Bailey]

Not only is it possible but, IIRC, it has been done, and thereby allowed the Godel theorem to be proven by a computerised theorem-proving algorithm.

The logical system in which the theorem is written and proven must be strictly larger than the systems to which the theorem applies. Hence the theorem does not apply to the system in which the theorem is written. To prove the theorem for that larger system, we need to create an even larger system, and so on ad infinitum.

The inability of the larger system to prove the Godel Theorem about itself is what saves the whole thing from collapsing in paradox.

That is extremely interesting, but at the same time confusing. It seems as though humans are theorem-proving algorithms, or at least we employ them on some level. It also seems as though our understanding of Godels theorem extends to ANY theorem we choose, so that we can somehow know that our own Godel sentences are true. Are there possibly larger logical systems than us for which we cannot derive Godels theorem? I apologize if I'm rambling.

 

[andrewkirk]

Are there possibly larger logical systems than us for which we cannot derive Godels theorem?

Possibly. Godel's Theorem applies only to logical languages that are 'countable' and 'reasonable', where the latter has a specific technical meaning. So it is conceivable that there are uncountable languages (languages with an uncountable number of symbols) and if so it would not apply to them. Personally, I find it difficult to imagine an uncountable language, but that doesn't make them impossible.

If we restrict ourselves to countable, reasonable languages then the only languages for which we could not prove the theorem would be those that are in some loose sense too 'large' for any human or computer to deal with them. In practice we can prove it for any language we wish to use. If we want to then prove it for the language we used to prove that, we only need a slightly larger language. But if we iterate that a billion billion times, processing power for the formal theorem-proving might become an issue.

It's a while since I worked on Godel but my vague memory is that one of the issues preventing self-referentiality is that for the theorem - which on its own is just a bunch of symbols that obey certain rules - to mean anything it must have a semantic interpretation, which is a mapping from the symbols used in the theorem to the things they are talking about. In this case the things they are talking about are symbols in a logical language. If that's a logical language that is a proper subset of the language used to prove the theorem, there's no problem. Every symbol of the object language is the interpretation of a constant symbol in the proof language that maps to it. Then there are additional symbols in the proof language (like ##\forall, \exists, \to, x, y##) that are used to prove things about those constants. That means that there will be two versions of some symbols. For instance, presuming the object language to contain the logical symbol ##\to##, the proof language must contain a constant symbol, say ##\to^\dagger## that refers to that symbol as an object in the object language, as well as a symbol ##\to## that has the usual meaning in the proof language.

It follows from this that the proof cannot refer to the language in which it is written, as its alphabet must be strictly larger than the alphabet of the language to which it refers.

 

[Demystifier]

Is first order logic inconsistent or incomplete?

First order logic is both consistent and complete. Indeed, before proving his famous incompleteness theorems, Godel also proved a slightly less famous completeness theorem of first order logic.