First order logic with domain conditions

Freek Wiedijk and Jan Zwanenburg

Department of Computer Science, University of Nijmegen Toernooiveld 1, 6525 ED Nijmegen, The Netherlands

Abstract. This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. Often the problem is avoided by artificially making all functions total. However, that does not correspond to the practice of everyday mathematics. In type theory partial functions are modeled by giving functions extra arguments which are proof objects. In that case it will not be possible to apply functions outside their domain. However, having proofs as first class objects has the disadvantage that it will be unfamiliar to most mathematicians. Also many proof tools (like the theorem prover Otter) will not be usable for such a logic. Finally expressions get difficult to read because of these proof objects. The PVS system solves the problem of partial functions differently. PVS generates type-correctness conditions (TCCs) for statements in its language. These are proof obligations that have to be satisfied ‘on the side’ to show that statements are well-formed. We propose a TCC-like approach for the treatment of partial functions in type theory. We add domain conditions (DCs) to classical first-order logic and show the equivalence with a first order system that treats partial functions in the style of type theory.

1 Introduction

1.1 Problem.

Until a few decades ago mathematics was something that was done in human heads, on the blackboard or on paper. Only since the seventies have systems been developed that verify mathematics with the computer. The first of these was the Automath system from the Netherlands. Other early systems of this kind were the Mizar system [10] from Poland and the LCF system from the UK. Recently this kind of system has become widely used (mostly because of applications in computer science). Currently the most popular is the PVS system [13] from a US company called SRI International. Other contemporary systems of this kind are ACL2 [8], IMPS [6] and NuPRL [2] from the US, HOL [5] and Isabelle [12] from the UK and Germany, and the Coq system [16] from France. This last system is an implementation of an approach to formalizing mathematics called type theory.

This paper addresses the question of how to treat partial functions in formal mathematics. The prototypical example of a partial function is division: the quotient 1/0 is problematic because 0 is outside the domain of the division function. Formal systems have to take a position on how to deal with this kind of expression.

A traditional way to model partial functions in logic is by using relations. A statement about division is then interpreted as a statement about a ternary predicate div eq, that satisfies the equivalence:

div eq(x, y, z) ⟺ y ≠ 0 ∧ x/y = z

However when translating statements this way, they become an order of magnitude larger than the original. Therefore, for actual implementations of formal systems it is not attractive.

In [7], John Harrison enumerated the four main approaches to partial functions that one actually encounters in proof checkers:

1. Resolutely give each partial function a convenient value on points outside its domain.

2. Give each partial function some arbitrary value outside its domain.

3. Encode the domain of the partial function in its type and make its application to arguments outside that domain a type error.

4. Have a true logic of partial terms.

In the first case one would define 1/0 = 0, in the second case 1/0 would be some real number but one would not be able to prove which one it is, in the third case 1/0 would be a type error, and in the last case 1/0 would be an allowed expression but it would not denote anything (and one would be able to prove so).

In the systems listed above, ACL2 uses the first approach, HOL, Isabelle and Mizar use a mixture of the first and second approaches, Coq, NuPRL and PVS use the third approach, and IMPS uses the fourth approach.

In this paper we explore a variant of Harrison’s approach number 3. Although we do present a system of our own, it is not a ‘logic of partial terms’. It does not allow one to write 1/0 or any other undefined term and there is no way to state whether a term is defined (because it always is).

The approach that we present here is inspired by type theory, but our logic actually is one-sorted, so the variables of our logic all have the same ‘type’. It is easy to generalize our approach to a many-sorted logic. We restricted ourselves to the one-sorted case for simplicity.

The problem that we address in this paper is how to be able to follow approach number 3, while still doing the proofs in the ordinary first order predicate logic with total functions.

There are two reasons why it is worthwhile not to have to give up first order logic:

– First order logic is the best known logic. Users of a proof checker will understand the system better if the logic is ordinary first order logic.

– There is much technology for first order logic. For instance there are many theorem provers for it. The best known of these is Otter [18], but there are many more. They even compete in first order theorem prover competitions like the CADE system competition. It is valuable to be able to use this technology in a proof checker.

1.2 Approach.

We will introduce three logical systems, called system T, system D and system P. The names of those systems are abbreviations of ‘total’, ‘domain’ and ‘partial’. These systems are:

System T. Ordinary first order logic with total functions.

System D. Exactly the same logic as system T, but in this system undefined expressions are not allowed. This means that all functions have to have the arguments inside their domain. System P. A system in type theoretical style. Extra arguments which are proof objects ensure that it is not possible to write an undefined term.

Systems T and D have exactly the same set of expressions: only the derivations of both systems differ. System P has a different set of expressions, because it also has expressions for proof terms.

(For technical reasons we have an ‘if-then-else’ construction in all three systems. Therefore system T is not really ordinary first order logic, because it has something extra. However this if-then-else should not be considered to be an essential extension to the system. It should be considered ‘syntactic sugar’. We do not treat the relation between the systems with and without the if-then-else in this paper. However we expect it to be unproblematic.)

Then for system T we introduce a notion of domain conditions. This is a set of proof obligations that has to be satisfied to ensure that functions are not applied outside their domain. For example the domain conditions of division are such that:

DC(\frac{1}{x − 1} − \frac{1}{x + 1} = \frac{2}{x^{2} − 1}) = \{ ⊢ x − 1 ≠ 0, ⊢ x + 1 ≠ 0, ⊢ x^{2} − 1 ≠ 0\}

