arithmetic in ZF
in [Logic]
|
Prev: What is wrong with this argument?
Next: Courage?
From: Babylonian on 30 Apr 2005 19:25 george wrote: > > > Obviously, ZF-provability includes provability by > > means of LEM, > > PuhLEEZE. Obviously, it doesn't. > LEM is from classical logic, not from ZF. > You can apply intuitionistic logic to the same > old ZF axiom-set. > The theory obtained by adding the axioms of ZF to intuitionist logic is not the theory of ZF sets. PuhLEEZE.
From: george on 1 May 2005 15:52 > > If you can prove p -> q then you ought to be > > able to prove ~q -> ~p (it is equivalent). > > In the case of Ex[Px] -> p&~p, the contrapositive is > > (pv~p) -> ~Ex[Px], Babylonian wrote: > No, the contrapositive is > ~(p&~p) -> ~Ex[Px] and the inference > ~(p&~p) => ~pv~~p is not constructively valid, > nor is the inference ~~p => p. OK, I'm sorry. I'm just intrinsically hostile to intuitionistic logic (I don't even consider it a bivalent logic; it is "really" something modal with a great many degrees of modality and truth-values), so I I forgot something that basic. In int., you can't derive pv~p from nothing; it's not tautologous; int. does not obey LEM. I'm repeating that to myself to try not forgetting it again. But you CAN derive ~(p&~p) from nothing, right? There IS a underlying basic assumption of consistency, right? There is also the question of how to deMorgan/deny first-order quantified statements. Classically, ~(p&~p) is ~pvp, but intutitionistically, it is not anything simple; it is something like (p&~p)->(q&~q) for some q, right? But given that you can't deny a conjunction simply/deMorgan, what happens when you try to deny a universally quantified statement? That is just the infinitary version of the same difference, right? If we have have Ax[~Px], we can deny it classically to get ~Ax[~Px] <=df=> Ex[~~Px] <=df=> Ex[Px]. I guess that is the kind of non-constructivity you are bemoaning, right? Intuitionistically, Ax[~Px] -> p&~p IS enough to get you ~Ax[~Px], but you CAN'T get from there to Ex[Px] intuitionistically, right? Is that the problem? > > which basically invites you to prove > > ~Ex[Px] by cases, first under the assumption that p, > > and secondly under the assumption that ~p. > > Proof by cases is an informal rule, not a formal rule, > if it matters. Maybe it is informal intuitionistically (it would probably not even be sound in that case), but it is formal in classical logic. > Formally, you use a v-introduction rule. Formally, classically, you use whatever dialect of formalism you like, because classically, they are all equivalent. Classically, v doesn't need to exist; it is eliminable as well as introducible. Since pvq =df= ~(~p&~q), anything you wanted to say with v can be said without it. But classically, ((pvq) -> r) <-> ((p->r) & (q->r)) is a a tautology, therefore, proof by cases IS formal. > I do not deny that nonconstructive proofs can guide > the search for constructive proofs - but in this case, > all you have us doing is starting over and looking for > a proof of (pv~p)->~(Ex)Px. I fear I dropped a ~ somewhere. > We'd rather prove (qv~q)->(Ex)Px, That's the case I *meant* to be talking about. It doesn't matter whether the "P" in question is P or is ~P. Both of them are P's. > and prove q or prove ~q. Well, that's the whole constructive-vs.LEM part. But that's the ONLY place that part is located. My point being that both the classical AND intuitionistic/constructive approaches agree that proving (qv~q)->Ex[Px] is important. But the classical people are willing to stop there, (Ex[Px], by itself, follows immediately, classically), whereas the intuitionistic/constructive people have to then go on to try to prove one of q or ~q. On the classical side, there is real scope for creativity and research, because not just ANY old q will do; despite the fact that pv~p is equivalent(as a tautology)to qv~q for all p and all q, they are NOT all equally USEFUL as hypotheses from which to prove Ex[Px]; contrapositively, classically, if Ax[~Px] leads you to a contradiction, it doesn't lead you to all of them equally; it leads you to a particular (complicated) one FIRST (and only thereAFTER to all equally). But I guess the real difference is this: classically, because you get qv~q for free, you really might want to try desigining/ discovering a q that would get you TWO prongs of help, where q might help produce Ex[Px] in one way, while ~q might help in another. Intuitionistically, however, you only need one, and the other doesn't matter, so bothering with qv~q is irrelevant. Given a proof of ~q -> Ex[Px], what you next want intuitionistically is a proof of q ->p&~p. While that will also work classically, classically you have the additional option -- the "easy way out" -- of proving q -> Ex[Px] and invoking LEM. My remaining gripe is that I still don't see how that is "non-constructive" -- both q -> Ex[Px] and ~q -> Ex[Px] could be constructive.
From: george on 1 May 2005 16:00 Babylonian wrote: > > > Obviously, ZF-provability includes provability by > > > means of LEM, > george wrote: > > PuhLEEZE. Obviously, it doesn't. > > LEM is from classical logic, not from ZF. > > You can apply intuitionistic logic to the same > > old ZF axiom-set. B > The theory obtained by adding the axioms > of ZF to intuitionist logic is not the theory > of ZF sets. PuhLEEZE. This is silly. One cannot "add" the axioms of ZF or of any other first-order language to "intuitionistic logic". Intuitionistic logic IS A LOGIC. It is NOT an axiom-set (which is what ZF is). Axioms do NOT get ADDED TO intuitionistic logic or classical logic or any other logic. Rather, logics are USED to INFER (sentences from other sentences, using rules of inference; they prove theorems from axioms. If you start with the first-order ZF axioms, you will get one theory if you close them under first-order classical consequence and a DIFFERENT theory if you close them intuitionistically. But to say that the classical way "is" "ZF-provability", while the intuitionistic way isn't, is discriminating against yourself. Intuitionistic provability is every bit as legitimate as classical provability (you personally would in fact say moreso), completely IRrespective of whether the axiom-set-that-theorems-are-being-proved-from is ZF or is anything else.
From: george on 1 May 2005 16:35 > > Babylonian wrote: > > > Classicaly, if we assume ~(Ex)Px and > > > prove p&~p, we can infer (Ex)Px. > > > THIS inference leads to belief in > > > objects whose existence is > > > "non-algorithmic and essentially > > > unverifiable constructively", george wrote: > > Why "essentially"? > > If you can prove p -> q then you ought to be > > able to prove ~q -> ~p (it is equivalent). > > In the case of Ex[Px] -> p&~p, the contrapositive is > > (pv~p) -> ~Ex[Px], I dropped a ~ there. The original context was, "if we assume ~(Ex)Px". I said, "in the case of Ex[Px]". I should've had the case of ~Ex[Px]. But classically, ~Ex[Px] is equivalent to Ax[~Px]. So, instead, let's start there. Let's assume that we have derived Ax[~Px] -> p&~p. What follows? Well, both intuitionistically AND classically, ~Ax[~Px] follows. > No, the contrapositive is > ~(p&~p) -> ~Ex[Px] and the inference > ~(p&~p) => ~pv~~p is not constructively valid, > nor is the inference ~~p => p. Right, and just as it is not intuitionistically simple/deMorgan to deny binary 0th-order conjunctions, it is not simple to deny the infinitary first-order-analogous universal quantifier; we cannot get (intuitionistically) from ~Ax[~Px] to Ex[~~Px], and even if we could, we could not get from there to Ex[Px]. Classically, this chain is easy: Ax[~Px] -> q&~q int&cl=> ~Ax[~Px] cl=> Ex[~~Px] cl=> Ex[Px] but intuitionistically, only the first link holds. This proof is therefore non-intuitionistic, but why is it also non-constructive? Because I was off by one ~, I got correctly corrected this way: > I do not deny that nonconstructive proofs can guide > the search for constructive proofs - but in this case, > all you have us doing is starting over and looking for > a proof of > (pv~p)->~(Ex)Px. Yeah, but that was by accident. > We'd rather prove (qv~q)->(Ex)Px, Right. This is actually the case I wanted to be talking about. > and prove q or prove ~q. Let's take the contrapositive of that "shared first link" above and begin by assuming we have a proof of (qv~q)->Ex[Px], both intuitionistically and classically. How do we get from here to Ex[Px] ? Classically we get there trivially by LEM, but if that is not available, how do we discharge the qv~q hypothesis both intuitionistically and constructively? The q arose out of a non-constructive proof and we begin by asking if it provides guidance for an intuitionistic one. The classical proof didn't produce Just Any old contradiction; it produced one with specific relevance to the problem. Is its relevance strong enough that ~q->Ex[Px] is provable? If it is, then, classically, we might be able to do this by cases instead of by LEM. Having proved ~q->Ex[Px], you could then either a) prove ~q, which would work both intuitionistically and classically, or b) prove q->Ex[Px], which would not work intuitionistically but would work classically. My problem with calling one of these inferior to or less constructive than the other is that I don't see how you can dismiss the proof as non-constructive if both q ->Ex[Px] and ~q ->Ex[Px] are constructive. "Intuitionistic" and "constructive" are slightly different notions here.
From: Ross A. Finlayson on 1 May 2005 17:32
Barb Knox wrote: > In article <1114872483.068141.225400(a)o13g2000cwo.googlegroups.com>, > "Ross A. Finlayson" <raf(a)tiki-lounge.com> wrote: > [snip] > > >To be blunt, The Dedekind-slash-Cauchy definition of the reals is not > >adequate to define the real numbers, missing for example the "un-" or > >"non-" "computable" real numbers. > > Not so. The uncomputable reals correspond exactly to the the uncomputable > sequences of rationals that are their Cauchy sequences. The Cauchy etc. > definitions of real numbers say nothing whatsovever about computability. > > I guess I'm just against the notion of non-computable or non-constructible reals. I was of the opinion that there weren't any non-computable Cauchy sequences, now, I'm not. One reason I think that is because I think the reals are non-standard in the sense that besides being a field that they are as well a contiguous sequence of points. I think that a real number can be expressed in base one or base infinity. You're right. I have a vague notion, that besides that all real numbers are computable and that V = L, that the universe is the constructible universe, that Dedekind/Cauchy comprise equivalent definitions and are not adequate to represent all of the real numbers, basically again due to the continuity of the number line, a sequence of points. So, that there are non-computable Cauchy sequences because for non-constant terms no finite sequence ever completes, agrees with you. Basically, that gets into .999... vis-a-vis 1, or more accurately the right endpoints of intervals (0,1) and (0,1], which are not equal. There are various ways of defining those things. It's easy to see why (.9, .99, .999, ...) converges to one, but not that (.9, .99, .999, ..9998, ...) does. With (1, 1.0, 1.00, ...), the difference of consecutive terms appear to be a constant, but there are real numbers between 1 and 1.1, 1.01, 1.001, .... The sum of 1/2^n for all positive integers n is equal to one. Anyways, thanks Barb, that helps clear my understanding somewhat. This post doesn't have much to do with arithmetic in ZF, except V = L. It seems that arithmetic as here discussed is about, to some extent, bijecting the naturals or ordinals to some set of formulae. I think ZF is inconsistent, because of regularity, and that instead the universe of discourse is basically comprised of naturals, or alternatively ordinals with the cumulative hierarchy. That's a similar notion as to how a computer register, a finite sequence of zeros and ones, can be interpreted as signed or unsigned number, where for the infinite ordinals there is exactly one, in a specified way, finite ordinal, and that that infinite ordinals is basically the negation or additive inverse of that finite ordinal. In ZF there is the Burali-Forti paradox, that the order type of ordinals would be an ordinal, confoundingly, there's a paradox in ZF with respect to, basically, arithmetic. That's the same problem as that infinity+1 = infinity, and Cantor's paradox that the set of all sets is its own powerset, and using flexible definitions Russell, the Liar, etcetera, and a solution has to do with the dual representation of the minimal and maximal. Ross |