8 Assumption variables and constants

8. Assumption variables and constants

S:AssumptionVarConst

8.1. Assumption variables. Assumption variables are for proofs what variables are for terms. The main difference, however, is that assumption variables have formulas as types, and that formulas may contain free variables. Therefore we must be careful when substituting terms for variables in assumption variables. Our solution (as in Matthes’ thesis [9]) is to consider an assumption variable as a pair of a (typefree) identiﬁer and a formula, and to take equality of assumption variables to mean that both components are equal. Rather than using symbols as identiﬁers we prefer to use numbers (i.e. indices). However, sometimes it is useful to provide an optional string as name for display purposes.

We need a constructor, accessors and tests for assumption variables.

	(make-avar formula index name)		constructor
	(avar-to-formula avar)		accessor
	(avar-to-index avar)		accessor
	(avar-to-name avar)		accessor
	(avar? x)		test
	(avar=? avar1 avar2)		test.

For convenience we have the function

(mk-avar formula <index> <name>)

The formula is a required argument; however, the remaining arguments are optional. The default for the name string is u. We also require that a function

(formula-to-new-avar formula)

is deﬁned that returns an assumption variable of the requested formula different from all assumption variables that have ever been returned by any of the speciﬁed functions so far.

An assumption constant appears in a proof, as an axiom, a theorem or a global assumption. Its formula is given as an “uninstantiated formula”, where only type and predicate variables can occur freely; these are considered to be bound in the assumption constant. In the proof the bound type variables are implicitely instantiated by types, and the bound predicate variables by comprehension terms (the arity of a comprehension term is the type-instantiated arity of the corresponding predicate variable). Since we do not have type and predicate quantiﬁcation in formulas, the assumption constant contains these parts left implicit in the proof: tsubst and pinst (which will become a psubst, once the arities of predicate variables are type-instantiated with tsubst).

So we have assumption constants of the following kinds:

axioms,
theorems, and
global assumptions.

To normalize a proof we will ﬁrst translate it into a term, then normalize the term and ﬁnally translate the normal term back into a proof. To make this work, in case of axioms we pass to the term appropriate formulas: all-formulas for induction, an existential formula for existence introduction, and an existential formula together with a conclusion for existence elimination. During normalization of the term these formulas are passed along. When the normal form is reached, we have to translate back into a proof. Then these formulas are used to reconstruct the axiom in question.

Internally, the formula of an assumption constant is split into an uninstantiated formula where only type and predicate variables can occur freely, and a substitution for at most these type and predicate variables. The formula assumed by the constant is the result of carrying out this substitution in the uninstantiated formula. Note that free variables may again occur in the assumed formula. For example, assumption constants axiomatizing the existential quantiﬁer will internally have the form

	(aconst Ex-Intro ∀^α.() →∃^α() (ατ,^(α){ ^τ ∣ A}))
	(aconst Ex-Elim ∃^α() → (∀^α.() →) →
	(ατ,^(α){ ^τ ∣ A},{ ∣ B }))

Interface for general assumption constants. To avoid duplication of code it is useful to formulate some procedures generally for arbitrary assumption constants, i.e. for all of the forms listed above.

	(make-aconst name kind uninst-formula tpsubst
	repro-formula1 ...)		constructor
	(aconst-to-name aconst)		accessor
	(aconst-to-kind aconst)		accessor
	(aconst-to-uninst-formula aconst)		accessor
	(aconst-to-tpsubst aconst)		accessor
	(aconst-to-repro-formulas aconst)		accessor
	(aconst? x)		test.

To construct the formula associated with an aconst, it is useful to separate the instantiated formula from the variables to be generalized. The latter can be obtained as free variables in inst-formula. We therefore provide

	(aconst-to-inst-formula aconst)
	(aconst-to-formula aconst)

We also provide

	(aconst? aconst)
	(aconst=? aconst1 aconst2)
	(aconst-without-rules? aconst)
	(aconst-to-string aconst)

8.2. Axiom constants.

SS:AxiomConst

We use the natural numbers as a prototypical ﬁnitary algebra; recall Figure 1. Assume that n, p are variables of type nat, boole. Let ≈ denote the equality relation in the model. Recall the domain of type boole, consisting of tt, ff and the bottom element bb. The boolean valued functions equality = _nat: nat → nat → boole and existence (deﬁnedness, totality) e_nat: nat → boole need to be continuous. So we have

