2.1 Brouwer, Markov, and Bishop

The first fully constructive mathematics and philosophy began with L.E.J. Brouwer’s 1907 PhD thesis [Reference Brouwer9, Reference Heyting33]. Brouwer condemned a logical foundation of mathematics independent of proper a priori human mental concepts. For otherwise one builds a linguistic structure definitely distinct from mathematics, see [Reference Brouwer9, pp. 179–180]. Brouwer’s PhD student Arend Heyting on [Reference Heyting34, p. 7] wrote that

Brouwer’s intuitionism includes what are called choice sequences, a notion which he considered intuitively clear. Nonetheless he struggled at times in dealing with them, see [Reference Heyting34, p. 11]. Brouwer’s intuitionism is not consistent with classical mathematics, see Theorem 3.6 on [Reference Bridges and Richman8, p. 115].

On [Reference Kushner42, p. 559] Boris A. Kushner writes

The objects in A.A. Markov’s constructive mathematics may be considered as words over finite alphabets. Some Markov constructivists contemplated broader possibilities. For example, Vladik Kreinovich offers a list of five main challenges on [Reference Kreinovich39, p. 218], of which the first two are:

• • The need to extend constructive mathematics to more complex mathematical objects.

• • To be useful for data processing, algorithms must be able to handle possibly non-constructive data.

On the one hand Markov didn’t recognize Brouwer’s choice sequences in his own philosophy. On the other he accepted a principle now called Markov’s principle. Markov’s constructivism is not consistent with classical mathematics, see Theorem 6.5 on [Reference Bridges and Richman8, p. 69].

Arguably the first substantial body of constructive mathematics is in [Reference Bishop6] where, on [Reference Bishop6, p. ix] Errett Bishop wrote that

Bishop’s constructivism includes choice principles extending Countable Choice. His constructivism is consistent with classical mathematics. Bishop’s book is restricted to constructive analysis. For constructive algebra, see [Reference Mines, Richman and Ruitenburg46].

2.2 Topos theory

In the early 1960s appeared theorems about categories which, as Johnstone wrote on [Reference Johnstone36, p. xii],

The development of principal interest to us began with F.W. Lawvere’s [Reference Lawvere43], titled An elementary theory of the category of sets. Once Lawvere turned his attention to Grothendieck toposes as generalized set theories, a new theory of the category of sets evolved called (elementary) topos theory. A name which Johnstone on page [Reference Johnstone36, p. xii], in an earlier context, called “…slightly unfortunate …”. Topos theory is a major part of an autonomous development of category theory as a foundation for mathematics. What makes topos theory also constructive is, that the mathematics done on the inside is in general restricted to the rules of intuitionistic logic shared by the three ‘schools’ mentioned before.

Internal topos mathematics is consistent with classical mathematics, but doesn’t axiomatize any choice principles, not even Countable Choice. An additional natural number object also has an elementary category theoretic axiomatization, as shown by P. Freyd in [Reference Freyd15]. Internal topos mathematics allows for a so-called truth value object with which one can, using set terminology, freely construct power sets of sets. Such liberal set constructions are not part of Brouwer’s intuitionism.

5.1 Propositional logic

Before considering full predicate logic, we restrict ourselves to a new proof interpretation for propositional logic. One advantage is that we can use simpler notation. We choose the usual logical constants $\land $ , $\lor $ , $\rightarrow $ , $\top $ , and $\bot $ of intuitionistic propositional logic. Negation $\neg A$ is defined by $A \rightarrow \bot $ , and bi-implication $A \leftrightarrow B$ is defined by $(A \rightarrow B) \land (B \rightarrow A)$ . It may be possible to add new ones, for example a new version of $\neg A$ distinct from $A \rightarrow \bot $ . In this paper we consider no constructively distinct new proposition logical constants.

For each pair of formulas A and B we have a conjunction formula $A \land B$ with $\land $ the intended meaning of ‘and’. There are trivial proofs $(A \land B, \pi _1, A)$ and $(A \land B, \pi _2, B)$ . These come with the intended meaning of an assumption of form $A \land B$ . Consequently, with composition, a proof $(C, \sigma , A \land B)$ implies that we have proofs $(C, \pi _1 \sigma , A)$ and $(C, \pi _2 \sigma , B)$ . In the other direction, if we have proofs $(C, \pi , A)$ and $(C, \sigma , B)$ , then there is a proof which we name $(C, \langle \pi ,\sigma \rangle , A \land B)$ , and which we construct in a uniform way in terms of $\pi $ and $\sigma $ . The constructive principles remain sound when the proofs employ additional assumptions. So we have rules

$$ \begin{align*} \displaystyle{\frac{C \vdash_{\vec{D}} A \land B}{C \vdash_{\vec{D}} A}}\quad \text{and} \quad \displaystyle{\frac{C \vdash_{\vec{D}} A \land B}{C \vdash_{\vec{D}} B}} \quad \text{and} \quad \displaystyle{\frac{C \vdash_{\vec{D}} A \quad C \vdash_{\vec{D}} B}{C\vdash_{\vec{D}} A \land B}}. \end{align*} $$

By the intended meaning of $\land $ , if a proof has assumptions A and B, then there is an essentially identical proof with assumption $A \land B$ . We have a proof $(A,B,\vec {D}, \pi , C)$ exactly when we have a proof $(A \land B,\vec {D}, \sigma , C)$ . So we have rules

$$ \begin{align*} \displaystyle{\frac{A \vdash_{B,\vec{D}} C}{A \land B \vdash_{\vec{D}}C}} \quad \text{and} \quad \displaystyle{\frac{A \land B \vdash_{\vec{D}} C}{A \vdash_{B,\vec{D}}C}}. \end{align*} $$

We include a symbol $\top $ with intended meaning ‘true’, standing for a trivially proved statement. For every $\vec {D}$ there is a trivial proof $(\vec {D}, \pi , \top )$ , and axiom

$$ \begin{align*} \vdash_{\vec{D}} \top. \end{align*} $$

For each pair of formulas A and B we have a disjunction formula $A \lor B$ with $\lor $ the intended meaning of ‘or’. There are trivial proofs $(A,\sigma _1, A \lor B)$ and $(B,\sigma _2, A \lor B)$ . Consequently, with composition, a proof $(A \lor B,\pi ,C)$ implies that we have proofs $(A, \pi \sigma _1, C)$ and $(B, \pi \sigma _2, C)$ . In the other direction, if we have proofs $(A,\pi ,C)$ and $(B,\sigma ,C)$ , then there is a proof which we name $(A \lor B, [\pi ,\sigma ], C)$ , and which we construct in a uniform way in terms of $\pi $ and $\sigma $ . This clarifies what it means to assume a disjunction $A \lor B$ . The constructive principles remain sound when the proofs employ additional assumptions. So we have rules

$$ \begin{align*} \displaystyle{\frac{A \lor B \vdash_{\vec{D}} C}{A \vdash_{\vec{D}} C}}\quad \text{and} \quad \displaystyle{\frac{A \lor B \vdash_{\vec{D}} C}{B \vdash_{\vec{D}} C}} \quad \text{and} \quad \displaystyle{\frac{A \vdash_{\vec{D}} C \quad B \vdash_{\vec{D}} C}{A \lor B \vdash_{\vec{D}} C}}. \end{align*} $$

