arithmetic in ZF
in [Logic]
|
Prev: What is wrong with this argument?
Next: Courage?
From: george on 3 May 2005 08:42 > "george" <greeneg(a)cs.unc.edu> writes: > > ... 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? Alan Smaill wrote: > 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, I would sincerely appreciate an example. > eg in a context like arithmetic. I don't intuit how arithmetic is any more helpful than any other context in enabling one to prove Qv~Q, "constructively", in intuitionistic propositional calculus, without being able to prove either of Q or ~Q. Or is "constructive" only meaningful at first (&higher) order?
From: Alan Smaill on 3 May 2005 08:56 "george" <greeneg(a)cs.unc.edu> writes: >> "george" <greeneg(a)cs.unc.edu> writes: >> > ... 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? > > Alan Smaill wrote: >> 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, > > I would sincerely appreciate an example. > >> eg in a context like arithmetic. > > I don't intuit how arithmetic is any more helpful > than any other context in enabling one to prove Qv~Q, > "constructively", in intuitionistic propositional calculus, > without being able to prove either of Q or ~Q. > Or is "constructive" only meaningful at first (&higher) order? In the arithmetic case, we are talking first order. A proof of x=y v ~x=y will typically use induction and correspond to a decision procedure for equality of natural numbers. This gives constructive justification for case splits over equality of terms denoting natural numbers. But in the propositional case, where there are non-logical axioms, then the same phenomenon can occur; of course, there can be axioms of the form r v ~ r, or less trivially axioms that allow proof of X v ~ X, where X is some propositional combination of atoms. -- Alan Smaill
From: george on 3 May 2005 08:58 Alan Smaill wrote: > .. 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, "Babylonian" is later going to say that this is impossible, that it is a meta-theorem about provability under IPC that pvq is provable iff p is provable or q is provable.
From: Alan Smaill on 3 May 2005 09:03 "george" <greeneg(a)cs.unc.edu> writes: > Alan Smaill wrote: >> .. 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, > > "Babylonian" is later going to say that this is impossible, > that it is a meta-theorem about provability under IPC that > pvq is provable iff p is provable or q is provable. > OK for propositional logic with no non-logical axioms; but that doesn't mean it follows for set theory in constructive FOL, which is I take it what is at issue. -- Alan Smaill
From: george on 3 May 2005 09:51
Babylonian wrote: > Intuitionist logic has the following theorem: > pvq is provable if and > only if p is provable or q is provable. Remember this. I was trying. It was made harder by the fact that a dueling expositor had insisted earlier in the thread that there could exist contexts (he cited "arithmetic" specifically) where qv~q could be intuitionistically provable even though neither q nor ~q was. I have another reply reminding him that you said this. If you want to take this issue on that branch (with him, not me!) I would buy a ticket to that bout. > > The class of finite sets that provably exist IS the same > > under both logics. > > Is that a constructive theorem, or a classical one? Constructive, whence it follows that it is also classical. > Here is a classically finite set: Oh, bullshit. > C={{}} if the CH is true > C={} if the CH is false. C is NOT a set. C is a VARIABLE whose VALUE you do NOT know. But I think I know what you meant. ZF has an axiom of separation, which mandates the existence of a (constant) set that is a subset of some bounding set. If O=df={} then you could let the bounding set be {O}={{}} and you could invoke separation to produce the subset of those x in it for which CH(x) is true (even though CH(.) actually takes 0 arguments and not 1; presumably there is a way of phrasing it using an x that it ignores). That { xe{O}: CH(x) } is either O or {O} is a theorem of ZF. Classically, that means it holds in every model of ZF. If you have some intuitionistically-definable "structure" where it doesn't hold, then WE would just say that that is NOT a model of ZF. But I don't know that we get away with that, because YOU are the one who is obligated to say what "intuitionistic model theory" is. > I just want to know: > > (i) does C exist in all models of the > theory generated by intuitionist logic? That depends on how you define "C". If you define it as the the necessarily-extant output from the separation-axiom-schema for the input-pair ({O},CH), THEN YES, C DOES exist in every intuitionistic model of ZF, DESPITE the fact that I don't know jack about intuitionistic model theory. > I say by the comprehension axiom it does. But precisely BECAUSE that's an AXIOM-schema, this is not yet a model-theoretic question. It is an AXIOM OF ZF that "this set exists". And it is a theorem of the theory that "this set" is a subset of {O}. And {O} only has two subsets. > (ii) is C={}v~C={} true in all said models? > I say it isn't, You've got a much bigger problem. "C" DOESN'T EVEN OCCUR IN THE LANGUAGE of ZF, intuitionistically OR classically. You have to *define* "C" as ABBREVIATING some linguistic term that DOES occur in that language. If C =df= Sep[{O},CH], then Az[zeC->ze{O,{O}}] IS A THEOREM of ZF. By the pairing axiom (and extensionality), this REALLY DOES PROVE C=O v C={O}. > because CHv~CH is only provable if either > CH or ~CH are provable, That is starting to look questionable. I mean, we have just seen that C=O v C={O} is provable (I just proved it), even though neither C=O nor C={O} is provable. > there is a model where C={}v~C={} is false. Well, it would have to be both false and provable, in that case. Again, you owe some intuitionistic model theory. I have no idea what int/con thinks a model is. We need to hope you do. > That is a model where CH is neither true nor false, But we really do have a problem, if we have a problem with dueling definitions of "false". Classically, we have false as the opposite of true. Intuitionistically, "~P is true" and "P is false" apparently mean DIFFERENT things. They are not on the same level. One of them (defining ~) is proof-theoretic; it means P->(p&~p) is provable. That CANNOT VARY from model to model. Truth (and, therefore, presumably, falsity) CAN so vary. > because ~(C={}v~C={}) is the statement that there can > never be a proof of C={}v~C={}. Well, not exactly; it is the meta-assertion that assuming it would lead to contradiction, and thus that the denied statement is (classically) DISprovable. ~ comes with a modality here. So how can you say that something is just PLAIN false, as OPPOSED to provably false? Classically, we can answer that because we have truth IN MODELS and we have a completeness theorem. Intuitionistically, you have a model theory that you are not doing a good job of defining. Whether there does or doesn't exist a proof of something is NOT the kind of thing that can vary from model to model. The TRUTH-value is what varies from model to model. Or not. Only if it FAILS to vary is something (classically) provable; if it succeeds in varying then the sentence is not provable, period, and that is NOT model-dependent. We've got to come up with some framework-language / meta-language that is neutral between both logics. We can't discuss this right if "false" means something different in the two places. We were already having enough trouble because ~ did. |