Now the main theorem that we prove consists of Propositions 9 and 18 below. Together these state that:

A statement together with its domain conditions are provable in system T iff that statement is provable in system P.

This means that we can morally imagine ourselves as being in system P, while doing our proofs and the presentation of the statements in system T, as long as we also prove the domain conditions.

The relation between the three systems is outlined in the following diagram:

[figure: T; ∩; D; P; | · |; *]

The | · | operation is called erasure (it is defined in Section 8). It erases all proof terms from the expressions. The ∗ operation is an auxiliary operation (as defined in Section 9) involved in the proof of the main theorem. It lifts a T proof to a D analogue.

1.3 Related work.

There are many logics of partial terms, like Scott’s E-logic [14, 17] and Beeson’s LPT [1]. See [9] for an overview of the field. However our approach is not a logic of partial terms because we do not allow undefined terms. We think that 1/0 should be illegal, and not just an undefined but legal expression.

Our paper integrates the type theoretical way to model partial functions with the PVS approach of having correctness conditions on the side. The type theoretical approach of having proof terms as an argument to model partial functions already dates from the Automath project (see [11] page 710). For a discussion of type-correctness conditions in PVS, see [15].

The approach that we propose here is similar to the one implemented in the LAMBDA system of Fourman [3], where each function f has an associated domain predicate DOM'f. However there is a difference in spirit: the LAMBDA system follows approach number 2 from the list on page 2,^{1} while we follow approach number 3. This is also apparent from the fact that in [3] the DC operation (called << >> there) only appears in axioms corresponding to function definitions, while in our approach it takes a much more central position.

2 Examples

We will now list some examples of partial functions and show how they are treated in the systems T and P. Some of these functions occur in a proof of the fundamental theorem of algebra in the Coq system [4]. The experiences we had in this ‘FTA project’ was one of the motivations to write this paper.

– Division. In system T the division operator x/y gets a domain condition that has to be proved to show that the expression is well-formed:

DC(x/y) = { ⊢ y ≠ 0}

1 [3], p. 86: ‘we regard a function application f(x) as always defined, but if x is outside the intended domain of f, we will not be able to prove anything about its value.’

In system P division becomes a ternary function:

div(x, y, α)

having three arguments x, y and α, where α is a proof that y ≠ 0. This is an example of the general pattern. In system P all partial functions get one extra ‘domain’ argument. Therefore, in system P a function application f(x_{1}, …, x_{n}) becomes f(x_{1}, …, x_{n}, α), where α is a proof of D_{f}(x_{1}, …, x_{n}) with the predicate D_{f} representing the domain of the function f.

– Square root. The domain condition of the real square root in system T is DC(\sqrt{x}) = \{ ⊢ x ≥ 0\}. Again, in system P the square root function sqrt(x, α) has an extra argument, where α is a proof of x ≥ 0.

– Limit of a sequence. The domain conditions of the limit operation are in system T:

DC( lim_{n→∞} a_{n}) = { ⊢ the sequence (a_{n}) converges }

In system P the limit operation becomes lim(a, α) where a is a sequence and where α is a proof that that sequence converges. The natural way to express the limit operation in type theory is not first order, because the a argument is a function. But the theory we present here is first order. This means that this example should be considered in the context of set theory (like in the Mizar system) where one can talk about functions using a first order language.

– Function application in set theory. Set theory is untyped. When one defines function application in it, it becomes a partial operation. In set theory in the style of system T, function application would get the domain condition:

DC(f(a)) = { ⊢ f is a function ∧ a ∈ dom f}

Note that the dom function that occurs in this condition has a domain condition as well:

DC(dom f) = { ⊢ f is a relation}

In system P function application becomes ternary, apply(f, a, α), where α is a proof of ‘f is a function ∧ a ∈ dom f’.

3 System T

We will now define the first of our three systems, namely first order predicate logic extended with an if-then-else operation.

To define our systems we fix a signature with finitely many constant, function and predicate symbols:

– constant symbols c_{1}, …, c_{k}

– function symbols f_{1}, …, f_{n} with arities a_{1}, …, a_{n}

– predicate symbols P_{1}, …, P_{m} with arities r_{1}, …, r_{m} We also have variables:

– term variables x_{0}, x_{1}, x_{2}, …

– proof variables h_{0}, h_{1}, h_{2}, …

(System T and D will only use term variables, but system P will also need proof variables.)

For each function symbol f of arity a there is a designated predicate symbol D_{f} (which is one of the P_{i}’s) that also has arity a. D_{f} is the predicate that represents the domain of the function f. Note that this D_{f} is not an extralogical abbreviation of a formula: it is a predicate symbol.

Constants could have been avoided by considering them to be nullary functions. However in that case our main result (Proposition 18 on page 15) would not have been true.^{2}

System T has four kinds of expressions: terms, formulas, contexts and judgments. These expressions are defined inductively as the smallest sets T , F, C and J satisfying:

T ::= x_{i} | c_{i} | f_{i}(T , …, T ) | (if F then T else T )
F ::= ⊥ | P_{i}(T , …, T ) | T = T | (F → F) | (∀x_{i}. F)
C ::= ϵ | C, x_{i} | C, F
J ::= C ⊢ wf | C ⊢ T wf | C ⊢ F wf | C ⊢ F

The four kinds of judgments mean respectively that the context is well-formed, that a term is well-formed, that a formula is well-formed and that a formula is provable.

Finally, system T has the following set of derivation rules:

