Chris Menzel wrote: > On Wed, 21 Jul 2010 20:29:03 -0600, Nam Nguyen <namducngu...@shaw.ca> > said: >> Chris Menzel wrote: >>> On Mon, 19 Jul 2010 07:26:03 -0700 (PDT), George Greene >>> <gree...@email.unc.edu> said: >>>> On Jul 19, 1:13 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> >>>> wrote: >>>>> A system may well be consistent even if some of its axioms are >>>>> false. >>>> By definition, if the system is consistent, IT HAS A MODEL. >>> True, certainly, for first-order systems, but not by definitiion. >> Otoh, would you think that if it's impossible to know if a system is >> consistent, it could still have a model by whatever process you've >> referred to as "not by definition"?
> It obviously would, if the system is consistent.
But the premise of my question is different though: "if it's impossible to know if a system is consistent ..."!
> The "process" by which > this is known is a *proof*. It applies to any consistent system, > irrespective of whether its consistency is knowable by us finite, > cognitively limited beings. Our epistemological capacities are simply > and utterly irrelevant to the theorem.
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Frederick Williams wrote: > Nam Nguyen wrote: >> Chris Menzel wrote: >>> On Mon, 19 Jul 2010 07:26:03 -0700 (PDT), George Greene >>> <gree...@email.unc.edu> said: >>>> On Jul 19, 1:13 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote: >>>>> A system may well be consistent even if some of its axioms are false. >>>> By definition, if the system is consistent, IT HAS A MODEL. >>> True, certainly, for first-order systems, but not by definitiion. >> Otoh, would you think that if it's impossible to know if a system is >> consistent, it could still have a model by whatever process you've >> referred to as "not by definition"?
> This "process" is no mystery. See Henkin.
It'd be a mystery if it's indeed _impossible_ to know if the underlying formal system is consistent, as my question is really about.
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Nam Nguyen wrote: > Chris Menzel wrote: >> On Wed, 21 Jul 2010 20:29:03 -0600, Nam Nguyen <namducngu...@shaw.ca> >> said: >>> Chris Menzel wrote: >>>> On Mon, 19 Jul 2010 07:26:03 -0700 (PDT), George Greene >>>> <gree...@email.unc.edu> said: >>>>> On Jul 19, 1:13 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> >>>>> wrote: >>>>>> A system may well be consistent even if some of its axioms are >>>>>> false. >>>>> By definition, if the system is consistent, IT HAS A MODEL. >>>> True, certainly, for first-order systems, but not by definitiion. >>> Otoh, would you think that if it's impossible to know if a system is >>> consistent, it could still have a model by whatever process you've >>> referred to as "not by definition"?
>> It obviously would, if the system is consistent.
> But the premise of my question is different though: "if it's impossible > to know if a system is consistent ..."!
>> The "process" by which >> this is known is a *proof*.
But it seems like that's a different kind of proof than the standard first order proof of, e.g., ExAy[~(y e x)] in ZF.
>> It applies to any consistent system, >> irrespective of whether its consistency is knowable by us finite, >> cognitively limited beings.
But if we can't know the formal system is consistent, what can we really know about its models?
>> Our epistemological capacities are simply >> and utterly irrelevant to the theorem.
But isn't it true that truths, theorems, and proofs would depend on knowledge, hence on knowledge capacities?
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Nam Nguyen wrote: > Frederick Williams wrote: >> Nam Nguyen wrote: >>> Chris Menzel wrote: >>>> On Mon, 19 Jul 2010 07:26:03 -0700 (PDT), George Greene >>>> <gree...@email.unc.edu> said: >>>>> On Jul 19, 1:13 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote: >>>>>> A system may well be consistent even if some of its axioms are false. >>>>> By definition, if the system is consistent, IT HAS A MODEL. >>>> True, certainly, for first-order systems, but not by definitiion. >>> Otoh, would you think that if it's impossible to know if a system is >>> consistent, it could still have a model by whatever process you've >>> referred to as "not by definition"?
>> This "process" is no mystery. See Henkin.
> It'd be a mystery if it's indeed _impossible_ to know if the > underlying formal system is consistent, as my question is really > about.
Let me rephrase my original question to better reflect the problem: would you think there could exist a formal system that can carry out the basic notions of arithmetic but that it's impossible (even in principle) to know its consistency? If your answer is yes, would it make sense to assume, speculate a model? If the answer is no, why?
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
> Nam Nguyen wrote: > > Frederick Williams wrote: > >> Nam Nguyen wrote: > >>> Chris Menzel wrote: > >>>> On Mon, 19 Jul 2010 07:26:03 -0700 (PDT), George Greene > >>>> <gree...@email.unc.edu> said: > >>>>> On Jul 19, 1:13 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote: > >>>>>> A system may well be consistent even if some of its axioms are false. > >>>>> By definition, if the system is consistent, IT HAS A MODEL. > >>>> True, certainly, for first-order systems, but not by definitiion. > >>> Otoh, would you think that if it's impossible to know if a system is > >>> consistent, it could still have a model by whatever process you've > >>> referred to as "not by definition"?
> >> This "process" is no mystery. See Henkin.
> > It'd be a mystery if it's indeed _impossible_ to know if the > > underlying formal system is consistent, as my question is really > > about.
> Let me rephrase my original question to better reflect the problem: > would you think there could exist a formal system that can carry > out the basic notions of arithmetic but that it's impossible (even > in principle) to know its consistency?
"impossible to know" how?
> If your answer is yes, would > it make sense to assume, speculate a model? If the answer is no, why?
Frederick Williams wrote: > Nam Nguyen wrote: >> Nam Nguyen wrote: >>> Frederick Williams wrote: >>>> Nam Nguyen wrote: >>>>> Chris Menzel wrote: >>>>>> On Mon, 19 Jul 2010 07:26:03 -0700 (PDT), George Greene >>>>>> <gree...@email.unc.edu> said: >>>>>>> On Jul 19, 1:13 am, Aatu Koskensilta <aatu.koskensi...@uta.fi> wrote: >>>>>>>> A system may well be consistent even if some of its axioms are false. >>>>>>> By definition, if the system is consistent, IT HAS A MODEL. >>>>>> True, certainly, for first-order systems, but not by definitiion. >>>>> Otoh, would you think that if it's impossible to know if a system is >>>>> consistent, it could still have a model by whatever process you've >>>>> referred to as "not by definition"? >>>> This "process" is no mystery. See Henkin. >>> It'd be a mystery if it's indeed _impossible_ to know if the >>> underlying formal system is consistent, as my question is really >>> about. >> Let me rephrase my original question to better reflect the problem: >> would you think there could exist a formal system that can carry >> out the basic notions of arithmetic but that it's impossible (even >> in principle) to know its consistency?
> "impossible to know" how?
Surely you must know, for example, it's impossible to disprove a formula by rules of inference, because rules of inference can only lead to proof, not to a disproof. That's how!
>> If your answer is yes, would >> it make sense to assume, speculate a model? If the answer is no, why?
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
On Sat, 24 Jul 2010 00:27:52 -0600, Nam Nguyen <namducngu...@shaw.ca> said:
> ... > Surely you must know, for example, it's impossible to disprove a > formula by rules of inference, because rules of inference can only > lead to proof, not to a disproof. That's how!
You don't think a proof of ~A is simultaneously a disproof of A?
Chris Menzel wrote: > On Sat, 24 Jul 2010 00:27:52 -0600, Nam Nguyen <namducngu...@shaw.ca> > said: >> ... >> Surely you must know, for example, it's impossible to disprove a >> formula by rules of inference, because rules of inference can only >> lead to proof, not to a disproof. That's how!
> You don't think a proof of ~A is simultaneously a disproof of A?
Of course not because in general there cases where there are proofs for _both_ A and ~A. (Naturally, I'm speaking of syntactical proofs using ruling of inference.)
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
On Tue, 27 Jul 2010 19:36:54 -0600, Nam Nguyen <namducngu...@shaw.ca> said:
> Chris Menzel wrote: >> On Sat, 24 Jul 2010 00:27:52 -0600, Nam Nguyen <namducngu...@shaw.ca> >> said: >>> ... >>> Surely you must know, for example, it's impossible to disprove a >>> formula by rules of inference, because rules of inference can only >>> lead to proof, not to a disproof. That's how!
>> You don't think a proof of ~A is simultaneously a disproof of A?
> Of course not because in general there cases where there are proofs > for _both_ A and ~A.
Then you simply have an inconsistent system in which everything is both provable and disprovable. So what?
Chris Menzel wrote: > On Tue, 27 Jul 2010 19:36:54 -0600, Nam Nguyen <namducngu...@shaw.ca> said: >> Chris Menzel wrote: >>> On Sat, 24 Jul 2010 00:27:52 -0600, Nam Nguyen <namducngu...@shaw.ca> >>> said: >>>> ... >>>> Surely you must know, for example, it's impossible to disprove a >>>> formula by rules of inference, because rules of inference can only >>>> lead to proof, not to a disproof. That's how! >>> You don't think a proof of ~A is simultaneously a disproof of A?
>> Of course not because in general there cases where there are proofs >> for _both_ A and ~A.
> Then you simply have an inconsistent system in which everything is both > provable and disprovable. So what?
So:
a) However much we _believe_ a formal system be consistent, especially one that is "sufficiently complex" (whatever that might mean) there's always a chance our belief might turn out to be simply incorrect!
Iow, we shouldn't trust intuition and what's "clearly evident" too much!
b) There's a chance that it's impossible (even in principle) to determine if a formula is provable in any extension of a formal system and the underlying extension is still consistent!
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Chris Menzel wrote: > On Tue, 27 Jul 2010 19:36:54 -0600, Nam Nguyen <namducngu...@shaw.ca> said: >> Chris Menzel wrote: >>> On Sat, 24 Jul 2010 00:27:52 -0600, Nam Nguyen <namducngu...@shaw.ca> >>> said: >>>> ... >>>> Surely you must know, for example, it's impossible to disprove a >>>> formula by rules of inference, because rules of inference can only >>>> lead to proof, not to a disproof. That's how! >>> You don't think a proof of ~A is simultaneously a disproof of A?
>> Of course not because in general there cases where there are proofs >> for _both_ A and ~A.
> Then you simply have an inconsistent system in which everything is both > provable and disprovable. So what?
Actually, what does it mean for a formula to be "disprovable" in an consistent formal system?
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Nam Nguyen wrote: > Chris Menzel wrote: >> On Tue, 27 Jul 2010 19:36:54 -0600, Nam Nguyen <namducngu...@shaw.ca> >> said: >>> Chris Menzel wrote: >>>> On Sat, 24 Jul 2010 00:27:52 -0600, Nam Nguyen <namducngu...@shaw.ca> >>>> said: >>>>> ... >>>>> Surely you must know, for example, it's impossible to disprove a >>>>> formula by rules of inference, because rules of inference can only >>>>> lead to proof, not to a disproof. That's how! >>>> You don't think a proof of ~A is simultaneously a disproof of A?
>>> Of course not because in general there cases where there are proofs >>> for _both_ A and ~A.
>> Then you simply have an inconsistent system in which everything is both >> provable and disprovable. So what?
> Actually, what does it mean for a formula to be "disprovable" in an > consistent > formal system?
Sorry for a typo: I meant to ask:
> Actually, what does it mean for a formula to be "disprovable" in an > _inconsistent_ formal system?
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Nam Nguyen wrote: > Chris Menzel wrote: >> On Tue, 27 Jul 2010 19:36:54 -0600, Nam Nguyen <namducngu...@shaw.ca> >> said: >>> Chris Menzel wrote: >>>> On Sat, 24 Jul 2010 00:27:52 -0600, Nam Nguyen <namducngu...@shaw.ca> >>>> said: >>>>> ... >>>>> Surely you must know, for example, it's impossible to disprove a >>>>> formula by rules of inference, because rules of inference can only >>>>> lead to proof, not to a disproof. That's how! >>>> You don't think a proof of ~A is simultaneously a disproof of A?
>>> Of course not because in general there cases where there are proofs >>> for _both_ A and ~A.
>> Then you simply have an inconsistent system in which everything is both >> provable and disprovable. So what?
> So:
> a) However much we _believe_ a formal system be consistent, especially > one that is "sufficiently complex" (whatever that might mean) there's > always a chance our belief might turn out to be simply incorrect!
> Iow, we shouldn't trust intuition and what's "clearly evident" too much!
> b) There's a chance that it's impossible (even in principle) to determine > if a formula is provable in any extension of a formal system and the > underlying extension is still consistent!
and
c) The concept of the natural numbers is a relative concept: at least relative to whether or not a certain formulas, e.g. pGC, are true or false.
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Nam Nguyen <namducngu...@shaw.ca> writes: > b) There's a chance that it's impossible (even in principle) to determine > if a formula is provable in any extension of a formal system and the > underlying extension is still consistent!
"There's a chance"? We know that in general the problem of determining whether a formula is provable in a theory is undecidable.
Alan Smaill wrote: > Nam Nguyen <namducngu...@shaw.ca> writes:
>> Sorry for a typo: I meant to ask:
>>> Actually, what does it mean for a formula to be "disprovable" in an >>> _inconsistent_ formal system?
> That there is a proof of its negation.
So an inconsistent system is also a consistent one then?
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Aatu Koskensilta wrote: > Nam Nguyen <namducngu...@shaw.ca> writes:
>> b) There's a chance that it's impossible (even in principle) to determine >> if a formula is provable in any extension of a formal system and the >> underlying extension is still consistent!
> "There's a chance"? We know that in general the problem of determining > whether a formula is provable in a theory is undecidable.
Then we don't really have anything to disagree on what I said in b). (Fwiw, I had in mind PA system and the formula pGC when saying b).
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Nam Nguyen wrote: > Aatu Koskensilta wrote: >> Nam Nguyen <namducngu...@shaw.ca> writes:
>>> b) There's a chance that it's impossible (even in principle) to >>> determine >>> if a formula is provable in any extension of a formal system and the >>> underlying extension is still consistent!
>> "There's a chance"? We know that in general the problem of determining >> whether a formula is provable in a theory is undecidable.
> Then we don't really have anything to disagree on what I said in b). > (Fwiw, I had in mind PA system and the formula pGC when saying b).
I do need some coffee: there was a typo. The formula I meant is cGC, not pGC. Sorry.
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
On Thu, 29 Jul 2010 08:05:52 -0600, Nam Nguyen <namducngu...@shaw.ca> said:
> Alan Smaill wrote: >> Nam Nguyen <namducngu...@shaw.ca> writes:
>>> Sorry for a typo: I meant to ask:
>>>> Actually, what does it mean for a formula to be "disprovable" in an >>>> _inconsistent_ formal system?
>> That there is a proof of its negation.
> So an inconsistent system is also a consistent one then?
Obviously not. Since the question has such an obvious answer, I'm guessing that your intention here is to imply that Alan's answer leads to the absurd conclusion that a system can be simultaneously consistent and inconsistent. It doesn't, of course, but why do you think it does?
Chris Menzel wrote: > On Thu, 29 Jul 2010 08:05:52 -0600, Nam Nguyen <namducngu...@shaw.ca> said: >> Alan Smaill wrote: >>> Nam Nguyen <namducngu...@shaw.ca> writes:
>>>> Sorry for a typo: I meant to ask:
>>>>> Actually, what does it mean for a formula to be "disprovable" in an >>>>> _inconsistent_ formal system? >>> That there is a proof of its negation. >> So an inconsistent system is also a consistent one then?
> Obviously not. Since the question has such an obvious answer, I'm > guessing that your intention here is to imply that Alan's answer leads > to the absurd conclusion that a system can be simultaneously consistent > and inconsistent. It doesn't, of course, but why do you think it does?
Because in a T if A is provable but ~A is "disprovable" then T should be consistent. "Provable" means having a proof and "disprovable" means otherwise, in the context of discussing (in)consistency of a system. And Alan was making the definition for an inconsistent theory where all formulas are supposed to be _provable_ (not disprovable).
Of course one could rename something to anything, but that would be an odd renaming.
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Chris Menzel <cmen...@remove-this.tamu.edu> writes: > On Thu, 29 Jul 2010 08:05:52 -0600, Nam Nguyen <namducngu...@shaw.ca> said: >> Alan Smaill wrote: >>> Nam Nguyen <namducngu...@shaw.ca> writes:
>>>> Sorry for a typo: I meant to ask:
>>>>> Actually, what does it mean for a formula to be "disprovable" in an >>>>> _inconsistent_ formal system?
>>> That there is a proof of its negation.
>> So an inconsistent system is also a consistent one then?
> Obviously not. Since the question has such an obvious answer, I'm > guessing that your intention here is to imply that Alan's answer leads > to the absurd conclusion that a system can be simultaneously consistent > and inconsistent. It doesn't, of course, but why do you think it does?
Probably because he's confusing "disprovable" (which I assume means "refutable") with "not provable".
In fact, here's what he says in reply:
Because in a T if A is provable but ~A is "disprovable" then T should be consistent. "Provable" means having a proof and "disprovable" means otherwise, in the context of discussing (in)consistency of a system.
-- "Customers have come to SCO asking what they can do to respect and help protect the rights of the SCO intellectual property in Linux. SCO has created the Intellectual Property License for Linux in response to these customers needs." -- SCO responds to needs.
Jesse F. Hughes wrote: > Chris Menzel <cmen...@remove-this.tamu.edu> writes:
>> On Thu, 29 Jul 2010 08:05:52 -0600, Nam Nguyen <namducngu...@shaw.ca> said: >>> Alan Smaill wrote: >>>> Nam Nguyen <namducngu...@shaw.ca> writes:
>>>>> Sorry for a typo: I meant to ask:
>>>>>> Actually, what does it mean for a formula to be "disprovable" in an >>>>>> _inconsistent_ formal system? >>>> That there is a proof of its negation. >>> So an inconsistent system is also a consistent one then? >> Obviously not. Since the question has such an obvious answer, I'm >> guessing that your intention here is to imply that Alan's answer leads >> to the absurd conclusion that a system can be simultaneously consistent >> and inconsistent. It doesn't, of course, but why do you think it does?
> Probably because he's confusing "disprovable" (which I assume means > "refutable") with "not provable".
Why was I the one who got confused when a) even you yourself only assumed (not asserted) "disprovable" would mean "refutable" and b) somebody else introduced (CM) or defined (AS) the term here which face-value seems to be ridiculous because the context is in an inconsistent system where *all formulas* are _provable_ by sheer technical definition, or consequences thereof?
> In fact, here's what he says in reply:
> Because in a T if A is provable but ~A is "disprovable" then T > should be consistent. "Provable" means having a proof and > "disprovable" means otherwise, in the context of discussing > (in)consistency of a system.
So, CM still doesn't answer my question above:
>>>>>> Actually, what does it mean for a formula to be "disprovable" in an >>>>>> _inconsistent_ formal system?
and AS' answer wouldn't make much sense in this context of an inconsistent formal system: all formulas would be _both_ provable and disprovable!
-- --------------------------------------------------- Time passes, there is no way we can hold it back. Why, then, do thoughts linger long after everything else is gone? Ryokan ---------------------------------------------------
Nam Nguyen <namducngu...@shaw.ca> writes: > Chris Menzel wrote: >> On Thu, 29 Jul 2010 08:05:52 -0600, Nam Nguyen <namducngu...@shaw.ca> said: >>> Alan Smaill wrote: >>>> Nam Nguyen <namducngu...@shaw.ca> writes:
>>>>> Sorry for a typo: I meant to ask:
>>>>>> Actually, what does it mean for a formula to be "disprovable" in an >>>>>> _inconsistent_ formal system? >>>> That there is a proof of its negation. >>> So an inconsistent system is also a consistent one then?
>> Obviously not. Since the question has such an obvious answer, I'm >> guessing that your intention here is to imply that Alan's answer leads >> to the absurd conclusion that a system can be simultaneously consistent >> and inconsistent. It doesn't, of course, but why do you think it does?
> Because in a T if A is provable but ~A is "disprovable" then T should > be consistent. "Provable" means having a proof and "disprovable" means > otherwise, in the context of discussing (in)consistency of a system. > And Alan was making the definition for an inconsistent theory where all > formulas are supposed to be _provable_ (not disprovable).
Right. In an inconsistent theory, all formulas are provable, and all formulas as disprovable also, in the sense I used above.
> Of course one could rename something to anything, but that would be an odd > renaming.
The term "unprovable" already exists; "disprovable" is normally used as above -- it does not mean the same thing as "unprovable".
Alan Smaill <sma...@SPAMinf.ed.ac.uk> writes: > The term "unprovable" already exists; "disprovable" is normally used > as above -- it does not mean the same thing as "unprovable".
This is indeed standard usage in mathematical logic.
On Jul 29, 7:19 pm, Nam Nguyen <namducngu...@shaw.ca> wrote:
> ... AS' answer wouldn't make much sense in this context of an inconsistent > formal system: all formulas would be _both_ provable and disprovable!
Both provable and disprovable! Why, that's hard to imagine. This suggests that such an "inconsistent" theory would be:
1. lacking in harmony between the different parts or elements; self-contradictory: an inconsistent story. 2. lacking agreement, as one thing with another or two or more things in relation to each other; at variance: a summary that is inconsistent with the previously stated facts. 3. not consistent in principles, conduct, etc.: He's so inconsistent we never know if he'll be kind or cruel.
etc.
Imagine that! A "self-contradictory" theory! We should come up with a name for that, if indeed anyone can demonstrate the possibility of such a thing.
|