=(0,0)	≈ tt
=(0,S) ≈ =(S,0)	≈ ff	e(0)	≈ tt
=(S₁,S₂)	≈ =(₁,₂)	e(S)	≈ e()
=(bb_nat,) ≈ =(,bb_nat)	≈ bb	e(bb_nat)	≈ bb
=(∞_nat,) ≈ =(,∞_nat)	≈ bb	e(∞_nat)	≈ bb

Write T, F for atom(tt), atom(ff), r = s for atom(=(r,s)) and E(r) for atom(e(r)). We stipulate as axioms

	T	Truth-Axiom
	≈	Eq-Refl
	₁ ≈₂ →₂ ≈₁	Eq-Symm
	₁ ≈₂ →₂ ≈₃ →₁ ≈₃	Eq-Trans
	∀ ₁ ≈ ₂ → ₁ ≈ ₂	Eq-Ext
	₁ ≈₂ →(₁) →(₂)	Eq-Compat
	Total_ρ→σ( ) ↔∀.Total_ρ() → Total_σ( )	Total
	Total_ρ(c)	Constr-Total
	Total(c) → Total(_i)	Constr-Total-Args
and for every ﬁnitary algebra, e.g. nat

	₁ ≈₂ → E(₁) →₁ = ₂	Eq-to-=-1-nat
	₁ ≈₂ → E(₂) →₁ = ₂	Eq-to-=-2-nat
	₁ = ₂ →₁ ≈₂	=-to-Eq-nat
	₁ = ₂ → E(₁)	=-to-E-1-nat
	₁ = ₂ → E(₂)	=-to-E-2-nat
	Total() → E()	Total-to-E-nat
	E() → Total()	E-to-Total-nat

Here c is a constructor. Notice that in Total(c ⃗
ˆx

) → Total(

_i), the type of (c ⃗
ˆx

) need not be a ﬁnitary algebra, and hence

_i may have a function type.

Remark. (E(₁) → ₁ = ₂) → (E(₂) → ₁ = ₂) → ₁ ≈ ₂ is not valid in our intended model (see Figure 1), since we have two distinct undeﬁned objects bb_nat and ∞_nat.

We abbreviate

	∀.Total_ρ() → A	by	∀xA,
	∃.Total_ρ() ∧ A	by	∃xA.

Formally, these abbreviations appear as axioms

	∀x(x) →∀.Total() →()	All-AllPartial
	(∀.Total() →()) →∀x(x)	AllPartial-All
	∃x(x) →∃.Total() ∧()	Ex-ExPartial
	(∃.Total() ∧()) →∃x(x)	ExPartial-Ex
and for every ﬁnitary algebra, e.g. nat

	∀n(n) →∀.E() →()	All-AllPartial-nat
	(∃.E() ∧()) →∃n(n)	ExPartial-Ex-nat

Notice that AllPartial-All-nat i.e. (∀

.E(

) →

(

)) →∀n

(n) is provable (since E(n)

T). Similarly, Ex-ExPartial-nat, i.e. ∃n

(n) →∃

.E(

) ∧

(

) is provable.

Finally we have axioms for the existential quantiﬁer

	∀^α.() →∃^α()		Ex-Intro
	∃^α() → (∀^α.() →) →		Ex-Elim

The assumption constants corresponding to these axioms are

	truth-aconst		for Truth-Axiom
	eq-refl-aconst		for Eq-Refl
	eq-symm-aconst		for Eq-Symm
	eq-trans-aconst		for Eq-Trans
	ext-aconst		for Eq-Ext
	eq-compat-aconst		for Eq-Compat
	total-aconst		for Total
	(finalg-to-eq-to-=-1-aconst finalg)		for Eq-to-=-1
	(finalg-to-eq-to-=-2-aconst finalg)		for Eq-to-=-2
	(finalg-to-=-to-eq-aconst finalg)		for =-to-Eq
	(finalg-to-=-to-e-1-aconst finalg)		for =-to-E-1
	(finalg-to-=-to-e-2-aconst finalg)		for =-to-E-2
	(finalg-to-total-to-e-aconst finalg)		for Total-to-E
	(finalg-to-e-to-total-aconst finalg)		for E-to-Total
	all-allpartial-aconst		for All-AllPartial
	allpartial-all-aconst		for AllPartial-All
	ex-expartial-aconst		for Ex-ExPartial
	expartial-ex-aconst		for ExPartial-Ex
	(finalg-to-all-allpartial-aconst finalg)		for All-AllPartial
	(finalg-to-expartial-ex-aconst finalg)		for ExPartial-Ex