C:  (ϵ-wf ) \overline{ϵ ⊢ wf} (decl-wf ) \frac{Γ ⊢ wf}{Γ, x_{i} ⊢ wf} (assum-wf ) \frac{Γ ⊢ φ wf}{Γ, φ ⊢ wf}

T :  (var-wf ) \frac{Γ ⊢ wf}{Γ ⊢ x_{i} wf} x_{i} ∈ Γ (const-wf ) \frac{Γ ⊢ wf}{Γ ⊢ c_{i} wf}

(fun-wf ) \frac{Γ ⊢ t_{1} wf ⋯ Γ ⊢ t_{a_{i}} wf Γ ⊢ wf}{Γ ⊢ f_{i}(t_{1}, …, t_{a_{i}}) wf}

F:  (⊥-wf ) \frac{Γ ⊢ wf}{Γ ⊢ ⊥ wf} (pred-wf ) \frac{Γ ⊢ t_{1} wf ⋯ Γ ⊢ t_{r_{i}} wf Γ ⊢ wf}{Γ ⊢ P_{i}(t_{1}, …, t_{r_{i}}) wf}

(if-wf ) \frac{Γ ⊢ φ wf Γ ⊢ t wf Γ ⊢ u wf}{Γ ⊢ (if φ then t else u) wf} 2 This is shown by the following (pathological) case: one function symbol f of arity 0

with D_{f} () ↔ ⊥ and φ ≡ ∃x. ⊤. This φ can be derived in the T system using witness

f(), but it cannot be derived in the P system. This shows that it is essential for our

theory to have constants c_{i} without domain conditions.

(→-wf ) \frac{Γ ⊢ φ wf Γ ⊢ ψ wf}{Γ ⊢ (φ → ψ) wf} (∀-wf ) \frac{Γ, x_{i} ⊢ φ wf}{Γ ⊢ (∀x_{i}. φ) wf}

P:  (assum) \frac{Γ ⊢ wf}{Γ ⊢ φ} φ ∈ Γ (raa) \frac{Γ ⊢ ¬¬φ}{Γ ⊢ φ}

(→-I ) \frac{Γ, φ ⊢ ψ}{Γ ⊢ (φ → ψ)} (→-E) \frac{Γ ⊢ (φ → ψ) Γ ⊢ φ}{Γ ⊢ ψ}
(∀-I ) \frac{Γ, x_{i} ⊢ φ}{Γ ⊢ (∀x_{i}. φ)} (∀-E) \frac{Γ ⊢ (∀x_{i}. φ) Γ ⊢ t wf}{Γ ⊢ φ[x_{i} := t]}
(refl) \frac{Γ ⊢ t wf}{Γ ⊢ t = t} (sym) \frac{Γ ⊢ t = u}{Γ ⊢ u = t} (trans) \frac{Γ ⊢ t = u Γ ⊢ u = v}{Γ ⊢ t = v}
(=-fun) \frac{Γ ⊢ t_{1} = t′_{1} ⋯ Γ ⊢ t_{a_{i}} = t′_{a_{i}} Γ ⊢ wf}{Γ ⊢ f_{i}(t_{1}, …, t_{a_{i}}) = f_{i}(t′_{1}, …, t′_{a_{i}})}
(=-pred) \frac{Γ ⊢ t_{1} = t′_{1} ⋯ Γ ⊢ t_{r_{i}} = t′_{r_{i}} Γ ⊢ wf}{Γ ⊢ P_{i}(t_{1}, …, t_{r_{i}}) → P_{i}(t′_{1}, …, t′_{r_{i}})}
(=-if-true) \frac{Γ ⊢ φ Γ ⊢ t wf Γ ⊢ u wf}{Γ ⊢ (if φ then t else u) = t}
(=-if-false) \frac{Γ ⊢ ¬φ Γ ⊢ t wf Γ ⊢ u wf}{Γ ⊢ (if φ then t else u) = u}

We identify expressions that are α-equivalent. Therefore we assume in these rules the Barendregt convention: all variable names are as different as possible.

Logical operations have to be read as abbreviations from ⊥, → and ∀:

¬φ ≡ φ → ⊥
φ ∨ ψ ≡ ¬φ → ψ
φ ∧ ψ ≡ ¬(φ → ¬ψ)
φ ↔ ψ ≡ (φ → ψ) ∧ (ψ → φ)

Some remarks about system T:

– Our presentation of first order logic is slightly non-standard in that we have variables in the contexts that bind the free variables in the terms and formulas. Instead of ‘x ≠ 0 ⊢ 1/x ≠ 0’ we write ‘x, x ≠ 0 ⊢ 1/x ≠ 0’. We do this for aesthetic reasons. It causes many well-formedness rules, but these are all trivial. In system T well-formedness just means that all free variables occur in the context.

– The condition Γ ⊢ wf in the rules fun-wf, pred-wf, =-fun and =-pred is needed for the case that a_{i} = 0 or r_{i} = 0.

– By symmetry of equality we can derive from rule =-pred the analogue rule with equivalence instead of implication:

(=-pred-iff ) \frac{Γ ⊢ t_{1} = t′_{1} ⋯ Γ ⊢ t_{r_{i}} = t′_{r_{i}} Γ ⊢ wf}{Γ ⊢ P_{i}(t_{1}, …, t_{r_{i}}) ↔ P_{i}(t′_{1}, …, t′_{r_{i}})}

– It is possible to replace the rules sym, trans, =-fun and =-pred by just one substitution rule:

(=-subst) \frac{Γ ⊢ t = u Γ ⊢ φ[x := t]}{Γ ⊢ φ[x := u]}