Lists $\vec {D}$ of additional assumptions are key in proving distributivity. Straightforward proofs yield $B \vdash _A (A \land B) \lor (A \land C)$ and $C \vdash _A (A \land B) \lor (A \land C)$ , so also

$$ \begin{align*} B \lor C \;\vdash_A\; (A \land B) \lor (A \land C). \end{align*} $$

Thus

$$ \begin{align*} A \land (B \lor C ) \;\vdash_{\vec{D}}\; (A \land B) \lor (A \land C). \end{align*} $$

We include a symbol $\bot $ with intended meaning ‘false’. Theories need not have an acceptable candidate for $\bot $ . For significant theories like arithmetic an atom like $1 = 0$ can perform this role. In such cases the word ‘false’ is only used in an abstract sense. If we have such a candidate atom, then for every $\vec {D}$ and B we have a proof $(\bot ,\vec {D}, \pi , B)$ , and axiom

$$ \begin{align*} \bot \vdash_{\vec{D}} B. \end{align*} $$

For each pair of formulas A and B we have an implication formula $A \rightarrow B$ with $\rightarrow $ the intended meaning of ‘implies’. We write $\neg A$ as abbreviation for $A \rightarrow \bot $ . Formula $A \rightarrow B$ has to reflect the meaning of $A \vdash B$ within the bounds of what is constructively acceptable. The critical issue of what these bounds are will be clarified below by permitted proof constructions on the one hand, and by weak counterexamples on the other. We needn’t bother with a more complicated notation like $A \rightarrow _{\vec {D}} B$ for $A \vdash _{\vec {D}} B$ , since the latter is equivalent to $(A \land \bigwedge \vec {D}) \rightarrow B$ . If we have a proof $(A \land B, \pi , C)$ , then we have a proof $(A, \pi _A, B \rightarrow C)$ , where $\pi _A$ takes proof $\pi $ , replaces its assumption $A \land B$ by assumption B and derives $A \land B$ using the assumption A of $\pi _A$ . Finally append that the result is a proof for conclusion $B \rightarrow C$ . We construct $\pi _A$ in a uniform way in terms of $\pi $ . The constructive principle remains sound when the proof employs additional assumptions. So we have rule

$$ \begin{align*} \displaystyle{\frac{A \land B \;\vdash_{\vec{D}}\; C}{A \;\vdash_{\vec{D}}\; B \rightarrow C}}. \end{align*} $$

Assume $A \rightarrow B$ and $B \rightarrow C$ . So we assume proofs $(A, \xi , B)$ and $(B, \eta , C)$ without specifying $\xi $ and $\eta $ any further. As Bishop wrote on [Reference Bishop6, p. 3]:

In this same sense $\xi $ and $\eta $ are hypothetical. From the assumed $\xi $ and $\eta $ we construct composition proof $(A, \eta \xi , C)$ in the hypothetical sense implied by Bishop. The constructive principle remains sound when the proof employs additional assumptions. So we have axiom

$$ \begin{align*} (A \rightarrow B) \land (B \rightarrow C) \;\vdash_{\vec{D}}\; A \rightarrow C. \end{align*} $$

In special cases we may have proofs at hand. For example consider proof $(A \land B, \pi , B)$ instead of $(A,\xi ,B)$ . In that case we get composition proof $(A \land B, \eta \pi , C)$ , where proof $\eta \pi $ may only become available after mathematics advances and a proof $\sigma $ can be substituted for $\eta $ . This special case indicates that from $A \land B \;\vdash \; B$ we can derive $(B \rightarrow C) \;\vdash \; (A \land B \rightarrow C)$ .

Assume $A \rightarrow B$ and $A \rightarrow C$ . So we assume proofs $(A, \xi , B)$ and $(A, \eta , C)$ . So we have proof $(A, \langle \xi , \eta \rangle , B \land C)$ . The constructive principle remains sound when the proof employs additional assumptions, so we have axiom

$$ \begin{align*} (A \rightarrow B) \land (A \rightarrow C) \;\vdash_{\vec{D}}\; A \rightarrow (B \land C). \end{align*} $$

Assume $B \rightarrow A$ and $C \rightarrow A$ . So we assume proofs $(B, \xi , A)$ and $(C, \eta , A)$ . So we have proof $(B \lor C, [\xi ,\eta ], A)$ . The constructive principle remains sound when the proof employs additional assumptions, so we have axiom

$$ \begin{align*} (B \rightarrow A) \land (C \rightarrow A) \;\vdash_{\vec{D}}\; (B \lor C) \rightarrow A. \end{align*} $$

This completes our axiomatization when restricted to the language of propositional logic. Our system axiomatizes the BasicFootnote ¹⁰ Propositional Logic of Albert Visser in [Reference Visser57], and is a proper subsystem of Intuitionistic Propositional Logic.

From a historical perspective, the constructive nature of Basic Propositional Logic is not controversial, only the matter of why we stop here is. We sketch below by means of general weak counterexamples why we stop here. To get Intuitionistic Propositional Logic it suffices to add schema $\top \rightarrow A \;\vdash \; A$ to Basic Propositional Logic. The schema allows one to derive modus ponens $A \land (A \rightarrow B) \;\vdash \; B$ . Before discussing the general weak counterexamples, we show that our concerns are far from new, with a further focus on why $\top \rightarrow A \;\vdash \; A$ as a general principle should be excluded from constructive logic.

Heyting wrote on [Reference Heyting32, p. 5] that

This agrees with Brouwer’s view. As Mark van Atten points out on [Reference van Atten4, p. 3], (with his citation adapted to our list of references)

Dummett wrote on [Reference Dummett14, p. 274]:

We don’t agree with Dummett’s follow-up

This is not an acceptable explanation. One doesn’t know what to recognize as an effective operation as new methods of reasoning may be discovered. The following paragraph demonstrates that a survey or circumscription of possible future operations is unavoidable.

The principle $\top \rightarrow A \;\vdash \; A$ as a general mathematical theorem fails to respect the observations of Heyting, van Atten, and Dummett when applied to a general theory of constructions and proofs. For comparison consider the case $(A \rightarrow B) \land (B \rightarrow C) \vdash (A \rightarrow C)$ , which we justify by converting assumptions $(A,\xi ,B)$ and $(B,\eta ,C)$ into $(A,\eta \xi ,C)$ . Composition $\eta \xi $ exists without a need to ‘look inside’ $\xi $ and $\eta $ , so is constructively justified. All Basic logic axioms and rules are elementary, or are justified by building new constructions from old ones without a need to ‘look inside’ them. By contrast, consider a proof $((\top \rightarrow A), \pi , A)$ . This is different from $(A,\rho ,A)$ , where we may assume a proof of A in an idealized sense,Footnote ¹¹ we always conclude A from its assumption. Construction $\pi $ claims to turn an assumed proof $(\top , \xi , A)$ of A into a proof of A. Suppose that a construction $\sigma $ appears that fulfills $(\top ,\sigma ,A)$ . A constructivist understands $\sigma $ as a construction which permits us to form a proof of A. This may be understood before performing $\sigma $ . A constructivist doesn’t recognize a proof unseen. In the absence of other reasons why A has a proof, we must perform $\sigma $ to form a proof of A. This could be harmless were it not that the accumulation of proofs is open-ended. After sufficient completion of $\sigma $ we may discover new methods of reasoning. Such new methods of reasoning need not be part of performing $\pi $ when transforming a different $(\top ,\tau ,A)$ into a proof of A. The existence of $\pi $ is claimed prematurely. When we assume not a proof of A but rather assume that we have a construction for a proof of A, then we have a construction for a proof of A, which gives us $\top \rightarrow A \;\vdash \; \top \rightarrow A$ .

