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!