However this rule does not generalize to systems D and P. The term t might satisfy domain conditions that u does not.

Our systems are non-standard because they have an if-then-else construction, which corresponds to the mathematical practice of definition by cases. For example one can write ‘if x ≠ 0 then 1/x else 0’ as an expression. The if-then-else operator occurs in all three systems, T, D and P.

We would have preferred not to have this construction in our systems. In that case system T would really have been ordinary first order logic. However we need to have this construction to keep our definitions and proofs manageable. We have tried to develop the theory without it, but it became too complex.

We believe that the if-then-else is not essential to the systems. The theorem to be proved for this is conservativity of the extended system over the basic system:

If a judgment Γ ⊢ φ does not contain any if-then-elses, then it is provable in the system with if-then-else iff it is provable in the system without ifthen-else.

However we will not prove this theorem in this paper.

The if-then-elses can be eliminated systematically from a formula by replacing P [(if φ then t else u)] by (φ → P [t]) ∧ (¬φ → P [u]). As an example (if x ≠ 0 then 1/x else 0) · x = 1 then becomes (x ≠ 0 → (1/x) · x = 1) ∧ (x = 0 → 0 · x = 1).

4 System D

The expressions of system D are exactly the same as the expressions of system T. Only the set of rules is different. We show the rules that differ from the corresponding rules in system T:

T :  (fun-wf ) \frac{Γ ⊢ D_{f_{i}}(t_{1}, …, t_{a_{i}})}{Γ ⊢ f_{i}(t_{1}, …, t_{a_{i}}) wf} (if-wf ) \frac{Γ, φ ⊢ t wf Γ, ¬φ ⊢ u wf}{Γ ⊢ (if φ then t else u) wf}

F:  (→-wf ) \frac{Γ, φ ⊢ ψ wf}{Γ ⊢ (φ → ψ) wf}

P:  (=-fun) \frac{\begin{matrix}Γ ⊢ t_{1} = t′_{1} ⋯ Γ ⊢ t_{a_{i}} = t′_{a_{i}} \\ Γ ⊢ D_{f_{i}}(t_{1}, …, t_{a_{i}}) Γ ⊢ D_{f_{i}}(t′_{1}, …, t′_{a_{i}}) \end{matrix}}{Γ ⊢ f_{i}(t_{1}, …, t_{a_{i}}) = f_{i}(t′_{1}, …, t′_{a_{i}})}

(=-if-true) \frac{Γ ⊢ φ Γ, φ ⊢ t wf Γ, ¬φ ⊢ u wf}{Γ ⊢ (if φ then t else u) = t}

(=-if-false) \frac{Γ ⊢ ¬φ Γ, φ ⊢ t wf Γ, ¬φ ⊢ u wf}{Γ ⊢ (if φ then t else u) = u}

The essential differences between systems T and D are the rules fun-wf and =- fun. In system D you are only allowed to apply a function if you can prove that the arguments are in its domain.

The other differences are not essential: rules if-wf, →-wf, =-if-true and =-if-false in system T could have been the same as in system D. (But not the other way around: in system D these rules have to be the way they are.) However we have chosen to use in system T the simpler variants of those rules. The slight differences between systems T and D in this respect do not cause any problems in the proofs below.

5 System P

The expressions of system P follow the same basic structure as the expressions of system T and D. However there is an extra kind of expression P, for proof terms.

T ::= x_{i} | c_{i} | f_{i}(T , …, T , P) | (if F then λh_{i}. T else λh_{j}. T )
F ::= ⊥ | P_{i}(T , …, T ) | T = T | (Πh_{i} : F. F) | (∀x_{i}. F)
P ::= h_{i} | (λh_{i} : F. P) | (PP) | (λx_{i}. P) | (PT )
| raa(P) | refl(T ) | sym(P) | trans(P, P)
| eqfun(P, … P, P, P) | eqpred(i, P, … P)
| iftrue(P, λh_{i}. T , λh_{j}. T ) | iffalse(P, λh_{i}. T , λh_{j}. T )
C ::= ϵ | C, x_{i} | C, h_{i} : F
J ::= C ⊢ wf | C ⊢ T wf | C ⊢ F wf | C ⊢ P : F

Here are the rules for system P. They exactly parallel the rules for system D.

C:  (ϵ-wf ) \overline{ϵ ⊢ wf} (decl-wf ) \frac{Γ ⊢ wf}{Γ, x_{i} ⊢ wf} (assum-wf ) \frac{Γ ⊢ φ wf}{Γ, h_{i} : φ ⊢ wf}

T :  (var-wf ) \frac{Γ ⊢ wf}{Γ ⊢ x_{i} wf} x_{i} ∈ Γ (const-wf ) \frac{Γ ⊢ wf}{Γ ⊢ c_{i} wf}

(fun-wf ) \frac{Γ ⊢ α : D_{f_{i}}(t_{1}, …, t_{a_{i}})}{Γ ⊢ f_{i}(t_{1}, …, t_{a_{i}}, α) wf} (if-wf ) \frac{Γ, h_{i} : φ ⊢ t wf Γ, h_{j} : ¬φ ⊢ u wf}{Γ ⊢ (if φ then λh_{i}. t else λh_{j}. u) wf}

F:  (⊥-wf ) \frac{Γ ⊢ wf}{Γ ⊢ ⊥ wf} (pred-wf ) \frac{Γ ⊢ t_{1} wf ⋯ Γ ⊢ t_{r_{i}} wf Γ ⊢ wf}{Γ ⊢ P_{i}(t_{1}, …, t_{r_{i}}) wf}

