Can Mathematics be Translated to First-Order Language?

[julypraise]

Main Question:
Does every language used in mathematics (such as mathematical symbols and English to describe formulas, theorems, definition, proofs, and etc.) can be translated (or reduced) to first-order (predicate) language?



Sub Question:
Does every informal proof can be formalized (that is, to be a formal proof)? (Note that: the mathematical proofs in publications such as papers and books, in general, are informal proofs.)



Related Question:

(1) Did the logicism project of Russell and Whitehead in Principia Mathematica fail? If failed, then why?

(2) What is the implication of Godel's Incompleteness Theorem to the logicism activity?




* I would be really grateful if anyone suggest me good, authoritative reference books that answer or discuss these questions.

 

[Preno]

The received view seems to be yes and yes.

In actual fact (i.e. my opinion), first-order logic is incapable of expressing even such basic concepts as infinity (no, first-order set theory doesn't help), hence is too limited to serve as a basis for mathematics. The reasons for its near-universal adoption seem to be historical chance, technical convenience and the (related) fact that it's the best researched logic out there, not its philosophical primacy (or even adequacy).

As for formalization, trivially every proof can be formalized if you add the appropriate conditionals to your axioms. The real underlying question is, I assume, whether every mathematical concept can be exhausted with a formal definition, to which I have to answer (probably) no. There doesn't seem to be any reason why we should a priori expect it to be. For example, one might argue that our notion of set contains the truth of an infinite hierarchy of large cardinal axioms, and there is certainly no formal definition of a large cardinal axiom, identifying one requires some conceptual insight. Similarly, our notion of natural numbers is not exhausted by PA or some of its recursive extensions - the axiom of induction is arguably a second-order one, not an infinite collection of first-order axioms. You might want to research indefinitely extensible concepts.

 

[SW VandeCarr]

The received view seems to be yes and yes.

In actual fact (i.e. my opinion), first-order logic is incapable of expressing even such basic concepts as infinity (no, first-order set theory doesn't help), hence is too limited to serve as a basis for mathematics.[

Since no one has challenged this statement, I will; although there are others who post here that are more knowledgeable in this area. If you are correct, I don't understand why. "..expressing even such basic concepts as infinity.." is itself not a very rigorous statement. Saying that the transfinite cardinal \aleph_0 is larger than any integer certainly "expresses" the concept of infinity assuming we already agree that for any integer n, no matter how large, there exists a larger successor n+1.

 

[Preno]

Since no one has challenged this statement, I will; although there are others who post here that are more knowledgeable in this area. If you are correct, I don't understand why. "..expressing even such basic concepts as infinity.." is itself not a very rigorous statement.

No, it's perfectly rigorous. Expanded, it means: there is no formula of first-order logic with identity stating that there is an infinite number of \varphis.

(More precisely, an infinite set of formulas of first-order logic can express this proposition, but still the point remains that even no set of formulas of first-order logic can express the proposition that there is a finite number of \varphis.)

Saying that the transfinite cardinal \aleph_0 is larger than any integer certainly "expresses" the concept of infinity assuming we already agree that for any integer n, no matter how large, there exists a larger successor n+1.

That, however, is a sentence of set theory, not first-order logic. The above point applies to first-order set theory no less than to any other first-order theory. There is no sentence of first-order set theory expressing the proposition that there is an infinite number of sets satisfying some condition \varphi. No doubt you want to interject and claim that the sentence "there is an injection from \omega into set X" expresses this claim, but that is not true. For one thing, it may be the case that X is infinite without there being such a bijection - all sentences of the form "X has more than n members" (whether expressed in pure first-order logic or via the existence of an injection of some finite ordinal into X) may be true without there being an injection from \omega into X (this is a manifestation of omega-inconsistency). For another, our question was concerning the condition \varphi, not the set X. As not all conditions define sets, even this flawed solution doesn't apply to all \varphi.

In short, set theory offers only a simulation of our notion of infinity, close enough for most practical purposes but in no way immune from the general point concerning any first-order theory.

 

[yossell]

That, however, is a sentence of set theory, not first-order logic.

Strictly, there's no incompatibility here. First-order formulations of set-theory exist. First order formulations of number theory exist. Both are strong enough to entail the existence of infinitely many numbers.

However, a case can be made for the following: there is no first order sentence which has precisely the content of 'there are infinitely many Fs'. For the first order theorist will need to express this via a sentence that mentions numbers or sets or some other structure, and so, in a sense, the first order sentence will say too much - as `there are infinitely many Fs' does not seem to talk about such things.

I'm not convinced by this line of reasoning for two reasons: (a) it's not clear to me that the concept of infinity *is* really free of a notion of number, and therefore a sensible counter is that number is appearing implicitly here, the first order formulation only makes this explicit. (b) it's not clear to me that the first order formalisation of our concepts in mathematical terms should not be allowed to make use (first order) defined mathematical objects, even when those mathematical objects don't obviously appear in the original proposition being analysed.


It is more typical to see the case made against the first order theorist along the following lines. The first order theorist is unable to formalise even the number system, or the set-theoretic hierarchy in first order terms. The trouble is that there are models for the first order axioms of arithmetic which contain `non-standard' numbers. A number is non-standard if it is greater than 0, greater than 1, greater than 2...

This does seem to lead to problems in defining infinitely and finitely - even if the first order theorist is allowed to talk about numbers and sets: for the above construction seems to show that, no matter what he says about numbers in his first order language, he cannot guarantee that each natural number is the result of a FINITE number of applications of the successor operation.

At this point, a fight ensues about the significance of such model-theoretic results, and matters become contentious. It should be noted that, second order theories in effect avoid these results simply by allowing themselves the ability to quantify over ALL the SUBSETS of the first order domain. If you don't like sets, if you think the concept of all the subsets of an infinite domain are problematic, you won't like this answer very much.


Logicism was an attempt to reduce Mathematics to Logic. But Frege's expanded notion of logic turned out to be inconsistent. In trying to patch the inconsistency, Russell found himself moving to a system of axioms that, while still strong enough to be a foundation for mathematics, despite his efforts, no longer looked like axioms of pure logic. Given this failure plus the fact that ZFC set-theory was a much simpler way of providing a foundation for mathematics, attention turned away from Principia.

Note that in recent years, it has been argued/discovered that one of the damaging axioms of Frege's system was, in fact, never really a good candidate for an axiom of logic; that this axiom could and should be dropped and replaced with another axiom which *does* have a better claim to be a truth of logic; that the resulting weaker system provides a foundation for a good deal of mathematics - not the upper reaches of set-theory - in particular, all the mathematics that has physical or scientific applications. I.e. (say they) all the maths you should care about.

The implication of Godel's theorem depends upon what you were expecting from the logicist project. If you were hoping from your logicism a system which could provide a foundations for all mathematical objects and notions of mathematical truth, I don't think it has much impact. But if you were also hoping for a system in which every piece of mathematics was provable, some kind of system which would reduce all mathematics to a nothing more than a very long and boring algorithm, which would eventually crank out all the mathematical truths and all the mathematical falsehoods, then Godel's incompleteness theorem makes life problematic. For it shows that any sufficiently strong consistent theory, there is some arithmetical statement P such that P is not provable and ¬P is not provable in the theory. Many feel this in an intolerable limitation in logicism. Certainly, it makes it a little harder for those who want to reduce mathematical truth to mathematical provability.

 

[Preno]

However, a case can be made for the following: there is no first order sentence which has precisely the content of 'there are infinitely many Fs'.

Yes, that's precisely what I was saying. Not, however, for this reason:

For the first order theorist will need to express this via a sentence that mentions numbers or sets or some other structure, and so, in a sense, the first order sentence will say too much - as `there are infinitely many Fs' does not seem to talk about such things.

but because, as I said, (1) there is no sentence of first-order set theory expressing that there are infinitely many sets satisfying some condition F (moving to NGB doesn't help, because then the claim we cannot express merely becomes: there are infinitely many classes satisfying some condition F), and (2) there can be infinite sets (sets which have more than 1 member, more than 2 members, ...) for which the set theoretic definition of infinity as the existence of a function from omega to a given set fails.

(Granted, a theory with an infinite hierarchy of hyper-hyperclasses wouldn't necessarily suffer from the first defect. We might argue that there is no sentence expressing that there infinitely many hyperclasses of the sort corresponding to the limit ordinal of the hyperclass hierarchy - say, omega - but the person using this hyperclass-language isn't necessarily committed to there being such hyperclasses, whereas someone using ZFC certainly is eo ipso committed to the existence of sets and someone using NBG is thereby committed to the existence of classes.)

[edit] Also, as I just realized, (3) the set theoretic definition requires us to model everything as sets. Until we've interpreted what a wibble is set-theoretically, we don't know how to say that there are infinitely many wibbles. (This issue remains somewhat hidden, because we pretty much automatically introduce stuff set-theoretically, but there is no reason why that should be taken for granted. For example, it's certainly possible to understand - yes, properly understand - what a group or a vector space is without having learned set theory. The submerging of these concept into the set-theoretical ocean is a secondary development.) Of course, people who propose to define infinity set-theoretically may not accept the presupposition that mathematical objects can legitimately be introduced in a non-set-theoretical way, manifestly true as it is historically.

I'm not convinced by this line of reasoning for two reasons: (a) it's not clear to me that the concept of infinity *is* really free of a notion of number, and therefore a sensible counter is that number is appearing implicitly here, the first order formulation only makes this explicit. (b) it's not clear to me that the first order formalisation of our concepts in mathematical terms should not be allowed to make use (first order) defined mathematical objects, even when those mathematical objects don't obviously appear in the original proposition being analysed.

I agree with those two points, but they're not really directed towards my claim. I'm not saying that mentioning sets is illegitimate, I'm saying that mentioning sets still doesn't allow you to express that there are infinitely many Fs.

The rest of your post was a fair summary, imo, except I'd say that what Godel's results prevent us from doing (or make it harder for us to do) is reducing mathematical provability to provability in a given formal system, not reducing mathematical truth to mathematical provability. The lesson is, imo, that our language (and the conceptual apparatus in contains) is extendible, not that there is some determinate mathematical truth outside the reach of provability.

 

[yossell]

Hi Preno,

but they're not really directed towards my claim

yeah, I intended for my post to complement yours in certain ways, certainly didn't mean to take issue with everything!

We both agree that there's an issue with infinity for first order theories, but perhaps there's still a disagreement as to what this issue is.

(1) there is no sentence of first-order set theory expressing that there are infinitely many sets satisfying some condition F

Do you agree with the following? There is a sentence of first-order set-theory that entails that there are infinitely many sets. Similarly, there are sentences of first order number theory that entails that there are infinitely many numbers. So there are first order sentences which entail there are infinitely many numbers which F.

If so, why do you maintain (1)? (a) Is it because you have a special condition F in mind? (b) Is it that you think it is not enough to entail the existence of infinitely many Fs for a sentence to express that this is so?

(2) there can be infinite sets (sets which have more than 1 member, more than 2 members, ...) for which the set theoretic definition of infinity as the existence of a function from omega to a given set fails.

Are you thinking of non-standard models, where omega in effect contains non-standard ordinals: since an infinite set can be put into 1-1 correspondence with a proper initial segment of omega, it thereby gets (incorrectly) classified as a finite set by the model?

(3) the set theoretic definition requires us to model everything as sets

Why so? It's true that pure set-theorists, as a matter of mathematical convenience, suppose that their domain contains nothing but sets, and treat the heirarachy as `built up' from the empty set. But it's perfectly legitimate to consider a set-theory with urelements; there's no reason why the first order theorist can't allow functions from non-sets to sets - he'd better, if he's to make sense of applied mathematics, if he wants to count people and chairs.

As a final question: are you sympathetic to the second order solution? For my own part, I am not sure it introduces any notion which someone familiar with the concepts of first order logic would object to: all you do is quantify over all the subsets of the domain. Or do you think that the logic has to be expanded in some way, with new, primitive, infinitary quantifiers?

 

[Preno]

Do you agree with the following? There is a sentence of first-order set-theory that entails that there are infinitely many sets. Similarly, there are sentences of first order number theory that entails that there are infinitely many numbers. So there are first order sentences which entail there are infinitely many numbers which F.

Yes.

If so, why do you maintain (1)? (a) Is it because you have a special condition F in mind? (b) Is it that you think it is not enough to entail the existence of infinitely many Fs for a sentence to express that this is so?

Yes, it's because such sentence say more than "there are infinitely many Fs" (so the sentence may be false in a non-standard model even if there are infinitely many Fs).

Are you thinking of non-standard models, where omega in effect contains non-standard ordinals: since an infinite set can be put into 1-1 correspondence with a proper initial segment of omega, it thereby gets (incorrectly) classified as a finite set by the model?

That or models which lack certain functions from omega to some other set.

Why so? It's true that pure set-theorists, as a matter of mathematical convenience, suppose that their domain contains nothing but sets, and treat the heirarachy as `built up' from the empty set. But it's perfectly legitimate to consider a set-theory with urelements; there's no reason why the first order theorist can't allow functions from non-sets to sets - he'd better, if he's to make sense of applied mathematics, if he wants to count people and chairs.

Tbh I did fail to consider set theories with urelements. But I'm not quite sure admitting urelements helps us here. (I have zero practical familiarity with set theories with urelements, so please bear with me.) Let's say I want to say that all groups such that ... are infinite. How would I express that if we take group elements as urelements from a set-theoretical point of view? I would presumably need to talk about a injection from omega to the group (say, Z), but if we treat the group elements as urelements, I don't think set theory guarantees us the existence of such a function - it does, as far as I understand, guarantee us the existence of every finite set of group elements, but not of the set consisting of all elements of a group (I maybe be mistaken here, but I don't think the axiom of replacement helps us here). Now in this particular case it might not be such a problem, we might simply accept that if we want to talk about groups, we ought to accept the existence of a set consisting of all the elements of any group (although I'm not sure whether this is sufficient to prove the existence of an injection from omega to Z if we treat the whole numbers as urelements), but the point is that we are still potentially missing plenty of infinite sets. So while we wouldn't need to submerge group theory as a whole into set theory, it seems to me that we would still need specific axioms regarding the existence of sets of group elements. Or would it be enough to add an axiom schema of group-theoretic specification / replacement? (Does that make any sense?)

As a final question: are you sympathetic to the second order solution? For my own part, I am not sure it introduces any notion which someone familiar with the concepts of first order logic would object to: all you do is quantify over all the subsets of the domain.

Yes, I generally am. The way I interpret it, the morale of the story about incompleteness is that we may need to rely on introducing new concepts (like sets) in order to prove theorems (such as those concerning in/finity) about our old concepts (like the naturals), and second-order language allows us to do that.