Despite the absence of full modus ponens, limited versions still hold. For example $\vdash \; A \rightarrow B$ implies $A \vdash B$ , see [Reference Visser57]. So Basic Propositional Logic satisfies the rule

$$ \begin{align*} \displaystyle{\frac{C \vdash_{\vec{D}} A \quad \vdash A \rightarrow B}{C \vdash_{\vec{D}} B}}. \end{align*} $$

As a special case, $\vdash \top \rightarrow A$ implies $\vdash A$ . From [Reference Ardeshir and Ruitenburg2, p. 323] we see that Basic Propositional Logic satisfies $\top \rightarrow A \;\vdash \; A$ exactly when A is equivalent to a formula of the form $((\top \rightarrow B) \rightarrow B) \rightarrow (\top \rightarrow B)$ .

Do we have a complete set of axioms and rules for constructive propositional logic? As in the intuitionistic case, the evidence for non-provability is different in nature from provability. Both in [Reference Visser57] and in [Reference Ardeshir and Ruitenburg2] we find a completeness theorem for Basic Propositional Logic with transitive Kripke models, that is, Kripke models where the world relation is transitive but not necessarily reflexive as in the case of Intuitionistic Propositional Logic. Using transitive Kripke models as weak counterexamples to constructive provability of propositional statements has similar limited value as when using reflexive transitive Kripke models as a tool to make weak counterexamples in the intuitionistic case. Imagine a Kripke model $\mathfrak {A}$ on a structure $(W, \sqsubset )$ of nodes or worlds W, with transitive relation $\sqsubset $ , and with structures $\mathfrak {A}_{\alpha }$ at nodes $\alpha \in W$ . A weakly increasing function $f : \mathbb {N} \rightarrow W$ simulates temporal information, where what is forced at $f(n) = \alpha $ indicates what the constructivist can know at stage n about a structure of interest. The constructivist has no knowledge whether f ever increases or in what way. Each node $\alpha $ represents what a constructivist can know with the methods of reasoning at that node, and with the knowledge at that node about the intended structure. At node $\alpha $ , nodes $\beta \sqsupset \alpha $ represent possible versions of knowledge with newly conceived operations or further understanding about the intended structure. In terms of the proof interpretation, at node $\beta $ constructions c at stage $\alpha $ for implications $A \rightarrow B$ have been sufficiently completed to obtain proofs $(A, \pi , B)$ . The superstructure of such nodes and structures above $\alpha $ present the limits on what a constructivist can know at node $\alpha $ . Kripke models as so described may be seen as classical ‘platonistic’ (in the sense that possible future stages are all held in common existence) models of evidence which may convince constructivists that certain logical statements are not derivable. By definition we have $\alpha \;\Vdash \; A \rightarrow B$ exactly when for all $\beta \sqsupset \alpha $ we have $\beta \Vdash A$ implies $\beta \Vdash B$ . By definition we have $\alpha \;\Vdash \; (A \vdash B)$ exactly when for all $\beta \sqsupseteq \alpha $ we have $\beta \Vdash A$ implies $\beta \Vdash B$ . Situation $\alpha \not \sqsubset \alpha $ of an irreflexive node simulates a constructivist who is in possession of constructions, maybe idealized or in anticipation, of proofs which may lead to newly conceived operations or to further understanding about the intended structure. If we further have $\beta \Vdash A$ for all $\beta \sqsupset \alpha $ , we simulate that at node $\alpha $ the constructivist has a construction, maybe idealized or in anticipation, of a proof of A. So $\alpha \;\Vdash \; \top \rightarrow A$ . Subcase $\alpha \Vdash A$ simulates that the constructivist has a proof (construction) for A. Subcase $\alpha \nVdash A$ simulates that the constructivist has a construction c for a proof (construction) of A which, when c has been sufficiently completed, reveals a proof (construction) for A which employs new methods of reasoning. An irreflexive node $\alpha $ with $\alpha \Vdash A \rightarrow B$ allows us to simulate a constructivist who can have a construction c, in anticipation or in content or other, for a proof $(A,\xi ,B)$ such that after sufficient completion of c a proof $(A,\pi ,B)$ is produced with possibly new methods of reasoning. Such $\pi $ are again constructions. Consider the special case where $\alpha \Vdash A \rightarrow (B_1 \rightarrow B_2)$ . In that case sufficient completion of c results in a proof $(A,\pi ,B_1 \rightarrow B_2)$ . If $\alpha \sqsubset \beta \Vdash A$ , then $\beta \Vdash B_1 \rightarrow B_2$ , which simulates that at this further stage there is a construction d for $(B_1,\eta ,B_2)$ . For irreflexive $\beta $ this allows for the possibility that only after further completion of d we get a proof $(B_1,\sigma ,B_2)$ employing still further new methods of reasoning. Are transitive Kripke models insufficient? Yes. Are they evidence of non-provability? Also yes. If one is willing to accept the transitive Kripke models and the completeness theorem as evidence, then Basic Propositional Logic is complete.

Over Basic Propositional Logic we have the equivalence of $\neg \neg A$ with $\neg \neg \neg \neg A$ , see [Reference Alizadeh, Ardeshir and Ruitenburg1, Proposition 4.1.4, p. 145]. Brouwer writes in [Reference Brouwer11] that even $\neg A$ and $\neg \neg \neg A$ are equivalent. The key stepFootnote ¹² in his argument is that A implies $\neg \neg A$ . We follow Heyting and equate $\neg A$ with $A \rightarrow \bot $ . A special case of the key step is the claim $\top \;\vdash \; (\top \rightarrow \bot ) \rightarrow \bot $ which over Basic Propositional Logic is equivalent to $(\top \rightarrow \bot ) \;\vdash \; \bot $ since Basic Propositional Logic is faithful, see [Reference Ardeshir and Ruitenburg2, pp. 321 and 329]. Using our ‘axiomatic’ notation, the key step implies that there exists a constructive proof $((\top \rightarrow \bot ), \pi , \bot )$ which turns a hypothetical proof of inconsistency into an actual proof of a contradiction. This is too broad an acceptance of proof-in-principle for a growing universe of mathematical objects and proofs since such a future (hypothetical) construction may not be constructively acceptable at present.

5.2 Predicate logic

When we broaden from propositional logic to predicate logic, we extend from propositional letters P to predicates $P(x_1,x_2,\ldots ,x_m)$ of arities $m \geq 0$ . For convenience we may write ${\mathbf {x}}$ for lists $x_1, x_2,\ldots , x_m$ of variables of finite length $m \geq 0$ . We write ${\mathbf {xy}}$ for concatenated lists $x_1, x_2, \ldots , x_m, y_1, y_2, \ldots , y_n$ . We write $P(\mathbf {x})$ for atoms $P(x_1,x_2,\ldots ,x_m)$ , and $A \mathbf {x}$ for formulas A when we want to emphasize that all free variables of A are among those in ${\mathbf {x}}$ . For constant symbols $c_1, c_2, \ldots , c_k$ we use similar conventions.