(Π-wf ) \frac{Γ, h_{i} : φ ⊢ ψ wf}{Γ ⊢ (Πh_{i} : φ. ψ) wf} (∀-wf ) \frac{Γ, x_{i} ⊢ φ wf}{Γ ⊢ (∀x_{i}. φ) wf}

P:  (assum) \frac{Γ ⊢ wf}{Γ ⊢ h_{i} : φ} h_{i} : φ ∈ Γ (raa) \frac{Γ ⊢ α : ¬¬φ}{Γ ⊢ raa(α) : φ}

(Π-I ) \frac{Γ, h_{i} : φ ⊢ α : ψ}{Γ ⊢ (λh_{i} : φ. α) : (Πh_{i} : φ. ψ)} (Π-E) \frac{Γ ⊢ α : (Πh_{i} : φ. ψ) Γ ⊢ β : φ}{Γ ⊢ (αβ) : ψ[h_{i} := β]}
(∀-I ) \frac{Γ, x_{i} ⊢ α : φ}{Γ ⊢ (λx_{i}. α) : (∀x_{i}. φ)} (∀-E) \frac{Γ ⊢ α : (∀x_{i}. φ) Γ ⊢ t wf}{Γ ⊢ (αt) : φ[x_{i} := t]}
(refl) \frac{Γ ⊢ t wf}{Γ ⊢ refl(t) : t = t} (sym) \frac{Γ ⊢ α : t = u}{Γ ⊢ sym(α) : u = t}
(trans) \frac{Γ ⊢ α : t = u Γ ⊢ β : u = v}{Γ ⊢ trans(α, β) : t = v}

(=-fun) \frac{\begin{matrix}Γ ⊢ α_{1} : t_{1} = t′_{1} ⋯ Γ ⊢ α_{a_{i}} : t_{a_{i}} = t′_{a_{i}} \\ Γ ⊢ β : D_{f_{i}}(t_{1}, …, t_{a_{i}}) Γ ⊢ β′ : D_{f_{i}}(t′_{1}, …, t′_{a_{i}}) \end{matrix}}{Γ ⊢ eqfun(α_{1}, … α_{a_{i}}, β, β′) : f_{i}(t_{1}, …, t_{a_{i}}, β) = f_{i}(t′_{1}, …, t′_{a_{i}}, β′)}
(=-pred) \frac{Γ ⊢ α_{1} : t_{1} = t′_{1} ⋯ Γ ⊢ α_{r_{i}} : t_{r_{i}} = t′_{r_{i}} Γ ⊢ wf}{Γ ⊢ eqpred(i, α_{1}, … α_{r_{i}}) : P_{i}(t_{1}, …, t_{r_{i}}) → P_{i}(t′_{1}, …, t′_{r_{i}})}
(=-if-true) \frac{Γ ⊢ α : φ Γ, h_{i} : φ ⊢ t wf Γ, h_{j} : ¬φ ⊢ u wf}{Γ ⊢ iftrue(α, λh_{i}. t, λh_{j}. u) : (if φ then λh_{i}. t else λh_{j}. u) = t[h_{i} := α]}
(=-if-false) \frac{Γ ⊢ α : ¬φ Γ, h_{i} : φ ⊢ t wf Γ, h_{j} : ¬φ ⊢ u wf}{Γ ⊢ iffalse(α, λh_{i}. t, λh_{j}. u) : (if φ then λh_{i}. t else λh_{j}. u) = u[h_{j} := α]}

We will write Γ ⊢ φ if for some α we can derive that Γ ⊢ α : φ. If h_{i} does not occur in ψ we write φ → ψ for Πh_{i} : φ. ψ like before.

The expressions for the if-then-else bind two proof variables: one for the then branch and one for the else branch. This is indicated by putting λs in the ifthen-else, iffalse and iftrue expressions. These λs should not be confused with the λ-expressions that occur in the proof terms of an implication or universally quantified formula, which are introduced by the Π-I and ∀-I rules.

System P does not have a conversion rule. Without a conversion rule the system does not satisfy the property of subject reduction. We do not think a conversion rule is relevant for our application. We expect that adding a conversion rule will not affect the results from this paper.

Proof terms only occur as the final arguments of functions.

6 Some properties of derivations

The systems T, D and P are well behaved. All three systems satisfy the following four propositions (where X is anything that can occur after a ⊢):

Proposition 1. Γ, Γ′ ⊢ X then with a shorter derivation Γ ⊢ wf Proposition 2. Γ, φ, Γ′ ⊢ X then with a shorter derivation Γ ⊢ φ wf

Proposition 3. Γ ⊢ φ implies Γ ⊢ φ wf .

Proposition 4 (weakening). Γ ⊢ X and Γ, Γ′ ⊢ wf imply Γ, Γ′ ⊢ X.

7 The domain conditions

We now define the domain conditions of an expression. For each system T expression (term, formula, judgment), its domain conditions are a set of judgments that state that in the expression no function is applied outside its domain.

Domain conditions are defined relative to a context Γ which we put as a subscript to the DC symbol.

DC_{Γ} : T^{T} → P(J^{T})
DC_{Γ} (x_{i}) = DC_{Γ} (c_{i}) = ∅

DC_{Γ} (f_{i}(t_{1}, …, t_{a_{i}})) = DC_{Γ} (t_{1}) ∪ … ∪ DC_{Γ} (t_{a_{i}}) ∪ {Γ ⊢^{T} D_{f_{i}}(t_{1}, …, t_{a_{i}})}

