Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Classical First-Order Logic, Axiomatic Set Theory, and Undecidable Propositions

  1. Jan 20, 2007 #1
    It has been known for some time that the Axiom of Choice (if you treat it as a proposition to be proved rather than an axiom) and the Continuum Hypothesis are independent of Zermelo-Fraenkel set theory (ZF). These and other statements (Suslin's Problem, Whitehead's Problem, the existence of large cardinals...) can neither be proved true or false from the ZF axioms.

    ZF itself is built over classical first-order logic which includes the law of the excluded middle, which requires a proposition to be either true or false.

    Doesn't this result in an inconsistency?
  2. jcsd
  3. Jan 20, 2007 #2


    User Avatar
    Homework Helper

    You first, does it?
  4. Jan 20, 2007 #3
    Cagey, aren't you?

    Alright. There is at first "glance" a loophole, which is a semantic one. If I recall correctly, the definition of truth and falsehood of mathematical propositions preferred by the mainstream comes down to us from Tarski which is "validity with respect to a structure". Truth as being able to prove truth and falsehood as being able to prove the negation is the intuitionistic/constructivist notion. The problem though is that undecidable/independent statements mean that models of the structure in question exist in which the statement is valid, as well as models where the statement is not valid.

    So, as far as I see it at the moment, it does appear to result in an inconsistency.

    What I suspect is going on here is as follows...

    A platonist is going to insist on classical FOL as propositions of the mathematical world are either going to be true or false (it's just one world, all things are answered, and its consistent... by faith). One just needs to add the necessary extensions to an axiomatic theory to deal with a given "undecidable" proposition (an endless process though, which one might think has stalled out for ZF). The platonist can say "fine, I know this system is incomplete".

    For a formalist though, the game is supposed to be played by the rules and without appealing to rules that might be given in the future!
  5. Jan 20, 2007 #4
    To finish that thought off, it appears nobody is a thorough-going formalist anymore, and if you rub any set theorist or logician hard enough, you will find a platonist underneath. ;-)
  6. Jan 20, 2007 #5


    User Avatar
    Homework Helper

    I'm no mathematician, but I (naively) would think that one should fix the model per the discussion, so if one wanted to assume the continuum hypothesis for a discussion or not, or leave it undecided, that would be fine.
  7. Jan 20, 2007 #6


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    Incidentally, set-theory is a red herring here: you're simply having trouble with the notion of an incomplete theory. Try considering elementary group theory instead: it is also an incomplete theory of first order logic, and I suspect there will be fewer mental blocks associated with it.

    You're using a few words incorrectly -- I can go through and try and correct your usage if you want.

    (IMO, truth isn't a good way to think about logic, but I'll try to explain from that viewpoint anyways)

    In formal logic, truth isn't an inherit property of formulae: it is simply the result of plugging a formula into a truth function. Any consistent theory has at least one truth function in which every statement of the theory is true; an incomplete theory has many truth functions.

    The law of the excluded middle does not assert that any proposition is true or false. It merely asserts that v(P or not P) = T for any truth function v. That v(P) = T or v(P) = F is simply what it means for your logic to be two-valued. Even classical mathematics doesn't require binary logic: it works in any boolean logic.

    This is wrong. Formally, it's all the same: truth is the result of evaluating a truth function, satisfaction is defined in terms of interpretations, provability is defined in terms of rules of deduction, et cetera. Of course, some of the details might change. e.g. it seems most useful to study category-theoretic interpretations of intuitionist logic, rather than set-theoretic interpretations. Alas, classical and intuitionist are the only ones I really know much about.
  8. Jan 20, 2007 #7


    User Avatar
    Science Advisor

    There is a difference between saying something "cannot be proved" and saying it is "neither true nor false". Personally, I think it is better to avoid the words "true" and "false" in mathematics, using instead "valid" and "invalid"- i.e. "can be proven" or "can be disproven". In that case the "law of the excluded middle" asserts that there are no statements that can be both proven and disproven. It does not assert that there are no statements that can be neither proven nor disproven.
  9. Jan 20, 2007 #8


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    At the risk of being overly technical, "valid" means "holds in every interpretation". A priori, it has absolutely nothing to do with provability. (It is only through Gödel's completeness theorem that we see a formula is valid iff it can be proven without assuming any hypotheses)
  10. Jan 20, 2007 #9
    None of this would be an issue if the theory at hand were, say, Euclidean plane geometry or Presberger arithmetic.
  11. Jan 20, 2007 #10


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    But I didn't suggest you look at a complete theory as an alternative. :tongue: I suggested you look at something like the arithmetic of an abelian group. That's certainly an incomplete theory! E.g. [itex]\exists x \exists y: x \neq y[/itex] is independent of the abelian group axioms.
    Last edited: Jan 20, 2007
  12. Feb 16, 2007 #11
    Hurkyl's got it basically right.
    Maybe waxing technical will help eliminate confusion, so... permit me :)

    A theory is just a set of sentences of first-order logic (FOL) in some language. Examples include: the set of all sentences (which has no models), the theory of Abelian groups, ordered fields, ZFC, Peano arithmetic (PA), the empty set of sentences. If T is a theory and p a sentence in a given language, we write
    T |- p
    if p can be deduced from T in FOL -- T proves p. "|-" is intended to be one symbol ('turnstile'). If T is empty, then one drops the 'T' before the turnstile. In this case,
    |- p
    means p is provable, outright, in FOL.

    Godel's Completeness Theorem states that for all T and p,
    T |- p iff p is true in all models of T
    (= every model of T is a model of p -- models whose structure is appropriate for the language of T and p, that is).

    By the Completeness Theorem,
    |- p iff p is true in all models, i.e. p is universally valid.
    Valid sentences include the tautologies -- sentences true solely by virtue of their propositional form, such as (p or ~p), where '~' is negation. (As an example of a valid but non-tautologous sentence schema, consider Ex Ay P(x, y) => Ay Ex P(x, y).)

    A theory is called complete if for every p,
    either T |- p or T |- ~p
    So, if a theory T is not complete (incomplete), then for some sentence p,
    neither T |- p nor T |- ~p

    Of course it's true for any p that
    |- (p or ~p),
    hence for every theory T,
    T |- (p or ~p);
    but only some theories are complete! The empty theory is certainly not complete: not every sentence is either universally valid or inconsistent (true in no models, just plain false). The theory of Abelian groups is not complete; PA isn't; ZF(C) isn't; the theory of real closed fields is; Presburger arithmetic is.

    A theory T is consistent if no contradiction can be derived/deduced from T (= not every sentence can be deduced from T). An equivalent formulation of the Completeness Theorem is:
    T is consistent iff T has a model.
    It's easy to see that the Completeness Theorem implies this; to prove the converse, the Deduction Theorem,
    T |- (p => q) iff T + {p} |- q
    comes in handy (using '+' for union).

    Again by the completeness theorem, if both T + {p} and T + {~p} have models, then T proves neither p nor ~p (p is independent of T) -- and conversely. Because both ZFC + {CH} and ZFC + {~CH} have models, both are consistent, and ZFC proves neither CH nor ~CH -- CH is independent of ZFC. Nevertheless,
    ZFC |- (CH or ~CH)
    since of course
    |- (CH or ~CH).

    I've managed to write all of the above without saying much at all about truth of sentences in models. Let me change that :) in order to note a few final relevant facts. If M is a model, considered as a structure, let T(M), the theory of M, be the set of all sentences of the appropriate language which are true in M. T(M) is always a complete theory. Nevertheless, it is certainly possible to have T(M) = T(M') for non-isomorphic M and M' -- indeed, M, M' can have different, and then necessarily infinite, cardinalities (by the Lowenheim-Skolem-Tarski Theorem). First order theories -- even complete theories -- can characterize only finite models up to isomorphism. Finally, by the Compactness Theorem, if a theory has models of unboundedly large finite sizes, then the theory also has infinite models.

    Hope that helps!
    Last edited: Feb 16, 2007
  13. Feb 18, 2007 #12
    > it appears nobody is a thorough-going formalist anymore
    Not since 1932 ;)
    Hilbert's thorough-going Formalism was a philosophy of mathematics together with a program to validate it -- namely, proving that purely formal, "finitary" methods suffice both to derive all mathematical truths as well as to establish the consistency of mathematics. Godel's Incompleteness Theorems showed that the program simply cannot be carried out. In their aftermath, adhering to (thorough-going) Formalism would be like still believing in the "ether".

    But Hilbert's program lives on: it has become the branch of logic known as proof theory. Nor is Formalism dead and discredited as a philosophy of mathematics. There are contemporary logicians who have considered themselves Formalists (partial-going Formalists, reformed Formalists) inasmuch as they do not believe there is a single mathematical universe, Cantor's paradise, whose truths we endeavor to discern. A noteworthy example is Paul Cohen, who discovered (perhaps he would say "invented") forcing, and used it to build a model of ZFC + ~CH, thereby establishing the independence of CH from ZFC. The late proof theorist Solomon Feferman is another. It's fair to say that most set theorists are Platonists, if one must choose from among the usual three or four mathematico-philosophical pigeonholes. Most believe that, independence notwithstanding, CH is nevertheless either *really* true or, as most believe, *really* false -- in the (one, true) universe of set theory. Cohen and Feferman dismiss the question "Is CH true?" as meaningless.
    Last edited: Feb 18, 2007
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook