[FOM] Concerning Ancestral Logic

[Arnon Avron]

On Fri, Nov 03, 2006 at 03:35:20PM +1300, Bill Taylor wrote:
> This query is mainly directed to Arnon Avron, but no doubt others
> may feel like joining in.
> 
> Arnon - you have been extolling the virtues of AL as an alternative,
> (an extension?), of FOL.  It sounds good, but I don't yet 
> know what it is.   You mention it was given a treatment 
> in Shapiro's F-without-F, but I don't
> recall noticing it from when I read that.
> 
> So I wonder if you could give us all a brief rundown on it.
> Nothing too massively technical, but just enough to get the flavour
> and main ideas.  

Richard Heck has already partially replied to the question
what is ancestral logic. Let me add to what he wrote the following:

1) Actually, for full generality, one should consider not a single
TC operator, but for every n an operator TC^n, which applied to an
2n-ary predicate produces a new 2n-ary predicate (its transitive 
closure).  Thus the intuitive meaning of 
(TC^2_{x_1,x_2,y_1,y_2}A)(s_1,s_2,t_1,t_2) is:

 A(S_1,S_2,t_1,t_2) 

      or

 \exists z_1,w_1.
   A(s_1,s_2,z_1,w_1) and A(z_1,w_1,t_1,t_2) 

      or

 \exists z_1,w_1,z_2,w_2.
   A(s_1,s_2,z_1,w_1) and A(z_1,w_1,z_2,w_2) and A(z_2,w_2,t_1,t_2)

     or

     ...

(As I wrote in a previous posting, the main idea in using TC is
indeed to incorporate into the language a formal counterpart of 
"...", without introducing new objects).

In practice, it seems, one does not need more than TC^1 and TC^2. 
Of course, if the language contains the means to  introduce
ordered pairs than TC^1 suffices for defining TC^n for every n.
However, this is not the case without the presence of ordered pairs.
Thus + is not definable in the the language of 0 and S using
only TC_1. However, it  is easily definable if we use TC_2.
So although the natural numbers can be characterize categorically
in FOL(0,S)+TC^1, the expressive power of this language is too weak.
The exact situation is as follows: all recursive functions and 
relations are definable in either of:

FOL(=,0,S)    plus TC^2
FOL(=,0,S,+)  plus TC_1
FOL(=,0,S,+,x)          

[instead of FOL(=,0,S,+,x) one can use FOL(=,0,S,+,|) 
(where | is "divides")]

2) By generalizing a particular case which has been used by Gentzen
in his proof of the consistency of PA, mathematical induction can be 
presented as a *logical* rule of languages with $TC$. Indeed,
Using a Gentzen-type format, a general form of this principle in
the case of $TC^1$ can be formulated as follows:

\Gamma, A(x), B(x,y) => A(y), \Delta
-------------------------------------
\Gamma, A(s), (TC^1_{x,y})B(s,t) => A(t), \Delta

where $x$ and $y$ are not free in $\Gamma,\Delta$, and $y$ is 
not free in B.  

This is an introduction rule on the left. There are also obvious rules
for introducing TC on the right. In this way one gets a very natural
logical system in which, I believe (but have not tried to prove yet),
cuts are eliminable. I also believe that this system
is "complete" in some intuitive, imprecise sense, (or at least is 
strong enough for most needs).

3) In his paper "Finitary Inductively Presented Logics" (in
Logic Colloquium 1988, Amsterdam, North-Holland, pp.  191-220. 
Reprinted in the collection "What is a Logical System?", edited 
by D. Gabbay, Oxford Science Publications, Clarendon Press, 
Oxford, 1994), Feferman developed a general framework (called FS_0) 
for introducing and investigating formal systems. The main feature 
of FS_0 is that it provides a "comprehensive definition of a 
finitary inductive system which includes both languages and logics, 
and which covers all examples met in practice". The main observation 
on which FS_0 is based is that all major concepts needed to 
understand and use formal systems (like terms, formulas, and formal 
proofs) are inductively defined. Now the intended mathematical 
structure on which Feferman's framework is based is V_0, which is 
the  smallest set including $0$ and closed under the operation 
of pairing (as Feferman has shown, it is much more natural to work 
within V_0 than within the natural numbers, the use of which for 
the same goal requires heavy machinery of unnatural coding). 
Now FS_0 can most naturally be developed within a language which 
includes first-order variables, the constant 0, a binary function
symbol P (for a pairing function), equality, conjunction, disjunction,
negation and TC^1 (the existential quantifier can easily be defined
using TC_1). This is shown in my paper "Transitive Closure and the
mechanization of Mathematics"  (available from
my homepage: http://www.math.tau.ac.il/~aa). In that paper I proved 
also a result I have mentioned in a previous posting: that the 
relations on V_0 which are definable by the negation-free formulas 
of the above language are exactly the r.e. relations on V_0.

  These facts show that TC (together with the ability to introduce
ordered pairs) is exactly what one needs (and I claim: should) add
to FOL in order to introduce and investigate formal systems. In other
words: ONE CANNOT UNDERSTAND WHAT IS FIRST-ORDER LOGIC WITHOUT 
UNDERSTANDING TC and assuming the ability to use it.

4) Significant attention to logics with TC have been given 
within the area of Finite Model Theory (FMT).  The idea there is to
give purely logical characterizations to various complexity
classes. For this goal various "fix-point" logics have been
introduced, and ancestral logic belongs to this class (or is
a close relative of it). Details and references can be found
in one of the several textbooks on FMT which are now available
(e.g. the book of Ebbinghous and Flum, or the book of Libkin).
However, I don't think that the work on FMT has much relevance 
to FOM (but maybe other people on this list think otherwise).


Arnon Avron