Constant symbols are intended to stand for descriptions. The word ‘description’ replaces the use of ‘construction’ or other terminology of earlier proof interpretations in describing elements of the domain of discourse. On [Reference Bishop6, pp. 6–7] Bishop uses the word ‘description’ for sets defined in a possibly incomplete way. We broaden this approach to all objects. Logic expresses very general mathematical theorems which includes theorems about mathematics where descriptions may be less complete. Descriptions may be idealized constructions, or ones in anticipation. The universe of descriptions itself may be an open-ended accumulation like the universe of proofs, we may discover new descriptions as mathematics advances.

Variables x are intended to range over descriptions including ones that are not yet recognized to be of elements of the intended domain. We write $\operatorname {\mathrm {E}} x$ or $\operatorname {\mathrm {E}}(x)$ for the propositional statement that the element described by x is sound, that is, the element described by x belongs to the intended domain. This is in line with Dana Scott’s existence predicate of [Reference Scott51]. We may write $\operatorname {\mathrm {E}}\mathbf {x}$ or $\operatorname {\mathrm {E}}(\mathbf {x})$ for $\operatorname {\mathrm {E}} x_1 \land \operatorname {\mathrm {E}} x_2 \land \cdots \land \operatorname {\mathrm {E}} x_n$ . We treat existence as a primitive $\operatorname {\mathrm {E}} x$ , thereby preserving optimal generality when axiomatizing our very general mathematical theorems.

We write $(\vec {A}, \pi \mathbf {x}, B)$ for a proof $\pi \mathbf {x}$ with assumptions $\vec {A}$ and conclusion B, where list ${\mathbf {x}}$ includes all variables that occur free in $\vec {A},B$ . Besides assumptions $\vec {A}$ and conclusion B, proof $\pi \mathbf {x}$ also holds all substitution places of variables ${\mathbf {x}}$ in those formulas. We write $A \vdash _{\mathbf {x},\vec {B}} C$ if a proof $(A,\vec {B}, \pi \mathbf {x}, C)$ exists, with the expected abbreviations when A is absent or $\vec {B} = ()$ or $\mathbf {x} = ()$ . For convenience we ignore the order of the variables in ${\mathbf {x}}$ , or duplications among them. Proof $\pi \mathbf {x}$ is such that no further meaning is assigned to the variables $x_i$ in ${\mathbf {x}}$ in deriving C, beyond what follows from assuming $A,\vec {B}$ . This clarifies what it means to assume formulas with free variables.

We allow the ‘empty’ description $\ell $ , a description of ‘nothing’, an extreme version of an incomplete description for elements of the intended domain. So there is at least one description. There is no element in the intended domain described by $\ell $ . One technical advantage of $\ell $ is that variables range over at least one object, see the relevant substitution schema below where a free variable y is replaced by $\ell $ . The atomic existence sentence $\operatorname {\mathrm {E}} \ell $ can play the role of an abstract symbol $\bot $ . We have $\bot $ in the language, and a trivial proof $(\operatorname {\mathrm {E}} \ell , \pi , \bot )$ . So also axiom

$$ \begin{align*} \operatorname{\mathrm{E}} \ell \;\vdash_{\mathbf{x},\vec{D}}\; \bot. \end{align*} $$

If y isn’t specified in proof $\pi \mathbf {x}$ , then we can modify the proof to $\pi '\mathbf {x}y$ by adding such y. If, instead, variable y in proof $(A,\vec {D}, \pi \mathbf {x}y, C)$ doesn’t occur in $A,\vec {D},C$ , then we can remove y, for example by replacing y by the empty description $\ell $ . So we have rules

$$ \begin{align*} \displaystyle{\frac{A \;\vdash_{\mathbf{x}y,\vec{D}}\; C}{A \;\vdash_{\mathbf{x},\vec{D}}\; C}} \quad y \text{ not free in } A,\vec{D},C, \quad \text{and} \quad \displaystyle{\frac{A \;\vdash_{\mathbf{x},\vec{D}}\; C}{A \;\vdash_{\mathbf{x}y,\vec{D}}\; C}}. \end{align*} $$

No further meaning is assigned to the variables $x_i$ in ${\mathbf {x}}$ in deriving C, beyond what follows from assuming $A,\vec {D}$ , so we can substitute other free variables for them. A proof $(A\mathbf {x},\vec {D}\mathbf {x}, \pi \mathbf {x}, C\mathbf {x})$ implies a proof $(A\mathbf {y},\vec {D}\mathbf {y}, \pi \mathbf {y}, C\mathbf {y})$ , where no variable of ${\mathbf {y}}$ is allowed to become bound after substitution. So we have substitution rule

$$ \begin{align*} \displaystyle{\frac{A\mathbf{x} \;\vdash_{\mathbf{x},\vec{D}\mathbf{x}}\; C\mathbf{x}}{A\mathbf{y} \;\vdash_{\mathbf{y},\vec{D}\mathbf{y}}\; C\mathbf{y}}} \quad \text{no variable of } {\mathbf{y}} \text{ becomes bound}. \end{align*} $$

Substitution is more general than renaming free variables since we may substitute the same variable y for different variables x and $x'$ . Substitution by constants is easier. So we have substitution rule

$$ \begin{align*} \displaystyle{\frac{A\mathbf{xy} \;\vdash_{\mathbf{xy},\vec{D}\mathbf{xy}}\; C\mathbf{xy}}{A\mathbf{xc} \;\vdash_{\mathbf{x},\vec{D}\mathbf{xc}}\; C\mathbf{ xc}}}. \end{align*} $$

We have the expected generalizations of the rules preceding Section 5.1, essentially by adding variables ${\mathbf {x}}$ where necessary or permitted. For example, we have rules

$$ \begin{align*} \displaystyle{\frac{A \vdash_{\mathbf{x}.\vec{D}} C}{A \vdash_{\mathbf{x},B, \vec{D}} C}} \quad \text{and} \quad \displaystyle{\frac{\vdash_{\mathbf{x},B,\vec{D}} C}{B \vdash_{\mathbf{x},\vec{D}} C}} \quad \text{and} \quad \displaystyle{\frac{B \vdash_{\mathbf{x},\vec{D}} C}{\vdash_{\mathbf{x}, B,\vec{D}} C}}, \end{align*} $$

where ${\mathbf {x}}$ includes all free variables that occur. Similarly for axiom and rule

$$ \begin{align*} A \vdash_{\mathbf{x},\vec{D}} A \quad \text{and} \quad \displaystyle{\frac{A \vdash_{\mathbf{x},\vec{D}} B \quad B \vdash_{\mathbf{x}, \vec{D}} C}{A \vdash_{\mathbf{x},\vec{D}} C}}. \end{align*} $$

The proposition logical rules of derivations for $A \land B$ , $\top $ , $A \lor B$ , and $\bot $ also remain essentially unchanged. In principle the same holds for implication $A \rightarrow B$ . However, we replace the proposition logical rules for implication by different ones when we combine implication with universal quantification.

