[1]

So the AXIOMS are a *CONSTRAINT* what formula are allowed.

[2]

only in FOL.

Axioms (R here) are 2OL or 3OL (Regularity)

so they range over all expressions within their own theory
(including P and Q)
and LIMIT the usage/range of certain symbols.

[3]

ALL(set)  mem e set    IFF  p(mem,set)
         AND  EXIST(anotherset) mem e anotherset

This is what ZFC does, limits the relation 'e'.

[4]

What's the difference between Predicate Calculus
and Naive Set Theory.

They are both ZERO-AXIOM logic systems.

If NST is inconsistent, what rules in Predicate Calculus
are you using to ensure ZFC does not inherit NST inconsistency?

Herc

On Oct 9, 6:01 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

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.

You are LYING.  Tautologies are from *0*-OL.

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!

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.

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.

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.

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.

On Oct 12, 1:23 am, George Greene <gree...@email.unc.edu> wrote:

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..

et voila!

NOT( EXIST(INFERENCE) INFERENCXE=  ExAy[ yex <-> phi(y) ] )

******************

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.

Herc

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

No, it's not BARRED.  It isn't even a formula.
It's a SCHEMA.  It's A WHOLE BUNCH of formulas.
AND ONE of them, the one that you get when phi(y)=~yey,
PRODUCES A CONTRADICTION.
So this canNOT be an AXIOM-SCHEMA.  It is barred from THAT role.
But no formula, not even contradictions, is EVER barred just from
BEING a formula
and being IN the language, IF it's well-formed according to the rules
defining the language.
It's just false.  Or provably false.  But you would not be ABLE to
prove it "false" UNLESS
it first WERE a formula!  It is NOT *barred*, just because it is
disproved!

SHUT UP.  I'M the one with two degrees in it.
You do NOT KNOW enough to be telling me that *I* am calling anything
wrongly.
It is long past time you figured out WHO is TEACHING this course and
who is taking it.
You can type
"predicate calculus" "first-order logic" into Google and SEE FOR
YOURSELF what kind of relationship they are generally known to have.

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

Why do you keep starting sentences with "you're saying"??
and then following them with stuff *I*NEVER*SAID*???

I certainly never said that anything like what you are posting here is
FOL.
The things you just posted are TAUTOLOGIES FROM *0th*-order logic!

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

NO, DUMBASS, you get the paradox WITHOUT DEFINING ANY meaning for e.
ErAx[xRr <--> ~xrx]
is contradictory FOR ALL binary relations r, REGARDLESS of whether R
is
a, b, c, d, e, f, g, h, i, j, k, u, v, w, or shaves, or contains, or
wanks.

On Oct 11, 4:03 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

I'm certainly not THE ONLY one calling it that way, DUMBASS.

http://en.wikipedia.org/wiki/First-order_logic

On Oct 12, 2:06 pm, George Greene <gree...@email.unc.edu> wrote:

Hilbert-style systems and natural deduction

A deduction in a Hilbert-style deductive system is a list of formulas,
each of which is a logical axiom, a hypothesis that has been assumed
for the derivation at hand, or follows from previous formulas via a
rule of inference. The logical axioms consist of several axiom schemes
of logically valid formulas; these encompass a significant amount of
propositional logic. The rules of inference enable the manipulation of
quantifiers. Typical Hilbert-style systems have a small number of
rules of inference, along with several infinite schemes of logical
axioms. It is common to have only modus ponens and universal
generalization as rules of inference.

Natural deduction systems resemble Hilbert-style systems in that a
deduction is a finite list of formulas. However, natural deduction
systems have no logical axioms; they compensate by adding additional
rules of inference that can be used to manipulate the logical
connectives in formulas in the proof.

first-order logic is undecidable (although semidecidable), provided
that the language has at least one predicate of arity at least 2
(other than equality). This means that there is no decision procedure
that determines whether arbitrary formulas are logically valid. This
result was established independently by Alonzo Church and Alan Turing
in 1936 and 1937

******************

Also, this is what I was calling "AXIOMS" of predicate calculus the
other day.

http://en.wikipedia.org/wiki/First-order_logic#Provable_identities

Herc

On Oct 12, 3:02 am, Graham Cooper <grahamcoop...@gmail.com> wrote:

Something that is provABLE is BY DEFINITION *not* an AXIOM!
Axioms are what theorems get proven *FROM* --
THE WAY IT WORKS
is that you USE the rules of inference TO PROVE
*theorems*
FROM
the axioms!
So the fact that YOU were referring to something that is "a provable
identity"
as "an axiom" PROVES YOU'RE STUPID.
Or at least under-informed about what is going on around here.
But THAT
is not even the point.
THE POINT is that THERE ARE MANY EQUIVALENT
ways in which to define standard classical first-order logic
and the way I WAS TEACHING YOU *IN*THIS* course
is a way that defines it WITH NO AXIOMS AT ALL, because
it prefers instead to define it via RULES OF INFERENCE.
That would've been helpful FOR YOU because it would have
AVOIDED CONFUSING YOU
between axioms OF THE OBJECT THEORY (set theory
in this case) and axioms of THE LOGIC, which is a separate framework.

On Oct 12, 3:02 am, Graham Cooper <grahamcoop...@gmail.com> wrote:

Why are you bothering to quote a difference between
Hilbert-systems and natural-deduction-systems?

What difference does THAT make?

On Oct 13, 5:40 am, George Greene <gree...@email.unc.edu> wrote:

deductive system is a list of formulas,
each of which is a logical axiom

there is no decision procedure
that determines whether arbitrary formulas are logically valid

