Formal Theory means all sentences in the Theory are systematically
enumerated.
ZFC is NOT a formal Theory!
There is no method given to distinguish between theorems and predicate
calculus formulas.
X=X is a formula.
!(X=X) is a formula.
E(X) !(X=X) is a formula.
XeX is a formula
!(XeX) is a formula
XeY is a formula
XeY <-> !(XeX) is a formula
A(X) XeY <-> !(XeX) is a formula
E(Y)A(X) XeY <-> !(XeX) is a formula
there are many, many wrong formulas in Predicate Calculus.
> Formal Theory means all sentences in the Theory are systematically
> enumerated.
> ZFC is NOT a formal Theory!
> There is no method given to distinguish between theorems and predicate
> calculus formulas.
> [...]
> You have NO WAY of enumerating Theorems!
What is enumerated is G\"odel numbers of theorems. So which theorem
comes first depends on the enumerator and the G\"odel numbering.
-- Where are the songs of Summer?--With the sun,
Oping the dusky eyelids of the south,
Till shade and silence waken up as one,
And morning sings with a warm odorous mouth.
> interpreter BASIC ............. you must be 60 years old.
My first access to computers was with an interpreted basic system in the
early 1970's. Odd that when I first read your comment about being 60 it
seemed way too high. But them I remembered I'm 56 soon, so 60 really is
about right. Odd that I don't feel anything like "60". I think that's
because I started to ignore my age once I hit 50 so I still feel like I'm
in my 40's. :)
> > interpreter BASIC ............. you must be 60 years old.
> My first access to computers was with an interpreted basic system in the
> early 1970's. Odd that when I first read your comment about being 60 it
> seemed way too high. But them I remembered I'm 56 soon, so 60 really is
> about right. Odd that I don't feel anything like "60". I think that's
> because I started to ignore my age once I hit 50 so I still feel like I'm
> in my 40's. :)
The question shouldn't be "When did you *first* use interpreted basic?". It
should be "When might someone reasonably *last* have used it?" I recall
using line-numbered basic at work in the late 1980s, so 60 is way to high as
you first thought.
> > > interpreter BASIC ............. you must be 60 years old.
> > My first access to computers was with an interpreted basic system in the
> > early 1970's. Odd that when I first read your comment about being 60 it
> > seemed way too high. But them I remembered I'm 56 soon, so 60 really is
> > about right. Odd that I don't feel anything like "60". I think that's
> > because I started to ignore my age once I hit 50 so I still feel like I'm
> > in my 40's. :)
> The question shouldn't be "When did you *first* use interpreted basic?". It
> should be "When might someone reasonably *last* have used it?" I recall
> using line-numbered basic at work in the late 1980s, so 60 is way to high as
> you first thought.
> Another point that makes enumeration irrelevant is that all the new
> theorems
> that you get from the axioms were in fact already present from the
> UNDERLYING VALIDITIES that were provable FROM NO axioms,
> because every proved theorem only USES a FINITE number of the axioms.
> Thus, if the theorem was "h" and the axioms (or instances of axioms)
> used
> to prove it were a,b,c,d,f, and g, then
> a^b^c^d^f^f->h
> WAS ALREADY A THEOREM of *pure* predicate calculus, was ALREADY
> a first-order validity. So there really is a sense in which the
> axioms merely
> highlight a subset of the validities, as opposed to adding new stuff.
> The order in which this highlighting occurs IS NOT important.
> I'm SORRY FOR YOU, HERC, that the only treatment YOU have seen
> HAPPENS to STRESS the "enumeration". You're a victim of a lame
> education.
> Which would be easily cured if you only had sense enough to read
> ANOTHER book.
You can stick to "ENUMERABLE" if you are too clueless to WORK_OUT the
ENUMERATION.
ATLEAST THAT'S SOMETHING TANGIBLE!
BUT YOU ARE CONTRADICTING YOURSELF ALL OVER THE PLACE.
YOU SAID THE SET OF TRUTHS ARE 'AUTOMATIC' AND NOT POSSIBLE TO DERIVE
FROM AN ALGORITHM.
Herc
--
GEORGE'S SET THEORY!
*****************************
GEORGE'S RELATION ALGEBRA!
aRb
GEORGE'S INFERENCE RULES!
P -> P
~(X -> ~X)
a^b^c^d^f^g->h
> > Formal Theory means all sentences in the Theory are systematically
> > enumerated.
> > ZFC is NOT a formal Theory!
> > There is no method given to distinguish between theorems and predicate
> > calculus formulas.
> > [...]
> > You have NO WAY of enumerating Theorems!
> What is enumerated is G\"odel numbers of theorems. So which theorem
> comes first depends on the enumerator and the G\"odel numbering.
Give them the Godel number consisting of the number of the first
symbol times 100 plus the number of the second symbol etc. so the
order of the numbers and of the wffs coincide. Then the first one is
the theorem that is alphabetically first. Which one is that?
Or better yout, just start enumerating theorems and stop after the
first one and tell us what it is ok?
What is theorem 1? Excellent question. A question that one could
easily answer for any genuine axiomatic system!!!!!
> --
> Where are the songs of Summer?--With the sun,
> Oping the dusky eyelids of the south,
> Till shade and silence waken up as one,
> And morning sings with a warm odorous mouth.
> On Oct 9, 6:01 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> > So the AXIOMS are a *CONSTRAINT* what formula are allowed.
> No. *NOTHING* is "allowed". "Allowed" is not a relevant status.
> The formulas come from a first-order LANGUAGE with a SIGNATURE.
> The signature is a list of predicate- and function- NAMES, each of
> which has an -arity (a number of arguments). ALL of the well-formed
> formulas in the relevant
> first-order LANGUAGE are built out of logical symbols predicates,
> applied to arguments that are built out of these functions.
> > [2]
> > > (P->Q)->((P^R)->Q) IS A TAUTOLOGY -- and there are MANY SIMPLE
> > > "algorithms" that PROVE THAT THAT IS A TAUTOLOGY!
> > only in FOL.
> You are LYING. Tautologies are from *0*-OL.
> > Axioms (R here) are 2OL or 3OL (Regularity)
> NO, you are lying AGAIN. The VERSION of set theory that we are
> talking about
> here IS *1ST*-order ZFC! The LANGUAGE that all these formulas
> (including
> all the axioms) come from is a *1ST*-order language! The LOGIC in
> which
> we are deriving these proofs IS *1ST*-order logic!
> > >You need ZFC to tell you what sets DO exist! -- This validity ONLY
> > >tells you that a certain kind of set canNOT exist!
> > ALL(set) mem e set IFF p(mem,set)
> > AND EXIST(anotherset) mem e anotherset
> > This is what ZFC does, limits the relation 'e'.
> Exactly. It *defines* e.
> With no axioms, e wouldn't mean anything at all.
> With no axioms, you would HAVE NO WAY OF TELLING whether
> the "e" in ~Er[ xer <-> ~xex ] meant
> "_ shaves _ " (in which case the sentence would mean "there is no
> barber
> who shaves all and only those barbers who don't shave themselves") or
> "set _ is a member of set _ " (in which case the sentence would mean
> there
> is no set whose members are all&only those sets that are not members
> of themselves).
> In all these theories, the axioms constrain the meaning or
> interpretation
> of the functions and predicates occuring in them.
> > [4]
> > What's the difference between Predicate Calculus
> > and Naive Set Theory.
> Predicate calculus is a calculus. It's a logic. It is defined by its
> INFERENCE RULES. It's used to prove/derive/infer THEOREMS
> *from*prior* assumptions.
> SOME theorems (like P V~P) can be inferred or derived (USING THESE
> RULES, AND USING THE ALGORITHMS DEFINED for applying these rules) FROM
> NO prior assumptions. But the formulas so proved/derived/assumed need
> to be in a first-
> order LANGUAGE, first.
> Naive set theory is a theory. WITH AXIOMS.
> > They are both ZERO-AXIOM logic systems.
> NO, THEY ARE NOT. Naive Set Theory IS NOT a "logic system".
> It's a A THEORY. WITH SOME AXIOMS. ONE OF ITS AXIOMS IS
> the NAIVE set-COMPRENSION axiom, ExAy[ yex <-> phi(y) ].
> This is an axiom-schema saying that you get an axiomatic automatically
> proven-true theorem confirming the existence of a set corresponding
> to EVERY predicate phi(.) that is definable in the language.
> In particular, it says you get a set when phi(y) means ~yey.
> SO THIS THEORY IS INCONSISTENT.
> This theory is *IN* predicate calculus. It's UNDER predicate
> calculus.
> It's worked with USING predicate calculus, IN THE FRAMEWORK of
> predicate calculus.
> > If NST is inconsistent, what rules in Predicate Calculus
> > are you using to ensure ZFC does not inherit NST inconsistency?
> We are using THE SAME rules of predicate calculus FOR BOTH
> ZFC and NST.
> There is NO inheritance because ZFC *replaces* NST's
> NAIVE set-COMPREHENSION axiom with the axiom of
> SEPARATION.
> It is the naive set-comprehension axiom that causes the problem.
> That axiom is inconsistent/paradoxical in itself.
> It simply CANnot be the case that EVERY predicate defines a set.
> You need a more complicated, less naive set of axioms to define sets.
> Zermelo gave a first one in 1903.
> Frankel filled in an obvious hole later (That is how we got ZF).
> The axiom of choice seemed like an obvious hole too, but that
> got very complicated for about 30 years from 1936-66.
So this formula is barred!
ExAy[ yex <-> phi(y) ].
Now you're saying Predicate Calculus (with only infererence rules
over predicates which you wrongly call FOL)
P -> P
~P v P
(P ^ Q) -> P
....
and a few more like that..
OK so you DEFINE THE MEANING OF 'e' purely for use at the AXIOM LEVEL.
and you STILL GET THE PARADOX:
E(rs) A(x) x ee rs <-> !(x ee rs)
in Predicate Calculus.
Predicate Calculus WORKS ALL OF THIS OUT,
it does resolution, consistency checks, et al
(using FOL INFERENCE RULES (ranging over variables))
PC is consistent because it derives
NOT[ EXIST(rs) A(x) x ee rs <-> !(x ee rs) ]
and prevents E(rs) going on the LHS of any further consistent
inferences.
BUT, JUST TO BE DOUBLE SURE...
the SETS REALLY DO EXIST IN THE AXIOMS LEVEL
by BARRING rs from instantiating with 'e' too.
since 'e' is now a reserved letter,
(implicit by being a new symbol in the axioms)
***********
WRONG GEORGE!
You're flicking in and out of
FORMULA SYNTAX CALCULUS
1OL, 2OL, 3OL
INFERENCE vs MODUS PONENS
NAIVE SET THEORY
CONSISTENCY BY VERIFICATION THEORY
CONSISTENCY BY STRATIFICATION THEORY
CONSISTENCY BY FORMULA RESTRICTION
(of the term 'e')
You have no LOGIC THEORY, you have an ORACLE, you have DERIVED SETS
with no RUSSELL SET
for the 20TH TIME HERE:
E(X) NOT(X=X)
is in the language of predicate calculus.
YOU DON"T HAVE A TRANSITIVE CLOSURE OF LOGIC
BASED ON INFERENCE RULES
and if you did THEY CERTAINLY WOULDN'T BE FOL
THEY WOULD NECESSARILY RANGE OVER FORMULAS.
> The consequence relation for standard classical first-order logic IS
> SEMI-decidable.
> The reason it is not a decision procedure is that there is no
> algorithm that can confirm
> (in the general case) that a first-order wff is NOT valid when it's
> NOT (although that is also
> confirmable SOMEtimes -- every confirmation that a wff IS valid is
> also a confirmation&proof
> that its denial is not).
> > So much for your ALGORITHMIC proof that
> > ~E(r) xer <-> ~xex
> > is a part of ZFC AUTOMATICALLY.
> NO, DUMBASS -- THERE IS a proof -- so, therefore, there is, also, by
> definition, AN ALGORITHM that CONFIRMS
> the existence of a proof -- that
> ~Er[ xer <--> ~xex ] is valid.
> If you had any sense you would just PRESENT THIS PROOF YOURSELF.
I don't present proofs.
I enter them into proof software and claim the theorem is true as far
as the axioms and consistency of the proof software is concerned.
> BECAUSE this proof depends ON NO axioms -- LOGICAL OR OTHERWISE --
> this sentence is necessarily valid
> and necessarily a theorem OF ALL first-order formal theories in which
> IT CAN BE STATED AT ALL, i.e., in which
> a binary predicate e is in THE FIRST-ORDER LANGUAGE in which the
> theory is being phrased.
> All those theories "have" or "contain" (a theory is a set of sentences
> that is closed under logical consequence)
> all the first-order validities PLUS their axioms PLUS the theorems
> THAT FOLLOW FROM their axioms.
..because you say so.
Where on EARTH have you guys been HIDING this
******************************************************
*PLATONIC WORLD OF ABSOLUTE TRUTHS*
******************************************************
FOR THE LAST 10 YEARS YOU'VE BEEN DENYING
1 SINGLE FORMULA IS BONA FIDE TRUE#.
As far as MATHS AND LOGIC is CONCERNED
#TRUE = W.R.T. STATED AXIOMS
I have not SEEN a FORMAL PROOF BY RESOLUTION ONCE on SCI.LOGIC.
I wan't born with
T |- formula & ~formula
->
! (T |- formula )
&
T |- ~EXIST(formula)
embedded into my AXIOMLESS AUTOMATIC Thought Processes!!
Last chance George, put up THEOREM 1 of your AXIOMLESS LOGIC THEORY or
SHUT UP!
In article <458567d7-d298-4c8f-af7d-36473f1ae...@n16g2000yqi.googlegroups.com>,
<camgi...@hush.com> wrote:
>> THERE IS, however, an algorithm that CONFIRMS that a formula is
>> logically valid WHEN IT IS.
>so why can't you do brute force lexicographically on ALL formulas and
>output
>VALID
>NOT VALID
Because there isn't an algorithm that confirms that a formula is
invalid when it is.
> In article <458567d7-d298-4c8f-af7d-36473f1ae...@n16g2000yqi.googlegroups.com>,
> <camgi...@hush.com> wrote:
> >> THERE IS, however, an algorithm that CONFIRMS that a formula is
> >> logically valid WHEN IT IS.
> >so why can't you do brute force lexicographically on ALL formulas and
> >output
> >VALID
> >NOT VALID
> Because there isn't an algorithm that confirms that a formula is
> invalid when it is.
> -- Richard
[GG]
THERE IS, however, an algorithm that CONFIRMS that a formula is
logically valid WHEN IT IS.
Use this!
if (valid(formula)) write (formula + " is valid")
else write (formula + " is not valid")
What are you saying, valid() doesn't halt when the formula is invalid?
So FUCKING what??
That's a quote in the context OF THAT treatment. And you should have
NAMED the treatment or article.
Nothing IS EVER "a quote from WIKI". What it IS is "a quote from the
Wikipedia article on <whatever>."
DIFFERENT wikipedia articles are going to treat the SAME topic
DIFFERENTLY!!
Any time anybody is trying to explain anything to you, they may have
to tell you
what THEIR terms mean in the context of THEIR presentation. This does
NOT
obligate OTHER people to use those terms in the same way. FOR
EXAMPLE:
IF YOU GOOGLE (jointly) the pair of terms "Deductive System" and
"Inference Rule",
you will get, FROM THE WIKIPEDIA ARTICLE ON First-Order Logic, (all
that follows is quoted from the article)
>> Deductive systems
A deductive system is used to demonstrate, on a purely syntactic
basis, that one formula is a logical consequence of another formula.
There are many such systems for first-order logic, including Hilbert-
style deductive systems, natural deduction, the sequent calculus, the
tableaux method, and resolution. These share the common property that
a deduction is a finite syntactic object; the format of this object,
and the way it is constructed, vary widely. These finite deductions
themselves are often called derivations in proof theory. They are also
often called proofs, but are completely formalized unlike natural-
language mathematical proofs.
A deductive system is sound if any formula that can be derived in the
system is logically valid. Conversely, a deductive system is complete
if every logically valid formula is derivable. All of the systems
discussed in this article are both sound and complete. They also share
the property that it is possible to effectively verify that a
purportedly valid deduction is actually a deduction; such deduction
systems are called effective.
A key property of deductive systems is that they are purely syntactic,
so that derivations can be verified without considering any
interpretation. Thus a sound argument is correct in every possible
interpretation of the language, regardless whether that interpretation
is about mathematics, economics, or some other area.
In general, logical consequence in first-order logic is only
semidecidable: if a sentence A logically implies a sentence B then
this can be discovered (for example, by searching for a proof until
one is found, using some effective, sound, complete proof system).
However, if A does not logically imply B, this does not mean that A
logically implies the negation of B. There is no effective procedure
that, given formulas A and B, always correctly decides whether A
logically implies B.
Rules of inference
Further information: List of rules of inference
A rule of inference states that, given a particular formula (or set of
formulas) with a certain property as a hypothesis, another specific
formula (or set of formulas) can be derived as a conclusion. The rule
is sound (or truth-preserving) if it preserves validity in the sense
that whenever any interpretation satisfies the hypothesis, that
interpretation also satisfies the conclusion.
For example, one common rule of inference is the rule of substitution.
> So FUCKING what??
> That's a quote in the context OF THAT treatment. And you should have
> NAMED the treatment or article.
You can't follow the context of this quote?
----8<----------------------------
> > >http://en.wikipedia.org/wiki/First-order_logic > On Oct 12, 3:02 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
> > Hilbert-style systems and natural deduction
> Why are you bothering to quote a difference between
> Hilbert-systems and natural-deduction-systems?
> What difference does THAT make?
deductive system is a list of formulas,
each of which is a logical axiom
(taken from full paragraph in previous post which you didn't read)
> So FUCKING what??
> That's a quote in the context OF THAT treatment. And you should have
> NAMED the treatment or article.
> Nothing IS EVER "a quote from WIKI". What it IS is "a quote from the
> Wikipedia article on <whatever>."
> DIFFERENT wikipedia articles are going to treat the SAME topic
> DIFFERENTLY!!
> Any time anybody is trying to explain anything to you, they may have
> to tell you
> what THEIR terms mean in the context of THEIR presentation. This does
> NOT
> obligate OTHER people to use those terms in the same way. FOR
> EXAMPLE:
> IF YOU GOOGLE (jointly) the pair of terms "Deductive System" and
> "Inference Rule",
> you will get, FROM THE WIKIPEDIA ARTICLE ON First-Order Logic, (all
> that follows is quoted from the article)>> Deductive systems
> A deductive system is used to demonstrate, on a purely syntactic
> basis, that one formula is a logical consequence of another formula.
> There are many such systems for first-order logic, including Hilbert-
> style deductive systems, natural deduction, the sequent calculus, the
> tableaux method, and resolution. These share the common property that
> a deduction is a finite syntactic object; the format of this object,
> and the way it is constructed, vary widely. These finite deductions
> themselves are often called derivations in proof theory. They are also
> often called proofs, but are completely formalized unlike natural-
> language mathematical proofs.
> A deductive system is sound if any formula that can be derived in the
> system is logically valid. Conversely, a deductive system is complete
> if every logically valid formula is derivable. All of the systems
> discussed in this article are both sound and complete. They also share
> the property that it is possible to effectively verify that a
> purportedly valid deduction is actually a deduction; such deduction
> systems are called effective.
> A key property of deductive systems is that they are purely syntactic,
> so that derivations can be verified without considering any
> interpretation. Thus a sound argument is correct in every possible
> interpretation of the language, regardless whether that interpretation
> is about mathematics, economics, or some other area.
> In general, logical consequence in first-order logic is only
> semidecidable: if a sentence A logically implies a sentence B then
> this can be discovered (for example, by searching for a proof until
> one is found, using some effective, sound, complete proof system).
> However, if A does not logically imply B, this does not mean that A
> logically implies the negation of B. There is no effective procedure
> that, given formulas A and B, always correctly decides whether A
> logically implies B.
> Rules of inference
> Further information: List of rules of inference
These are just INFERENCES mind you.
You still owe me some BASE THEOREMS, otherwise all your "proofs" are
Oracular.
Mind you, only 1 inference rule is needed, modus ponens and it can
pattern match the rest as axioms, since modus ponens will CREATE A NEW
FORMULA as well as derive it, so there only has to be one inference
rule that instantiates new formula.
But anything in the form LHS -> RHS can be used to instantiate a new
line, fine with me. ;-)
On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> RESOLUTION IS STATED AS:
> ((p v q) ^ (!p v r)) -> (q v r)
> So you have to get
> xRr <-> !xRr
> p = xRr
> !p = xRr
> ???
> Mind you, only 1 inference rule is needed, modus ponens
Resolution is also complete as an "only needed" inference rule, but
these things
are not complete in the way you think. If you are using MP as your
only inference rule
then --> IS YOUR ONLY CONNECTIVE, so you have to RE-WRITE any and
everything
that started out using /\ , V , or <--> TO USE --> INSTEAD,
IF you are going to use nothing but MP.
Similarly, since resolution ONLY operates on conjunctions of
disjunctions,
IF you are going to use resolution as your only inference rule, THEN
you AGAIN
have TO REWRITE everything that PREVIOUSLY had <--> or /\ in it AS a
collection
of disjunctions.
In particular (going for resolution),
p <--> q becomes
p --> q And q --> p; so, therefore,
--> is the wrong connective for resolution; you have to translate -->
to V in order to use resolution.
Since, by definition, p --> q means ~p V q, the above pair of converse
conditionals become
~rRr V ~rRr and rRr V rRr .
Since disjunction is idempotent, each of these two-disjunct
disjunctions becomes a ONE-junct -junction (a "unit clause"), and the
two things you are trying to "resolve" become
~rRr resolved with rRr.
If you resolve THOSE two WITH EACH OTHER then you very quickly get
THE EMPTY CLAUSE, which is a "proof of false", which proves that the
original collection
of disjunctions was inherently contradictory, which is exactly the
result you want,
since this REALLY IS a paradox.
On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> You still owe me some BASE THEOREMS, otherwise all your "proofs" are
> Oracular.
No, I don't. I can just say that rule "EM" (that is what I choose to
call it)
allows me to infer P V ~P *FROM*NOTHING*.
Moreover, I can call the universal generalization of that (with P as
the variable) an inference rule (if I want to)
and say that if P is ANY WFF WHATSOEVER in the first-order langauge I
am using, then
P V ~P is inferred, as the conclusion of this inference rule, and as a
theorem,
FROM NOTHING.
That does NOT make anything "oracular" and it does NOT make anything a
"logical axiom".
I can [AND DO] JUST say that it is an inference rule that any
instance of a propositional tautology is a theorem.
camgi...@hush.com writes:
> On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:
>> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
>> > deductive system is a list of formulas,
>> > each of which is a logical axiom
>> NO, a deductive system IS NOT a list of formulas.
>> JEEzus.
> That's a quote from WIKI
Actually wiki says something quite different:
"A deduction in a Hilbert-style deductive system is a list of formulas,
each of which is ..."
> >> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> >> > deductive system is a list of formulas,
> >> > each of which is a logical axiom
> > On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:
> >> NO, a deductive system IS NOT a list of formulas.
> >> JEEzus.
> >> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com>
wrote:
> > That's a quote from WIKI
On Oct 14, 1:40 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
> camgi...@hush.com writes:
> Actually wiki says something quite different:
> "A deduction in a Hilbert-style deductive system is a list of formulas,
> each of which is ..."
> Alan Smaill
To Alan: Thank you kindly for your support.
To Herc: please try to prove that you are smart enough to parse a
complete sentence -- AS OPPOSED to stupid enough to take the object of
a prepositional phrase OUT OF CONTEXT and MISTAKE it for the subject
of the main verb (which subject you were stupid enough to cut, if you
were smart enough to even read it in the first place).
Clue: If you can't hack THE BASIC GRAMMAR OF *YOUR*OWN* native
language then there IS VERY LITTLE point in your even TRYING to deal
with a first-order language or any formal language! GRAMMAR IS
FUNDAMENTAL!
> > >> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> > >> > deductive system is a list of formulas,
> > >> > each of which is a logical axiom
> > > On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:
> > >> NO, a deductive system IS NOT a list of formulas.
> > >> JEEzus.
> > >> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com>
> wrote:
> > > That's a quote from WIKI
> On Oct 14, 1:40 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
> > "A deduction in a Hilbert-style deductive system is a list of formulas,
> > each of which is ..."
> > Alan Smaill
> To Alan: Thank you kindly for your support.
> To Herc: please try to prove that you are smart enough to parse a
> complete sentence -- AS OPPOSED to stupid enough to take the object of
> a prepositional phrase OUT OF CONTEXT and MISTAKE it for the subject
> of the main verb (which subject you were stupid enough to cut, if you
> were smart enough to even read it in the first place).
> Clue: If you can't hack THE BASIC GRAMMAR OF *YOUR*OWN* native
> language then there IS VERY LITTLE point in your even TRYING to deal
> with a first-order language or any formal language! GRAMMAR IS
> FUNDAMENTAL!
Hey don't burst an artery!
I quoted the whole paragraph and you ignored it!
You said WHY QUOTE THE DIFFERENCE BETWEEN
NATURAL AND HILBERT SYSTEMS?
so I quoted the part with ... IT HAS LOGIC AXIOMS.
LOGIC AXIOMS! THE TOPIC FOR 2 WEEKS.
the fact I made it look like a LIST OF LIST OF FORMULA
instead of a LIST OF FORMULA
is a typo!
YOU STILL LOSE, LOSERS!
You are a LONG WAY from PROVING
~E(r) xer <-> ~xex
with INFERENCE RULES.
FOR 1 THING - THERE IS A VARIABLE INSTANTIATION
and George is struggling with Supercombinator Theory to even know how
to do that with RULES.
*******
And for the 20th time!
Stop writing novels about OBJECT LANGUAGE CRAP!
What you are saying takes 1 line!
-> is logical implication
--> is implied theorem addition to the physical theory.
REMINDER
The topic is:
~E(r) xer <-> ~xex
is a formula *included* in ZFC (without axioms)
YOU HAVE NOT SHOWN THIS.
I think with a few RELATIONAL ALGEGRA AXIOMS
and VARIABLE INSTANTIATION RULES
you may be able to.
but I win, NO AXIOMS, no ~E(russell set) as a THEOREM in ZFC.
