Hilbert's -operator, a foundational device for forming indefinite descriptions, has long been overshadowed by standard quantifiers in first-order logic. However, its capacity to eliminate quantifiers and reframe logical derivations makes it a compelling tool for alternative proof strategies and automated reasoning. This paper revisits the -calculus, ofering a streamlined proof of completeness adapted from Hasenjaeger's 1953 approach. Building on earlier work by Leisenring, Davis, and Fechter, we present a variant of the -calculus that omits all predicate symbols aside from equality. The development follows the conventional structure of logical systems-syntax, semantics, and deductive calculus-culminating in a soundness and completeness result. The aim is to reafirm the -operator's relevance in the foundations of logic through a simplified and accessible formal treatment. MS Classification 2020: 03B10, 68V15
Hilbert’s -symbol, despite the key role it played in the historical Hilbert–Bernays treatise [
It is used to form indefinite descriptions of the form . (read: “one such that ”), where
is a formula and a variable. Each such expression is a term denoting an entity—if any exists—that
satisfies ; when no such entity exists, nonetheless . designates some element of the domain
of discourse. As shown, e.g., in [
The completeness proof for first-order predicate logic has progressively simplified from Gödel’s
original (ca. 1930) to Leon Henkin’s (ca. 1949) and later to Gisbert Hasenjaeger’s (1953). We adapt the
third of these to Hilbert’s -calculus, further streamlining the path to this fundamental metalogical
result. Our approach to the -calculus builds on the work of Albert Leisenring [
The material is organized according to the standard structure of most logical formalisms: syntax (Sec. 1), semantics (Sec. 2), calculus (understood as a system of deduction, Sec. 3), and soundness and completeness of the proposed calculus (Sec. 4). The concluding Sec. 5 ofers a commentary on the work presented.
A first-order language ℒ(Λ) is identified by a signature Λ = ( ℱ , d), where d : ℱ →−
N , consisting of a set ℱ of symbols called functors paired with a function d, called degree, sending each functor to its expected number of arguments—a nonnegative integer.
The other primitive symbols of ℒ(Λ) are: the equality relator ‘=’, the denumerable infinity 0, 1, . . . of (free) individual variables, the propositional connectives ‘f’, ‘→’, and the punctuation marks ‘)’, ‘(’, ‘,’.
The terms of ℒ(Λ) are strings of symbols from ℒ(Λ) , defined recursively as follows:
2. A string of the form ( 1, . . . , d()), where ∈ ℱ and 1, . . . , d() are terms, is also a term.
(Here, parentheses are omitted when is a constant, that is, when d() = 0.) The formulae of ℒ(Λ) are strings of symbols from ℒ(Λ) , defined recursively as follows: Atomic formulae are: ∘ Strings of the form 1 = 2, where 1 and 2 are terms of ℒ(Λ) .
∘ The propositional constant f.
Compound formulae are of the form ( → ), where and are formulae, atomic or compound.
(Quite often, the outermost parentheses of a compound formula will be dropped.)
The familiar propositional connectives ¬ , ∨ , & , and ↔ , as well as the inequality relator ̸=, are treated here as derived constructs:
(¬ ) := ( → f), 1 ̸= 2 := ¬ ( 1 = 2), ( ∨ ) := ((¬ ) → ), ( ↔ ) := (( → ) & ( → )).
( & ) := ¬ ( → (¬ )), Later, we will introduce quantifiers by means of somewhat more engaging abbreviations. Definition 1.1 (-adic formula). A formula of ℒ(Λ) is said to be -adic, where ∈ N, if the only variables occurring in are 0, 1, 2, . . . , (namely, the first + 1 variables in the standard list), with the only possible exception of 0 .
Then, ( 0, 1, . . . , ) denotes the formula obtained from by simultaneously replacing each with the corresponding term . ⊣
Definition 1.2 (Key formula). An -adic formula of ℒ(Λ) is called a key formula if:
1. Every term appearing in , if not a variable, contains at least one occurrence of 0.
2. Each of the variables 1, . . . , occurs in exactly once.
3. The variables 1, . . . , appear in from left to right in exactly that order.
⊣
Example 1.1. Set 0 := 0 = 0 and +1 := ( & 0 ̸= +1). Then is a key formula for each . ⊣
Theorem 1.1 (From [
≡ [](, 1, . . . , ) , meaning that and [](, 1, . . . , ) are syntactically identical,1 and such that is the least integer for which such a decomposition exists.
Proof. The following algorithm determines (in the only possible way) the sought , 1, . . . , , and [].
Initially, place a cursor immediately before the first symbol of the first occurrence of a term in , and set := 0.
As long as, in some occurrence after within , there is a term (possibly equal to previous ones) that does not involve , proceed as follows: • Locate the first occurrence (after ) of such a term in . • Set := + 1 and record := along with the position of this occurrence. • Advance the cursor to the end of this occurrence of in .
• replacing with 0, • and, for each = 1, . . . , , replacing, at position , the occurrence of with the variable .
This yields the desired decomposition, where is minimal. Moreover, the triple (︀ , [], ( 1, . . . , )︀) is uniquely determined by and , due to the syntactic nature of the construction.
Example 1.2. Given ≡ ︀( = (, ) → (, ) = (, ))︀ , where , , stand for distinct variables and , are functors of degree 2, the algorithm just seen produces [] ≡ (︀ 0 = ( 0, 0) → 1 = 2)︀ ,
so that ≡ [](︀ , (, ), (, ))︀ , [] ≡ (︀ 1 = 2 → ( 3, 0) = ( 0, 4)︀) , so that ≡ [](︀ , , (, ), , )︀ , [] ≡ ︀( 1 = 2 → ( 0, 3) = ( 4, 0)︀) , so that ≡ [](︀ , , (, ), , )︀ , and [] ≡ (︀ 1 = 2 → 3 = 4)︀ ,
so that ≡ [](︀ , , (, ), (, ), (, ))︀ , where is any variable distinct from , , . Thus, [] is a 2-adic key formula, while [], [], and [] are 4-adic formulae. Note also that, for example, [] is obtained from by replacing both occurrences of with 0, the first occurrence of with 1, the term (, ) with 2, and the first and second occurrences of by 3 and 4, respectively. This clearly shows that the construction of key formulae is based on the positions of terms within the syntactic structure of , as shown in the proof of Thm. 1.1. ⊣ Definition 1.3. Let be a formula, a variable, and a term. We denote by the formula obtained from by simultaneously replacing all occurrences of with . ⊣ Remark 1. The identity ≡ [](, 1, . . . , ) is clear—where 1, . . . , are as described above. ⊣ Remark 2. Let 1 ≡ [] and 2 ≡ [] be an -adic key formula and an -adic key formula, respectively resulting, in the manner described above, from , and from , . Then we have the syntactical identities (¬ )[] ≡ ¬ ︀( [])︀ and ( → )[] ≡ ︀( []( 0, 1, . . . , ) → []( 0, +1, . . . , +))︀ . Moreover, ( ↔ )[] is a (2 + 2 )-adic key formula such that the syntactical identity (, 1, . . . , , 1, . . . , , 1, . . . , , 1, . . . , ) ≡
︀( [](, 1, . . . , ) ↔ [](, 1, . . . , ))︀ , holds for every (1 + + )-tuple (, 1, . . . , , 1, . . . , ) of terms. ⊣ 1‘Syntactical identity’ refers to the condition of being exactly the same in syntactic form—that is, the symbols and their arrangement are identical. However, to claim that ≡ , one must first remove any derived constructs (i.e., shortcuts, or abbreviations defined in terms of more basic symbols) by expanding both and into their full definitions.
Finally, let the Skolem completion Λ ∞ of the initial signature Λ 0 be the signature whose set of functors ℱ ∞ is given by ℱ ∞ := ∪ ℱ ℓ .
ℓ∈N 1. For every -adic key formula of ℒ(Λ ℓ) that does not belong to ℒ(Λ ℓ− 1) (if ℓ > 0), associate a new functor ℎ of degree d(ℎ ) = . Each such functor is called a Skolem functor.
2. Define ℱ ℓ+1 by adding these Skolem functors ℎ to ℱ ℓ, and extend d accordingly.
Skolem expansions and completion of a signature. Our next goal is to complete, in a minimal way, any initial signature Λ 0 with functors ℱ 0 to a signature Λ ∞ with functors ℱ ∞, where ℱ 0 ⊆ ℱ ∞, so that every key formula of ℒ(Λ ∞) is associated, in an injective manner, with a new functor ℎ of the same degree as . We achieve this by defining an increasing sequence of signatures (Λ ℓ)ℓ∈N, where each Λ ℓ+1 is obtained from Λ ℓ as follows:
. Descriptors and quantifiers. We will now introduce Hilbert’s descriptors , Peano’s descriptors , and the usual quantifiers ∃ and ∀ , where is an individual variable. These can be read, respectively, as: “an such that”, “the such that”, “there is an such that”, and “for every , it holds that”.
Consider a formula of ℒ(Λ ∞). Moreover, let be the key formula [] determined—along with and 1, . . . , —as in Thm. 1.1. We introduce the said derived constructs through the following abbreviating rules: descriptor . or . , or within a subformula of the form (∃ . ) or (∀ . ). In fact, applying a
The formulae of ℒ(Λ ∞) in which no variables occur are called sentences. If a given formula involves descriptors or quantifiers, it is unnecessary to unravel these constructs to establish that it is a sentence. It sufices to check that each apparent occurrence of a variable within it appears within a quantifier ∃ or ∀ to a formula in which occurs decreases the number of variables by 1. This holds because, despite appearances, occurs neither in . nor in .(︀ ¬ )︀ .
Remark 3. Based on Example 1.1, we observe that the expansion of Λ 0 to Λ 1 introduces infinitely many new functors. A similar construction, replacing each variable +1 with a term of the form ℎ ( +1), shows that Λ ℓ+2 is endowed with an infinitely richer collection of functors than Λ ℓ+1. ⊣ and, accordingly, .(¬ ) :=
ℎ¬ ( 1, . . . , ); i.e., (∃ . ) := (︀ ℎ ( 1, . . . , ), 1, . . . , ︀) ; i.e., (∀ . ) := (︀ ℎ¬ ( 1, . . . , ), 1, . . . , ︀) ; → = ))︀ , where is a variable distinct from . :=
ℎ ( 1, . . . , ) (∃ . ) := . , (∀ . ) := .(¬ ) ,
:= .(︀ ∀ .(
The formulae of a language ℒ(Λ) are interpreted using a structure I = (D, F), whose • domain of discourse, D, is a set consisting of at least two so-called individuals; and whose • functor interpretation, F, belongs to ∏︀ DDd() . This means that, for every functor , ∈ℱ
F() : Dd() →−
D is a function sending each d()-tuple of individuals to an individual, for every functor . ⊣ ⊣
We now provide recursive rules for evaluating the terms and formulae of ℒ(Λ) in such a structure. Along with I, since terms may involve variables about which the structure itself says nothing, we must also consider a denumerable sequence N = (0, 1, . . . ) of individuals drawn from D, called a (variable) assignment. This assignment associates to each variable the individual in D. As a preliminar, we introduce the following definition.
Definition 2.1 (Truth-value assignment). Denote by f , t falsehood and truth, respectively. A truth value assignment for ℒ(Λ) is a function T : {formulae of ℒ(Λ) } →− { f , t} such that • T(f) = f ; • T(︀ ( (a) Terms.
→ ))︀ = if T( ) = t then T( ) else t , ⊣ Definition 2.2 (Evaluation rules). Let I = (D, F) be a structure and N an assignment. The evaluation function valI,N(· ) assigns values to syntactic expressions of ℒ(Λ) as follows: for all formulae , . • valI,N( ) := , for each variable ; • valI,N(︀ ( 1, . . . , d())︀) := F()(︀ valI,N( 1) , . . . , valI,N(︀ d()︀) )︀ ,
for each functor and every d()-tuple of terms ( 1, . . . , d()). (b) Atomic formulae.
• valI,N(f) := f ; • valI,N( = ) := if valI,N( ) = valI,N( ) then t else f , for all terms , . (c) Compound formulae.
The evaluation function is extended to compound formulae by structural induction, following the semantics of truth-value assignments given in Definition 2.1. Specifically, we define:
valI,N(( → )) := if valI,N( ) = t then valI,N( ) else t, for each compound formula of ℒ(Λ) of the form ( → ), where and are formulae (atomic or compound). ⊣ Remark 4. The evaluation function valI,N( ) defined above is total on the syntactic expressions of ℒ(Λ) , returning domain elements for terms and truth values for formulae. Its restriction to formulae yields a truth-value assignment in the sense of Definition 2.1. ⊣ The fact that (I, N) models a formula , in the sense that valI,N( ) = t, is also denoted by (I, N) |= .
|= , Moreover, if ∪ { } is a collection of formulae, the notation |= (read: “ is a logical consequence of ”) indicates that (I, N) |= holds for all pairs (I, N) that model each formula in . We say that is valid, written as if (I, N) |= holds for all pairs (I, N) . Clearly, this is the case if T( ) = t holds in every truth-value assignment T; in the latter case, is called a tautology .
Let ℒ(Λ) be a language interpreted by a structure I = (D, F), and let be any formula of ℒ(Λ) . Also, let be an integer that bounds the indices of all variables occurring in , that is, every in satisfies ⩽ . Then, for all D-valued assignments N = (0, 1, . . . ) and N′ = (′0, ′1, . . . ) such that = ′ for = 0, 1, . . . , , we have: (I, N) |= ⇐⇒ (I, N′) |= . (In particular, if is a sentence, then its evaluation is independent of any D-valued assignment.)
This observation justifies the following definition. in . For any (+1)-tuple ⃗ := (0, 1, . . . , ) in D+1, we write Definition 2.3 (Satisfaction by a tuple). Let ℒ(Λ) be a language interpreted by a structure I = (D, F), and let be any formula of ℒ(Λ) . Let be an integer that bounds the indices of all variables occurring (I, ⃗) |= enrichment of the structure I, as explained next. and say that ⃗ satisfies in I to mean that for every assignment N = (0, 1, . . . ) over D such that = for all = 0, . . . , , it holds that (I, N) |= .
Extending the evaluation rules canonically to the Skolem completion ℒ(Λ ∞ ) of ℒ(Λ 0) requires an
As a preliminary step, we equip any structure I = (D, F) with a function c : P(D) →−
D , where P(D) denotes the power set of D, such that: • for every nonempty subset ⊆
D, we have c() ∈ ; • and c(∅) ̸= c(D).
This can be done by a plain application of the Axiom of Choice. The second condition, while arbitrary, ensures that c distinguishes between the empty set and the entire domain—this will be useful in what follows.
We call the resulting triple I(c) = (D, F, c) a selective structure, and refer to c( ) as the associated selection function.
Remark 5 (Why do we need no relator other than equality?). Renouncing structures whose domain of discourse has cardinality 1, as we have done, entails no drawbacks; on the contrary, it ofers an advantage: if we define t := . =
and f := . ̸= , equality, by a functor of the same degree as , constrained to satisfy our semantics will ensure that t ̸= f .2 After that, we can surrogate every relation symbol , except for ︁( ∀ 1 . · · · ︁( ∀ .︀( (1 . . . , )︀ = t ∨ (1 . . . , )︀ = f )︀ ︁) · · · ︁) .
Thus, we can use ( 1, . . . , ︀) = t instead of the atomic formula ( 1, . . . , ) . described below. ℎ in ℱ ℓ+1 ∖ ℱ ℓ:
Next we expand step by step a selective structure I(0c) := (D, F0, c), based on our initial signature Λ 0 := Λ , to its Skolem completion Λ ∞. For each integer ℓ ⩾ 0, obtain I(ℓc+)1 := (D, Fℓ+1, c) from I(ℓc) as Embed Fℓ in Fℓ+1, i.e., put Fℓ+1() := Fℓ() for every functor in ℱ ℓ. Then, for every functor • Determine the number such that the key formula is -adic (and hence d(ℎ ) = ). • For each -tuple ⃗ = (1, . . . , ) in D, consider the (possibly empty) set ⃗ of those elements ∈ D such that ︀( Iℓ, (, 1, . . . , ) ︀) |= . 2We will see in Sec. 2.2 how to evaluate this sentence. Nonetheless, the interpretation we are about to define allows for the evaluation of every formula of ℒ(Λ∞). ⊣ ⊣ • pick as the image (︀ Fℓ+1(ℎ ))︀ (⃗) of ⃗ under the interpretation of ℎ the representative c(⃗) of ⃗, namely, set
︀( Fℓ+1(ℎ ))︀ (⃗) := c(⃗).
Finally, define I∞ = (D, F∞), where F∞ := ℓ∪∈NFℓ.
It is straightforward that for each term or formula in the language ℒ(Λ ∞), there exists a number ℓ such that valIℓ+,N() = valI∞,N() holds for each D-valued sequence N and for all ∈ N. Remark 6 (Why does c disappear in the completed interpretation I∞ ?). It would be pointless to write I(∞c) instead of simply I∞, because c only serves to enable the extension of each Iℓ from the signature Λ ℓ to the next signature Λ ℓ+1. Once the signature reaches the plateau, this auxiliary role of c becomes redundant, because all sentences of ℒ(Λ ∞) can be evaluated in the interpretation (D, F∞). ⊣ Remark 7. Let I∞ = (D, F∞) be the canonical completion of a selective structure (D, F, c), as above. Let be any -adic key formula, for some ∈ N, so that ¬ is also an -adic key formula. For any -tuple ⃗ = (1, . . . , ) in D, we claim that Indeed, since it follows that
︀( F∞(ℎ ))︀ (⃗) ̸= (︀ F∞(ℎ¬ ))︀ (⃗). ⃗ ¬ = ∅ ∩ ⃗ and ⃗ ¬ = D,
∪ ⃗ ︀( F∞(ℎ ))︀ (⃗) = c(⃗) ̸= c(¬⃗ ) = (︀ F∞(ℎ¬ ))︀ (⃗) as claimed. ⊣ Remark 8. We show, in some detail, that for every formula of ℒ(Λ ∞)—where Λ ∞ is the Skolem completion of an initial signature Λ —the formula . ̸= . ¬ is valid. In particular, when ≡ ( = ), we recover the validity of t ̸= f, where t := . = and f := . ̸= , as stated in Remark 5.
Let I∞ = (D, F∞) be the canonical completion of an arbitrary selective structure I(c) := (D, F, c), and let N be an arbitrary variable assignment over D. It sufices to show that
(I∞, N) |= . ̸= . ¬ .
Let be the -adic key formula [] determined—along with and the terms 1, . . . , , none of which involves —as in Thm. 1.1. Then we have . ≡ ℎ ( 1, . . . , ) and .(¬ ) ≡ ℎ¬ ( 1, . . . , ). Define ⃗ := (1, . . . , ) ∈ D, where := valI∞,N( ) for = 1, . . . , . Then: valI∞,N(ℎ ( 1, . . . , )) = F∞(ℎ )(1, . . . , )
̸= F∞(ℎ¬ )(1, . . . , ) = valI∞,N(ℎ¬ ( 1, . . . , )) .
Thus, (I∞, N) |= ℎ ( 1, . . . , ) ̸= ℎ¬ ( 1, . . . , ), namely (I∞, N) |= . ̸= . ¬ . Since both the selective structure I(c) and its canonical completion I∞, as well as the assignment N, were arbitrary, it follows that the formula . ̸= . ¬ is valid. ⊣ 3. Logical Laws, Modus Ponens Rule, and Derivations in the -calculus We will explain how to properly enchain lists of formulae of ℒ(Λ ∞), where Λ ∞ originates from an initial signature Λ 0 in the manner discussed above, so that such a list can be regarded as a derivation in the Λ 0-based -calculus. The components of a derivation are called its steps, each of which is either a logical axiom, a proper axiom, or the immediate consequence of preceding steps. We will group logical axioms under a small number of schemes, referred to as logical laws. The proper axioms pertain to a specific intended use of our logical machinery. A single, historically significant inference rule, known as modus ponens, will sufice for our needs.
Here is a somewhat redundant selection of logical laws drawn from the valid formulae of ℒ(Λ ∞): 0. Tautologies belonging to ℒ(Λ ∞
) — see p. 5. 1. All instances of the equivalential properties of equality: = and = ′ → ( ′ = → = ), where , ′, and are arbitrary terms of ℒ(Λ ∞). 2. All instances of the congruence property of equality. Here 0, 0, 1, 1, . . . , , , and , are terms and a functor of ℒ(Λ ∞); moreover, d() = + 1. 3. Exclusion formulae. These have the form 4. Epsilon formulae. These have the form → . (see Remark 1); that is, more explicitly, [](, 1, . . . , )
→ []( ., 1, . . . , ) , or, even more explicitly, [](, 1, . . . , )
→ [](ℎ ( 1, . . . , ), 1, . . . , ) . associated with during the Skolem completion of the signature.
Here, is a term and a formula of ℒ(Λ ∞). Moreover, [] is the key formula of degree , 1, . . . , are the terms—none of which involves —whose existence and uniqueness are established in Thm. 1.1, such that ≡ [](, 1, . . . , ). The functor ℎ is the one uniquely 5. Leisenring’s axioms (cf. [6, p. 13 and p. 40]. These have the form ︀( ∀ . ( ↔ ) )︀ → . = . , where , , are variables, and and are formulae of ℒ(Λ ∞), neither of which involves . of formulae of ℒ(Λ ∞
) Definition 3.1 (Derivability). Consider a collection ∪ { } of formulae of ℒ(Λ ∞). A finite sequence
= ( 0, 1, . . . , ℓ) one of the following conditions : is called a derivation of from the set of premises when ℓ ≡ and each (for = 0, . . . , ℓ) satisfies Logical axiom: is an instance of one of the logical laws listed above.
implies ⊢ (completeness).
Modus Ponens: There exist indices and such that < , < , and ≡ ( → ) .
The existence of such a list is indicated by the notation ⊢ —or simply ⊢ when = ∅. ⊣
In Sec. 4, we will establish that ⊢ implies |= (soundness) and, conversely, that |=
The -calculus, as introduced in the previous section, enjoys the following crucial metalogical property: Theorem 4.1 (Soundness). Let ∪ { } be a set of formulae of ℒ(Λ ∞). If ⊢ , then |= . follow directly from the validity of every logical axiom.
This claim is proved by induction on the length of a derivation of from . To justify the modus ponens rule, observe that when T(︀ ( → ))︀ = t and T( ) = t hold in a truth-value assignment T, then clearly T( ) = t. It follows that |= (
→ ) and |= imply |= . Soundness will therefore Lemma 4.1. Every logical axiom is valid.
Proof. Let the structure I ∞ = (D, F
∞ in Sec. 2.2, and let the sequence N bind the variables to values in D as described right before Def. 2.1. We must prove that (I∞, N) |= holds for every instance of a logical law, where N is any D-valued sequence. This is readily verified for laws 0, 1, and 2. As for law 3, its validity has already been established in Remark 8. The remaining two laws will be addressed next.
Epsilon formulae. A formula falls under this law if and only if it can be written as ) stem from a selective structure I(c) = (D, F0, c) as discussed 0 ≡ ︁( (, 1, . . . , ) → (︀ ℎ ( 1, . . . , ), 1, . . . , ︀) , ︁) is the functor uniquely associated with in the Skolem completion of the signature. where ≡ ( 0, 1, . . . , ) is an -adic key formula, , 1, . . . , are terms of ℒ(Λ ∞), and ℎ To show that (I∞, N) |= , observe that the implication holds trivially unless
(I∞, N) |= (, 1, . . . , ). (I∞, ⃗) |=
and 0 ∈ ⃗ – , (I∞, ⃗ * ) |= . the tuples ⃗ := (0, 1, . . . , ) and ⃗ – := (1, . . . , ). Then, by Definition 2.3, we have Assume this is the case. Let 0 := valI∞,N( ) and := valI∞,N( ) for = 1, . . . , , and define so that ⃗ – ̸= ∅. Thus, by construction of the canonical completion (see Remark 8), the element c(⃗ – ) belongs to ⃗ – , and so replacing 0 with c(⃗ – ) in ⃗ yields another tuple ⃗ * such that therefore But ⃗ * = (︀ valI∞,N(ℎ ( 1, . . . , )) , 1, . . . , )︀ by definition of the interpretation of ℎ , and (I∞, N) |= (ℎ ( 1, . . . , ), 1, . . . , ).
Hence, (I∞, N) |= , as required.
Leisenring’s formulae. Written explicitly, Leisenring’s axioms take the form ︁( 1(︀ .(¬ ), 1, . . . , ︀) ↔ 2(︀ .(¬ ), 1, . . . , ︀) ︁)
→ ℎ 1 ( 1, . . . , ) = ℎ 2 ( 1, . . . , ) , where: • 1, 2, and are key formulae of ℒ(Λ ∞), with 1 being -adic and 2 being -adic; • 1, . . . , , 1, . . . , are terms of ℒ(Λ ∞); and • is the (2 + 2 )-adic key formula associated, relative to the variable , with the formula 1(, 1, . . . , )
↔ 2(, 1, . . . , ) (Clue: In light of the more compact earlier formulation of these axioms, the guiding idea is that 1 and 2 stand for ( )[] and ( )[], respectively — see Remark 2.) Assuming that
(I∞, N) |= 1(︀ .(¬ ), 1, . . . , ︀) ↔ 2(︀ .(¬ ), 1, . . . , ︀) holds, we proceed to verify that (I∞, N) |=
ℎ 1 ( 1, . . . , ) = ℎ 2 ( 1, . . . , ).
Clearly, we have (I∞, Ñ︀ ) |= 1 ↔ 2( 0, +1, . . . , +), where Ñ︀ is any D-valued sequence whose initial segment (0, 1, . . . , +) consists of the values 0 = valI∞,N( .(¬ )), = valI∞,N( ) for = 1, . . . , , and + = valI∞,N( ), for = 1, . . . , . For each in D, let us denote by N1 and N2 generic D-valued sequences having, respectively, initial segments (, 1, . . . , ) and (, +1, . . . , +); accordingly, we have (I∞, N10 ) |= 1 if and only if (I∞, N20 ) |= 2.
Consider the first ℓ such that 1 and 2 are formulae, and 1, . . . , , 1, . . . , are terms, of ℒ(Λ ℓ). Then, by construction, the set 1 of those in D such that (Iℓ, N1) |= 1 coincides with the set 2 of those in D such that (Iℓ, N2) |= 2 . It easily follows that valIℓ+1, Ñ︀ (ℎ 1 ( 1, . . . , )) = c( 1 ) = c( 2 ) = valIℓ+1, Ñ︀ (ℎ 2 ( 1, . . . , )) and therefore (Iℓ+1, Ñ︀ ) |= ℎ 1 ( 1, . . . , ) = ℎ 2 ( 1, . . . , ), whence (I∞, N) |= ℎ 1 ( 1, . . . , ) = ℎ 2 ( 1, . . . , ), as desired.
In preparation for the completeness proof, let us momentarily digress to check that the -calculus
satisfies all the properties of a Boolean logic, as intended in [
Here are the presupposed notions: Definition 4.1.
A logic is a pair (, ⊢ ) consisting of • a set ̸= ∅ whose elements are called statements and • a relation ⊢ included in P () × , called derivability, which satisfies the following conditions, for all , ∈ : L1. { } ⊢ .
L2. (Monotonicity) ⊢ implies ℬ ⊢ when ⊆ ℬ ⊆ .
L3. (Compactness) ⊢ implies that ℱ ⊢ holds for some finite set ℱ ⊆ .
L4. (Cut) From ⊢ and ℬ ∪ { } ⊢ it follows that ∪ ℬ ⊢ .
Definition 4.2.
A Boolean logic is a quadruple
L
= (, ⊢ , , ⇒ ) • a distinguished statement ∈ , and • a dyadic operation ⇒ : × →−
, which satisfies the following conditions, for all ⊆ and ∈ : B1. (Deduction principle) ⊢
⇒ holds if and only if ∪ { } ⊢ .
B2. (Double negation principle) {(
⇒ ) ⇒ } ⊢ .
The syntactic operation ⇒ is called implication (just like the operation on truth-values denoted by →), and its first and second operands are called its antecedent and consequent, respectively. ⊣ In what follows, assuming that • is the set of all formulae of ℒ(Λ ∞), • ⊢ is the derivability relation ⊢ introduced in Def. 3.1, • is the formula f, and • ⇒ constructs the formula (
→ ) from a given antecedent and consequent , we proceed to verify that the conditions L1.–L4., B1., and B2. are all satisfied.
In fact, • L1., L2., and L3. are immediate; • L4. is almost so; • B2. is derived in three steps: – ( → f) → f , – (( → f) → f) → , and – , which correspond to the premise, a tautology, and the result of modus ponens, respectively. As for B1., assume first that the sequence ( 0, 1, . . . , ℓ) derives ( → ) ≡ ℓ from in the -calculus; then, by adding two more steps— and —at the end, we obtain a derivation of from ∪ { } . To get the converse, suppose that ( 0, 1, . . . , ℓ) is a derivation of from ∪ { } . Inductively, for each = 0, 1, . . . , ℓ, we construct a derivation of → from as follows.
• If ≡ , then → is a tautology; a one-step derivation proves it. • If is a logical axiom or belongs to , then a three-step derivation – , – → ( → ), – → does the job. • If is obtained from preceding steps and → , we concatenate the derivations of (which exist, by the induction hypothesis), and continue with the tautology then conclude as desired, by applying modus ponens twice.
→ and → ( → ) ︀( → ( → )︀) → ︀( ( → ) → ( → )︀) ; In the special case when = ℓ , we obtain a derivation of → from .
This completes the verification of B1., thereby showing that the -calculus is a Boolean logic.
Before recalling three important metalogical propositions, we define: there exist statements in such that ⊬ , i.e., is not derivable from .
Definition 4.3.
A set of statements of a Boolean logic L = (, ⊢ , , ⇒ ) is said to be consistent if ⊣
Here are the announced propositions, whose proofs can be found in [
Lemma 4.2 (Lindenbaum). For every consistent set of statements in a Boolean logic L, there exists . That is, ℳ is consistent, and for satisfying the following conditions: Lemma 4.3. If ⊬ in a Boolean logic L as above, then there exists an assignment T : →− { f , t} • T( ) = f , • T︀(
⇒ )︀ • T( ) = t , for all ∈ .
= if T( ) = t then T( ) else t , for all , in , and stated in Lemma 4.3 sends to t, then ⊢ holds.
Theorem 4.2 (Key theorem for Boolean logics). Let L be a Boolean logic as above. Let be a set of statements, and a statement, in L. If every assignment T : →− { f , t} satisfying the three conditions
Relying on the fact that the -calculus constitutes a Boolean logic—particularly its deduction principle— we conclude with two instructive derivations. These establish standard quantifier equivalences which, though often taken for granted in classical logic, require formal justification within the -calculus.
Recall that, in our notation: ¬ (∃ .(¬ )) from the premise (∀ . ). 4.2.1. Interdeducibility of ¬(∃ . ¬ ) and (∀ . ), and between ¬(∀ . ¬ ) and (∃ . ) We now demonstrate how the -calculus supports two classical equivalences involving quantifiers and negation: the equivalence between universal quantification and the negation of an existential, and vice versa. While these relationships are well known, formalizing them within the -calculus requires careful manipulation of -terms and the use of Leisenring’s axioms. These derivations underscore the expressive power and internal coherence of the -calculus as a Boolean logic.
It is straightforward to derive (∀ . ) from the single premise ¬(∃ .(¬ )) and, conversely, to derive ¬(∃ .(¬ ) ≡ ¬ ¬ ︀( .¬ ︀) and (∀ . ) ≡ .¬ .
Thus, to derive (∀ . ) from {¬(∃ .(¬ )} in the -calculus, it sufices to prove: Since the -calculus is a Boolean logic, by the Deduction Principle B1, this reduces to proving: ︀{ ¬ ¬ ︀( .¬ ︀)}
⊢ .¬ .
This implication is trivially valid, being a tautology—an axiom of type 0.
The converse direction, namely the derivation of ¬(∃ .(¬ )) from {(∀ . )}, follows by a symmetric 3A fully general proof of Lindenbaum’s lemma follows straightforwardly from the Zorn lemma. A more elementary proof can be given (see, e.g., [7, pp.8–9]) for the case when the set is countable and efectively listable.
We now turn to the more involved equivalence between ¬ (∀ .(¬ )) and (∃ . ). In our notation: ¬ (∀ .(¬ )) ≡ ¬ ¬ .(¬(¬ )) ︁( ︁) and (∃ . ) ≡ . .
To derive (∃ . ) from {︀ ¬ (∀ .(¬ ))}︀ , we aim to prove: {︁ (︁ ¬ ¬ .(¬(¬ )) ︁)}︁
⊢ . .
.(¬(¬ )) . ︀( ¬(¬( .¬ )))︀ ↔ .¬ .
We begin by applying modus ponens to the tautology (︁ (︁ ︁(
︁) premise ¬ ¬ .(¬(¬ )) , obtaining: ¬ ¬ .(¬(¬ )) ︁) → .(¬(¬ )) and the
Now, let := (︀ (¬(¬ )) ↔ )︀ . Then, (︀ ∀.((¬(¬ )) ↔ ))︀ is expressed as: We include in the derivation the tautology (2), along with the following instance of Leisenring’s axiom: (1) (2) (3) (4) (5) (6) Applying modus ponens to (3) and (2) yields:
We rely on the general theorem ︀( ¬(¬( .¬ )))︀ ↔ .¬ ︀)
→ .(︀ ¬(¬( )))︀ = . .
.(︀ ¬(¬( )))︀ = . . ⊢ .(︀ ¬(¬( )))︀ = . → ︁( .(¬(¬ )) → . ︁) , whose proof proceeds by structural induction on .
Applying modus ponens to (5) and (4), we obtain:
.(¬(¬ )) → . .
Finally, from (1) and (6), we derive . by modus ponens, completing the proof.
A symmetric argument shows that ¬ (∀ .¬ ) can likewise be derived from the premise (∃ . ).
Theorem 4.3 (Completeness). Consider a set ∪ { } of sentences of ℒ(Λ ∞). If |= , then ⊢ . of how the D-valued sequence N is chosen.
Proof. Suppose |
= . Let ℰ denote the collection of all logical axioms of ℒ(Λ ∞ tautologies. Now consider a generic truth value assignment T for ℒ(Λ ∞), as defined in Def. 2.1, such that T( ) = t for every in ∪ ℰ . We will show that T( ) = t. It will then follow, by the key theorem for Boolean logics (as presented in Sec. 4.2 and applicable to the -calculus), that ∪ ℰ ⊢ . Since ℰ ) other than consists of logical axioms, we can conclude that ⊢ , as required.
A preliminary step in proving that T( ) = t consists in constructing a selective structure I(c) = 0 (D, F, c) that complies with T in the sense that valI∞,N( ) = T( ) for every formula , independently
As the domain of discourse D of I0 (and, consequently, of I∞), we adopt the quotient of the collection of all terms of ℒ(Λ ∞
) with respect to the equivalence relation ≈ , where ≈ holds between two terms and if and only if T( = ) = t. Each functor in Λ ∞ is interpreted as the function F() that maps every d()-tuple (︀ 1, . . . , d()
︀) of terms to the term (︀ 1, . . . , d()︀) . This definition is well-posed because ︀( 1, . . . , d() ≈ ︀( 1, . . . , d() ︀) ︀) follows from readily.
1 ≈ 1, . . . , d() ≈ d() thanks to the inclusion of all instances of the congruence property of equality among the logical axioms.
The preservation of truth values—namely, the identity valI∞,N( ) = T( )—is proved by a
straighttherefore valI∞,N( ) = t, thanks to hypothesis |= . The sought conclusion T( ) = t follows
1. The version of the -calculus proposed above builds on—but slightly difers from—the one
presented in [
• The restoration of Leisenring’s logical law, which was missing from [
A minor change is the introduction of what we dub exclusion formulae among the logical axioms,
along with a corresponding revision to the semantics.
2. In [
Another simplification consists in postulating, instead of all instances of the reflexive property of equality ( = , where can be any term), only those of the form = , where is a variable. 5. We have formulated exclusion formulae as
However, for the purpose of ensuring completeness, it would sufice to include only restricted instances of such formulae—namely, those of the form
This restricted version captures all cases needed in the completeness proof, while reducing the logical overhead. This contribution was partially supported by the research program PIAno di inCEntivi per la Ricerca di Ateneo 2024/2026 – Linea di Intervento I “Progetti di ricerca collaborativa”, Università di Catania, under the project “Semantic Web of EveryThing through Ontological Protocols” (SWETOP).
The first author is afiliated with the National Centre for HPC, Big Data and Quantum Computing (Project CN00000013, Spoke 10), co-funded by the European Union – NextGenerationEU.
All authors are members of the GNCS (Gruppo Nazionale per il Calcolo Scientifico) of INdAM.
The author(s) have not employed any Generative AI tools.