Predicates P stand for statements about elements of the intended domain. So predicates are strict, that is, we have abstract axiom schemas of form $(P(\mathbf {x}), \pi \mathbf {x}, \operatorname {\mathrm {E}} \mathbf {x})$ and axioms

$$ \begin{align*} P(\mathbf{x}) \;\vdash_{\mathbf{xy},\vec{D}}\; \operatorname{\mathrm{E}} \mathbf{x}. \end{align*} $$

A proof interpretation presupposes the constructive nature of atomic statements. So for the axiomatized object $\pi \mathbf {x}$ evidence must be substituted in concrete situations.

For each formula A we have formulas $\exists x A$ with $\exists x$ the intended meaning ‘there exists x’. We freely rename variables bound by $\exists $ , with the usual restrictions that with substitution the new variables don’t become bound by other quantifiers, and unchanged variables don’t become bound by the new variable attached to this $\exists $ . There are trivial proofs $(A \land \operatorname {\mathrm {E}} x, \sigma x\mathbf {y}, \exists x A)$ . Suppose we have a proof $(\exists x A, \pi \mathbf {y}, B)$ , where x doesn’t occur in ${\mathbf {y}}$ . We can trivially modify the proof by adding a variable so that we have $(\exists x A, \pi x\mathbf {y}, B)$ . By composition we have a proof $(A \land \operatorname {\mathrm {E}} x, (\pi \sigma )x\mathbf {y}, B)$ . In the other direction, suppose we have a proof $(A \land \operatorname {\mathrm {E}} x, \pi x\mathbf {y}, B)$ , where x isn’t free in B. Then there is a proof which we name $(\exists x A, [\pi ]\mathbf {y}, B)$ , and which we construct in a uniform way in terms of $\pi x\mathbf {y}$ . This clarifies what it means to assume $\exists x A$ . Further assumptions $\vec {D}$ are permitted when they don’t limit the meaning of x. So we have rules

$$ \begin{align*} \displaystyle{\frac{A \land \operatorname{\mathrm{E}} x \;\vdash_{x\mathbf{y},\vec{D}}\; B}{\exists x A \;\vdash_{\mathbf{y},\vec{D}}\; B}} \quad x \text{ not free in } B,\vec{D} \quad\text{and} \quad \displaystyle{\frac{\exists x A \;\vdash_{\mathbf{y},\vec{D}}\; B}{A \land \operatorname{\mathrm{E}} x \;\vdash_{x\mathbf{y},\vec{D}}\; B}}. \end{align*} $$

Lists $\vec {D}$ of additional assumptions are key in proving existential distributivity. A straightforward proof yields $B \land \operatorname {\mathrm {E}} x \;\vdash _{x\mathbf {y},A}\; \exists x (A \land B)$ . So if x is not free in A, then

$$ \begin{align*} \exists x B \;\vdash_{\mathbf{y},A}\; \exists x (A \land B). \end{align*} $$

Thus

$$ \begin{align*} A \land \exists x B \;\vdash_{\mathbf{y},\vec{D}}\; \exists x (A \land B) \quad x \text{ not free in } A. \end{align*} $$

We introduce implication and universal quantification using one single format. The combination formulas are essentially more elaborate than the form $\forall x A$ . Implications $A \rightarrow B$ are definable in a uniform way as special cases.

We briefly employ proposition logical implication to clarify the reasons for the choice of a new format. Suppose we have a proof $(A \land \operatorname {\mathrm {E}} x, \pi x\mathbf {y}, B)$ with x not free in A. So we have a proof $(A, \pi _A x\mathbf {y}, \operatorname {\mathrm {E}} x \rightarrow B)$ , where $\pi _A x\mathbf {y}$ takes proof $\pi x\mathbf {y}$ , replaces its assumptions $A \land \operatorname {\mathrm {E}} x$ by assumption $\operatorname {\mathrm {E}} x$ and derives $A \land \operatorname {\mathrm {E}} x$ using the assumption A of $\pi _A x\mathbf {y}$ . Finally append that the result is a proof of conclusion $\operatorname {\mathrm {E}} x \rightarrow B$ . Since variable x isn’t free in A, construction $\pi _A x\mathbf {y}$ works for any description c one may ever substitute for x, where $\operatorname {\mathrm {E}} c$ restricts the choice of descriptions to those of elements assumed to belong to the intended domain. So we have a proof $(A, \sigma \mathbf {y},\forall x (\operatorname {\mathrm {E}} x \rightarrow B))$ with $\forall x$ the intended meaning ‘for all x’. Basic logic lacks full modus ponens, so the arrow in $\operatorname {\mathrm {E}} x \rightarrow B$ is no longer always removable over domains with elements. This differs from the case of existential quantification, where formulas $\exists x A$ and $\exists x (\operatorname {\mathrm {E}} x \land A)$ remain equivalent. Quantification is intended to only apply to descriptions of elements of the intended domain, so formula $\forall x (\operatorname {\mathrm {E}} x \rightarrow B)$ is equivalent to $\forall x (\top \rightarrow B)$ . We employ two ways to broaden our new notation. First, by the same argument why it is constructively acceptable to conclude $A \vdash _{\mathbf {y},\vec {D}} \forall x (\top \rightarrow C)$ from $A \land \operatorname {\mathrm {E}} x \vdash _{x\mathbf {y},\vec {D}} C$ (x not free in $A,\vec {D}$ ), it is constructively acceptable to conclude $A \vdash _{\mathbf {y},\vec {D}} \forall x (B \rightarrow C)$ from ${A \land B \land \operatorname {\mathrm {E}} x \vdash _{x\mathbf {y},\vec {D}} C}$ (x not free in $A,\vec {D}$ ). Second, since nested quantifications like $\forall x \forall y (A \rightarrow B)$ aren’t well defined, we include multi-variable universal quantifications like $\forall xy (A \rightarrow B)$ as primitive new notations.

Combining the motivations of the previous paragraph, we have for each pair of formulas A and B universal implication formulas $\forall \mathbf {x} (A \rightarrow B)$ with the intended meaning that for all lists ${\mathbf {x}}$ assumed in the intended domain and for which A is assumed to hold, formula B also holds. Formula $\forall \mathbf {x} (A \rightarrow B)$ has to reflect the meaning of $A \land \operatorname {\mathrm {E}} \mathbf {x} \vdash _{\mathbf {xy}, \vec {D}} B$ within the bounds of what is constructively acceptable. We freely rename variables bound by $\forall $ , with the restrictions that with substitution the new variables don’t become bound by other quantifiers or by each other, and unchanged variables don’t become bound by the new variables attached to this $\forall $ . For convenience we ignore the order of the variables in ${\mathbf {x}}$ , or duplications among them, in our notation. List ${\mathbf {x}}$ is allowed to have length $0$ . In that case we write $A \rightarrow B$ as short for $\forall (A \rightarrow B)$ .

