Contradiction or paradox
translogi
What is the fine logical difference between a paradox and a
contradiction?
Can something be a contradiction without being a paradox?
Can something be a paradox without being a contradiction?
Or is a contradiction just a solvable "paradox" (there is a way out of
it)
Hope for a lot of discussion
Aatu Koskensilta
> What is the fine logical difference between a paradox and a
> contradiction?
A contradiction is simply a logically false statement, that is a statement
that is false not because of the way the world happens to be but because
it's not possible for it to be true, e.g. "this post is written by Aatu and
is not written by Aatu".
One of the roles contradictions play in our reasoning is when we show that
some statements can't be simultaneously true. For if we can, from some
statements A_1, ..., A_n, derive a contradiction by a valid argument, we
conclude that at least one of the A_i must be false. As a particular
application, if we know that A, B and C are true, and derive a contradiction
by an argument with A, B, C and D as assumptions, we can conclude that D
must be false.
A paradox is a contradiction that follows from seemingly true premises. For
example, it seems obvious that the following holds for all statements
"A" is true iff A
But if we consider the sentence
(*) This sentence is not true.
We can derive, using apparently obviously correct principles, a paradox: (*)
is true and (*) is not true. The problem, then, is trying to work out which
of the seemingly obvious principles and modes of reasoning are errorneous,
and why.
--
Aatu Koskensilta (aatu.kos...@xortec.fi)
"Wovon man nicht sprechen kann, daruber muss man schweigen"
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus
G. Frege
>
> Getting more and more confused.
>
> What is the fine logical difference between a paradox and a
> contradiction?
>
Well, one might claim that a paradox is a contradiction that follows from
seemingly true "assumption" (i.e. some basic facts which seem to be true).
While on the other hand, from a formal point of view, a /contradiction/ is
just (or may be defined as) a statement of the form
A & ~A
for some sentence/statement (or proposition) A.
>
> Can something be a contradiction without being a paradox?
>
Yes.
If you are dealing with a system of natural deduction, for applying the rule
RAA you regularly deal with contradictions which are no paradoxes. With other
words, it's easy to "rectify" them.
[A] assumption
:
B & ~B
------ RAA
~A
>
> Can something be a paradox without being a contradiction?
>
No, I won't think so. I guess a paradox always has to be something of the
form: there is (happens to be, or whatever) A and ("at the same time") there
is non-A (or: A is not).
>
> Or is a contradiction just a solvable "paradox" (there is a way out of
> it)
>
In a system of natural deduction this is indeed the case (in the sense
explained above).
On the other hand... Consider a /mathematical theory/ based on some AXIOMs.
And assume we can derive from this axioms a contradiction, now THAT would be
_very_ bad, since this could not be "resolved" with an application of RAA
(since an _axiom_ is not just an _assumption_ --- in the sense of a system of
natural deduction). Such a _contradiction_ would prove our system to be
_inconsistent_.
F.
--
E-mail: info<at>simple-line<dot>de
Arturo Magidin
Aatu Koskensilta <aatu.kos...@xortec.fi> wrote:
[...]
>A paradox is a contradiction that follows from seemingly true
premises.
Actually, "paradox" encompasses other notions, does it not?
Merriam-Webster says:
Latin paradoxum, from Greek paradoxon, from neuter of paradoxos
contrary to expectation, from para- + dokein to think, seem -- more
at DECENT
1 : a tenet contrary to received opinion
2 a : a statement that is seemingly contradictory or opposed to common
sense and yet is perhaps true b : a self-contradictory statement
that at first seems true c : an argument that apparently derives
self-contradictory conclusions by valid deduction from acceptable
premises
3 : one (as a person, situation, or action) having seemingly
contradictory qualities or phases
As I understand it, "paradox" refers to statements that seem to
contradict common sense or expectations. It includes the notion you
describe, because in that case we have something that contradicts what
is expected to be true (premises). But it also includes things like
the Banach-Tarski Paradox, which is by no means a "contradiction that
follows from seemingly true premises".
It also includes the "Gilbert-Sullivan Theorem" that someone born on
February 29 will have only had five birthdays by the time he turns 21
years old. A most ingenious paradox indeed...
--
======================================================================
"It's not denial. I'm just very selective about
what I accept as reality."
--- Calvin ("Calvin and Hobbes" by Bill Watterson)
======================================================================
Arturo Magidin
magidin-at-member-ams-org
Aatu Koskensilta
> Actually, "paradox" encompasses other notions, does it not?
Indeed it does. Perhaps most uses are subsumed under the following
formulation: a paradox is a seemingly false statement that nevertheless
follows from commonly accepted or obvious premises. I doubt many people
would call just any statement that is contrary to common beliefs or
knowledge a paradox -- "bananas are planted by aliens from Sirius" does not
strike me as particularly paradoxical -- unless there was also some grounds
for believing the statement. In some cases, as with certain whimsical
paradoxes, these grounds might not amount to an actual argument but simply
rely on creatively reinterpreting the statement.
Thanks for pointing out the deficiency in my explanation.
LauLuna
There are some paradoxes that do not immediately lead to the scheme:
(1) X & -X
but to the scheme:
(2) X <-> -X
Consider the Liar and its kin; consider Russell's, Grelling's, and
more generally any paradox that violates the theorem:
(3) -Ex Ay Rxy <-> -Ryy
Of course, (1) and (2) are equivalent in propositional logic. But I
guess that the fact that we immediately obtain (2) and not (1) makes
sometimes a difference: (2) suggests circularity while (1) does not.
Circularity seems to be the heart of this kind of paradoxes.
Regards
G. Frege
wrote:
>
> (1) X & -X
> (2) X <-> -X
>
> (1) and (2) are equivalent in propositional logic.
>
Right.
One direction ((1) => (2)) is immediate:
P & Q |- P <-> Q
1 (1) P & Q A
2 (2) P A
1 (3) Q 1 &E
1 (4) P -> Q 3 ->I (2)
5 (5) Q A
1 (6) P 1 &E
1 (7) Q -> P 6 ->I (5)
1 (8) P <-> Q 4,7 <->I
Substitution instance: X & -X |- X <-> -X
The other direction ((2) => (1)) is slightly more involved:
X <-> -X |- X & -X
1 (1) X <-> -X A
(2) X v -X TND
3 (3) X A
1 (4) X -> -X 1 <->E
1,3 (5) -X 3,4 ->E
1,3 (6) X & -X 3,5 &I
7 (7) -X A
1 (8) -X -> X 1 <->E
1,7 (9) X 7,8 ->E
1,7 (10) X & -X 7,9 &I
1 (11) X & -X 2,3,6,7,10 vE
Charlie-Boo
wrote:
> On 2007-04-19, translogi wrote:
> > What is the fine logical difference between a paradox and a
> > contradiction?
>
> A contradiction is simply a logically false statement, that is a statement
> that is false not because of the way the world happens to be but because
> it's not possible for it to be true, e.g. "this post is written by Aatu and
> is not written by Aatu".
>
> One of the roles contradictions play in our reasoning is when we show that
> some statements can't be simultaneously true. For if we can, from some
> statements A_1, ..., A_n, derive a contradiction by a valid argument, we
> conclude that at least one of the A_i must be false. As a particular
> application, if we know that A, B and C are true, and derive a contradiction
> by an argument with A, B, C and D as assumptions, we can conclude that D
> must be false.
>
> A paradox is a contradiction that follows from seemingly true premises. For
> example, it seems obvious that the following holds for all statements
>
> "A" is true iff A
>
> But if we consider the sentence
>
> (*) This sentence is not true.
>
> We can derive, using apparently obviously correct principles, a paradox: (*)
> is true and (*) is not true.
Well, the fact of the matter is that it is not both, but rather it is
neither. With this possibility in mind, you can't prove it is both,
only that it is neither.
> The problem, then, is trying to work out which
> of the seemingly obvious principles and modes of reasoning are errorneous,
> and why.
In the Liar in particular, and many paradoxes in general, the problem
is not with the reasoning, but rather with the assumptions made of the
system. All paradoxes begin with contradictory assumptions. This
includes both the self-referential type paradoxes (Russell, Liar) and
the others (e.g. Raven and Unexpected Examination.)
C-B
> --
> Aatu Koskensilta (aatu.koskensi...@xortec.fi)
Charlie-Boo
> On 19 Apr 2007 05:48:09 -0700, translogi <wilem...@googlemail.com> wrote:
>
>
>
> > Getting more and more confused.
>
> > What is the fine logical difference between a paradox and a
> > contradiction?
>
> Well, one might claim that a paradox is a contradiction that follows from
> seemingly true "assumption" (i.e. some basic facts which seem to be true).
>
> While on the other hand, from a formal point of view, a /contradiction/ is
> just (or may be defined as) a statement of the form
>
> A & ~A
>
> for some sentence/statement (or proposition) A.
No, it is anything equivalent to FALSE e.g. X<3 & x >10 is a
contradiction and equivalent to FALSE, but not of that form. (Of
course, being equivalent to FALSE we can show it equvalent to other
assertions of the form A & ~A but that misses the point that
inconsistency is not just A & ~A.)
C-B
Charlie-Boo
> On 19 Apr 2007 12:43:03 -0700, LauLuna <laureanol...@yahoo.es>
> wrote:
>
>
>
> > (1) X & -X
> > (2) X <-> -X
>
> > (1) and (2) are equivalent in propositional logic.
>
> Right.
>
> One direction ((1) => (2)) is immediate:
>
> P & Q |- P <-> Q
>
> 1 (1) P & Q A
> 2 (2) P A
> 1 (3) Q 1 &E
> 1 (4) P -> Q 3 ->I (2)
> 5 (5) Q A
> 1 (6) P 1 &E
> 1 (7) Q -> P 6 ->I (5)
> 1 (8) P <-> Q 4,7 <->I
>
> Substitution instance: X & -X |- X <-> -X
>
> The other direction ((2) => (1)) is slightly more involved:
>
> X <-> -X |- X & -X
>
> 1 (1) X <-> -X A
> (2) X v -X TND
> 3 (3) X A
You'll have to do better than that, Frege. Each line in a formal
proof must be justified as being an axiom, premise of the theorem
being proven, or deduced from earlier lines via a rule of inference.
You didn't do that for line (3).
Can you fix it?
C-B
translogi
>
> - Show quoted text -- Hide quoted text -
>
> - Show quoted text -
Dear Charlie Boo
Did you ever study natural deduction?
like 3 and line 7 are assumptions
line 11 discharges them both
that is how vE works
See one of the many books on natural deduction.
philn...@yahoo.com
>
> - Show quoted text -
CRITICISMS FROM INTERNAL CONSISTENCY--BROWNIAN MOTION AND THE
RELATIVITY OF SIMULTANEITY
Still another criticism has to do with the mathematics Einstein
adopted in order to express special relativity. Unaware of the
polemics involved in the response to Cantorian set theory, he
enthusiastically embraced Poincare's approach in SCIENCE AND
HYPOTHESIS. He was unaware that Poincare's goal in this book was to
develop an approach to mathematics which would "solve" or "avoid" the
supposed paradoxes of set theory.
The polemical position developed--now called natural mathematics (see
P. Maddy, NATURALISM IN MATHEMATICS)--asserts that mathematical
formulations are inherently anomalous; the evidence of this is that
they generate paradoxes. Therefore, the idea that mathematics is an
aspect of human perception, must be made a part of mathematical
formulations even if it plays no internally consistent role in any
natural mathematical formulation. According to Howard and Stachel in
their recent book on Einstein's formative years (John Stachel is
director of the Center for Einstein Studies at Boston University),
Einstein made a “careful reading” of Poincare's formulation of this
point of view.
Poincare believed that “the mind has a direct intuition of this power
['proof by recurrence' or 'mathematical induction'], and experiment
can only be for [the mind] an opportunity of using it, and thereby of
becoming conscious of it.” In geometry “we are brought to [the concept
of space] solely by studying the laws by which…[muscular] sensations
succeed one another.” This idea of “succession” was vital if the
“standstill” to which the “paradoxes” had brought mathematics, was to
be overcome.
Natural mathematics gained widespread acceptance before Einstein came
to it, and when he adopted its precepts, it caused him problems, even
before the formulation of special relativity. As indicated in the
Brown and Stachel book, it was employed in Einstin's 1905 paper on
Brownian motion, with disturbing results: “Einstein begins with an
assumption whose status is still problematic and troubled his
contemporaries: that there exists ‘a time interval τ, which shall be
very small compared with observable time intervals but still so large
that all motions performed by a particle during two consecutive time
intervals τ may be considered as mutually independent events….” As the
author of this passage notes, “[t]his is essentially a very strong
Markov postulate. Einstein makes no attempt to justify it….[W]here
mathematics ends and physics begins is far from clear….”
>From here, Einstein went on to apply natural mathematics to his
formulation of the relativity of simultaneity (here the geometric
formulation in RELATIVITY, where its use is particularly clear):
Are two events (e.g. the two strokes of lightning A and B) which are
simultaneous with reference to the railway embankment also
simultaneous relatively to the train? We shall show directly that the
answer must be in the negative. When we say that the lightning strokes
A and B are simultaneous with respect to be embankment, we mean: the
rays of light emitted at the places A and B, where the lightning
occurs, meet each other at the mid-point M of the length AB of the
embankment. But the events A and B also correspond to positions A and
B on the train. Let M1 be the mid-point of the distance AB on the
traveling train. Just when the flashes (as judged from the embankment)
of lightning occur, this point M1 naturally coincides with the point M
but it moves…with the velocity…of the train.
The criticism is that the term “naturally coincides” has no meaning
and leads to logical problems. Einstein does not define it. If it is
dropped, the assumption of two Cartesian coordinate systems leads to a
contradictory conclusion of only one. The idea is that if two parallel
coordinate systems coincide at one point, they coincide at all points
and are one coordinate system, not two. So far, this criticism has not
been overcome.
The natural mathematics justification for the use of the term is that
it “allows” one point to “succeed” another, and so permits the notion
of the relativity of simultaneity to go forward. The criticism is that
that does not resolve the logical problem of the use of "natural"
coincidence in the argument.
Charlie-Boo
No "Just following orders" defense, please. Axiomatic theorem proving
is the presentation of a linear representation of a proof tree, where
each node is an axiom at a leaf or a rule applied to its children, and
the root is the theorem. Do you agree?
I ask again, can you make it in that format? Are you in fact being
superfluous when you go outside of the classic model?
You are using reductio ad absurdum to produce a proof within a proof.
Proof trees can be transformed because they are not the normal form of
clauses.
If you don't know what I mean, please don't jump to the conclusion
that it is meaningless nor be afraid to ask. I can give you examples
of transforming a proof tree.
C-B
> See one of the many books on natural deduction.- Hide quoted text -
Fuckwit
wrote:
>
> [...] Axiomatic theorem proving is the presentation of a linear
> representation of a proof tree, where each node is an axiom at a
> leaf or a rule applied to its children, and the root is the
> theorem. Do you agree?
>
G. Frege
wrote:
>>
>> Did you ever study natural deduction?
>> like 3 and line 7 are assumptions
>> line 11 discharges them both
>> that is how vE works
>>
> No "Just following orders" defense, please. Axiomatic theorem proving
> is [bla bla]
>
Look, Charlie, most systems of natural deduction (for PC/FOPL) do not
have any _axioms_. (Instead of axioms they have _rules_.)
Hence the question "Did you ever study natural deduction?" is indeed
relevant here. Did you?
Note, that your question
>>>
>>> Can you fix it?
>>>
is rather idiotic, since there is nothing to fix, in the first place.
>
> I ask again, can you make it in that format?
>
Sure I _could_. But in this case I would have to prove the theorem in
_a different_ system (i.e. an axiomatic system). So what?
>>
>> See one of the many books on natural deduction.
>>
Please do!
G. Frege
>
> Note, that your question
>
> "Can you fix it?"
>
> is rather idiotic, since there is nothing to fix, in the
> first place.
>
With other words, there's nothing wrong with the following proofs.
P & Q |- P <-> Q
Proof:
1 (1) P & Q A (=Assumption)
2 (2) P A (=Assumption)
1 (3) Q 1 &E
1 (4) P -> Q 3 ->I (2)
5 (5) Q A
1 (6) P 1 &E
1 (7) Q -> P 6 ->I (5)
1 (8) P <-> Q 4,7 <->I
Substitution instance ("X" for "P" and "-X" for "Q") gives:
X & -X |- X <-> -X.
The other direction is slightly more involved:
X <-> -X |- X & -X
Proof:
1 (1) X <-> -X A (=Assumption)
(2) X v -X TND (Theorem)
3 (3) X A (=Assumption)
1 (4) X -> -X 1 <->E
1,3 (5) -X 3,4 ->E
1,3 (6) X & -X 3,5 &I
7 (7) -X A
1 (8) -X -> X 1 <->E
1,7 (9) X 7,8 ->E
1,7 (10) X & -X 7,9 &I
1 (11) X & -X 2,3,6,7,10 vE
Hence: X & -X -||- X <-> -X.
F.
P.S.
Of course, there's a much simpler proof for
X & -X |- X <-> -X.
Proof:
1 (1) ~(X <-> -X) A (=Assumption)
2 (2) X & -X A (=Assumption)
2 (3) ~~(X <-> -X) 1,2 RAA
2 (4) X <-> -X 3 ~~E
or even (if we have the rules EFQ at our disposal):
1 (1) X & -X A (=Assumption)
1 (2) X <-> -X 1 EFQ
translogi
If you realy want to do it that way:
Right from the master himself
Principa Mathematica, Vol 1, pag 113 theorem *3.44
I don't understand the principa Mathematica but it looks OK
Maybe you can explain it to me.
* 3.44 |- :. q > p . r > p .>: q v r . > p
> represents the horseshoe (not an ascii symbol)
I saw an earlier post that would give you a link to fully worked out
proofs of the principa mathematica but i couldn't find it anymore
Sorry.
G. Frege
wrote:
>
> I don't understand the Principa Mathematica but it looks OK.
> Maybe you can explain it to me.
>
Why bother with an axiomatic system when the same result can be
achieved in a much simpler way in a system of natural deduction?
(Given the well known fact that |-_PM A iff |-_ND A for any wff A
which can be formulated in both systems; modulo some notational
differences.)
Hence the only relevant question still is:
"Did you ever study natural deduction [Charlie-Boo]?"
translogi
> On 26 Apr 2007 08:46:56 -0700, translogi <wilem...@googlemail.com>
> wrote:
>
>
>
> > I don't understand the Principa Mathematica but it looks OK.
> > Maybe you can explain it to me.
>
> Why bother with an axiomatic system when the same result can be
> achieved in a much simpler way in a system of natural deduction?
>
> (Given the well known fact that |-_PM A iff |-_ND A for any wff A
> which can be formulated in both systems; modulo some notational
> differences.)
>
> Hence the only relevant question still is:
>
> "Did you ever study natural deduction [Charlie-Boo]?"
>
> F.
Maybe he [Charlie Boo] is doing that right now
Would be good for him.
Charlie-Boo
> On 24 Apr 2007 12:16:42 -0700, Charlie-Boo <shymath...@gmail.com>
> wrote:
>
>
>
> > [...] Axiomatic theorem proving is the presentation of a linear
> > representation of a proof tree, where each node is an axiom at a
> > leaf or a rule applied to its children, and the root is the
> > theorem. Do you agree?
>
> "Did you ever study natural deduction?"
Your example alone illustrates the salient feature: more rules than
classic axiomatic theorem-proving. You do believe in Occam's Razor,
don't you (as well as it's enhanced version Occam/C-B's Razor)?
Adding additional (superfluous) rules (primitives) is a waste of time
- ask Occam!
C-B
Charlie-Boo
> On 24 Apr 2007 12:16:42 -0700, Charlie-Boo <shymath...@gmail.com>
> wrote:
>
>
>
> >> Did you ever study natural deduction?
> >> like 3 and line 7 are assumptions
> >> line 11 discharges them both
> >> that is how vE works
>
> > No "Just following orders" defense, please. Axiomatic theorem proving
> > is [bla bla]
>
> Look, Charlie, most systems of natural deduction (for PC/FOPL) do not
> have any _axioms_. (Instead of axioms they have _rules_.)
The example illustrates reality. I refer to the example as being
redundant and superfluous.
How many rules do we have as to what constitutes a good
formalization? Computer Programmers have tons, and I often apply them
to the formalizations of Mathematics/Computer Science that I develop
(all under the umbrella of CBL) - but what do Mathematicians have? As
they don't have the sense to use the rules that laboring Computer
Programmers have developed, they are left with just one so far:
Occam's Razor.
If you ignore Occam, what is your criteria for evaluating a system?
And how can you value the use of the example with additional rules
being needed?
QUESTION: Can you construct the proof without the assumption within a
proof being used?
C-B
> Hence the question "Did you ever study natural deduction?" is indeed
> relevant here. Did you?
Why would anyone's state of mind be relevant to anything outside of
Psychology or Criminal Law?
You're wrong - and it is arguably one of the most well-established
fallacies in logic: Attacking the Messenger.
"Tuck in your shirt-tail!"
> Note, that your question
>
> >>> Can you fix it?
>
> is rather idiotic, since there is nothing to fix, in the first place.
>
>
>
> > I ask again, can you make it in that format?
>
> Sure I _could_. But in this case I would have to prove the theorem in
> _a different_ system (i.e. an axiomatic system). So what?
It is a proper subset of what you like. You realize of course that
professors like to introduce new systems to justify grant money
requests, whereas it is a violation of Occam's Razor to go outside of
exisiting Mathematics if at all possible to avoid. And guess what?
It's possible to avoid.
How would you like a new operator for adding 37? And teach it to all
the children and practice using it? Why or why not?
> >> See one of the many books on natural deduction.
What does the above line prove?
Get you head out and smell the roses.
If you have a point, make it - substantiate!
You have no technical points - only your forte of misusing references
- in a number of different ways:
1. Some idiot redefining "Turing Machine" invalidates existing
conclusions about Turing Machines.
2. References should be given without mention of where the material
claimed can be found, much less quoting and showing HOW it actually
does accomplish the point.
3. Quoting a book title instead of making any kind of technical point.
C-B
Charlie-Boo
In the midst of a discussion as to the merits of Occam's Razor you
quote a 1,000 page formalization? GAD! That is the worst
formalization ever developed!!!
ASK OCCAM!!!!
Smart formalizations discover the small number of primitives and
express everything in terms of them. Stupid ones introduce new
primitives along the way and take up 1,000 pages doing so.
My 1 page computer program can generate your 1,000 pages of rules.
C-B
> I don't understand the principa Mathematica but it looks OK
*cringe*
> Maybe you can explain it to me.
>
> * 3.44 |- :. q > p . r > p .>: q v r . > p
>
> > represents the horseshoe (not an ascii symbol)
>
> I saw an earlier post that would give you a link to fully worked out
> proofs of the principa mathematica but i couldn't find it anymore
> Sorry.- Hide quoted text -
William Hale
Charlie-Boo <shyma...@gmail.com> wrote:
> On Apr 24, 6:52 pm, G. Frege <nomail@invalid> wrote:
> > On 24 Apr 2007 12:16:42 -0700, Charlie-Boo <shymath...@gmail.com>
> > wrote:
> >
> >
> >
> > >> Did you ever study natural deduction?
> > >> like 3 and line 7 are assumptions
> > >> line 11 discharges them both
> > >> that is how vE works
> >
> > > No "Just following orders" defense, please. Axiomatic theorem proving
> > > is [bla bla]
> >
> > Look, Charlie, most systems of natural deduction (for PC/FOPL) do not
> > have any _axioms_. (Instead of axioms they have _rules_.)
>
> The example illustrates reality. I refer to the example as being
> redundant and superfluous.
>
> How many rules do we have as to what constitutes a good
> formalization? Computer Programmers have tons, and I often apply them
> to the formalizations of Mathematics/Computer Science that I develop
> (all under the umbrella of CBL) - but what do Mathematicians have? As
> they don't have the sense to use the rules that laboring Computer
> Programmers have developed, they are left with just one so far:
> Occam's Razor.
Nonsense.
> If you ignore Occam, what is your criteria for evaluating a system?
> And how can you value the use of the example with additional rules
> being needed?
>
> QUESTION: Can you construct the proof without the assumption within a
> proof being used?
>
> C-B
>
> > Hence the question "Did you ever study natural deduction?" is indeed
> > relevant here. Did you?
>
> Why would anyone's state of mind be relevant to anything outside of
> Psychology or Criminal Law?
If you don't know about natural deduction, do you think you are can
discuss its merits and faults. I believe that you actually think you
can. But, your lack of knowledge of the natural deduction approach makes
our explaining its merits to you almost impossible since you cannot
follow what is being said (without us writing a treatise giving the
background of the natural deduction approach).
> You're wrong - and it is arguably one of the most well-established
> fallacies in logic: Attacking the Messenger.
>
> "Tuck in your shirt-tail!"
>
> > Note, that your question
> >
> > >>> Can you fix it?
> >
> > is rather idiotic, since there is nothing to fix, in the first place.
> >
> >
> >
> > > I ask again, can you make it in that format?
> >
> > Sure I _could_. But in this case I would have to prove the theorem in
> > _a different_ system (i.e. an axiomatic system). So what?
>
> It is a proper subset of what you like. You realize of course that
> professors like to introduce new systems to justify grant money
> requests, whereas it is a violation of Occam's Razor to go outside of
> exisiting Mathematics if at all possible to avoid. And guess what?
> It's possible to avoid.
>
> How would you like a new operator for adding 37? And teach it to all
> the children and practice using it? Why or why not?
I assume that you are saying that there is no need to have a different
way than the standard way for adding a number like 37 to another. I
don't agree with this.
Look at the following link to a you-tube video for a different way to
mulitply two numbers:
http://www.youtube.com/watch?v=kZKOPKIHsrc
I think it might be worth while teaching that to some children and let
them practice using it. I believe you are saying that only the "best"
way should be taught and no other way. What a misunderstanding of what
education is.
Charlie-Boo
> In article <1178047736.928009.241...@c35g2000hsg.googlegroups.com>,
How do you define this threshold? How do you detect it? How do you
know that you have passed this threshold? You need to justify
yourself if you are going to demand that others justify themselves.
How can you justify yourself?
That is just Conservative BS. Any reference to any particular person
is baby-shit.
It's not about natural deduction. It is about a proof that introduces
an assumption and later refutes it, which is not a process necessary
in classic axiomatic theorem-proving.
I pointed out that the particular proof is inferior by Occam's Razor.
Talking about other proofs and other aspects of the system and other
systems has nothing to do with it. My statement refers to the worth
of this one proof.
Now, if natural deduction cannnot produce anything other than inferior
proofs, then we can draw additional conclusions.
Can you express this proof without using that method? Then wouldn't
the proof be better if it used only classic logic and not this method
of ad hoc assumptions? Do you believe in Occam's Razor?
C-B
Charlie-Boo
> In article <1178047736.928009.241...@c35g2000hsg.googlegroups.com>,
>
>
>
>
>
No, an operator that means to add 37 e.g. x@ means x+37. Shall we add
@ to the family of + - * and / ?
> Look at the following link to a you-tube video for a different way to
> mulitply two numbers:
>
> http://www.youtube.com/watch?v=kZKOPKIHsrc
You are on a different planet.
> I think it might be worth while teaching that to some children and let
> them practice using it. I believe you are saying that only the "best"
> way should be taught and no other way. What a misunderstanding of what
> education is.
>
>
>
> > > >> See one of the many books on natural deduction.
>
> > What does the above line prove?
>
> > Get you head out and smell the roses.
>
> > If you have a point, make it - substantiate!
>
> > You have no technical points - only your forte of misusing references
> > - in a number of different ways:
>
> > 1. Some idiot redefining "Turing Machine" invalidates existing
> > conclusions about Turing Machines.
>
> > 2. References should be given without mention of where the material
> > claimed can be found, much less quoting and showing HOW it actually
> > does accomplish the point.
>
> > 3. Quoting a book title instead of making any kind of technical point.
>
> > C-B
>
> > > Please do!
>
> > > F.
>
> > > --
>
William Hale
Charlie-Boo <shyma...@gmail.com> wrote:
Level zero.
> How do you detect it?
Everyone is at least level zero.
> How do you know that you have passed this threshold?
Everyone has passed this threshold.
> You need to justify yourself if you are going to demand that others justify themselves.
I don't demand that others justify themselves.
> How can you justify yourself?
You are saying things other than that a proof by natural deduction is
inferior by Occam's Razor. This is what I am trying to point out.
In particular, you said that you wanted to see the complete formal,
axiomatic proof in natural deduction for the proof presented; but, the
natural deduction proof was complete as given. Posters were pointing
this out to you. They were not discussing whether natural deduction is
better or worse than CBL. You want to reduce every discussion to the
claim that CBL is better than any other logic system. I don't believe
that every statement is equivalent to the latter.
For another example, you said that the Metamath system can prove that
subtraction is associative. Yet, you drop out of this discussion when we
get to the heart of the matter. If you don't want to read up on the
Metamath system, that is fine. But, if you are going to discuss whether
subtraction is associative can be proved in the Metamath system, then
you need to discuss that assertion, not the assertion that Metamath is
an inferior system since it is too complex. Otherwise, you are
discussing a different assertion, namely, that Metamath is an inferior
system. Posters are discussing the former assertion, not the latter.
> That is just Conservative BS. Any reference to any particular person
> is baby-shit.
You are saying that books and articles claim things, but when you read
them you find that the claims are not there or are not justified.
You are making the claim: don't we have to refer to you to discuss it?
> It's not about natural deduction. It is about a proof that introduces
> an assumption and later refutes it, which is not a process necessary
> in classic axiomatic theorem-proving.
I thought the (sub-)discussion was about what constitutes a natural
deduction proof. You want to tranform the discussion from a natual
deduction proof to a discucsion of a proof that introduces an assumption
and later refutes it to discussion of whether it is an inferior proof.
This transformation of yours is not clear in what you write. Posters are
discussing what constitute a natural deduction proofs; they are not
discussing whether natural deduction proofs are inferior to axiomatic
proofs or CBL proofs.
> I pointed out that the particular proof is inferior by Occam's Razor.
> Talking about other proofs and other aspects of the system and other
> systems has nothing to do with it. My statement refers to the worth
> of this one proof.
Maybe I should reread what you wrote, but I did not get the impression
that you were discussing the worth of a natural deduction proof.
>
> Now, if natural deduction cannnot produce anything other than inferior
> proofs, then we can draw additional conclusions.
Yes.
> Can you express this proof without using that method?
Yes.
> Then wouldn't the proof be better if it used only classic logic and not this
> method of ad hoc assumptions?
Your definition of "better" is not my definition of "better".
> Do you believe in Occam's Razor?
Not in the way you are using it.
Charlie-Boo
> Getting more and more confused.
>
> What is the fine logical difference between a paradox and a
> contradiction?
>
>
>
> it)
>
Not much discussion is needed because the answer is simple. However,
surprisingly (paradoxically?) a lot of discussion ensues when the
solution is presented.
The Fundamental Proof of Paradox reaches an inconsistency (|-false)
from a system with 5 properties:
1. Consistency (CONS)
2. Completeness (COMP)
3. Self-Representation (SELF)
4. Negation (NEG)
5. Substitution (SUB)
Each of these often holds and is valuable. However, the "paradox" is
that we cannot achieve all 5. Thus Paradox is a set of conditions
such that:
1. Each is easy, useful and frequent.
2. Together they are impossible.
This is the fundamental definition of Paradox.
(I can show how to apply these 5 properties to any branch of Computer
Science: Set Theory, Theory of Computation, Recursion Theory,
Incompleteness in Logic (proof theory), Axiomatic Systems, Program
Systhesis, Paradoxes, etc.)
E.g. Program Synthesis is X # I / YES from which we derive the Program
Synthesis axioms and rules. Recursion Theory if X # X / YES, Set
Theory is X / SE etc.
C-B
translogi
How about prooftheory then and what do you mean (exactly ) with
1. Consistency (CONS)
2. Completeness (COMP)
3. Self-Representation (SELF)
4. Negation (NEG)
and
5. Substitution (SUB
Charlie-Boo
> On 26 Apr 2007 08:46:56 -0700, translogi <wilem...@googlemail.com>
> wrote:
>
>
>
> > I don't understand the Principa Mathematica but it looks OK.
> > Maybe you can explain it to me.
>
> Why bother with an axiomatic system when the same result can be
> achieved in a much simpler way in a system of natural deduction?
Occam
C-B
MoeBlee
> On Apr 26, 12:23 pm, G. Frege <nomail@invalid> wrote:
> > Why bother with an axiomatic system when the same result can be
> > achieved in a much simpler way in a system of natural deduction?
>
> Occam
Occam; you mock him.
MoeBlee
Charlie-Boo
Good choice. As this is a metamathematical result we will need a
Computationally Based Logic to express and prove the necessary facts,
as opposed to Propositionally Based Logics (e.g. Predicate Calculus)
which are unsuitable for formalizing metamathematics. (Nonetheless,
mathematicians routinely make the mistake of using Predicate Calculus
in an attempt to formalize Set Theory, a branch of metamathematics,
creating a horrible mess like ZFC for a very simple concept, the
notion of a set.)
Have you used a Computationally Based Logic before?
I use CBL, which is somewhat of a de facto standard for
Computationally Based Logics. The primitive assertion "mathematical
object M in system Q calculates mathematical process P" is formalized
as the expression M#P/Q. In the simplest case, P is a one-place
relation and Q is a two-place relation. This means that P =Q(M) that
is for all (a): P(a) = Q(M,a). Also P/Q means that there is an M such
that M#P/Q.
For example, if Q(a,b) iff Program a halts yes on input b, then P/Q
means that P is recursively enumerable. Do you see how to define Q to
make the assertion that P is expressible in some particular Logic?
That it is representable? That there is a set corresponding to P?
(Already we see the power of CBL. These primitive, useful notions -
r.e., expressible, representable, etc. - are not even formally
represented and manipulated in the published literature, while in CBL
they are all very simple expressions in a general system that
formalizes all of them.)
C-B
Charlie-Boo
Jesse F. Hughes
> I use CBL, which is somewhat of a de facto standard for
> Computationally Based Logics.
Is it? Keen. Who uses it besides you?
--
Jesse F. Hughes
"I'm ruler", said Yertle, "of all that I see.
But I don't see enough. That's the trouble with me."
-- Yertle the Turtle, by Dr. Suess
MoeBlee
> Charlie-Boo <shymath...@gmail.com> writes:
> > I use CBL, which is somewhat of a de facto standard for
> > Computationally Based Logics.
>
> Is it? Keen. Who uses it besides you?
I use it all the time. For basic gardening tasks, cleaning out vents,
removing carpet stains, and many other household chores...nothing
works like CBL. Sold in the big red bottle, that's "CBL", available at
stores everywhere!
MoeBlee
MoeBlee
> > > Occam
>
> > Occam; you mock him.
>
> See e.g.http://groups.google.com/group/sci.logic/msg/2361573a17f1dab6
I click on that link only to find yet more of your gobbledegook. I
guess that's fair though. A fair price I should pay for posting a
silly near-rhyme.
MoeBlee
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > I use CBL, which is somewhat of a de facto standard for
> > Computationally Based Logics.
>
> Is it? Keen. Who uses it besides you?
It is used to derive the shortest, simplest proof of Rosser's
extension to Godel's theorems published. If this were true, would
that be significant in of itself?
C-B
Charlie-Boo
How much space would it take for you to prove Rosser's 1936 extension
to Godel's theorems?
C-B
> MoeBlee
Charlie-Boo
> On May 17, 7:53 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > Occam
>
> > > Occam; you mock him.
>
> > See e.g.http://groups.google.com/group/sci.logic/msg/2361573a17f1dab6
>
> I click on that link only to find yet more of your gobbledegook.
What do you not understand?
C-B
MoeBlee
Nevermind that. What is truly impressive is how wonderfully CBL works
to clean stubborn dirt buildup in bathroom and kitchen tile grout.
CBL...in the big red bottle...available at stores everywhere!
MoeBlee
Charlie-Boo
> On May 17, 2:35 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>
>
>
> > On May 17, 2:50 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > On May 17, 8:17 am, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
>
> > > > Charlie-Boo <shymath...@gmail.com> writes:
> > > > > I use CBL, which is somewhat of a de facto standard for
> > > > > Computationally Based Logics.
>
> > > > Is it? Keen. Who uses it besides you?
>
> > > I use it all the time. For basic gardening tasks, cleaning out vents,
> > > removing carpet stains, and many other household chores...nothing
> > > works like CBL. Sold in the big red bottle, that's "CBL", available at
> > > stores everywhere!
>
> > How much space would it take for you to prove Rosser's 1936 extension
> > to Godel's theorems?
>
> Nevermind that.
That's a shame. This is the sci.logic group.
C-B
> What is truly impressive is how wonderfully CBL works
> to clean stubborn dirt buildup in bathroom and kitchen tile grout.
> CBL...in the big red bottle...available at stores everywhere!
>
> MoeBlee- Hide quoted text -
MoeBlee
> On May 17, 5:42 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
>
>
>
>
> > On May 17, 2:35 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > On May 17, 2:50 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > > On May 17, 8:17 am, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
>
> > > > > Charlie-Boo <shymath...@gmail.com> writes:
> > > > > > I use CBL, which is somewhat of a de facto standard for
> > > > > > Computationally Based Logics.
>
> > > > > Is it? Keen. Who uses it besides you?
>
> > > > I use it all the time. For basic gardening tasks, cleaning out vents,
> > > > removing carpet stains, and many other household chores...nothing
> > > > works like CBL. Sold in the big red bottle, that's "CBL", available at
> > > > stores everywhere!
>
> > > How much space would it take for you to prove Rosser's 1936 extension
> > > to Godel's theorems?
>
> > Nevermind that.
>
> That's a shame. This is the sci.logic group.
And you play your role in it to perfection.
MoeBlee
MoeBlee
> On May 17, 2:55 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > On May 17, 7:53 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > > Occam
>
> > > > Occam; you mock him.
>
> > > See e.g.http://groups.google.com/group/sci.logic/msg/2361573a17f1dab6
>
> > I click on that link only to find yet more of your gobbledegook.
>
> What do you not understand?
Why you don't just get yourself a proper understanding of the basics
of mathematical logic.
MoeBlee
Charlie-Boo
And you claim that what I say doesn't make sense?
Charlie-Boo
Great people talk about ideas, average people talk about things, and
small people talk about people.
I like the idea of a general axiomatization of Computer Science.
C-B
> MoeBlee
MoeBlee
> On May 17, 6:33 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
>
>
>
>
> > On May 17, 2:36 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > On May 17, 2:55 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > > On May 17, 7:53 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > > > > Occam
>
> > > > > > Occam; you mock him.
>
> > > > > See e.g.http://groups.google.com/group/sci.logic/msg/2361573a17f1dab6
>
> > > > I click on that link only to find yet more of your gobbledegook.
>
> > > What do you not understand?
>
> > Why you don't just get yourself a proper understanding of the basics
> > of mathematical logic.
>
> Great people talk about ideas, average people talk about things, and
> small people talk about people.
What you just said is statement about people.
> I like the idea of a general axiomatization of Computer Science.
What you just said is a statement about a particular person - not
surprisingly, yourself.
MoeBlee
Jesse F. Hughes
> On May 17, 11:17 am, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > I use CBL, which is somewhat of a de facto standard for
>> > Computationally Based Logics.
>>
>> Is it? Keen. Who uses it besides you?
>
> It is used to derive the shortest, simplest proof of Rosser's
> extension to Godel's theorems published. If this were true, would
> that be significant in of itself?
Yeah, that would be swell. If true.
But that is irrelevant. You said it was "somewhat of a de facto
standard for Computationally Based Logics".
Surely you agree that this suggests someone else uses CBL besides you,
yes? Who might that be?
--
Jesse F. Hughes
"Anything was possible last night. That was the trouble with last
nights. They were always followed by this mornings."
-- Terry Pratchett, /Small Gods/
G. Frege
wrote:
>>
>> Why bother with an axiomatic system when the same result can be
>> achieved in a much simpler way in a system of natural deduction?
>>
> Occam
>
Huh?! You know you are an idiot, C-B?
But right, I might "answer" /Gentzen/.
Does this help? (I guess not.)
"Ich wollte zunächst einmal einen Formalismus aufstellen,
der dem wirklichen Schließen möglichst nahe kommt. So
ergab sich ein 'Kalkül des natürlichen Schließens'."
(First I wished to construct a formalism that comes as
close as possible to actual reasoning. Thus arose a
"calculus of natural deduction".)
— Gerhard Gentzen, Untersuchungen über das logische
Schließen (Mathematische Zeitschrift 39, pp.176-210,
1935)
See:
http://en.wikipedia.org/wiki/Natural_deduction
MoeBlee
> And you claim that what I say doesn't make sense?
Most of what you say about mathematical logic is either incorrect,
misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
That you believe any of it is a testament to the power of conviction.
MoeBlee
G. Frege
wrote:
>>
>> And you claim that what I say doesn't make sense?
>>
> Most of what you say about mathematical logic is either incorrect,
> misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
>
I second that.
Once he claimed that he was the first to discover a /Quine atom/!
:-)
Charlie-Boo
> On May 17, 4:26 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>
>
>
> > On May 17, 6:33 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > On May 17, 2:36 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > On May 17, 2:55 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > > > On May 17, 7:53 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > > > > > Occam
>
> > > > > > > Occam; you mock him.
>
> > > > > > See e.g.http://groups.google.com/group/sci.logic/msg/2361573a17f1dab6
>
> > > > > I click on that link only to find yet more of your gobbledegook.
>
> > > > What do you not understand?
>
> > > Why you don't just get yourself a proper understanding of the basics
> > > of mathematical logic.
>
> > Great people talk about ideas, average people talk about things, and
> > small people talk about people.
>
> What you just said is statement about people.
the set/element distinction in in play
> > I like the idea of a general axiomatization of Computer Science.
>
> What you just said is a statement about a particular person - not
> surprisingly, yourself.
Because I am the only person to have axiomatized Computer Science?
That's true. They don't even claim to have. And they'd have to first
axiomatize several branches (e.g. Theory of Computation, Recursion
Theory, Program Synthesis, et. al.) in order to build that higher
level of abstraction. I don't think anything beyond Propositional
Calculus (and some attempts at Predicate Calculus) have been
axiomatized (outside of Computationally Based Logics.) Can you give
any counterexamples?
C-B
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On May 17, 11:17 am, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> > I use CBL, which is somewhat of a de facto standard for
> >> > Computationally Based Logics.
>
> >> Is it? Keen. Who uses it besides you?
>
> > It is used to derive the shortest, simplest proof of Rosser's
> > extension to Godel's theorems published. If this were true, would
> > that be significant in of itself?
> Yeah, that would be swell. If true.
How about "If a logic is both consistent and complete, then it's
unprovable sentences coincide with its refutable sentences, but the
latter is recursively enumerable while the former is not."?
(a) Not a proof of Rosser 1936. Reason: ____
(b) Not the shortest. Giver shorter: ____
(c) Not derived using CBL. Problem with CBL derivation: ____
C-B
Charlie-Boo
> On 15 May 2007 19:45:42 -0700, Charlie-Boo <shymath...@gmail.com>
> wrote:
> >> Why bother with an axiomatic system when the same result can be
> >> achieved in a much simpler way in a system of natural deduction?
>
> > Occam
>
> Huh?! You know you are an idiot, C-B?
>
> But right, I might "answer" /Gentzen/.
>
> Does this help? (I guess not.)
>
> "Ich wollte zunächst einmal einen Formalismus aufstellen,
> der dem wirklichen Schließen möglichst nahe kommt. So
> ergab sich ein 'Kalkül des natürlichen Schließens'."
>
> (First I wished to construct a formalism that comes as
> close as possible to actual reasoning. Thus arose a
> "calculus of natural deduction".)
My dear Mr. Frege, yet again you are confused - as well as continue
abusing the practice of citing the literature. (You quote only a
personal opinion - more politics.) The question regarded a single
proof and its use of an assumption within the proof. You are
confusing the proof with the system.
C-B
> - Gerhard Gentzen, Untersuchungen über das logische
Charlie-Boo
Yet why have you no examples?
When did I every say anything along the lines of "This is the
sci.logic group and you play your role in it to perfection."?
C-B
> MoeBlee
Charlie-Boo
> On 17 May 2007 16:49:19 -0700, MoeBlee <jazzm...@hotmail.com>
> wrote:
>
>
>
> >> And you claim that what I say doesn't make sense?
>
> > Most of what you say about mathematical logic is either incorrect,
> > misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
>
> I second that.
>
> Once he claimed that he was the first to discover a /Quine atom/!
> :-)
Defining Q to be Q={Q} no more constructs a Quine atom than defining N
to be a counter-example to Goldbach's Conjecture constructs a counter-
example.
How would you construct such a set? My solution is the first Google
match on Quine Atom.
http://cs.nyu.edu/pipermail/fom/2002-September/005844.html
C-B
G. Frege
wrote:
>
> The question regarded a single proof and its use of an assumption
> within the proof.
>
Right. You might try to learn something about /natural deduction/.
Jesse F. Hughes
> On May 17, 7:31 pm, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>> > It is used to derive the shortest, simplest proof of Rosser's
>> > extension to Godel's theorems published. If this were true, would
>> > that be significant in of itself?
>
>> Yeah, that would be swell. If true.
>
> How about "If a logic is both consistent and complete, then it's
> unprovable sentences coincide with its refutable sentences, but the
> latter is recursively enumerable while the former is not."?
>
> (a) Not a proof of Rosser 1936. Reason: ____
> (b) Not the shortest. Giver shorter: ____
> (c) Not derived using CBL. Problem with CBL derivation: ____
How would I know whether it was derived with CBL? I've never seen a
presentation of CBL.
But this is all quite irrelevant. You said it was a standard. I sure
am keen to see why you say this.
>> But that is irrelevant. You said it was "somewhat of a de facto
>> standard for Computationally Based Logics".
>>
>> Surely you agree that this suggests someone else uses CBL besides you,
>> yes? Who might that be?
Still holding my breath.
--
Jesse F. Hughes
"Everybody has a heart, except some people."
-- All About Eve
G. Frege
<je...@phiwumbda.org> wrote:
>>>
>>> Surely you agree that this suggests someone else uses CBL besides you,
>>> yes? Who might that be?
>>>
> Still holding my breath.
>
It might be his alter ego!
Charlie-Boo
> On 17 May 2007 17:11:34 -0700, Charlie-Boo <shymath...@gmail.com>
> wrote:
> > The question regarded a single proof and its use of an assumption
> > within the proof.
>
> Right. You might try to learn something about /natural deduction/.
That doesn't prove anything. Your proof still uses more primitives
than classic axiomatic theorem-proivng and is thus inferior by Occam's
Razor. Admit it.
C-B
Charlie-Boo
> On Thu, 17 May 2007 20:20:47 -0400, "Jesse F. Hughes"
>
>
> >>> Surely you agree that this suggests someone else uses CBL besides you,
> >>> yes? Who might that be?
>
> > Still holding my breath.
>
> It might be his alter ego!
Read thru past sci.logic postings and note the hearty souls who
actually read the seminal ARXIV paper, and say, "I read it and it's
pretty neat." Search the archives.
C-B
MoeBlee
> On May 17, 8:34 pm, G. Frege <nomail@invalid> wrote:
>
> > On Thu, 17 May 2007 20:20:47 -0400, "Jesse F. Hughes"
>
> > <j...@phiwumbda.org> wrote:
>
> > >>> Surely you agree that this suggests someone else uses CBL besides you,
> > >>> yes? Who might that be?
>
> > > Still holding my breath.
>
> > It might be his alter ego!
>
> Read thru past sci.logic postings and note the hearty souls who
> actually read the seminal ARXIV paper, and say, "I read it and it's
> pretty neat." Search the archives.
>
Great, so we search news group arcives to find someone who might have
said "That's neat" whereupon we conclude that Charlie Boo's typings
are "somewhat of a de facto standard for computability based logics".
MoeBlee
MoeBlee
Doesn't your chest ever get sore from your beating it in the manner of
ape?
It's difficult to fathom which is more remarkable - your wonderful
acheivements in formal axiomatization or mankind's abysmal and
universal failure to recognize them.
Or hasn't it ever occurred to you that what mathematicians and
logicians mean by 'formal axiomatization' isn't what you actually do?
MoeBlee
MoeBlee
> On May 17, 7:49 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > On May 17, 4:23 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > And you claim that what I say doesn't make sense?
>
> > Most of what you say about mathematical logic is either incorrect,
> > misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
> > That you believe any of it is a testament to the power of conviction.
>
> Yet why have you no examples?
Your posts a while back about ZFC while you don't understand that ZFC
is an extension of the predicate calculus is one example that comes to
mind of your ignorance. Your self-vaunted CBL is another example (did
you ever answer that poster who about a week ago gave you a point
blank critique?). Your mindless and irresponsible claims about Norm
Megill's system is another example. It's not too pleasant digging up
such examples, but still not hard to do.
MoeBlee
MoeBlee
> That doesn't prove anything. Your proof still uses more primitives
> than classic axiomatic theorem-proivng and is thus inferior by Occam's
> Razor.
There is no linear ordering by economy of expression when there are
different considerations at once. Some systems may have fewer axioms
but more primitives, or shorter proofs but more axioms, or fewer rules
but they're longer to formulate. There may be many considerations that
are advantages and disadvantages economy-wise that make systems and
formulations not so categorically comparable. It's not Occam's Magic
Wand as you use it, but rather a general heuristic (as well as a
philosophical principle with many different senses - from Occam
through revision and adaption to various subsequent philosophical and
scientific developments). Your running around beating your chest
continually exclaiming superority by way of Occam's razor isn't
mathematically persuasive but rather it just makes you a dope who
happens to know how to say "Occam's razor" and capable of nudging
various symbols around as you imagine, without properly stating and
communicating your syntax, that your vaious juxtapostions express some
kind of quintessentially elegant mathematics while all they do
represent are the disorganized rattlings in your brain, infatuated
with them though you may be.
MoeBlee
TXLogic
If you've ever been curious about the fact that no one on FOM replied
to your request for comments, I'd suggest you have a look at Peter
Aczel's well-known 1983 study Non-Well-Founded Sets, where the
mathematics of structures such as those in your little example is
studied in depth. Also recommdended is Barwise and Moss's terrific
1996 book Vicious Circles: On the Mathematics of Non-Wellfounded
Phenomena. You would be particular interested in the very general
account both works provide of the idea of a set being a solution to a
system of equations (of which your "x = {x,0}" is a simple special
case).
MoeBlee
> My solution is the first Google
> match on Quine Atom.
Which is a prime example of why it would be foolish to base serious
mathematical research on whatever flotsam and jetsam happens to float
on top of the results list of an Internet keyword search.
MoeBlee
Charlie-Boo
> On 17 May 2007 17:11:34 -0700, Charlie-Boo <shymath...@gmail.com>
> wrote:
>
>
>
> > The question regarded a single proof and its use of an assumption
> > within the proof.
>
> Right. You might try to learn something about /natural deduction/.
Why? The question concerns only that one proof.
C-B
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On May 17, 7:31 pm, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
> >> Charlie-Boo <shymath...@gmail.com> writes:
> >> > It is used to derive the shortest, simplest proof of Rosser's
> >> > extension to Godel's theorems published. If this were true, would
> >> > that be significant in of itself?
>
> >> Yeah, that would be swell. If true.
>
> > How about "If a logic is both consistent and complete, then it's
> > unprovable sentences coincide with its refutable sentences, but the
> > latter is recursively enumerable while the former is not."?
>
> > (a) Not a proof of Rosser 1936. Reason: ____
> > (b) Not the shortest. Giver shorter: ____
> > (c) Not derived using CBL. Problem with CBL derivation: ____
>
> How would I know whether it was derived with CBL? I've never seen a
> presentation of CBL.
I can't help it if you don't follow the literature. I have posted
explanations here as well.
> But this is all quite irrelevant. You said it was a standard. I sure
> am keen to see why you say this.
Who has axiomatized Computer Science in general?
Who has formally derived the theorems of Godel (1931), Rosser (1936),
Turing (1937)?
The ARXIV paper explains a lot of this in detail with lots of
examples.
> >> But that is irrelevant. You said it was "somewhat of a de facto
> >> standard for Computationally Based Logics".
>
> >> Surely you agree that this suggests someone else uses CBL besides you,
> >> yes?
Why would that be? One is a mathematical assertion and the other
deals with sociology.
> >> Who might that be?
How many people use Andrew Wile's method of proving Fermat's Last
Theorem?
> Still holding my breath.
What is the relevance?
"In questions of science, the authority of a thousand is not worth the
humble reasoning of a single individual." - Galileo Galilei
C-B
> --
> Jesse F. Hughes
>
> "Everybody has a heart, except some people."
> -- All About Eve- Hide quoted text -
Charlie-Boo
> On Thu, 17 May 2007 20:20:47 -0400, "Jesse F. Hughes"
>
>
> >>> Surely you agree that this suggests someone else uses CBL besides you,
> >>> yes? Who might that be?
>
> > Still holding my breath.
>
> It might be his alter ego!
I agree. Nobody else has even attempted some of my more advanced
results. They don't even come close! Take any branch of Computer
Science (Theory of Computation, Recursion Theory, Program Synthesis,
Proof Theory, etc.) and what axioms and rules have been presented?
What formal derivations have been given for the theorems of Godel,
Rosser, Turing?
I talk about principles of Mathematical Logic. You should try it!
C-B
Charlie-Boo
You've got yer wires crossed, Moeb.
If you want to say something intelligent, address the question of who
has given axioms, rules and formal proofs of any branch of Computer
Science outside of Propositional Calculus and parts of Predicate
Calculus. Who? This is sci.logic, remember? Can you be sci.logic-
al, huh?
C-B
> MoeBlee- Hide quoted text -
Charlie-Boo
> On May 17, 5:15 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > On May 17, 7:49 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > On May 17, 4:23 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > And you claim that what I say doesn't make sense?
>
> > > Most of what you say about mathematical logic is either incorrect,
> > > misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
> > > That you believe any of it is a testament to the power of conviction.
>
> > Yet why have you no examples?
>
> Your posts a while back about ZFC while you don't understand that ZFC
> is an extension of the predicate calculus is one example that comes to
> mind of your ignorance.
The fact that ZFC is written using the Predicate Calculus is a mistake
I have pointed out numerous times.
> Your self-vaunted CBL is another example
Where's the beef?
> (did you ever answer that poster who about a week ago gave you a point
> blank critique?).
Say what?
> Your mindless and irresponsible claims about Norm
> Megill's system is another example.
I pointed out specifics. You have not.
> It's not too pleasant digging up
> such examples, but still not hard to do.
You have proven nothing except that you are content to deal in
personal attacks rather than technical issues.
C-B
> MoeBlee
Charlie-Boo
> On May 17, 6:33 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > That doesn't prove anything. Your proof still uses more primitives
> > than classic axiomatic theorem-proivng and is thus inferior by Occam's
> > Razor.
>
> There is no linear ordering by economy of expression when there are
> different considerations at once.
You're doing it again. It's not the lengths of expressions, it's the
number of primitives (axioms, rules, definitions) in the system.
C-B
Charlie-Boo
Where do they show how to construct a Quine Atom? Defining Q to be
Q={Q} doesn't do it, nor does drawing a flowchart with arcs between
sets and their elements.
If you can construct a Quine Atom, then do so here. There's plenty of
room for you to prove your point (unless you're just BS-ing us, of
course. :)
C-B
Charlie-Boo
Wow!
C-B
> MoeBlee
Charlie-Boo
You're wrong, man. If you ever want to debate this intelligently,
then I would be glad to. I would start by enumerating the branches of
Computer Science, the fundamental theorems in each, and the axioms/
rules/proofs given for each. There is nothing beyond simple logic.
Then read the ARXIV paper and tell me what's wrong with the formal
derivations presented there.
Charlie-Boo
> On May 17, 7:19 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>
>
>
> > On May 17, 7:54 pm, G. Frege <nomail@invalid> wrote:
>
> > > On 17 May 2007 16:49:19 -0700, MoeBlee <jazzm...@hotmail.com>
> > > wrote:
>
> > > >> And you claim that what I say doesn't make sense?
>
> > > > Most of what you say about mathematical logic is either incorrect,
> > > > misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
>
> > > I second that.
>
> > > Once he claimed that he was the first to discover a /Quine atom/!
> > > :-)
>
> > Defining Q to be Q={Q} no more constructs a Quine atom than defining N
> > to be a counter-example to Goldbach's Conjecture constructs a counter-
> > example.
>
> > How would you construct such a set? My solution is the first Google
> > match on Quine Atom.
>
> >http://cs.nyu.edu/pipermail/fom/2002-September/005844.html
>
> to your request for comments,
False
> I'd suggest you have a look at Peter
> Aczel's well-known 1983 study Non-Well-Founded Sets, where the
> mathematics of structures such as those in your little example is
> studied in depth. Also recommdended is Barwise and Moss's terrific
> 1996 book Vicious Circles: On the Mathematics of Non-Wellfounded
> Phenomena. You would be particular interested in the very general
> account both works provide of the idea of a set being a solution to a
> system of equations (of which your "x = {x,0}" is a simple special
> case).- Hide quoted text -
Charlie-Boo
> On May 17, 5:15 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > On May 17, 7:49 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > > On May 17, 4:23 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > > And you claim that what I say doesn't make sense?
>
> > > Most of what you say about mathematical logic is either incorrect,
> > > misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
> > > That you believe any of it is a testament to the power of conviction.
>
> > Yet why have you no examples?
> Your mindless and irresponsible claims about Norm
> Megill's system is another example.
If you want to debate that system, it would help to start a new
thread. He uses an expression like xRy(Rz)=(xRy)Rz and substitutes +
for R but there is nothing at that point about + or - so - could
equally well be substituted for R.
There is also the general question of what ZFC alone can prove and
what he says regarding that question and what his site shows.
C-B
> MoeBlee
Jesse F. Hughes
> On May 17, 8:20 pm, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
>> Charlie-Boo <shymath...@gmail.com> writes:
>>
>> > How about "If a logic is both consistent and complete, then it's
>> > unprovable sentences coincide with its refutable sentences, but the
>> > latter is recursively enumerable while the former is not."?
>>
>> > (a) Not a proof of Rosser 1936. Reason: ____
>> > (b) Not the shortest. Giver shorter: ____
>> > (c) Not derived using CBL. Problem with CBL derivation: ____
>>
>> How would I know whether it was derived with CBL? I've never seen a
>> presentation of CBL.
>
> I can't help it if you don't follow the literature. I have posted
> explanations here as well.
>
>> But this is all quite irrelevant. You said it was a standard. I sure
>> am keen to see why you say this.
>
> Who has axiomatized Computer Science in general?
Yes, that is keen! Nobody but Charlie-Boo has completed such a
challenging task!
But that's quite beside the point. I asked who uses CBL besides you.
You *did* claim it was a "de facto standard", right? Surely there
must be many users. Indeed, I bet they are publishing their results.
So, can you name any users?
> Who has formally derived the theorems of Godel (1931), Rosser (1936),
> Turing (1937)?
>
> The ARXIV paper explains a lot of this in detail with lots of
> examples.
Great! But that's quite beside the point.
>> >> But that is irrelevant. You said it was "somewhat of a de facto
>> >> standard for Computationally Based Logics".
>>
>> >> Surely you agree that this suggests someone else uses CBL besides you,
>> >> yes?
>
> Why would that be? One is a mathematical assertion and the other
> deals with sociology.
Oh? The claim that CBL is "somewhat of a de facto standard for
Computationally Based Logics" is a *mathematical* assertion?
Great! Then let's see the proof!
Anyway, I must have been mighty confused. I thought it could be a
standard only if people actually use it. Isn't that silly?
>> >> Who might that be?
>
> How many people use Andrew Wile's method of proving Fermat's Last
> Theorem?
How would they *use* that? Did anyone claim that Wile's proof is
somehow a de facto standard for some kind of logic or other?
>> Still holding my breath.
>
> What is the relevance?
>
> "In questions of science, the authority of a thousand is not worth the
> humble reasoning of a single individual." - Galileo Galilei
--
Jesse F. Hughes
"The people who made up the words could have said 'newspaper' is
'trees'." -- Quincy P. Hughes, five-year-old Wittgensteinian
(This comment came out of the blue at breakfast.)
Charlie-Boo
> Charlie-Boo <shymath...@gmail.com> writes:
> > On May 17, 8:20 pm, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
> >> Charlie-Boo <shymath...@gmail.com> writes:
>
> >> > How about "If a logic is both consistent and complete, then it's
> >> > unprovable sentences coincide with its refutable sentences, but the
> >> > latter is recursively enumerable while the former is not."?
>
> >> > (a) Not a proof of Rosser 1936. Reason: ____
> >> > (b) Not the shortest. Giver shorter: ____
> >> > (c) Not derived using CBL. Problem with CBL derivation: ____
>
> >> How would I know whether it was derived with CBL? I've never seen a
> >> presentation of CBL.
>
> > I can't help it if you don't follow the literature. I have posted
> > explanations here as well.
>
> >> But this is all quite irrelevant. You said it was a standard. I sure
> >> am keen to see why you say this.
>
> > Who has axiomatized Computer Science in general?
>
> Yes, that is keen! Nobody but Charlie-Boo has completed such a
> challenging task!
>
> But that's quite beside the point. I asked who uses CBL besides you.
I thought you questioned whether it was a standard or not?
What difference does it make who uses it?
What is the standard proof of FLT? How many authors have given that
proof?
> You *did* claim it was a "de facto standard", right? Surely there
> must be many users. Indeed, I bet they are publishing their results.
What difference does that make? (I will NOT be sucked down to your
level.)
> So, can you name any users?
Can you name any other users of an axiomatization of Computer Science?
What is the standard axiomatization of Computer Science?
> > Who has formally derived the theorems of Godel (1931), Rosser (1936),
> > Turing (1937)?
>
> > The ARXIV paper explains a lot of this in detail with lots of
> > examples.
>
> Great! But that's quite beside the point.
I thought the question had to do with what the standard axiomatization
of Computer Science is?
> >> >> But that is irrelevant. You said it was "somewhat of a de facto
> >> >> standard for Computationally Based Logics".
Yes, Computability Based Logics are used to formalize metamathematical
results such as an axiomatization of Computer Science.
Maybe you're just not that clear on the subject? What do you know
about Computationally Based Logics?
C-B
> >> >> Surely you agree that this suggests someone else uses CBL besides you,
> >> >> yes?
>
> > Why would that be? One is a mathematical assertion and the other
> > deals with sociology.
>
> Oh? The claim that CBL is "somewhat of a de facto standard for
> Computationally Based Logics" is a *mathematical* assertion?
>
> Great! Then let's see the proof!
>
> Anyway, I must have been mighty confused. I thought it could be a
> standard only if people actually use it. Isn't that silly?
>
> >> >> Who might that be?
>
> > How many people use Andrew Wile's method of proving Fermat's Last
> > Theorem?
>
> How would they *use* that? Did anyone claim that Wile's proof is
> somehow a de facto standard for some kind of logic or other?
>
> >> Still holding my breath.
>
> > What is the relevance?
>
> > "In questions of science, the authority of a thousand is not worth the
> > humble reasoning of a single individual." - Galileo Galilei
>
> --
> Jesse F. Hughes
> "The people who made up the words could have said 'newspaper' is
> 'trees'." -- Quincy P. Hughes, five-year-old Wittgensteinian
> (This comment came out of the blue at breakfast.)- Hide quoted text -
Charlie-Boo
> On May 17, 7:19 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
>
>
>
>
> > On May 17, 7:54 pm, G. Frege <nomail@invalid> wrote:
>
> > > On 17 May 2007 16:49:19 -0700, MoeBlee <jazzm...@hotmail.com>
> > > wrote:
>
> > > >> And you claim that what I say doesn't make sense?
>
> > > > Most of what you say about mathematical logic is either incorrect,
> > > > misconceived, ill-premised, hand-waving, or self-serving mumbo jumbo.
>
> > > I second that.
>
> > > Once he claimed that he was the first to discover a /Quine atom/!
> > > :-)
>
> > Defining Q to be Q={Q} no more constructs a Quine atom than defining N
> > to be a counter-example to Goldbach's Conjecture constructs a counter-
> > example.
>
> > How would you construct such a set? My solution is the first Google
> > match on Quine Atom.
>
> >http://cs.nyu.edu/pipermail/fom/2002-September/005844.html
>
> If you've ever been curious about the fact that no one on FOM replied
> to your request for comments, I'd suggest you have a look at Peter
> Aczel's well-known 1983 study Non-Well-Founded Sets, where the
> mathematics of structures such as those in your little example is
> studied in depth.
A. You're chomping at the bit to prove me wrong. (You imply that
repeatedly.)
B. If you were to give a construction of a Quine Atom already
published:
1. You would prove me wrong.
2. Everyone would be able to see it and see that you're right.
3. You will have proved your point.
4. It would be an easy thing to do.
C. You decline to give a construction for a Quine Atom.
Which of A, B and C are not true?
C-B
> Also recommdended is Barwise and Moss's terrific
> 1996 book Vicious Circles: On the Mathematics of Non-Wellfounded
> Phenomena. You would be particular interested in the very general
> account both works provide of the idea of a set being a solution to a
> system of equations (of which your "x = {x,0}" is a simple special
> case).- Hide quoted text -
MoeBlee
The question was your assertion that that your typings are "somewhat
of a de facto standard for computability based logics".
MoeBlee
MoeBlee
> > (did you ever answer that poster who about a week ago gave you a point
> > blank critique?).
>
> Say what?
A post on May 8, 2007 by TXLogic in the thread 'ZFC Is Consistent - No
Axiom Infers The Negation Of Any Axiom', which is a thread you
started, and (as I now answer my own question) you did not answer the
post (at least not in that thread).
[begin post by TXLogic:]
On May 8, 5:29 am, David C. Ullrich <ullr...@math.okstate.edu> wrote:
> On 7 May 2007 07:00:13 -0700, Charlie-Boo <shymath...@gmail.com>
> wrote:
> ...
> >The assumption is that ~(x e x) is a wff
> Wow, this again. The term "wff" has a perfectly standard
> definition, and ~(x e x) _is_ a wff by that definition.
> If you claim it's not then you're using the word wff to
> mean something other than what everybody else means by it.
> In which case you have a lot of explaining to do.
> Starting with this:
> Exactly what is your definition of "wff"?
C-B appears to be a bit confused on this point, and on numerous
others. In his much cited (by him) Arxiv paper (http://arxiv.org/
html/
cs/0003071), he provides what is apparently supposed to be a BNF for
his "Program Calculus":
Programs will be represented using a semi-formal imaginary
miniature programming language. A program consists of a series
of lines. Each line consists of commands, each followed by one or
more arguments separated by commas. There are four different
commands: for, set, if and write.
for set-definition : For each element of a set defined by
set-definition, the variables in set-definition assume that value
and
the rest of the line is executed.
set variable = expression : The variable is assigned the value of
expression and the rest of the line is executed.
if expression : If the expression is true then continue executing
the
current line. Otherwise, continue at the previous for command on
the
current line, or the next line if there is no previous for on this
line.
write (expression , ...) : Output the tuple consisting of the
values
of
(expression , ...).
But nowhere in the "BNF are we told what a "set-definition", or even
an "expression", is; the BNF is lacking some crucial terminals here.
He also seems to think a casual discussion of the intended semantics
of his language suffices to support his many strong claims about what
his system CBL can do:
I. Program Transformations
Let P be an arbitrary predicate, such as a given number is prime or
there exists an employee who earns more than his manager. Let PP
be any computer program (program) that solves P by determining and
reporting to us whether P is true or false. (We decide upon a
single
programming language for all of our discussions.)
Assertion: There is a procedure (program) that will transform (map)
any such PP into another program PP' that solves ~P, the formal
negation of P.
Demonstration: A number of possible procedures come to mind. For
one, we could change every point where program PP is about to
report to us that P is true and change it to false, and vice-
versa.
Alternately, we could call program PP as a subroutine, and then
report the opposite of what PP does.
We call this assertion the NOT rule and signify it by P->P, where
in
general A->B means "any programs that solve A can be transformed
into a program that solves B".
We will consider two distinct types of programs: those that solve a
predicate, by reporting true or false, and those that solve a set,
by
listing its elements. We indicate what a program solves with a wff
(well-formed formula) of the Predicate Calculus.
While the standard syntax of the Predicate Calculus is used (~ not,
^ and, v or, $ there exists, @ for all, A B C ... variables, "..."
literals), we extend the semantics of wffs by giving special
meaning
to certain variables:
Unquantified input variables I, J, K, ... represent values that
must
be
supplied to the program as input. Unquantified output variables x,
y,
z, ... represent values that are output by the program.
We use single letter names P, Q, R ... to represent arbitrary
relations, and multiple letter names to represent specific
relations that we define. Thus, to solve P(I) a program would
have to take in a value I and output a value of true or false.
To solve Q(I,x) a program would take in a value I and output
every value for x. Note that in general I and x represent a
tuple of any number of individual values. Furthermore,
additional input variables, not explicitly represented, may be
present without altering the general principles and manipulations
being discussed.
A subscripted H is added to a wff containing output variables,
as in Q(I,x)_H, to indicate that the program must always halt.
(The set of values output must necessarily always be finite.)
For any wff W, the expression -W means that no program can
exist that solves W.
Notably, we are never provided with a rigorous definition of what a
program is, nor does the semantics provide a rigorous definition of
what it means for a program to halt; that is, there is no actual
mathematical definition of the notation Q(I,x)_H.
Of course, without an actual syntax for his theory and only an
informal, quasi-mathematical semantics, it is pretty much impossible
to verify all of the alleged theorems that follow, let alone C-B's
oft
repeated claims about how CBL proves the undecidability of the
halting
problem, Gödel's theorem, Rosser's theorem, etc. There is in
particular, AFAICS, no definition of the notion of a Turing machine;
in Section VI, the term "Turing Machine" suddenly appears without
definition in the assertion "We synthesize a program to list all
Turing Machines that halt no on themselves, proving that this set is
recursively enumerable." Numerous assertions follow that appear to
be
quantifying over TMs. But a definition of "Turing Machine" is not to
be found.
There is also no notion of natural number, so it is hard to see how
anything about incompleteness gets any purchase. Rather, an
"Incompleteness Axiom" just appears on the scene: -~YES(x,x). But
what the values of x are supposed to be here is unstated. YES itself
simply appears in the preceding sentence:
Thus, P(x) is solvable when there is a literal "?" such that
DEF:P(a) , YES("...",a).
Perhaps I just lack imagination, but I simply cannot see what is
going
on here. The system appears to be at best a desultory series of
assertions using a lot of traditional terminology but without any
definitions and with no actual foundation in any genuine mathematics.
[end post by TXLogic]
And that thread is yet another example of your ineptitude, as I and
other posters showed how very silly is your basic argument there.
> > Your mindless and irresponsible claims about Norm
> > Megill's system is another example.
>
> I pointed out specifics. You have not.
Your ineptitude (or dishonesty?) is again glaring there, as you failed
to take account of the fact that Megill's theorem has certain
hypotheses, which was pointed out to you by a few other posters but
for which you have no coherent response.
> > It's not too pleasant digging up
> > such examples, but still not hard to do.
>
> You have proven nothing except that you are content to deal in
> personal attacks rather than technical issues.
I have comments about you personally, but I talk about technical
issues with a number of posters quite often. And, for just one example
in which I did engage you technically, look again at the 'ZFC Is
Consistent - No Axiom Infers The Negation Of Any Axiom' thread in
which I and a number of people showed you TECHNICALLY how silly your
argument is there. Moreover, our VERY FIRST CONVERSATION was as to the
technical matter of the definition of 'wff of the language of ZFC' in
which I answered your question but you never (even after I asked you a
few times) responded to my question as to what your point is in asking
such a question and having people provide you with such information.
MoeBlee
MoeBlee
> On May 17, 11:39 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > On May 17, 6:33 pm, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > That doesn't prove anything. Your proof still uses more primitives
> > > than classic axiomatic theorem-proivng and is thus inferior by Occam's
> > > Razor.
>
> > There is no linear ordering by economy of expression when there are
> > different considerations at once.
>
> You're doing it again. It's not the lengths of expressions, it's the
> number of primitives (axioms, rules, definitions) in the system.
You skipped my argument:
> > Some systems may have fewer axioms
> > but more primitives, or shorter proofs but more axioms, or fewer rules
> > but they're longer to formulate. There may be many considerations that
> > are advantages and disadvantages economy-wise that make systems and
> > formulations not so categorically comparable. It's not Occam's Magic
> > Wand as you use it, but rather a general heuristic (as well as a
> > philosophical principle with many different senses - from Occam
> > through revision and adaption to various subsequent philosophical and
> > scientific developments). Your running around beating your chest
> > continually exclaiming superority by way of Occam's razor isn't
> > mathematically persuasive but rather it just makes you a dope who
> > happens to know how to say "Occam's razor" and capable of nudging
> > various symbols around as you imagine, without properly stating and
> > communicating your syntax, that your vaious juxtapostions express some
> > kind of quintessentially elegant mathematics while all they do
> > represent are the disorganized rattlings in your brain, infatuated
> > with them though you may be.
You've given no reason for preference of shorter proofs (as you
continually beat your chest about claiming that you have a shorter
proof of this or that) but not of shorter formulas themselves.
Moreover, even if we exclude length as a consideration, but consider
only such things as number of "axioms, rules, definitions", then
systems might not be comparable since, e.g., one may have fewer axioms
but more rules while another vice versa, etc. (Also, a conjuction of
axioms is one formula so that any theory with only finitely many
axioms is also axiomatized by a single axiom, and even a theory with
finitely many axiom schemata may then be axiomatized by a single axiom
schemata, trivial thought that may be.) Moreover, choices in how a
system is set up need not always be determined solely by economy but
by other considerations also. For example, the theory of Boolean
algebras can be axiomatized by a single axiom, but it is often more
instructive to see an axiomatization in which the duality principle is
immediately apparent and ready to be worked with. Your running around
claiming superiority of such and such a system by "Occam's razor" is a
function of your over-simplistic and narrow agenda of self-
aggrandizement and of your abysmal lack of understanding the scope,
context, and particulars of mathematical logic.
MoeBlee
MoeBlee
> MoeBlee wrote:
> > Or hasn't it ever occurred to you that what mathematicians and
> > logicians mean by 'formal axiomatization' isn't what you actually do?
>
> You're wrong, man. If you ever want to debate this intelligently,
> then I would be glad to. I would start by enumerating the branches of
> Computer Science, the fundamental theorems in each, and the axioms/
> rules/proofs given for each. There is nothing beyond simple logic.
> Then read the ARXIV paper and tell me what's wrong with the formal
> derivations presented there.
Why don't you first answer my question from well OVER A YEAR AGO, as
I've asked you a few times since?
Anyway, your paper doesn't even HAVE formal derivations.
MoeBlee
MoeBlee
> On May 18, 12:16 am, TXLogic <chris.men...@gmail.com> wrote:
> > no one on FOM replied
> > to your request for comments,
>
> False
Very well, then would you please indicate exactly where in the FOM
archives there is a reply?
> > I'd suggest you have a look at Peter
> > Aczel's well-known 1983 study Non-Well-Founded Sets, where the
> > mathematics of structures such as those in your little example is
> > studied in depth. Also recommdended is Barwise and Moss's terrific
> > 1996 book Vicious Circles: On the Mathematics of Non-Wellfounded
> > Phenomena. You would be particular interested in the very general
> > account both works provide of the idea of a set being a solution to a
> > system of equations (of which your "x = {x,0}" is a simple special
> > case.
MoeBlee
MoeBlee
> On May 17, 11:19 pm, MoeBlee <jazzm...@hotmail.com> wrote:
> > Your mindless and irresponsible claims about Norm
> > Megill's system is another example.
>
> If you want to debate that system, it would help to start a new
> thread. He uses an expression like xRy(Rz)=(xRy)Rz and substitutes +
> for R but there is nothing at that point about + or - so - could
> equally well be substituted for R.
Silly boy, there is an hypothesis of that theorem that you have not
shown is satisfied by subtraction. That has been pointed out to you
already by a few other posters.
> There is also the general question of what ZFC alone can prove and
> what he says regarding that question and what his site shows.
You don't know what ZFC is.
MoeBlee
G. Frege
wrote:
>>>>
>>>> Your proof still uses more primitives than classic axiomatic
>>>> theorem-proving and is thus inferior by Occam's Razor.
>>>>
Boy, this guy is an idiot. :-/
>>>
>>> There is no linear ordering by economy of expression when there are
>>> different considerations at once.
>>>
Right.
>>
>> You're doing it again. It's not the lengths of expressions, it's
>> the number of primitives (axioms, rules, definitions) in the system.
>>
*sigh*
There was a recent post concerning this topic in sci.math by a much
more resonable guy than C-B:
"One-Axiom Logic
suffices for classic logic, Boole algebra or whatever
isomorph structure. (No, I didn't memorize it.)
It is even weller knowner :-) that one function (NAND or
NOR) suffices to generate NOT, AND, ... etc.
Can you combine both? It would be trivial to rewrite
the mentioned axiom into NAND form but it's not
trivial at all to me that this new axiom would
generate all standard axioms." (Hauke Reddmann)
Here's my answer:
<start quote>
>
> Can you combine both?
>
Yes. This was first done by Nicod. See:
J.G. Nicod, A reduction in the number of primitive
propositions of logic, Proc. Camb. Phil. Soc. 19
(1917), 32-41.
Here's a quote from another source:
"Classical Sentential Logic --- In the Sheffer Stroke (D)
* In 1917, Nicod showed that the following 23-symbol formula (in
Polish notation) is a single axiom for classical sentential logic
(D is interpreted semantically as NAND, i.e., the Sheffer stroke):
DDpDqrDDtDttDDsqDDpsDps
* The only rule of inference for Nicod's single axiom system is the
following, somewhat odd, detachment rule for D:
From DpDqr and p, infer r.
* Lukasiewicz later showed that the following substitution instance
(t/s) of Nicod's axiom (N) would suffice:
DDpDqrDDsDssDDsqDDpsDps
* Lukasiewicz's student Mordchaj Wajsberg later discovered the
following organic [Footnote: A single axiom is organic if it
contains no tautologous subformulae. Nicod's original single axiom
(and Lukasiewicz's simplifcation of it) are non-organic, because
they contain tautologous subformulae of the form DxDxx.] 23-symbol
single axiom for D:
DDpDqrDDDsrDDpsDpsDpDpq
* Lukasiewicz later discovered another 23-symbol organic axiom:
DDpDqrDDpDrpDDsqDDpsDps2
* We have discovered many new 23-symbol single axioms, some of
which are organic and have only 4 variables, e.g.,
DDpDqrDDpDqrDDsrDDrsDps
* We can now report that the shortest single axioms for these
Sheffer Stroke systems contain 23 symbols. No shorter axioms
exist."
Source:
http://fitelson.org/ar.html#SH
<end quote>
So in this system(s) we would have:
no. of primitives: 1
no. of axioms: 1
no. of rules: 1
So applying C-B's itiotic criteria one might consider this system
to be superior to any other "by Occam's Razor" (C-B).
BUT...
"...choices in how a system is set up need not always be determined
solely by economy but by other considerations also. For example,
the theory of Boolean algebras can be axiomatized by a single
axiom, but it is often more instructive to see an axiomatization in
which the duality principle is immediately apparent and ready to be
worked with. Your running around claiming superiority of such and
such a system by "Occam's razor" is a function of your
over-simplistic and narrow agenda of self-aggrandizement and of
your abysmal lack of understanding the scope, context, and
particulars of mathematical logic." (MoeBlee)
Indeed!
"The choice of the initial formulas can be made in quite different
ways. One has taken great pains, in particular, to get by with the
smallest possible number of axioms, and in this respect the limit
of what is possible has indeed been reached. The purpose of logical
investigations is better served, however, when we separate, as in
the axiomatics for geometry, various groups of axioms from one
another, such that each group gives expression to the role of one
logical operation. The following list then emerges:
I Axioms of implication
II a) Axioms for &
II b) Axioms for v
III Axioms of negation.
This system of axioms generates through application of the rules
all valid formulas of propositional logic."
(Paul Bernays, Problems of Theoretical Logic, 1927)
G. Frege
wrote:
>
> "...choices in how a system is set up need not always be determined
> solely by economy but by other considerations also."
>
Obviously one of the (many) things C-B does not understand.
"Ich wollte zunächst einmal einen Formalismus aufstellen,
der dem wirklichen Schließen möglichst nahe kommt. So
ergab sich ein 'Kalkül des natürlichen Schließens'."
| (First I wished to construct a formalism that comes as
| close as possible to actual reasoning. Thus arose a
| "calculus of natural deduction".)
— Gerhard Gentzen, Untersuchungen über das logische
Schließen (Mathematische Zeitschrift 39, pp.176-210,
1935)
Source:
http://en.wikipedia.org/wiki/Natural_deduction
MoeBlee
> On May 18, 7:31 am, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
> I thought you questioned whether it was a standard or not?
What you claimed is that your typings (CBL or whatever) are "somewhat
of a de facto standard for computability based logics".
That would naturally suggest asking WHO, other than you, uses CBL so
that it is "somewhat of a de facto standard".
> What difference does it make who uses it?
It makes a difference as to the question of whether it is "somewhat of
a de facto standard".
> What is the standard proof of FLT? How many authors have given that
> proof?
A proof is not a system. Your implied analogy is irrelevent.
> > You *did* claim it was a "de facto standard", right? Surely there
> > must be many users. Indeed, I bet they are publishing their results.
>
> What difference does that make? (I will NOT be sucked down to your
> level.)
YOUR level is to make a claim of "somewhat of a de facto standard". So
we're just asking AT THAT LEVEL, who uses your CBL to make it
"somewhat of a de facto standard"?
> > So, can you name any users?
>
> Can you name any other users of an axiomatization of Computer Science?
You seem to be arguing that your CBL is an axiomatization (it isn't,
by the way) of computer science, and the only axiomatization of
computer science, thus you alone make a sufficient set of people to
call your CBL "somewhat of a de facto standard".
> What is the standard axiomatization of Computer Science?
In a formal sense, an axiomatization is of a theory (a set of
sentences in a formal language closed under entailment). So what
theory do you take "Computer Science" to be?
Meanwhile, what theorems in the study of computability (such as found
in ordinary textbooks by Davis, Hermes, Odifreddi, Cutland, Rogers,
Monk, Boolos, Shoenfield, Kleene, et. al) do you contend cannot be
proven in ZF?
> Maybe you're just not that clear on the subject? What do you know
> about Computationally Based Logics?
Define 'computbability based logics'.
MoeBlee
MoeBlee
> On 18 May 2007 10:00:04 -0700, MoeBlee <jazzm...@hotmail.com>
> wrote:
The line quote notation there makes it appear that I wrote the line:
"Can you combine both?"
For the record, that line was not written by me.
MoeBlee
Charlie-Boo
Do you deny that CBL is a Computationally Based Logic? Do you know of
any more standard Computationally Based Logics?
Charlie-Boo
Obviously you haven't read it.
> MoeBlee
Charlie-Boo
> On May 18, 3:48 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > On May 18, 12:16 am, TXLogic <chris.men...@gmail.com> wrote:
> > > no one on FOM replied
> > > to your request for comments,
>
> > False
>
> Very well, then would you please indicate exactly where in the FOM
> archives there is a reply?
You stupid fuck. http://cs.nyu.edu/pipermail/fom/2002-September/005854.html
Charlie-Boo
Published papers don't even agree as to what ZFC is. But I know
exactly what it is. What is it? Then I'll say. It has to do with
Computationally Based Logics.
C-B
> MoeBlee
Jesse F. Hughes
> On May 18, 7:31 am, "Jesse F. Hughes" <j...@phiwumbda.org> wrote:
>> So, can you name any users?
>
> Can you name any other users of an axiomatization of Computer Science?
Oh, I get it. Only one person has ever axiomatized CS. That person
is Charlie-Boo. He uses CBL. Consequently, CBL is a de facto
standard of axiomatizations of computer science.
Is this your half-thought?
If so, perhaps you should consider a refresher course in writing.
Evidently, you give entirely the wrong impression when you use words
like "de facto standard" to describe a theory[1] that is used by only
one slightly odd fellow[2].
> What is the standard axiomatization of Computer Science?
Did I ever claim that there was a standard axiomatization of CS?
Footnotes:
[1] I'm being generous in calling CBL a theory. TXLogic's criticism
shows just how generous this is.
[2] More generosity.
--
Jesse F. Hughes
"Penguins are so sensitive to my needs." --Lyle Lovett
TXLogic
> Defining Q to be Q={Q} no more constructs a Quine atom than defining
> N to be a counter-example to Goldbach's Conjecture constructs a
>
> How would you construct such a set? My solution is the first Google
> match on Quine Atom.
>
> > >http://cs.nyu.edu/pipermail/fom/2002-September/005844.html
>
> > If you've ever been curious about the fact that no one on FOM replied
> > to your request for comments, I'd suggest you have a look at Peter
> > Aczel's well-known 1983 study Non-Well-Founded Sets, where the
> > mathematics of structures such as those in your little example is
> > studied in depth.
>
> A. You're chomping
"champing" (Sorry, grammar geek here.)
> at the bit to prove me wrong. (You imply that repeatedly.)
Not at all. What I have on several occasions tried to point out is,
not that you are wrong, but that what you are doing doesn't qualify as
mathematics -- not, as you like to imply, because it runs contrary to
received wisdom. Rather, the problem is simply that your efforts do
not satisfy even the most minimal standards of rigor required for
something to *count* as mathematics. The problem with your little
example of a Quine atom, in particular, is not so much that it is
wrong but that is underspecified. You don't provide enough background
for it to count as a piece of mathematics. Additionally, you tend
then to present such underspecified results as if they were something
new. Notably, set theoretic structures containing Quine atoms are --
and had been for many years at the time of your FOM post -- extremely
well known and well understood; the two references I provided for you
study them in depth. (Aczel's study bases non-well-founded sets on
the theory of labeled graphs and uses that as a basis for proving what
he calls the Solution Lemma that characterizes precisely when a set is
a solution to a system of equations. Barwise and Moss go in the other
direction and start with the Solution Lemma as an axiom and derive the
correlations between non-wf sets and labeled graphs.)
To give just a bit more substance to my point about your example being
underspecified, here's what you say (I restrict attention to your
function s1):
> ...
> s1(x) = { x(x) }
>
> ...s1 takes in function x, applies x to x, and returns
> the set containing the value of x applied to x.
>
> 1. Consider the following specific set:
>
> s1(s1) = { s1(s1) }
>
> Thus s1(s1) is a Quine atom, a set that contains only itself.
Ok, that might be. What's missing is the specification of a framework
in which the claim can be assessed. Currently it is about as much an
example of a Quine atom as "Let n be an even number that is not the
sum of two primes" is a refutation of Goldbach's Conjecture ;-).
There are several ways to approach the problem here. First, you need
to specify a framework on which the notion of a self-applicable
function makes sense. In standard ZF set theory, of course, as well
as in the typed lambda calculus, such functions are impossible. So
the question is, what framework are you using? Since you say that
s1(s1) is a set, the appropriate framework would appear to be some non-
well-founded set theory, such as ZFA -- ZFC - foundation + AFA, where
AFA is perhaps the most widely-adopted of several possible anti-
foundation axioms. Is that the one you are using? Your claim simply
has no purchase until we know.
Now let's look more closely at s1. You define s1 to be a function
such that s1(x) = { x(x) }. So, a few questions. First, what is x(x)
when x is not a function? What is, e.g., 0(0)? You could of course
dispense with that via some sort of convention, e.g., that x(x) = x
when x is not a function; or you could figure out some other way of
specifying s1 that doesn't use functional notation. Or perhaps you
intend your universe to consist entirely of functions, as in the
untyped lambda calculus. But you, not your reader, should be the one
to figure that out.
Second, and more seriously, how do we know that s1 exists at all? And
if it does, how do we know it is a set and not a proper class? In the
context of non-well-founded set theories, it is obviously NOT a set,
as there are proper class many self-applicable functions. (Proof: for
every set s, consider the function f_s = {<f_s,f_s>,<s,s>}, i.e., the
function that returns itself given itself and s given s, and is
undefined otherwise -- note I said *the* function f_s, which itself
embodies an assumption (or theorem) that needs to be made explicit
regarding the *uniqueness* of the solution of a system of equations.)
Hence, since (in standard non-well-founded set theories) a proper
class cannot be a member of a set or of itself, s1 cannot be in its
own domain. So your specification "s1(s1) = {s1(s1)}" is simply ill-
defined.
So, the point is, not that your little example is wrong or incoherent;
rather, it is that it is not framed in the context of enough
mathematics for the claim even to be assessed. This is exactly the
problem that is pervasive in your Arxiv paper where you attempt to say
what CBL is. Every single one of your "theorems" take a form similar
to your "demonstration" above of the existence of a Quine atom. The
claims are not so much false as simply unverifiable, due to huge gaps
that need to be filled with concrete mathematics.
> B. If you were to give a construction of a Quine Atom already published:
>
> 1. You would prove me wrong.
> 2. Everyone would be able to see it and see that you're right.
> 3. You will have proved your point.
> 4. It would be an easy thing to do.
Easy yes in the sense that the mathematics is not difficult. Not easy
to do in a usenet post, and also entirely pointless, because the
mathematics in question would require one to copy quite a few pages
out of an easily accessible text. But I will be happy to point
everyone to the construction you seek in Barwise and Moss's Vivious
Circles: see Chapter 10, pages 119-121. The Quine atom in question is
called Omega. In the context of ZFA, Omega is the unique solution to
the equation x = {x}. (BTW, do you have a proof of uniqueness? Or
non-uniqueness? Both are possible depending on the framework.) And,
wonder of wonders, it appears that Aczel's book is available on the
web: http://standish.stanford.edu/pdf/00000056.pdf. It appears to
have been scanned in and is a rather huge 35MB. The mathematics
needed for the construction of Omega is given in the first 5 pages
(and more rigorously in later pages) and the construction of Omega
itself is found on page 6, with discussion on the following pages that
motivate the introduction of his axiom AFA. (BTW, the pictures of
graphs in Aczel's exposition are not "flowcharts", as you seem to
characterize such pictures in another post. They are just
representations of mathematical graphs that could just as easily have
been represented explicitly as ordered pairs consisting of a set of
nodes and a binary relation (the set of arcs) over the nodes. Such
pictures are standard fare in texts on mathematical graph theory.)
> C. You decline to give a construction for a Quine Atom.
This being the web and all, I take it that links to explicit
constructions of the sort you are looking for will suffice. I hope
you, or at least others, will find them useful and illuminating.
MoeBlee
> Do you deny that CBL is a Computationally Based Logic? Do you know of
> any more standard Computationally Based Logics?
Define 'computationally based logic'.
MoeBlee
MoeBlee
> On May 18, 1:09 pm, MoeBlee <jazzm...@hotmail.com> wrote:
> > Very well, then would you please indicate exactly where in the FOM
> > archives there is a reply?
>
> You stupid fuck. http://cs.nyu.edu/pipermail/fom/2002-September/005854.html
I simply asked you where such a post appears. And for that I get
called by you a "stupid fuck". You really got it going on there,
Charlie-Boo.
MoeBlee
MoeBlee
> On May 18, 1:13 pm, MoeBlee <jazzm...@hotmail.com> wrote:
>
> > On May 18, 4:12 am, Charlie-Boo <shymath...@gmail.com> wrote:
>
> > > On May 17, 11:19 pm, MoeBlee <jazzm...@hotmail.com> wrote:
> > > > Your mindless and irresponsible claims about Norm
> > > > Megill's system is another example.
>
> > > If you want to debate that system, it would help to start a new
> > > thread. He uses an expression like xRy(Rz)=(xRy)Rz and substitutes +
> > > for R but there is nothing at that point about + or - so - could
> > > equally well be substituted for R.
>
> > Silly boy, there is an hypothesis of that theorem that you have not
> > shown is satisfied by subtraction. That has been pointed out to you
> > already by a few other posters.
See, I repeat, you have not shown that subtraction satisfies the
hypotheses.
> > > There is also the general question of what ZFC alone can prove and
> > > what he says regarding that question and what his site shows.
> > You don't know what ZFC is.
> Published papers don't even agree as to what ZFC is. But I know
> exactly what it is. What is it? Then I'll say. It has to do with
> Computationally Based Logics.
There are various formulations of formal ZFC, but they are not so
dissimlar that a general definition can't be given. And what you know
exactly is what you BELIEVE ZFC to be. From your postings in the
thread that discussed ZFC proving general results in mathematics, it's
clear that you don't know what ZFC is.
MoeBlee
Charlie-Boo
*sigh*
A Propositionally Based Logic (e.g. PA) expresses assertions about
relationships among objects in a universal set. Call this an N-N
system where N is the cardinality of the universal set. This model is
suitable for expressing only mathematics.
In contrast, a Computationally Based Logic (e.g. CBL) expresses
relationships among disparant sets, of differing cardinalities.
Relating these sets (e.g. the set of Turing Machines and the set of
one-place functions from N to N) requires computing so that the
smaller set can equate with a subset of the larger set that includes
elements arbitrarily close to every element of the larger set.
Then assertions in a Computationally Based Logic are about the
computing power of various systems. Primitive assertions are not that
one element is less than another, but about the nature of the less
than relation itself. We can express assertions about sets being
expressible, representable, recursive, recursively enumerable,
defining a set, stateable in English, and a whole host of
metamathematical notions. CBL's are ideal for metamathematics.
Ok so far?
C-B
> MoeBlee