DC_{Γ} (if φ then t else u) = DC_{Γ} (φ) ∪ DC_{Γ,φ}(t) ∪ DC_{Γ,¬φ}(u)
DC_{Γ} : F^{T} → P(J^{T})
DC_{Γ} (⊥) = ∅
DC_{Γ} (P_{i}(t_{1}, …, t_{r_{i}})) = DC_{Γ} (t_{1}) ∪ … ∪ DC_{Γ} (t_{r_{i}})
DC_{Γ} (t = u) = DC(t) ∪ DC(u)
DC_{Γ} (φ → ψ) = DC_{Γ} (φ) ∪ DC_{Γ,φ}(ψ)
DC_{Γ} (∀x_{i}. φ) = DC_{Γ,x_{i}}(φ)
DC : C^{T} → P(J^{T})
DC(ϵ) = ∅
DC(Γ, x_{i}) = DC(Γ)
DC(Γ, φ) = DC(Γ) ∪ DC_{Γ} (φ)

Domain conditions are asymmetric in some of the propositional connectives. Therefore, although system T is just first order logic, the domain conditions do not respect logical equivalence. For instance:

DC(φ ∧ ψ) ≠ DC(ψ ∧ φ)

In the first case φ ∧ ψ ≡ ¬(φ → ¬ψ) and we can use φ for proving the domain conditions of ψ, while in the second case ψ ∧ φ ≡ ¬(ψ → ¬φ) so in that case we can not use φ for the domain conditions of ψ. As an example the domain conditions of (x ≠ 0) ∧ P [1/x] might be provable because we can use x ≠ 0 to prove the domain conditions of P [1/x], but the domain conditions of P [1/x] ∧ (x ≠ 0) might not be provable because in that case we have to prove the domain conditions of P [1/x] without the benefit of x ≠ 0. In this sense the ∧ connective in system T behaves like the && operator of the C programming language.

The predicate symbol D_{f} is a symbol that represents the domain of the function f. To give this symbol a meaning we have to have an equivalence in the context. For instance D_{/}(x, y) is the definedness predicate of the division. It should be equivalent to y ≠ 0. This means that we have to imagine that we are reasoning in a context:

Γ ≡ …, theory of division including ∀x, y. (D_{/}(x, y) ↔ y ≠ 0), …

The domain condition for division is: DC(x/y) = { ⊢ D_{/}(x, y)}. This domain condition is equivalent to y ≠ 0 in the proper context but it is not identical to it. (So actually in the examples on pages 3–5 we were not completely correct. We ‘cheated’ there for the sake of the presentation.)

8 The erasure: from P to T

The erasure operation |·| erases all proof terms from expressions. It maps system P expressions to system T. In such an erased expression all domain conditions hold. This is the easy direction of our main result.

| · | : T^{P} → T^{T}
|x_{i}| = x_{i} |c_{i}| = c_{i}
|f_{i}(t_{1}, …, t_{a_{i}}, α)| = f_{i}(|t_{1}|, …, |t_{a_{i}}|)
|(if φ then λh_{i}. t else λh_{j}. u)| = (if |φ| then |t| else |u|)
| · | : F^{P} → F^{T}
|⊥| = ⊥
|P_{i}(t_{1}, …, t_{r_{i}})| = P_{i}(|t_{1}|, …, |t_{r_{i}}|)
|t = u| = |t| = |u|
|(Πh_{i} : φ. ψ)| = (|φ| → |ψ|)
|(∀x_{i}. φ)| = (∀x_{i}. |φ|)
| · | : C^{P} → C^{T}
|ϵ| = ϵ
|Γ, x_{i}| = |Γ |, x_{i}
|Γ, h_{i} : φ| = |Γ |, |φ|

Proposition 5.

|t[x_{i} := u]| ≡ |t|[x_{i} := |u|].
|φ[x_{i} := u]| ≡ |φ|[x_{i} := |u|].
|t[h_{i} := α]| ≡ |t|.
|φ[h_{i} := α]| ≡ |φ|.

Proof. Simultaneous induction on the structure of t and φ.

Proposition 6 (from P to D).

Γ ⊢^{P} wf implies |Γ | ⊢^{D} wf .
Γ ⊢^{P} t wf implies |Γ | ⊢^{D} |t| wf .
Γ ⊢^{P} φ wf implies |Γ | ⊢^{D} |φ| wf .
Γ ⊢^{P} φ implies |Γ | ⊢^{D} |φ|.

Proof. Simultaneous induction on the size of the derivation in system P.

Proposition 7.

Γ, φ ⊢^{T} t wf implies Γ ⊢^{T} t wf .
Γ, φ ⊢^{T} ψ wf implies Γ ⊢^{T} ψ wf .

Proof. Well-formedness in system T just checks whether all free variables are in the context. Removing assumptions from the context does not affect that.

Proposition 8 (from D to T).

Γ ⊢^{D} wf implies Γ ⊢^{T} wf and DC(Γ).
Γ ⊢^{D} t wf implies Γ ⊢^{T} t wf and DC(Γ) and DC_{Γ} (t).
Γ ⊢^{D} φ wf implies Γ ⊢^{T} φ wf and DC(Γ) and DC_{Γ} (φ).
Γ ⊢^{D} φ implies Γ ⊢^{T} φ and DC(Γ) and DC_{Γ} (φ).

