RE: SUO: RE: Re: Peirce's MS 514
>The contributions of John S, Pat Hayes, Chris Menzel and
>others to this thread have helped clarify a lot of
>things that I thought I already understood. A short
>footnote to Pat's note--
>
>It is also amazing that there is such a large variety
>of useful (not necessarily complete) inference systems,
>involving various combinations of axioms,
>axiom schemata, and rules of inference. If
>one has only axioms, and no rules of inference, the theory
>is only the axioms (using theory to mean the body of
>statements that can be inferred, not the totality of
>what is entailed.) In logic programming, the rules in a
>program are usually regarded as axioms (insofar as we're
>speaking of rules with only logical intent). In extending
>prolog to a certain version of paraconsistent logic
>Vladimir Lifschitz proposes instead to regard the
>rules as rules of inference. This provides a completely
>new perspective on the 'meaning' of the logic programs
>in question.
Thanks for that note. Do you have a pointer to this work by Lifschitz?
There is a tradition called 'general logic' of rendering rules (of
inference) as assertions in another logic with a simpler or more
uniform system of rules. This has a lot in common with implementing
one virtual machine in another one, and many ties with computability
theory. In particular, there is a kind of uniform technique for
mapping many systems of rules into a 'universal logic' of functional
type theory - essentially, the lambda calculus with a sorted
functional syntax. The expressions of the orginal language map into
types, and the inference rules map into functions. Applying a rule
maps into a function call, where the type-matching of a function to
its arguments encodes the particular syntactic structures of the
original language. One can then think of this functional language as
a general-purpose meta-calculus for building *proofs* in the original
language; in other words, derivations map into terms. This makes
sense if you think of an inference rule as an operation on
derivations which 'outputs' a larger derivation when given smaller
ones as 'input', and you think of an expression as simply being a
kind of runty derivation (of itself from itself). See
http://www.dcs.ed.ac.uk/home/cdw/archive.html
and follow the links there for more information than one human brain can hold.
Pat Hayes
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes