This page is within the scope of WikiProject Wikipedia essays, a collaborative effort to organise and monitor the impact of Wikipedia essays. If you would like to participate, please visit the project page, where you can join the discussion. For a listing of essays see the essay directory.EssaysWikipedia:WikiProject EssaysTemplate:WikiProject EssaysWikiProject Wikipedia essays pages
This page is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
At several places a construction of the form "<theory> proves <proposition>" is used (for example: "Ideally, the article about a theorem should specify, which theories do prove it"). A theory is a set of sentences in some formal language. What is the meaning of a statement that a set proves something? If the intention is that the theory contains a sentence whose meaning, according to the semantics of the formal language, is the specified proposition, this should be expressed more clearly. --Lambiam 13:38, 5 March 2012 (UTC)[reply]
A truly formal approach to formal systems. But Wikipedia is not a formal system and I wrote about transtheoretical stuff not for nothing. What means "semantics" in such cases as (¬p ∨ q) → (p → q)? The theorem is a concrete propositional formula, which uses →, ∨, ¬ connectives and two different propositional variables (names of which do not matter). If a formal language has two binary and one unary connectives which we identify with aforementioned three, and a set of (indistinguishable) propositional variables with cardinality at least 2, then the proposition may be accurately encoded. This is the semantics in such cases. We actually cannot decide what is the "true" semantics of the material conditional, is it some Plato's eidos independent from all material beings, an average intuitive perception by humans, is its semantics defined by some set of logical systems which use the "→" symbol (this is also a possible answer), or all of the above. We can only rely on the sources which give us some spectrum of views about the thing denoted as "→". But this is a relatively simple case yet, and we can downplay the distinction between a formula in a formal language and a formula in a user's browser.
Things become even more complicated for such cases as Hahn–Banach theorem where potentially a huge number of slightly different variants of first-order logic, set theory, type theory and category theory may be used to encode an intended meaning and propositions of such theories unlikely would have unambiguous translation between all such variants. In complex cases we even cannot be sure in our translation (and sometimes reliable sources with such translations even do not exist at all), and I do not think that Wikipedia may really describe so complex cases. But there are sources indeed which state that known proofs relies on ZF-style postulates. We should cite these sources.
Which possibilities we have if we know a translation F of our "theorem" into a formal language? Actually, there are not only two, but three usually observed cases.
F is a theorem. This means that we have a proof, or we know an algorithm which produces it. In this case I say that "this theory proves that theorem".
Some metatheoretical reason indicates that F cannot be a theorem, for example (p → q) → (¬p ∨ q) or p ∨ ¬p in intuitionistic propositional calculus. This usually means that the (meta)hypothesis "F is a theorem" leads to metacontradiction. In this case I say that "this theory cannot prove that theorem", and this is always a metatheorem.
We actually do not know. Nor have we a formal proof of F, nor do we see that the hypothesis "F is a theorem" explodes our metatheory. It is also quite common under the name "unsolved problem". Applied to Wikipedia, this means that no reliable source indicates either the case 1 or the case 2.
Note that if some formal theory even proves ¬F, this does not really "prove" that F is not its theorem, if we do now know anything about consistency. Consistency of many theories is proved via set-theoretical models, i.e. many pieces of knowledge like "F is not a theorem" relies on quite doubtful foundations. Incnis Mrsi (talk) 19:20, 5 March 2012 (UTC)[reply]
To Lambiam: I think a better wording would be "from <theory>, one can deduce <proposition>". JRSpriggs (talk) 22:15, 5 March 2012 (UTC)[reply]
Indeed, I think the use of <theory> as the subject in a phrase of the form "<theory> proves <theorem>" is an unusual way of expressing the concept of provability, one with which our mathematics editors will generally not be familiar. This may make the essay/guideline in its current form rather ineffective. The essay/guideline states: "An article on formal theory ... should explain ... its intended semantics", and my use of the term "semantics" above was in light of that pronouncement. I'm sure the proposal was prompted by the identification of some urgent problem with Wikipedia articles concerned with the foundations of mathematics, but I'm less sure what that problem is and even less so how this proposal addresses it. --Lambiam 22:35, 5 March 2012 (UTC)[reply]
The problem is that almost all articles which ought to provide information about foundations (examples are logical connective, contradiction and propositional formula) undisputably provide some information about respective topics, but say little on how these notions constitute the foundations of mathematics. Incnis Mrsi (talk) 09:41, 7 March 2012 (UTC)[reply]
Or rather, ZFC is (for now) the standard-de-facto for the working mathematics, while other approaches are more or less experimental? Boris Tsirelson (talk) 06:41, 6 March 2012 (UTC)[reply]
ZFC is not a (unique) standard, but some kind of minimal standard, and even that actually is not enforced. If one managed to prove something in ZFC, this would be a commonly accepted mathematical result. But "working mathematics" suffers from a terrible tangle in definitions and terminology, and many results are actually derived from facts which are thought to be true in a particular domain and are expressed in set-theory-like form, not from ZFC foundations, even indirectly. One example is inclusionsembeddings Z ↪ Q ↪ R ↪ C, which are commonly accepted without special explanations in many domains of "working mathematics" such as calculus, algebra and number theory. But the set theory has different definitions of these sets, there are no (default) inclusions. I am not sure that any of well-known results about numbers do not rely on such use of this inclusionembedding chain which leads to a flawed proof in the proper ZFC notation. Incnis Mrsi (talk) 08:15, 6 March 2012 (UTC)[reply]
The perception that ZFC "is the most common foundation of mathematics" has its roots in a sceptical attitude of the "working mathematics" towards foundational problems in the last 50 years, and is not based on facts. ZFC does not distinguish 0 and ∅, 1 and {0}, but almost any "working mathematician" does. If you write on the blackboard something like ∅ + {0} = {0} , it will likely be perceived as a false proposition about Minkowski addition, than as a trivial theorem about addition of natural numbers. A rare differential geometer or a specialist in the function theory will even remember about that definition of numbers. The real "foundation of working 21st century mathematics" in most domains is a mixture of type theory semantics, categorial-style definitions and ZFC-style propositions like the axiom of choice, but thought in a such way that "any element is a set itself", a fundamental idea of the set theory, is subconsciously rejected. Incnis Mrsi (talk) 08:49, 6 March 2012 (UTC)[reply]
There is something about this in the last paragraph of the section Foundational crisis of our article Foundations of mathematics. I think it is the case that most working mathematicians do not work from axiomatic systems, and only have a vague notion of what ZFC entails. I also have the impression most are Platonists – even if not always aware of it – and feel they are exploring a mathematical "reality" that exists independent of their explorations, for which any attempt at foundational axiomatization is like making a map of pre-existing territory. --Lambiam 09:10, 6 March 2012 (UTC)[reply]
I agree with most facts you mention, but interpret them somewhat differently.
"Z ↪ Q ↪ R ↪ C ... there are no (default) inclusions" --- ?? Everyone knows the default embeddings (and what do you mean by default inclusions?).
ZFC proves existence of R as a structure, and its uniqueness up to isomorphism. Any specific encoding of R in sets is as unimportant as the encoding of images in bit strings in (say) the PNG file format. Even less important; the latter encoding is used in practice all the time, the former is not. This is why, indeed, ∅ + {0} = {0} looks wild. Give someone just a bit string, and he will not guess that you mean a (PNG encoded) image. But this is not (yet) a sign of crisis. (It is not that I am completely happy with ZFC, but not for this reason.) Boris Tsirelson (talk) 15:30, 6 March 2012 (UTC)[reply]
An interesting analogy with encoding. You persuaded me that it would be no problems with a ZFC translation of a typed expression (at least with known domains of discourse and defined ZFC encodings of these), but… it is not obvious that the property of an encoded statement to be a ZFC theorem will be independent of the choice of encodings. A (hypothetical) proof can use not only translated images of typed expressions, but arbitrary ZFC stuff, which is not typed itself. Maybe someone proved such a theorem, but I would believe only if such proof was constructive, not made with ZFC itself. You may say: I proved that D and D′ are isomorphic. But it is not yet a proof that any statement like ∀x ∈ D ∃y ∈ D ∀z ∈ D blah-blah-blah is a theorem iff ∀x ∈ D′ ∃y ∈ D′ ∀z ∈ D′ blah′-blah′-blah′ is a theorem. Incnis Mrsi (talk) 19:18, 6 March 2012 (UTC)[reply]
I did not think much on this. Now it seems to me that conditionals such as (∀x ∈ D ∃y ∈ D ∀z ∈ D blah-blah-blah) → (∀x ∈ D′ ∃y ∈ D′ ∀z ∈ D′ blah′-blah′-blah′) may be proven from D ∼D′ using structural induction. No apparent problem with different encodings. Incnis Mrsi (talk) 19:50, 6 March 2012 (UTC)[reply]
You are right! But you do not need to prove this metatheorem. It is contained in Bourbaki (vol. 1, of course). Frankly, I was always puzzled why they did it metatheorem, but now, it seems, I start to understand. Boris Tsirelson (talk) 20:17, 6 March 2012 (UTC)[reply]
And if you find the analogy with encoding interesting, maybe look also here; I was bold enough as to express my opinions on Citizendium. (Not approved, of course.) :-) Boris Tsirelson (talk) 20:22, 6 March 2012 (UTC)[reply]
By the way: do not think that I always prefer ZFC. In some situations I really prefer higher-order logic; see here. Boris Tsirelson (talk) 20:54, 6 March 2012 (UTC)[reply]