Suppose we have a proof $(A \land B \land \operatorname {\mathrm {E}} \mathbf {x}, \pi \mathbf {xy}, C)$ with none of the variables in list ${\mathbf {x}}$ free in A. Then we have a proof $(A, \pi _A\mathbf {xy}, (B \land \operatorname {\mathrm {E}} \mathbf {x}) \rightarrow C)$ , where $\pi _A\mathbf {xy}$ takes proof $\pi \mathbf {xy}$ , replaces its assumption $A \land B \land \operatorname {\mathrm {E}} \mathbf {x}$ by assumption $B \land \operatorname {\mathrm {E}} \mathbf {x}$ and derives $A \land B \land \operatorname {\mathrm {E}} \mathbf {x}$ using the assumption A of $\pi _A\mathbf {xy}$ . Finally append that the result is a proof for conclusion $(B \land \operatorname {\mathrm {E}} \mathbf {x}) \rightarrow C$ . Since variables ${\mathbf {x}}$ aren’t free in A, construction $\pi _A\mathbf {xy}$ works for any list of descriptions ${\mathbf {c}}$ one may ever substitute for the ${\mathbf {x}}$ , where $\operatorname {\mathrm {E}} \mathbf {c}$ restricts the choice of descriptions for B and C to those of elements assumed to belong to the intended domain. So we have a proof which we name $(A, \langle \pi _A \rangle \mathbf {y},\forall \mathbf { x} (B \rightarrow C))$ , and which we construct in a uniform way in terms of $\pi _A\mathbf {xy}$ . Further assumptions $\vec {D}$ are permitted when they don’t limit the meaning of ${\mathbf {x}}$ . Thus we have rule

$$ \begin{align*} \displaystyle{\frac{ A \land B \land \operatorname{\mathrm{E}} \mathbf{x} \;\vdash_{\mathbf{xy},\vec{D}}\; C}{A \;\vdash_{\mathbf{y},\vec{D}}\; \forall \mathbf{x} (B \rightarrow C)}} \quad \text{no variable of } {\mathbf{x}} \text{ free in } A,\vec{D}. \end{align*} $$

In particular $A \;\vdash _{\mathbf {y},\vec {D}}\; B \rightarrow C$ follows from $A \land B \;\vdash _{\mathbf {y},\vec {D}}\; C$ .

Universal implication broadens the rules for proposition logical implication. We get natural replacements for its proposition logical ‘formalization’ axioms. The earlier axioms for implication are replaced by

$$ \begin{align*} &\forall \mathbf{x} (A \rightarrow B) \land \forall \mathbf{x} (B \rightarrow C) \;\vdash_{\mathbf{y},\vec{D}}\; \forall \mathbf{x} (A \rightarrow C) \\ &\forall \mathbf{x} (A \rightarrow B) \land \forall \mathbf{x} (A \rightarrow C) \;\vdash_{\mathbf{y},\vec{D}}\; \forall \mathbf{x} (A \rightarrow (B \land C)) \\ &\forall \mathbf{x} (B \rightarrow A) \land \forall \mathbf{x} (C \rightarrow A) \;\vdash_{\mathbf{y},\vec{D}}\; \forall \mathbf{x} ((B \lor C) \rightarrow A). \end{align*} $$

Although their justifications are similar to the ones for implication in Section 5.1, there are complications which we could avoid in the proposition logical case. Consider a formula $\forall \mathbf {x}(A\mathbf {xy} \rightarrow B\mathbf {xy})$ , where ${\mathbf {xy}}$ includes all variables free in A or B, and lists ${\mathbf {x}}$ and ${\mathbf {y}}$ have no variables in common. When we assume this formula, the variables in ${\mathbf {x}}$ and ${\mathbf {y}}$ have different status. We have an assumed proof $(A\mathbf {xy} \land \operatorname {\mathrm {E}} \mathbf {x}, (\xi \mathbf {x})\mathbf { y},B\mathbf {xy})$ with $\xi $ a ‘hypothetical’ proof variable, and the parentheses in notation $(\xi \mathbf {x})$ indicate that ${\mathbf {x}}$ lists the variables over which $\xi $ is assumed to universally quantify. We assume a construction $\gamma $ of a proof (construction) $(\xi \mathbf {x})\mathbf { y}$ . Construction $\gamma $ may be idealized or in anticipation. Its intended meaning is as follows. We describe two possible scenarios, one focused on variables $\mathbf x$ , the other focused on variables ${\mathbf {y}}$ . Consider the variables ${\mathbf {x}}$ . After sufficient completion of $\gamma $ we may obtain a proof for $\xi $ such that from now on, but not before, we have that for all descriptions ${\mathbf {c}}$ of elements of the domain, we can perform composition $\xi \mathbf {c}$ and have $(\xi \mathbf {c}) \mathbf {y}$ . If $\mathbf {y} = ()$ is empty, then $(\xi \mathbf {c})$ is a proof of $A \mathbf {c}() \;\vdash \; B \mathbf {c}()$ . Now consider the variables ${\mathbf {y}}$ instead. For all descriptions ${\mathbf {d}}$ we have a proof $(\xi \mathbf {x})\mathbf {d}$ , still under construction, of $A\mathbf {xd} \;\vdash \; B\mathbf {xd}$ . Without sufficient completion of $\gamma $ , proof $(\xi \mathbf {x})\mathbf {d}$ may still be ‘hypothetical’. Even if $\mathbf {x} = ()$ is empty and descriptions ${\mathbf {d}}$ become available after some advancement in mathematics, we may at most have assumption $A()\mathbf {d} \rightarrow B()\mathbf {d}$ . Only after a sufficient completion of $\gamma $ we may obtain a proof for $(\xi )\mathbf {d}$ of $A()\mathbf {d} \vdash B()\mathbf {d}$ . This clarifies what it means to assume $\forall \mathbf {x}(A\mathbf {xy} \rightarrow B\mathbf { xy})$ . This is essentially more general than a proof for $A\mathbf {xy} \land \operatorname {\mathrm {E}} \mathbf {x} \;\vdash \; B\mathbf {xy}$ , from which we obtain a proof for $A\mathbf {xy} \land \operatorname {\mathrm {E}} \mathbf {xy} \;\vdash \; B\mathbf {xy}$ where variables ${\mathbf {x}}$ and ${\mathbf {y}}$ have the same status. For the first axiom above of ‘formalized’ composition consider assumed proofs $(A \land \operatorname {\mathrm {E}} \mathbf {x}, (\xi \mathbf {x})\mathbf {y}, B)$ and $(B \land \operatorname {\mathrm {E}} \mathbf {x}, (\eta \mathbf {x})\mathbf {y}, C)$ , where we may suppose that ${\mathbf {x}}$ and ${\mathbf {y}}$ are disjoint. The composition proof equals $(A \land \operatorname {\mathrm {E}} \mathbf {x}, ((\eta \xi )\mathbf {x})\mathbf {y}, C)$ with the distinct roles of the variables in ${\mathbf {x}}$ and ${\mathbf {y}}$ preserved. The same applies to the other two axioms.

When we broaden from propositional logic to predicate logic, further ‘formalization’ axioms are needed.

Assume $\forall \mathbf {x} (A \rightarrow B)$ . So we assume we have a proof $(A \land \operatorname {\mathrm {E}} \mathbf {x}, (\xi \mathbf { x})\mathbf {z}, B)$ with $\xi $ as proof variable. We can substitute new variables ${\mathbf {y}}$ for the ones in ${\mathbf {x}}$ with the usual restrictions that none of them become bound in A or B, and that ${\mathbf {y}}$ and ${\mathbf {z}}$ are disjoint. So we have a proof $(A[\mathbf {x}/\mathbf {y}] \land \operatorname {\mathrm {E}} \mathbf {y}, (\xi \mathbf {y})\mathbf {z}, B[\mathbf {x}/\mathbf {y}])$ . Thus we have axiom

