Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: Number of variables needed to axiomatize first order predicate calculus?
Replies: 6   Last Post: Mar 15, 2013 11:25 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
me 154934

Posts: 32
Registered: 10/1/12
Re: Number of variables needed to axiomatize first order predicate calculus?
Posted: Mar 15, 2013 8:55 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

On Mar 15, 1:46 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
> On Mar 13, 5:54 pm, George Greene <gree...@email.unc.edu> wrote:
>
>
>
>
>
>
>
>
>

> > On Mar 8, 6:02 pm, Frederick Williams <freddywilli...@btinternet.com>
> > wrote:

>
> > > It is well known that at least three variables are needed to axiomatize
> > > sentential calculus, by which I mean that at least three letters are
> > > needed to write down the axioms and rules.

>
> > Come ON!  You can't take your own question seriously until
> > and UNLESS YOU FIRST *specify* a *specification*LANGUAGE*!!

>
> > The specification-language you used to specify the axioms of
> > propositional calculus
> > is one that NO ONE HAS *EVER* seen used IN ANY other context!
> > It basically just copies the grammar of the underlying language AS
> > ASSUMED
> > and then INTRODUCES A CONCEPT from a COMPLETELY HIGHER ORDER,
> > namely first-order, without ANY PRETEXT of explication!  It
> > universally quantifies
> > over the things that it is trying to "specify", even though universal
> > quantification
> > is EXPLICITLY PROHIBITED in the object-language and even though this
> > specification
> > language itself does NOT explicitly contain any quantifier-symbols!
> > It is EASY to
> > "get small" if you just LEAVE OUT WHOLE CHUNKS of explication of what
> > you
> > are doing!

>
> > The use of ","(comma) and "/"(slash) for clarifying that from some
> > finite collection
> > of input sentences, you can infer some other finite collection of
> > output sentences,
> > IS (thank god) used elsewhere and I suppose that could be tolerated as
> > being a
> > paradigm-wide linguisitic convention for the specification of logics-
> > as-collections-
> > of-rules-in-general ANYway.  You could certainly begin this quest by
> > saying that you
> > would like to state all the inference rules of first-order logic using
> > this comma/slash
> > framework.

>
> > But in general it is just going to be MUCH HARDER because arguably THE
> > MOST
> > important inference rule in FOL is NOT an inference rule simpliciter,
> > but RATHER
> > a META-inference rule, or, literally, a SECOND-ORDER*FIRST-ORDER*-
> > inference-rule,
> > namely, UNIVERSAL GENERALIZATION, in which you infer a sentence in FOL
> > (a universally
> > quantified sentence) NOT from some prior collection of sentences but
> > rather FROM A *PROOF*!
> > Basically, from [ B |- phi(x) ], where B is a finite set of sentences
> > with x not occurring in them,
> > you infer Ax[phi(x)].  The mere DARING of this NESTING of "|-" -- not
> > to mention, HOW MANY
> > VARIABLES does it take TO EVEN STATE the non-occurrence clause?? --
> > the rule could
> > basically be written [ B |- phi(x) ] |- Ax[phi(x)]  -- oh, and HOW
> > MANY VARIABLES does it
> > take to explain what x *as*parameter*of*phi(.)* means, as OPPOSED to
> > what variables
> > mean in other contexts -- remember, in your propositional/0th-order
> > treatment, variables
> > ONLY meant PROPOSITIONS -- is certainly BEYOND the pale of ANY
> > specification language that you might have been trying to use FOR ANY
> > OTHER purpose!
> > If the language in which you are doing this is not CONSTANT (or at
> > least constant in
> > paradigm or parametric profile) across the various languages&levels-of-
> > logics that
> > you are investigating, then "the number of variables it takes" is just
> > not going to be
> > meaningful as a metric.  Oh, yeah, and then you also have to ask how
> > many variables
> > it takes to explain what kind of thing "phi(.)" is.  Phi(.) is after
> > all ITSELF a universally
> > quantified VARIABLE.

>
> Eventually you should arrive at a n-OL logic with syntax complex
> enough to encapsulate n-OL.
>
> But 2OL needn't be MORE complex SYNTAX, just fewer restrictions.
>
> e.g.  lowercase = terms, uppercase = variables
>
> 1OL
> add( M, 0, M )
> add( M, s(N), (S) ) <-  add( M, N, S ).
>
> 2OL
> P(s(0)) <- ( P(X) -> P(s(X) ) & P(0) )
>
> this is HIGH ORDER PROLOG where predicates may be VARIABLES and match
> to generic prolog clauses.  e.g. P could match with notsmallest(X),
> where notsmallest(X)->notsmallest(X+1)
>
> -------------------------------
>
> Now all the AXIOMS of the theory may be written in a SUBSET of the
> full 1OL.
>
> e.g.  HORN CLAUSES using only
>
> p1(...) & p2(...) & p3(...)  ->   pa(...)
>
> -----------------------------
>
> What you want to look for is a SUBSET of the (1OL) language that can
> perform some computational feat - e.g. be Turing Machine Equivalent.
>
> Horn Clauses have this property since
>
> UNIFY(  f(a,b,c...)  , f2(z,y,x,...) )
>
> which finds a COMMON predicate between 2
> is Turing Equivalent.
>
> Then this computation method must be utilised to EXPAND on the limited
> 2OL syntax.
>
> -------------------------
>
> The way I do this is using Naive Set Definition to specify which
> variable in each predicate a SET is referencing.
>
> e( A, evens ) :-  even(A).
>
> *this example is simple, even() only has one argument.
>
> Then I can process ALL() quantifiers via Set References, rather than
> explicitly stating which term to Quantify over in Quantified Logic
> style..  A(x), p(...x...) >=...
> which is rather messy with partial formula insides hanging out like
> that!.
>
> ---------------------------
>
> So yes you can INCREASE the complexity of 2OL syntax, but it's going
> to get convoluted with string processing and looking inside predicate
> types, or you can use a subset of 1OL syntax to write the axioms which
> work on a simpler processing system which can still do the computing
> work necessary.
>
> e.g.   Not All Numbers Are Evens
>
> ~A(X) e( X, evens )
>
> I bypass referencing internals by using Set Referencing
>
> !(ss( nats, evens ))
>
> Not all members of nats are members of evens.
>
> -------------------------
>
> which is in Horn Clause format same as 2OL axioms and computable!
>
> !(ss( S1, S2 )  <-   intersect( S1, !(S2)).
>
> A 2OL Axiom.
>
> (which will return the 1st ODD when invoked)
>
> Herc
>
> --www.BLoCKPROLOG.com


Oix



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.