Proof. Simultaneous induction on the size of the derivation in system D using Proposition 7 for the →-wf, if-wf, =-if-true and =-if-false rules.

Proposition 9 (main correspondence theorem from P to T). Γ ⊢^{P} φ implies |Γ | ⊢^{T} |φ| and DC(|Γ |) and DC_{|Γ |}(|φ|).

Proof. Propositions 6 and 8 combined.

9 The * operation: from T to D

Consider a statement for which the domain conditions hold. A system T proof of this statement and a system D proof of the same statement are different things. In the first case, although the domain conditions of the statement are satisfied, the proof might violate some domain conditions (for instance, it might reason about 1/0 as a number). But in the second case the domain conditions have to hold in all steps of the proof. We will show that despite this difference these two kinds of provability are equivalent (this is Proposition 15 below). For this we will use the ∗ operation.

The ∗ operation maps system T to system D. It makes the partial functions total by setting them to the constant c_{1} outside their domain. Then system T proofs are interpreted in system D as talking about these ‘extended’ functions.

·^{∗} : T^{T} → T^{D}
x_{i}^{∗} = x_{i} c_{i}^{∗} = c_{i}
f_{i}(t_{1}, …, t_{a_{i}})^{∗} = (if D_{f_{i}}(t_{1}^{∗}, …, t_{a_{i}}^{∗}) then f_{i}(t_{1}^{∗}, …, t_{a_{i}}^{∗}) else c_{1})
(if φ then t else u)^{∗} = (if φ^{∗} then t^{∗} else u^{∗})
·^{∗} : F^{T} → F^{D}
⊥^{∗} = ⊥
P_{i}(t_{1}, …, t_{r_{i}})^{∗} = P_{i}(t_{1}^{∗}, …, t_{r_{i}}^{∗})
(t = u)^{∗} = t^{∗} = u^{∗}
(φ → ψ)^{∗} = (φ^{∗} → ψ^{∗})
(∀x_{i}. φ)^{∗} = (∀x_{i}. φ^{∗})
·^{∗} : C^{T} → C^{D}

ϵ^{∗} = ϵ
(Γ, x_{i})^{∗} = Γ^{∗}, x_{i}
(Γ, φ)^{∗} = Γ^{∗}, φ^{∗}

Proposition 10.

Γ ⊢^{D} t wf implies Γ ⊢^{D} t = t^{∗}.

Γ ⊢^{D} φ wf implies Γ ⊢^{D} φ ↔ φ^{∗}.

Proof. Simultaneous induction on the structure of t and φ. Proposition 11. Γ ⊢^{D} wf implies that Γ ⊢^{D} φ iff Γ^{∗} ⊢^{D} φ. Proof. Induction on the structure of Γ using the second part of Proposition 10. Proposition 12.

Γ ⊢^{T} wf implies Γ^{∗} ⊢^{D} wf .

Γ ⊢^{T} t wf implies Γ^{∗} ⊢^{D} t^{∗} wf .
Γ ⊢^{T} φ wf implies Γ^{∗} ⊢^{D} φ^{∗} wf .
Γ ⊢^{T} φ implies Γ^{∗} ⊢^{D} φ^{∗}.

Proof. Simultaneous induction on the size of the derivation in system T using the previous two propositions. Proposition 13.

Γ ⊢^{D} wf and DC_{Γ} (t) imply Γ ⊢^{D} t = t^{∗}.

Γ ⊢^{D} wf and DC_{Γ} (φ) imply Γ ⊢^{D} φ ↔ φ^{∗}.

Proof. Simultaneous induction on the structure of t and φ. Proposition 14. DC(Γ) implies that Γ ⊢^{D} φ iff Γ^{∗} ⊢^{D} φ. Proof. Induction on the structure of Γ using the second part of Proposition 13. Proposition 15. DC(Γ) and DC_{Γ} (φ) and Γ ⊢^{T} φ imply Γ ⊢^{D} φ. Proof. Assume DC(Γ), DC_{Γ} (φ) and Γ ⊢^{T} φ. Then Γ^{∗} ⊢^{D} φ^{∗} by Proposition 12 and then Γ ⊢^{D} φ^{∗} by Proposition 14 and therefore Γ ⊢^{D} φ by the second part of Proposition 13.

10 From D to P

In the previous section we got from T to D. Now we show how to get from D to P. To ‘fill in’ the proof objects in a system D proof we need a property called proof irrelevance. It says that a P expression does not change its meaning if we replace proof terms in it with different proofs of the same statements. This is stated ‘locally’ in the =-fun rule of system P:

\frac{\begin{matrix}Γ ⊢ t_{1} = t′_{1} ⋯ Γ ⊢ t_{a_{i}} = t′_{a_{i}} \\ Γ ⊢ β : D_{f_{i}}(t_{1}, …, t_{a_{i}}) Γ ⊢ β′ : D_{f_{i}}(t′_{1}, …, t′_{a_{i}}) \end{matrix}}{Γ ⊢ f_{i}(t_{1}, …, t_{a_{i}}, β) = f_{i}(t′_{1}, …, t′_{a_{i}}, β′)}

The two terms are equal despite the proof terms β and β′ being different. But the property of proof irrelevance is also true ‘globally’:

Proposition 16 (proof irrelevance).

Γ ⊢^{P} t wf and Γ ⊢^{P} t′ wf and |t| ≡ |t′| imply Γ ⊢^{P} t = t′.
Γ ⊢^{P} φ wf and Γ ⊢^{P} φ′ wf and |φ| ≡ |φ′| imply Γ ⊢^{P} φ ↔ φ′.

