Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language

Abstract

It is well-known that concepts and methods of logic (more specifically constructive logic) occupy a central place in computer science. While it is quite common to identify ‘logic’ with ‘first-order logic’ (FOL), a careful examination of the various applications of logic in computer science reveals that FOL is insufficient for most of them, and that its most crucial shortcoming is its inability to provide inductive definitions in general, and the notion of the transitive closure in particular. The minimal logic that can serve for this goal is ancestral logic (AL).

In this paper we define a constructive version of AL, pure intuitionistic ancestral logic (iAL), extending pure intuitionistic first-order logic (iFOL). This logic is a dependently typed abstract programming language with computational functionality beyond iFOL, given by its realizer for the transitive closure operator TC, which corresponds to recursive programs. We derive this operator from the natural type theoretic definition of TC using intersection type. We show that provable formulas in iAL are uniformly realizable, thus iAL is sound with respect to constructive type theory. We further outline how iAL can serve as a natural framework for reasoning about programs.

Appendix

In this appendix we provide full proofs of some of the results above.

1.1 Proof of Proposition 2:

The result immediately follows from TC Ind by taking $A\left( u,v\right)$ to be the formula $G\left( u\right) \Rightarrow G\left( v\right)$. $\square$

Lemma 1

The following are provable in iAL:

$$\begin{aligned} A\left( x,z\right) ,A^{+}\left( z,y\right)&\vdash A^{+}\left( x,y\right) \end{aligned}$$

(5)

$$\begin{aligned} A^{+}\left( x,z\right) ,A\left( z,y\right)&\vdash A^{+}\left( x,y\right) \end{aligned}$$

(6)

1.2 Proof of Lemma 1:

Both sequents are derivable by one application of TC Base followed by an application of TC Trans. $\square$

1.3 Proof of Proposition 3:

Denote by $\varphi \left( x,y\right)$ the formula $\exists z\left( A\left( x,z\right) \wedge A^{+}\left( z,y\right) \right)$. For (1) apply TC Ind on the following two subgoals:

• 1. $A\left( u,v\right) \vdash A\left( u,v\right) \vee \varphi \left( u,v\right)$

• 2. $A\left( u,v\right) \vee \varphi \left( u,v\right) ,A\left( v,w\right) \vee \varphi \left( v,w\right) \vdash A\left( u,w\right) \vee \varphi \left( u,w\right)$

(1) is clearly provable in iFOL. For (2) it suffices to prove the following four subgoals, from which (2) is derivable using Or Decomposition and Or Composition:

• 1. $A\left( u,v\right) ,A\left( v,w\right) \vdash \varphi \left( u,w\right)$

• 2. $A\left( u,v\right) ,\varphi \left( v,w\right) \vdash \varphi \left( u,w\right)$

• 3. $\varphi \left( u,v\right) ,A\left( v,w\right) \vdash \varphi \left( u,w\right)$

• 4. $\varphi \left( u,v\right) ,\varphi \left( v,w\right) \vdash \varphi \left( u,w\right)$

We prove $\varphi \left( u,v\right) ,\varphi \left( v,w\right) \vdash \varphi \left( u,w\right)$, the other proofs are similar. It is easy to prove (using Lemma 1) that $\exists z\left( A\left( v,z\right) \wedge A^{+}\left( z,w\right) \right) \vdash A^{+}\left( v,w\right)$. By TC Trans we can deduce $d:D,A\left( u,d\right) ,A^{+}\left( d,v\right) ,A^{+}\left( v,w\right) \vdash A^{+}\left( d,w\right)$, from which $\exists z\left( A\left( u,z\right) \wedge A^{+}\left( z,w\right) \right)$ is easily derivable.

The proof of (2) is similar. $\square$

1.4 Proof of Proposition 4:

(3) is derivable applying TC Ind on the following two subgoals:

• 1. $A\left( x,y\right) \vdash \exists zA\left( x,z\right)$, which is easily provable in iFOL.

• 2. $\exists zA\left( u,z\right) ,\exists zA\left( v,z\right) \vdash \exists zA\left( u,z\right)$, which is valid due to Hypothesis.

The proof of (4) is symmetric. $\square$

1.5 Proof of Proposition 5:

Denote by $\varphi \left( u,v\right)$ the formula $A\left( u,\overrightarrow{y}\right) \vee A\left( v,\overrightarrow{y}\right)$. The right-to-left implication follows from Proposition 4 since $\exists z\left( A\left( u,\overrightarrow{y}\right) \vee A\left( z,\overrightarrow{y}\right) \right) \vdash \exists xA\left( x,\overrightarrow{y}\right)$ can be easily proven in iFOL, and Proposition 4 entails that $\varphi ^{+}\left( u,v\right) \vdash \exists z\varphi \left( u,z\right)$. For the left-to-right implication it suffices to prove $d:D,A\left( d,\overrightarrow{y}\right) \vdash \varphi ^{+}\left( u,v\right)$. Clearly, in iFOL, $d:D,A\left( d,\overrightarrow{y}\right) \vdash \varphi \left( d,v\right)$ is provable, from which we can deduce by TC Base $d:D,A\left( d,\overrightarrow{y}\right) \vdash \varphi ^{+}\left( d,v\right)$. Since we also have $d:D,A\left( d,\overrightarrow{y}\right) \vdash \varphi \left( u,d\right)$, by Lemma 1 we obtain $d:D,A\left( d,\overrightarrow{y}\right) \vdash \varphi ^{+}\left( u,v\right)$. $\square$

Proposition 6

The following is provable in iAL:

$$\begin{aligned} \left( A^{+}\right) ^{+}\left( x,y\right) \vdash A^{+}\left( x,y\right) \end{aligned}$$

1.6 Proof of Proposition 6:

Applying TC Ind on $A^{+}\left( u,v\right) ,A^{+}\left( v,w\right) \vdash A^{+}\left( u,w\right)$ (which is derivable using TC Trans) and $A^{+}\left( x,y\right) \vdash A^{+}\left( x,y\right)$ (which is clearly provable) results in the desired proof. $\square$