We now spell out what precisely we mean by induction over simultaneous free algebras = μ, with goal formulas ∀x_j^μ_j _j(x_j). For the constructor type

κi = ⃗ρ → (⃗σ1 → αj1) → ⋅⋅⋅ → (⃗σn → αjn) → αj ∈ KT( ⃗α)

we have the step formula

D_i := ∀y₁^ρ₁,…,y_m^ρ_m,y_m+1^{₁ →μ_j₁},…,y_m+n^{_n →μ_{j_n}}.	∀^₁ _j₁(y_m+1) →→
	∀^_n _{j_n}(y_m+n) →
	_j(constr_i()).

Here

= y₁^ρ₁,…,y_m^ρ_m,y_m+1^{₁→μ_j₁},…,y_m+n^{_n→μ_{j_n}} are the components of the object constr_i(

) of type μ_j under consideration, and

∀⃗x⃗σ1Pˆj (ym+1⃗x),...,∀⃗x⃗σn ˆPj (ym+n⃗x) 1 n

are the hypotheses available when proving the induction step. The induction axiom Ind_{μ_j} then proves the formula

Ind : D → ⋅⋅⋅ → D → ∀x μjˆP (x ). μj 1 k j j j

We will often write Ind_j for Ind_{μ_j}.

An example is

	E₁ → E₂ → E₃ → E₄ →∀x₁^tree₁(x₁)
with

	E₁ := ₁(Leaf),
	E₂ := ∀x^tlist.₂(x) →₁(Branch(x)),
	E₃ := ₂(Empty),
	E₄ := ∀x₁^tree,x₂^tlist.₁(x₁) →₂(x₂) →₂(Tcons(x₁,x₂)).

Here the fact that we deal with a simultaneous induction (over tree and tlist), and that we prove a formula of the form ∀x^tree…, can all be inferred from what is given: the ∀x^tree… is right there, and for tlist we can look up the simultaneously deﬁned algebras. – The internal representation is

	(aconst Ind E₁ → E₂ → E₃ → E₄ →∀x₁^tree₁(x₁)
	(₁{x₁^tree ∣ A₁ },₂{x₂^tlist ∣ A₂ }))

A simpliﬁed version (without the recursive calls) of the induction axiom is the following cases axiom.

	(aconst Cases E₁ → E₂ →∀x₁^tree₁(x₁) (₁{x₁^tree ∣ A₁ }))
with

	E₁ := ₁(Leaf),
	E₂ := ∀x^tlist₁(Branch(x)).

However, rather than using this as an assumption constant we will – parallel to the if-construct for terms – use a cases-construct for proofs. This does not change our notion of proof; it is done to have the if-construct in the extracted programs.

The assumption constants corresponding to these axioms are generated by

	(all-formulas-to-ind-aconst all-formula1 ...)		for Ind
	(all-formula-to-cases-aconst all-formula)		for Cases

For the introduction and elimination axioms Ex-Intro and Ex-Elim for the existential quantiﬁer we provide

	(ex-formula-to-ex-intro-aconst ex-formula)
	(ex-formula-and-concl-to-ex-elim-aconst ex-formula concl)

and similarly for exnc instead of ex.

To deal with inductively deﬁned predicate constants, we need additional axioms with names “Intro” and “Elim”, which can be generated by

	(number-and-idpredconst-to-intro-aconst i idpc)
	(imp-formulas-to-elim-aconst imp-formula1 ...);

here an imp-formula is expected to have the form I(

) → A.

8.3. Theorems.

SS:Theorems

A theorem is a special assumption constant. Theorems are normally created after successfully completing an interactive proof. One may also create a theorem from an explicitely given (closed) proof. The command is

(add-theorem string . opt-proof)

or save

From a theorem name we can access its aconst, its (original) proof and also its instantiated proof by

	(theorem-name-to-aconst string)
	(theorem-name-to-proof string)
	(theorem-name-to-inst-proof string)