Proof. Simultaneous induction on the size of |t| and |φ| using Proposition 5 and the =-fun, =-pred, =-if-true and =-if-false rules.

Once we have proof irrelevance, getting a system P derivation from a system D derivation is straightforward. Together with the earlier propositions this then allows us to prove the main result of this paper.

Proposition 17. If Γ ⊢^{P} wf then:

|Γ | ⊢^{D} t′ wf imply that there exists a t with |t| ≡ t′ such that Γ ⊢^{P} t wf . |Γ | ⊢^{D} φ′ wf imply that there exists a φ with |φ| ≡ φ′ such that Γ ⊢^{P} φ wf .

|Γ | ⊢^{D} φ′ imply that there exists a φ with |φ| ≡ φ′ such that Γ ⊢^{P} φ.

Proof. Simultaneous induction on the size of the derivation in system D using Propositions 5 and 16.

Proposition 18 (main correspondence theorem from T to P). Γ ⊢^{P} wf and |Γ | ⊢^{T} φ′ and DC_{|Γ |}(φ′) imply that there exists a φ with |φ| ≡ φ′ such that Γ ⊢^{P} φ.

Proof. Assume Γ ⊢^{P} wf , |Γ | ⊢^{T} φ′ and DC_{|Γ |}(φ′). Then DC(|Γ |) by Proposition 9 and then |Γ | ⊢^{D} φ′ by Proposition 15 and therefore there exists a suitable φ by Proposition 17.

Proposition 19 (corollary). Γ′ ⊢^{T} φ′ and DC(Γ′) and DC_{Γ′}(φ′) imply that there exist Γ and φ with |Γ | ≡ Γ′ and |φ| ≡ φ′ such that Γ ⊢^{P} φ.

Proof. Γ′ ⊢^{D} φ′ by Proposition 15, from which Γ′ ⊢^{D} wf . Then Γ′ ⊢^{D} wf implies that there exists a Γ with |Γ | ≡ Γ′ such that Γ ⊢^{P} wf , by induction on the structure of Γ′ using Proposition 17. Finally we get φ from Proposition 18.

11 Conclusion

The main things left to be done are:

1. Prove the systems with if-then-else conservative over the same systems without this construction.

2. Build a proof assistant that implements the approach of reasoning in system T with domain conditions, to study how well it works in practice.

3. Investigate whether the theory from this paper extends to higher order logic.

Acknowledgments. Thanks to Herman Geuvers, Paula Severi and Venanzio Capretta for stimulating discussions. Thanks to Gilles Barthe for the idea of how to fit this paper in 16 pages. Thanks to the anonymous referees for valuable comments.

References

1. M.J. Beeson. Foundations of constructive mathematics. Springer-Verlag, 1985.

2. Robert L. Constable, Stuart F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, Douglas J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, James T. Sasaki, and Scott F. Smith. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986.

3. Simon Finn, Michael Fourman, and John Longley. Partial Functions in a Total Setting. Journal of Automated Reasoning, 18:85–104, 1997.

4. H. Geuvers, F. Wiedijk, and J. Zwanenburg. Equational Reasoning via Partial Reflection. In Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, volume 1869 of LNCS, pages 162–178, Berlin, Heidelberg, New York, 2000. Springer Verlag.

5. M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL. Cambridge University Press, Cambridge, 1993.

6. J.D. Guttman and F.J. Thayer. IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning, 11:213–248, 1993.

7. John Harrison. Re: Undefined terms. Message <"swan.cl.cam.:266770:

950519095422"@cl.cam.ac.uk> as sent to the QED mailing list, <http://www.
ftp.cl.cam.ac.uk/ftp/hvg/qed-project-archive/03xx/0380>, 1995.

8. Matt Kaufmann, Panagiotis Manolios, and J. Strother Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston, 2000.

9. J. Kuper. Partiality in Logic and Computation – Aspects of Undefinedness. PhD thesis, University of Twente, Dept INF, Enschede, The Netherlands, 1994.

10. M. Muzalewski. An Outline of PC Mizar. Fondation Philippe le Hodey, Brussels,

1993. <http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz>.

11. R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer. Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. Elsevier Science, Amsterdam, 1994.

12. T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002.

13. S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of LNAI, pages 748–752, Berlin, Heidelberg, New York, 1992. Springer-Verlag.

14. D.S. Scott. Identity and existence in intuitionistic logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, Applications of Sheaves, volume 753 of Lecture Notes in Mathematics, pages 660–696, Berlin, 1979. Springer-Verlag.

15. Natarajan Shankar and Sam Owre. Principles and Pragmatics of Subtyping in PVS. In Didier Bert, Christine Choppy, and Peter Mosses, editors, Recent Trends in Algebraic Development Techniques, WADT ’99, volume 1827 of LNCS, pages 37–52, Toulouse, France, September 1999. Springer-Verlag.

16. The Coq Development Team. The Coq Proof Assistant Reference Manual,

2002. <ftp://ftp.inria.fr/INRIA/coq/current/doc/Reference-Manual-all.
ps.gz>.

17. A. Troelstra and D. van Dalen. Constructivism in Mathematics, an Introduction, Vols. 1-2, volume 121 and 123 of Studies in Logic and The Foundations of Mathematics. North-Holland, 1988.

18. L. Wos. The Automation of Reasoning: An Experimenter’s Notebook with Otter Tutorial. Academic Press, New York, 1996.