arithmetic in ZF
in [Logic]
|
Prev: What is wrong with this argument?
Next: Courage?
From: george on 30 Apr 2005 00:34 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", 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], which basically invites you to prove ~Ex[Px] by cases, first under the assumption that p, and secondly under the assumption that ~p. The point is, even though any old p will get you a contradiction if you conjoin it with ~p, you do NOT get just ANY old p when perform a non-constructive indirect proof of an existential. The PARTICULAR contradiction you derive may prove to be of some USE as a hypothesis in proving the contrapositive.
From: george on 30 Apr 2005 00:47 Babylonian wrote: > That was actually part of my point, to wit: > he appears to think that > Tarskian theory makes the notion of truth > "non-algorithmic and > essentially unverifiable constructively", > and it doesn't. Well, even if it isn't Tarski, SOMEthing sure does. If you are using first-order quantification over an infinite domain then the truth of a universally quantified statement depends on infinitely many 0th-order conjuncts, and the truth of an existentially quantified one on infinitely many disjuncts. This REALLY IS NOT algorithmically confirmable for first- order theories rich enough to satisfy the hypotheses of Godel's 1st incompleteness theorem. This doesn't have to be blamed on Tarski specifically but it is still important and relevant and it remains so even when one restricts one's practice to the Tarskian paradigm. > And, what he wants to do is none other than define truth! This is trivial. In the case of sentences in the language of PA, we LONG ago defined truth, because PA had a raison d'etre. It wasn't created JUST to BE PA; it was created to approximate actual arithmetic truth. Modern parlance says that a sentence in the language of PA is true iff it is true in the standard model, and truth in a model HAS a clear Tarskian definition. And NO, that is NOT algorithmically confirmable. Read his > post; here is a quote: > > "I was seeking to avoid such circularity > by attempting to define the > 'truth' and 'falsity' of PA propositions > in terms of ZF-provability in > a model of PA, As I had said throughout, ZF allows people to define differing models of PA, so this was always hopeless. > 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. > so reconcile that if you can with this: > > "I feel that such interpretations need to be > balanced by an alternative, constructive and > intuitionistically unobjectionable, > interpretation - of classical foundational > concepts - in which non-algorithmic truth > (satisfiability) is defined effectively." Trying to reconcile whatever-Bhup-was-talking-about with ANYthing is a MISTAKE. Bhup was NAIVE. He DIDN'T KNOW what he was talking about. Please don't compound his error by reacting to it as though there were some there there. > You do of course understand that an intuitionist > will not define the class of true PA sentences as > the class of sentences whose double-negation > translation holds in the natural numbers. The classical/Tarskian paradigm does NOT define "truth [simpliciter] AT ALL. It defines truth UNDER AN INTERPRETATION or truth IN A MODEL. If you are going to try to compare this with some sort of intuitionistic analogue then the FIRST thing you will have to supply is some intuitionistic model theory, NOT the intuitionistic "definition of truth". Which is, from a Tarskian perspective, irrelevant anyhow.
From: Ross A. Finlayson on 30 Apr 2005 10:48 Hi Keith, Correspondingly to the cumulative hierarchy, I'm trying to figure out a place for the real numbers among the ubiquitous ordinals or naturals. One notion is that they are simply serialized, the line runs in a line, and due to the dual representation and thus "great circle" of the integers, it is as well the completion of the reals, towards utilitarian purposes. 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. Instead, they, the real numbers, are a synthetic construct to do with the rest of the numbers and their manifestation of spaces. I hope you can help me understand why when Vitali says that the sum of infinitely many values can not be between one and three, that that's wrong. Consider for example how the the sum of 1/2^n over all natural integers, including zero, is two. The point with that is not to start (acceptable) debate about the definition of limit and the suitability of the inductive limit to derive that value without direct regard for infinitesimals, well, actually it is. It is because the hyperintegers are the same thing as the integers, and the hyperreals are the same thing as the reals. So, if Vitali has a problem with infinitely many values summing to some finite number, for example sum n=1^oo 1/2^x, or int x=0^2 dx, then maybe Banach-Tarksi requires a different explanation, because then there would be no non-measurable sets. Ross
From: Barb Knox on 30 Apr 2005 17:32 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. [snip] -- --------------------------- | BBB b \ Barbara at LivingHistory stop co stop uk | B B aa rrr b | | BBB a a r bbb | Quidquid latine dictum sit, | B B a a r b b | altum viditur. | BBB aa a r bbb | -----------------------------
From: Babylonian on 30 Apr 2005 19:16
george wrote: > 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", > > 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], 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. > 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. Formally, you use a v-introduction rule. > The point is, even though any old p will get you > a contradiction if you conjoin it with ~p, you do NOT > get just ANY old p when perform a non-constructive > indirect proof of an existential. The PARTICULAR > contradiction you derive may prove to be of some USE > as a hypothesis in proving the contrapositive. 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. We'd rather prove (qv~q)->(Ex)Px, and prove q or prove ~q. |