- #1

- 26

- 0

- Thread starter T S Bailey
- Start date

- #1

- 26

- 0

- #2

- 3,861

- 1,440

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.

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

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 '<'.Does this still apply to formal systems which, instead of creating Godel numbers for arithmetical formulas, created them for first order logic operations?

First order logic is aIs first order logic inconsistent or incomplete?

Last edited:

- #3

- 145

- 34

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

And according to that article, a formal system has

- A finite set of symbols (i.e. the alphabet), that can be used for constructing formulas (i.e. finite strings of symbols).
- 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. - A set of axioms or axiom schemata: each axiom must be a wff.
- 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?

- #4

- 3,861

- 1,440

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

The logical axioms, together with the rules of inference, determine how one can go about deducing things in

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)

- #5

- 145

- 34

- #6

- 3,861

- 1,440

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.

Yes. The mathematical system, like the collection of numbers or of geometrical objects is generally regarded as aSo in a way, a mathematical formal system exists as a distinct entity from the logical formal system which undergirds it?

- #7

- 675

- 319

Don't you meanIn 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 inanytheory 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)

##(F\to G)\to(\neg G\to\neg F)##

?

- #8

- 145

- 34

Good catch on the contrapositive. :D

- #9

- 3,861

- 1,440

Yes, d'oh!Don't you mean

##(F\to G)\to(\neg G\to\neg F)##

?

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

- #10

- 675

- 319

I thought maybe it was one of those non-logical axioms.Yes, d'oh!

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

- #11

- 26

- 0

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?

Last edited:

- #12

- 3,861

- 1,440

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.Is there a way to construct a formal system F such that one of the derivable theorems is Godels Incompleteness Theorem?

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.

- #13

- 26

- 0

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.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.

- #14

- 3,861

- 1,440

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.Are there possibly larger logical systems than us for which we cannot derive Godels theorem?

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

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.

- #15

- 11,007

- 3,721

First order logic is both consistent and complete. Indeed, before proving his famousIs first order logic inconsistent or incomplete?