arithmetic in ZF
in [Logic]
|
Prev: What is wrong with this argument?
Next: Courage?
From: Alan Smaill on 1 May 2005 18:09 "george" <greeneg(a)cs.unc.edu> writes: .... >> 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? I'm note sure what distinction you have in mind between intuitionistic and constructive here. There are variants around, but most folk use intuitionistic/constructive FOL to mean the same thing. > 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? By providing an intuitionist/constructive proof of qv~q, which may go via a proof of q, or of ~q, or indeed of qv~q where neither q nor ~q is provable, eg in a context like arithmetic. > 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. You would get a constructive proof of ( q v ~q ) -> Ex[Px] simply from these ingredients; but if you throw away the constructive proof of ( q v ~q ) you do not have the ingredients for the constructive proof of Ex[Px]. The classical proof does this by not indicating that q is false, which is needed for the constructive content of a proof of Ex[Px], which should enable the computation of a witness for x. eg, with equality Ex[ (0=1 & x=1) v (~0=1 & x=2) ] The constructive proof gives us implicitly a witness (here, 2). -- Alan Smaill
From: Chris Menzel on 1 May 2005 19:17 On 1 May 2005 14:32:17 -0700, Ross A. Finlayson <raf(a)tiki-lounge.com> said: > I think ZF is inconsistent, because of regularity, Well, you should stop thinking that, because if ZF is inconsistent, so is ZF without regularity. > In ZF there is the Burali-Forti paradox, No there isn't (assuming ZF isn't inconsistent for other reasons). The axioms do not permit the construction of the BF paradox.
From: Ross A. Finlayson on 1 May 2005 19:58 Chris Menzel wrote: > On 1 May 2005 14:32:17 -0700, Ross A. Finlayson <raf(a)tiki-lounge.com> said: > > I think ZF is inconsistent, because of regularity, > > Well, you should stop thinking that, because if ZF is inconsistent, so > is ZF without regularity. > > > In ZF there is the Burali-Forti paradox, > > No there isn't (assuming ZF isn't inconsistent for other reasons). The > axioms do not permit the construction of the BF paradox. But, I think quantification implies a universal set, thus that there is an irregular set, .... (I'm reminded of sets containing the empty set as trivially regular.) What's the class of all classes? It would be similar to the set of all sets. Maybe you think those are just absurdities, if other theories address them and ZF is dumb, in the sense of being mute, then ZF is missing some expressive power. Mechanically, the set of all ordinals would appear to be the same form as the order type of ordinals, or the class of all ordinals. Where there are only finite ordinals, a similar problem arises. Thus, and where I surmise there is only one proper class, any resolution to these paradoxes with remarkably similar construction to each other would need take place in the first-order. One example I have been frequently reusing is that of the physical universe, and physical objects in the physical universe, where functions between physical objects are themselves physical objects. That leads to a conclusion that the (physical) universe is infinite and infinite sets are equivalent. Chris, I think the axioms demand to preclude those things, and can't. With warm regards, Ross F.
From: Chris Menzel on 1 May 2005 20:19 On 1 May 2005 16:58:17 -0700, Ross A. Finlayson <raf(a)tiki-lounge.com> said: > Chris Menzel wrote: >> On 1 May 2005 14:32:17 -0700, Ross A. Finlayson <raf(a)tiki-lounge.com> > said: >> > I think ZF is inconsistent, because of regularity, >> >> Well, you should stop thinking that, because if ZF is inconsistent, so >> is ZF without regularity. >> >> > In ZF there is the Burali-Forti paradox, >> >> No there isn't (assuming ZF isn't inconsistent for other reasons). The >> axioms do not permit the construction of the BF paradox. > > But, I think quantification implies a universal set, Well, stop thinking that. :-) More seriously, if you are using ZF as a basis for your account of quantification, then it is provable that there is no universal set. Hence, in that framework, quantification does not imply a universal set. Maybe you want to work in a framework like NF that does have a universal set. Fine. The point is you just can't assert flat out that quantification implies a universal set; you need to specify your background set theory for the assertion to have any definite purchase. > thus that there is an irregular set, .... (I'm reminded of sets > containing the empty set as trivially regular.) It shouldn't. In set theories without regularity there are many irregular, i.e., non-wellfounded, sets that contain the empty set, for example, sets A satisfying A = {A,{}}. > What's the class of all classes? In most set theories there is no such thing. > It would be similar to the set of all sets. Insofar as, in such theories, there is no such thing. > Maybe you think those are just absurdities, No, there are theories that make sense of them. > if other theories address them and ZF is dumb, in the sense of being > mute, then ZF is missing some expressive power. No, it just has an alternative account of the nature and existence of sets. Chris Menzel
From: Keith Ramsay on 1 May 2005 21:20
george wrote: [...] |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? It all depends. Sometimes you can and sometimes you can't. There are some familiar tricks that sometimes work. It was originally proven that pi(n), the number of primes <=n, and li(n), the integral from 2 to n of 1/log t with respect to t, crossed, by showing it follows from the Riemann hypothesis and also by showing it follows from assuming that the Riemann hypothesis is false. Upon a little analysis, this can be seen to be equivalent to a result of the form: {Em R(m) v ~Em R(m)} -> En Q(n), where m and n range over integers, Q and R are primitive recursive predicates over the integers, RH is equivalent to ~EmR(m), and the desired result to the right hand side. There's a general metatheorem showing that if the conclusion is of the form En Q(n) with Q primitive recursive, then it can be proven using intuitionist logic too. In this sort of case, examining the proof that ~Em R(m) -> En Q(n) will show that it hides a constructive proof that EmR(m) v EnQ(n), i.e. either giving us an N where pi(n) and li(n) have crossed or a counterexample to the Riemann hypothesis. Then the other half of the proof just shows that if it's a counterexample to the Riemann hypothesis, then we can get the place where pi(n) and li(n) cross from it anyway. |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. Actually, (AvB)->C is equivalent both intuitionistically and classically to (A->C)&(B->C). So in particular (qv~q)->Ex[Px] is intuitionistically equivalent to (q->Ex[Px])&(~q->Ex[Px]). |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. Well, first, there are cheapo examples of the form Px := (x=1 and q or x=0 and ~q). The statement qv~q is already equivalent to an existence claim this way. One of the standard nonconstructivities in real analysis is the nonconstructivity of the intermediate value theorem. Say f(x) is defined as the function linear on [0,1/3], [1/3,2/3] and [2/3,1], with f(0)=-1, f(1/3)=f(2/3)=u, and f(1)=+1, where u is some real number. We can show that u<>0 implies f has a zero on [0,1], and also that u=0 implies f has a zero on [0,1], but to show that f has a zero on [0,1] is nonconstructive. If u<>0, then either u>0 and f has a zero on [0,1/3], or u<0 and f has a zero on [2/3,1]. If u=0, then f(x)=0 on [1/3,2/3]. If x ranges over the natural numbers and P is primitive recursive, then we have a metatheorem implying that there is a constructive proof of Ex[Px] too. The problem that typically seems to arise is like in this case, where the statement "q", in this case u<>0, has its own existential import. It implies that to some degree of approximation not necessarily known to us, q differs from 0. If we had in our hands the natural number N such that |u|>1/N, we'd be home free. Or if we knew for a fact that there was no such N. |"Intuitionistic" and "constructive" are slightly different |notions here. Generally, intuitionism pertains to Brouwer's particular brand of constructivism. Intuitionistic logic is a particular attempt at formalizing the logic in it. (Brouwer was generally against formalization, though.) One could have a constructive system with a different logic in it. But in this particular case, having the deductive rule {(qv~q)->Ex[Px]} => Ex[Px] is incompatible with constructivity, so it's somewhat moot. Keith Ramsay |