$$ \begin{align*} &\forall \mathbf{x} (A\mathbf{x} \rightarrow B\mathbf{x}) \;\vdash_{\mathbf{z},\vec{D}}\;\forall \mathbf{y} (A\mathbf{y} \rightarrow B\mathbf{y}) \quad \text{ no variable in } {\mathbf{y}} \text{ becomes bound in } A \\ &\qquad\text{or } B, \text{ and } {\mathbf{y}} \text{ and } {\mathbf{z}} \text{ are disjoint}. \end{align*} $$

This axiom is more general than renaming variables. For example we also have

$$ \begin{align*} \forall xx' (Axx' \rightarrow Bxx') \;\vdash\; \forall y (Ayy \rightarrow Byy), \end{align*} $$

subject to the usual variable substitution restrictions.

For the existential quantifier $\exists $ we need a further such ‘formalization’ axiom. Assume $\forall \mathbf {x}y (A \rightarrow B)$ , with y not free in B. So we assume we have a proof $(A \land \operatorname {\mathrm {E}} \mathbf {x}y, (\xi y\mathbf {x})\mathbf {z}, B)$ with $\xi $ as ‘hypothetical’ proof variable. So we have a proof $(\exists y A \land \operatorname {\mathrm {E}} \mathbf {x}, ([\xi ]\mathbf {x})\mathbf {z}, B)$ . Thus we have axiom

$$ \begin{align*} \forall \mathbf{x}y (A \rightarrow B) \;\vdash_{\mathbf{z},\vec{D}}\; \forall \mathbf{x} (\exists y A \rightarrow B) \quad y \text{ not free in } B. \end{align*} $$

Assuming a universal implication $\forall \mathbf {x} (A \rightarrow B)$ implies that we have an assumed proof $(A \land \operatorname {\mathrm {E}} \mathbf {x}y, (\xi \mathbf {x}y)\mathbf {z}, B)$ , where we choose to add a variable y not free in A or B. Absence of a free y in A or B allows this assumption of trivial universal quantification of $\xi $ over y. So we have axiom

$$ \begin{align*} \forall \mathbf{x} (A \rightarrow B) \;\vdash_{\mathbf{z},\vec{D}}\; \forall \mathbf{x}y (A \rightarrow B) \quad y \text{ not free in any of the formulas}. \end{align*} $$

There are trivial proofs $(\forall \mathbf {x}y (A \rightarrow B), \pi {y\mathbf {z}}, \forall \mathbf {x} ((A \land \operatorname {\mathrm {E}} y) \rightarrow B))$ . These come with the intended meaning of assuming a universal implication $\forall \mathbf {x}y (A \rightarrow B)$ , in this case an assumed proof $(A \land \operatorname {\mathrm {E}} \mathbf { x}y, (\xi \mathbf {x}y)\mathbf {z}, B)$ . Replace $(\xi \mathbf {x}y)\mathbf {z}$ by $(\eta \mathbf {x})y\mathbf {z}$ by ignoring the universal quantification over y. Consequently, with composition, a proof $(C, \sigma {y\mathbf {z}},\forall \mathbf {x}y (A \rightarrow B))$ implies that we have a proof

$$ \begin{align*} (C, (\pi\sigma){y\mathbf{z}},\forall \mathbf{x} ((A \land \operatorname{\mathrm{E}} y) \rightarrow B)). \end{align*} $$

Further assumptions $\vec {D}$ are permitted. So we have rule

$$ \begin{align*} \displaystyle{\frac{C \;\vdash_{y\mathbf{z},\vec{D}}\; \forall \mathbf{x}y (A \rightarrow B)}{C \;\vdash_{y\mathbf{z},\vec{D}}\; \forall \mathbf{x} ((A \land \operatorname{\mathrm{E}} y) \rightarrow B)}}. \end{align*} $$

This completes our axiomatization of Basic Predicate Logic.

The system includes the Basic Predicate Calculus $\operatorname {\mathrm {BQC}}$ of [Reference Ruitenburg49] when we ignore function symbols and equality. Over our new system we have both $\exists x A \;\vdash \; \exists x (\operatorname {\mathrm {E}} x \land A)$ and $\exists x (\operatorname {\mathrm {E}} x \land A) \;\vdash \; \exists x A$ , and both $\forall \mathbf {x} (A \rightarrow B) \;\vdash \; \forall \mathbf {x} ((A \land \operatorname {\mathrm {E}} \mathbf {x}) \rightarrow B)$ and $\forall \mathbf {x} ((A \land \operatorname {\mathrm {E}} \mathbf {x}) \rightarrow B) \;\vdash \; \forall \mathbf {x} (A \rightarrow B)$ . So $\operatorname {\mathrm {BQC}}$ without existence predicate but with inhabited intended domain embeds in the new system by relativization of quantifiers plus axiom $\vdash \exists x \top $ . Additionally replace entailments $A \vdash B$ of $\operatorname {\mathrm {BQC}}$ by $A \land \operatorname {\mathrm {E}} \mathbf {x} \vdash B$ , where ${\mathbf {x}}$ lists the free variables of A and B.

Conversely, embed the new system in $\operatorname {\mathrm {BQC}}$ by adding a new predicate $F x$ to the language of $\operatorname {\mathrm {BQC}}$ , and then relativize quantifiers to F while sending $\operatorname {\mathrm {E}}$ to F. The presence of $\ell $ makes that over the $\operatorname {\mathrm {BQC}}$ language with extra predicate $F x$ the overall domain has an element, as is required.