So much for your ALGORITHMIC proof that

~E(r) xer <-> ~xex

is a part of ZFC AUTOMATICALLY.

Herc

On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

NO, a deductive system IS NOT a list of formulas.

JEEzus.

THERE IS, however, an algorithm that CONFIRMS that a formula is
logically valid WHEN IT IS.
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).

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.

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.

On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:

That's a quote from WIKI

so why can't you do brute force lexicographically on ALL formulas and
output

VALID
NOT VALID

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 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!

Herc

In article <458567d7-d298-4c8f-af7d-36473f1ae...@n16g2000yqi.googlegroups.com>,

Because there isn't an algorithm that confirms that a formula is
invalid when it is.

-- Richard

On 13 Oct, 10:45, rich...@cogsci.ed.ac.uk (Richard Tobin) wrote:

[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?

Herc

On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

This is entirely -- ENTIRELY -- analogous to the case where there is
no TM-that-always-halts
(no decision procedure) that determines whether an arbitrary TM halts
on an arbitrary input-
string: THERE IS, HOWEVER, a TM that CONFIRMS that an arbitrary TM
*does* halt on an
arbitrary input string, WHEN the tm DOES halt on the string.
That's called the universal TM -- it can run ANY tm on ANY string and
just SEE WHAT HAPPENS.
If the TM halts on the string then the universal TM emulating that run
ALSO halts (yes/true/accept).

If a first-order formula is valid (or contradictory) then there IS an
algorithm that CONFIRMS that,
that halts PROVING that the formula is valid (or that its denial is
contradictory).
But it is not a decision-procedure in the general case, because in the
OTHER case,
in the OPPOSITE case, in the case where the formula you throw at this
algorithm
is NEITHER valid nor contradictory, the algorithm may fail to halt or
to give any final answer.
Just as will happen with the universal TM if you give it a TM and a
string on which the TM does NOT halt.

On Oct 12, 8:37 pm, camgi...@hush.com wrote:

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)

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.

On Oct 12, 8:52 pm, camgi...@hush.com wrote:

WELL DONE!
Congratulations!

On Oct 14, 1:48 am, George Greene <gree...@email.unc.edu> wrote:

You can't follow the context of this quote?

----8<----------------------------

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)

---------------------------

Logic axiom being the topic for the last 2 weeks.

Herc

On Oct 14, 1:48 am, George Greene <gree...@email.unc.edu> wrote:

These are just INFERENCES mind you.

You still owe me some BASE THEOREMS, otherwise all your "proofs" are
Oracular.

I'll print the table here, nice one!

http://en.wikipedia.org/wiki/List_of_rules_of_inference

----------------------------------

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 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.  ;-)

Herc

On Oct 13, 3:36 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > >
On Oct 12, 8:37 pm, camgi...@hush.com wrote:

Idiot,
YOU MISQUOTED IT.
 IT *DID*NOT*SAY* that "a deductive system is a list of formulas"!
IT SAID,
"A deduction in a Hilbert-style deductive system is a list of
formulas, each of which is a logical axiom, a hypothesis that has been
assumed for the derivation at hand, or follows from previous formulas
via a rule of inference."

It said a DEDUCTION, *NOT* "a deductive system", was a list of
formulas!
DAMN, you're stupid!
And it IS consistent with this for ZERO of them to be logical axioms!
What *IT* means by "logical axiom" CAN VARY from ONE Hilber-style
system TO ANOTHER.
AND THERE ARE SOME WITH *NO* "logical axioms"!

On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

NO, I DON'T.

In the NON-logical context, in the SET THEORY or NUMBER THEORY (Peano
Arithmetic)
or group theory OR ANY OTHER AXIOMATIC THEORY context, in the context
of anything
for which you might actually be USING first-order logic, any
investigation TO WHICH you might
be APPLYING first-order logic, what YOU are calling a "base theorem"
is called AN AXIOM.
That's what axioms ARE FOR.  They are true DESPITE not having any
proofs (other than "it's an axiom".)

In the pure-logical context, there is no difference between a logical
axiom and the conclusion of an inference
rule that infers/derives that conclusion FROM AN EMPTY set of
premises.
I'm NOT being ORACULAR when I insist that P V ~ P
is true, withOUT any proof in a FIRST-order system.  P V ~P
*is*ZEROth*-order, to start with.
First-order PRESUMES all that IN ONE handwave!

On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:

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,

rRr <--> ~rRr
becomes
(rRr -->  ~rRr)  and  (~rRr --> rRr).

--> 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:

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.

On Oct 14, 10:06 am, George Greene <gree...@email.unc.edu> wrote:

George, I don't care!

*I* use MODUS PONENS for inference and ANY OLE AXIOM and ANY THEOREM
SO FAR.

a & (a->b) --> b

*I* use double arrow --> for NEW THEOREM

If you want to use a list of inferences distinct from axioms, may I
suggest

(P ^ Q) --> Q

so we know it's not a THEOREM/AXIOM

The only lesson here is that there is SOME / ONE rule that operates ON
the theory by creating --> new formula which is distinct from the
theorems.

*************

In MY TERMINOLOGY, since you use "model" to mean "deduction sequence"
is meaningless.

A MODEL is CREATED in the theory like so:

a & (a ->[p->q]) -> [p->q]

NOW you have a 2ND LEVEL OF INFERENCE RULES  [p->q]

You could JUST USE MODUS PONENS TO DO THIS and a set of tautology
formula

but you like to have a list

1 P --> P
2 !P --> !P
...

which forces the prover into a single model.

Herc