We also provide

	(remove-theorem string1 ...)
	(display-theorems string1 ...)

Initially we provide the following theorems

	atom(p) → p = tt	Atom-True
	(atom(p) → F) → p = ff	Atom-False
	F → atom(p)	Efq-Atom
	((atom(p) → F) → F) → atom(p)	Stab-Atom
and for every ﬁnitary algebra, e.g. nat

	n = n	=-Refl-nat
	₁ = ₂ →₂ = ₁	=-Symm-nat
	₁ = ₂ →₂ = ₃ →₁ = ₃	=-Trans-nat

Proof of Atom-True. By Ind. In case tt use Eq-Compat with tt ≈ =(tt,tt) to infer atom(=(tt,tt)) (i.e. tt = tt) from atom(tt). In case ff use Eq-Compat with ff ≈ =(ff,tt) to infer atom(=(ff,tt)) (i.e. ff = tt) from atom(ff). _

Proof of Atom-False. Use Ind, and Truth-Axiom in both cases. – Notice that the more general (atom( ) → F) → = ff does not hold with bb for , since =(bb,ff) ≈ bb. _

Proof of Efq-Atom. Again by Ind. In case tt use Truth-Axiom, and the case ff is obvious. _

Proof of Stab-Atom. By Ind. In case tt use Truth-Axiom, and the case ff is obvious. _

Remark. Notice that from Efq-Atom one easily obtains F → A for every formula A all whose strictly positions occurrences of prime formulas are of the form atom(r), by induction on A. For all other formulas we shall make use of the global assumption Efq: F → (cf. Section 8.4). Similarly, Notice that from Stab-Atom one again obtains ((A → F) → F) → A for every formula A all whose strictly positions occurrences of prime formulas are of the form atom(r), by induction on A. For all other formulas we shall make use of the global assumption Stab: (( → F) → F) → (cf. Section 8.4).

Proof of =-Refl-nat. Use Ind, and Truth-Axiom in both cases. – Notice that = does not hold, since =(bb,bb) ≈ bb. _

Here are some other examples of theorems; we give the internal representation as assumption constants, which show how the assumed formula is split into an uninstantiated formula and a substitution, in this case a type substitution αρ, an object substitution f^α→natg^ρ→nat and a predicate variable substitution ˆ
P ^(α){ ^ρ ∣ A}.

	(aconst Cvind-with-measure-11
	∀f^α→nat.∀x^α.∀y(f(y)<f(x) →(y)) →(x) →∀x(x)
	(αρ,f^α→natg^ρ→nat,^(α){ ^ρ ∣ A})).
	(aconst Minpr-with-measure-l11
	∀f^α→nat.∃clx^α(x) →∃clx.(x)!∀y.f(y)<f(x) →(y) →⊥
	(αρ,f^α→natg^ρ→nat,^(α){ ^ρ ∣ A})).

Here ∃cl is the classical existential quantiﬁer deﬁned by ∃clxA := ∀x(A →⊥) →⊥ with the logical form of falsity ⊥ (as opposed to the arithmetical form (atom ff)). l indicates “logic” (we have used the logical form of falsity), the ﬁrst 1 that we have one predicate variable

, and the second that we quantify over just one variable x. Both theorems can easily be generalized to more such parameters.

When dealing with classical logic it will be useful to have

(

→

₁) → ((

→⊥) →

₁) →

₁

Cases-Log

The proof uses the global assumption Stab-Log (see below) for

₁; hence we cannot extract a term from it.

The assumption constants corresponding to these theorems are generated by

(theorem-name-to-aconst name)

8.4. Global assumptions.

SS:GlobalAss

A global assumption is a special assumption constant. It provides a proposition whose proof does not concern us presently. Global assumptions are added, removed and displayed by

	(add-global-assumption name formula) (abbreviated aga)
	(remove-global-assumption string1 ...)
	(display-global-assumptions string1 ...)

We initially supply global assumptions for ex-falso-quodlibet and stability, both in logical and arithmetical form (for our two forms of falsity).

	⊥→		Efq-Log
	(( →⊥) →⊥) →		Stab-Log
	F →		Efq
	(( → F) → F) →		Stab

The assumption constants corresponding to these global assumptions are generated by

(global-assumption-name-to-aconst name)

[next] [prev] [prev-tail] [front] [up]