Do we have a complete set of axioms and rules for constructive predicate logic? The evidence for non-provability is different in nature from provability. In [Reference Ruitenburg49] we find a completeness theorem for $\operatorname {\mathrm {BQC}}$ with transitive Kripke models. There is no Kripke model completeness theorem for the new system. Using transitive Kripke models as weak counterexamples to constructive provability has limited value as do reflexive transitive Kripke models in the intuitionistic case. Imagine a Kripke model $\mathfrak {M}$ on $(W, \sqsubset )$ with nodes W and transitive relation $\sqsubset $ , and with structures $\mathfrak {M}_{\alpha }$ at nodes $\alpha \in W$ with ‘extended’ domains $M_{\alpha }$ . The intended proper sub-domain at $\alpha $ is determined by those c for which $\alpha \Vdash \operatorname {\mathrm {E}} c$ . All relations from the predicate logic language are essentially restricted to these sub-domains. For all $\alpha \sqsubseteq \beta $ we have morphisms $\varphi ^{\alpha }_{\beta }$ such that $\varphi ^{\alpha }_{\alpha } = \text {id}$ , and $\varphi ^{\alpha }_{\gamma } = \varphi ^{\beta }_{\gamma } \varphi ^{\alpha }_{\beta }$ for all $\gamma \sqsupseteq \beta \sqsupseteq \alpha $ . A weakly increasing function $f : \mathbb {N} \rightarrow W$ simulates temporal information, where what is forced at $f(n) = \alpha $ indicates what the constructivist can know at stage n. Parts of this are motivated in the proposition logical case on page 13. We have $\alpha \;\Vdash _{\mathbf {y}}\; (A\mathbf {y} \vdash _{\mathbf {y}} B\mathbf {y})$ exactly when for all $\beta \sqsupseteq \alpha $ and $\mathbf {c} \in M_{\beta }$ we have $\beta \Vdash A\mathbf {c}$ implies $\beta \Vdash B\mathbf {c}$ . So we have $\alpha \;\Vdash _{\mathbf {y}}\; \forall \mathbf {x} (A\mathbf {xy} \rightarrow B\mathbf { xy})$ exactly when for all $\beta \sqsupseteq \alpha $ and $\mathbf {c} \in M_{\beta }$ we have $\beta \Vdash \forall \mathbf {x} (A\mathbf {xc} \rightarrow B\mathbf {xc})$ . We have $\alpha \;\Vdash \; \forall \mathbf {x} (A\mathbf {xc} \rightarrow B\mathbf {xc})$ exactly when for all $\beta \sqsupset \alpha $ and $\mathbf {d} \in M_{\beta }$ we have $\beta \;\Vdash \; (A\mathbf {dc} \land \operatorname {\mathrm {E}} \mathbf {d} \;\vdash \; B\mathbf {dc})$ . In terms of the proof interpretation, at node $\beta \sqsupset \alpha $ construction $\sigma $ at stage $\alpha $ for universal implication sentence $\forall \mathbf {x}(A\mathbf {x} \rightarrow B\mathbf {x})$ has been sufficiently completed to obtain a proof $(A\mathbf {x},\pi \mathbf {x}, B\mathbf {x})$ . In terms of the proof interpretation, at node $\beta \sqsupseteq \alpha $ with $\mathbf {c} \in M_{\beta }$ , construction $\sigma \mathbf {y}$ at stage $\alpha $ for universal implication formula $\forall \mathbf {x}(A\mathbf {xy} \rightarrow B\mathbf {xy})$ implies a construction $\sigma \mathbf {c}$ for universal implication sentence $\forall \mathbf {x}(A\mathbf {xc} \rightarrow B\mathbf {xc})$ . Are transitive Kripke models insufficient? Yes. Are they evidence of non-provability? Also yes. If one is willing to accept transitive Kripke models and the completeness theorem as evidence, then $\operatorname {\mathrm {BQC}}$ is complete. We give a non-trivial illustration. The following is the case:

$$\begin{align*}\text{Not a general rule:} \quad \displaystyle{\frac{C \;\vdash_{y\mathbf{z},\vec{D}}\; \forall \mathbf{x} ((A\land \operatorname {\mathrm {E}} y) \rightarrow B)}{C \;\vdash_{\mathbf{z},\vec{D}}\; \forall \mathbf{x}y (A \rightarrow B)}} \quad y \text{ not free in } C,\vec{D}. \end{align*}$$

An explanation of why this is not a general rule may benefit from the following observation over Basic Propositional Logic:

$$\begin{align*}\text{Not a general rule:} \quad \displaystyle{\frac{A \;\vdash\; \top \rightarrow B}{\top \;\vdash\; A \rightarrow B}}. \end{align*}$$

For consider a transitive Kripke model with nodes $\alpha \sqsubset \beta $ and $\beta $ irreflexive. Let all nodes $\delta \sqsupseteq \alpha $ be such that $\delta = \alpha $ or $\delta \sqsupseteq \beta $ . Set $\delta \Vdash A$ exactly when $\delta \sqsupseteq \beta $ and $\delta \Vdash B$ exactly when $\delta \sqsupset \beta $ . So $\alpha \;\Vdash \; (A \vdash (\top \rightarrow B))$ and $\alpha \;\nVdash \; (\top \vdash (A \rightarrow B))$ . A Kripke model sketches a possible constructive situation. We understand this model as an illustration of the significance of the order by which mathematics advances. In the given Kripke model mathematics has to advance twice. First we may advance and get a proof of A from which a proof of $\top \rightarrow B$ follows, say construction $\sigma $ . Second we advance by sufficiently completing $\sigma $ and get a proof of B. The bottom sequent of the rule doesn’t hold. In the Kripke model it implies that if mathematics advances we would get a proof $(A,\pi ,B)$ besides a proof of A, hence by composition (not modus ponens) a premature claim of a proof of B. So the order of advancement matters. As to the earlier rule: On one hand the rule holds in the special case when C equals $\top $ . On the other hand we even have the special case:

$$ \begin{align*} \text{Not a general rule:} \quad \displaystyle{\frac{C \;\vdash_y\; (\operatorname{\mathrm{E}} y \rightarrow By)}{C \;\vdash\; \forall y (\top \rightarrow By)}} \quad y \text{ not free in } C. \end{align*} $$

For consider a transitive Kripke model with nodes $\alpha \sqsubset \beta \sqsubset \gamma $ , and $\beta $ and $\gamma $ irreflexive. All other nodes $\delta \sqsupseteq \alpha $ satisfy $\delta \sqsupset \gamma $ . Set $\delta \Vdash C$ exactly when $\delta \sqsupseteq \beta $ . Let c be a new description of an element above $\gamma $ satisfying $\gamma \Vdash \operatorname {\mathrm {E}} c$ . Set $\delta \Vdash Bc$ exactly when $\delta \sqsupset \gamma $ . There are no other domain elements d above any node for which $\operatorname {\mathrm {E}} d$ holds. Now $\alpha \;\Vdash _y\; (C \vdash _y (\operatorname {\mathrm {E}} y \rightarrow By))$ and $\alpha \;\nVdash \; (C \vdash \forall y (\top \rightarrow By))$ . A Kripke model sketches a possible constructive situation. In the given Kripke model mathematics has to advance three times. First we may advance and get a proof of C from which a proof $\pi y$ of $\operatorname {\mathrm {E}} y \rightarrow By$ follows. In the Kripke model, construction $\pi y$ need not reveal new methods of reasoning on its own even after completion. Construction $\pi y$ only implies a further construction of a proof $(\operatorname {\mathrm {E}} d, \xi d, B d)$ after a description d is provided. Composition $\pi d$ is a construction for a proof $(\operatorname {\mathrm {E}} d, \xi d, B d)$ rather than a composition of proofs, which would have been a proof. In the model a proof $(\operatorname {\mathrm {E}} d, \rho d, B d)$ can only be obtained by sufficiently completing construction $\pi d$ . Second we will advance and get a description (in essence a construction) c and a proof of $\operatorname {\mathrm {E}} c$ . This gives us proof construction $\pi c$ of $\operatorname {\mathrm {E}} c \rightarrow Bc$ , so also a proof of $\top \rightarrow Bc$ . Finally mathematics has to advance a third time by sufficiently completing $\pi c$ to obtain a proof of $Bc$ . The bottom sequent doesn’t hold. It implies that if mathematics advances we get a proof of C from which a proof $\sigma $ of $\forall y (\top \rightarrow By)$ follows. Construction $\sigma $ is independent of y, so by sufficient completion of $\sigma $ mathematics advances with a proof $(\operatorname {\mathrm {E}} y, \tau y, By)$ . With the next advance with a description of c and proof of $\operatorname {\mathrm {E}} c$ we compose constructions and get $(\operatorname {\mathrm {E}} c, \tau c, Bc)$ , which with another proof composition allows us to claim $Bc$ prematurely.