On Infinitary Gödel logics
Nicholas Pischke





Hoch-Weiseler Str. 46, Butzbach, 35510, Hesse, Germany
pischkenicholas@gmail.com





We study propositional and first-order Gödel logics over infinitary languages which are motivated semantically by corresponding interpretations into the unit interval [0,1]. We provide infinitary Hilbert-style calculi for the particular (propositional and first-order) cases with con-/disjunctions of countable length and prove corresponding completeness theorems by extending the usual Lindenbaum-Tarski construction to the infinitary case for a respective algebraic semantics via complete linear Heyting algebras. We provide infinitary hypersequent calculi and prove corresponding cut-elimination theorems in the Schütte-Tait-style. Initial observations are made regarding truth-value sets other than [0,1].


On Infinitary Gödel logics
    Nicholas Pischke
    December 30, 2023
==========================





§ INTRODUCTION

Infinitary logics in a classical setting go back to <cit.> and over time became influential in various areas of mathematical logic like (finite) model theory, set theory and also formal arithmetic, among others. Model theoretically, they pose an interesting challenge since the usual propositional and first-order properties (like e.g. compactness) become more intertwined with set-theoretic principles (like e.g. large cardinal axioms).

We study infinitary extensions of Gödel logics. In the finitary setting, Gödel logics arose historically from a sequence of propositional finite-valued logics given by Gödel <cit.> to show that intuitionistic logic does not have a finite characteristic matrix. These were extended to an infinite-valued variant by Dummett <cit.> and the whole collection is today especially studied in the context of intermediate logics. Further, Gödel logics have been characterized as one of three main instances of t-norm based fuzzy logics by Hájek <cit.>. First-order versions were first described by Horn <cit.> and later rediscovered by Takeuti and Titani <cit.> under the name of intuitionistic fuzzy logics. The infinitary versions studied here assume a similar position among both the infinitary intermediate and infinitary fuzzy logics and the present work is thus, in that way, also a particular case study of these classes. For that purpose, Gödel logics pose an especially interesting case as they, in the intermediate context, are logics with many classical properties but which, at the same time, are distinct enough from classical or intuitionistic logic to still pose interesting methodical challenges for the adaption of well-known results (e.g. like interpolation). An example of this phenomenon in the infinitary setting is the work <cit.> by Aguilera where he studies analogues of the compactness results for classical infinitary logics in a Gödel setting where, although the classical results stay true modulo appropriate reformulations, the methods of Skolem functions used classically had to be reformulated using a certain theory of fuzzy ultraproducts.

By now, the work <cit.> is the only paper on infinitary Gödel logics and many interesting problems arising from generalizations of the classical case have remained open, like the study of propositional variants, the development of infinitary calculi and appropriate completeness theorems in the propositional and first-order case as well as infinitary structural proof theory, among others. We study all these previously named topics (in variable depth) and in particular prove the relevant completeness and cut-elimination theorems (where one naturally restricts to the instances with conjunctions and disjunctions of countable length and finitary quantifiers like in the classical (see <cit.>) and intuitionistic cases (see <cit.>)). At the end, we consider truth-value sets different than [0,1] and extend the results to some of these cases as well.


§ PROPOSITIONAL INFINITARY GÖDEL LOGICS



 §.§ Syntax and Fragments

Let κ be any cardinal number. The infinitary propositional language associated with κ is given by 

    ℒ_κ:ϕ ::= | x| (ϕ→ϕ)| (ϕϕ)|(ϕϕ)|⋀Φ|⋁Φ

where we have x∈ Var_κ:={x_λ|λ∈κ} and Φ is a set of formulas of size <κ. For the other classical operators, we define


  * ϕ:=ϕ→,

  * ⊤:=,

  * ϕ↔ψ:=(ϕ→ψ)(ψ→ϕ).

Given some formula ϕ, we denote the set of all subformulas (including ϕ) by sub(ϕ) and the set of variables of ϕ by var(ϕ). Both of these naturally extend to sets Γ.

We mostly deal with the special case of κ=ω_1 and in that context, we will mostly write ⋀_i∈ωϕ_i for ⋀{ϕ_i| i∈ω} and ⋁_i∈ωϕ_i for ⋁{ϕ_i| i∈ω} where (ϕ_i)_i∈ω is a countable family of formulas.

Related to that particular instance of κ=ω_1, we will also need the notion of a fragment. These fragments are (possibly countable) sublanguages of ℒ_ω_1 for which a Lindenbaum-Tarski construction is, nevertheless, still possible and they form a cornerstone of the proof of the completeness theorem. While these fragments, in particular the notation ℒ_A, originate from the connection of (classical) infinitary logic with admissible sets in the sense of Barwise <cit.>, we only need and use the following syntactic definition, in similarity to Nadel <cit.> in the context of infinitary intuitionistic logic.

A (distributive) fragment of ℒ_ω_1 is a set ℒ_A⊆ℒ_ω_1 such that


  * ∈ℒ_A,

  * ϕ∈ℒ_A implies sub(ϕ)⊆ℒ_A,

  * ϕ,ψ∈ℒ_A implies ϕ∘ψ∈ℒ_A for ∘∈{,,→},

  * ϕ,⋀_i∈ωϕ_i∈ℒ_A implies ⋀_i∈ω(ϕ→ϕ_i)∈ℒ_A,

  * ϕ,⋁_i∈ωϕ_i∈ℒ_A implies ⋀_i∈ω(ϕ_i→ϕ)∈ℒ_A,

  * ϕ,⋀_i∈ωϕ_i∈ℒ_A implies ⋀_i∈ω(ϕϕ_i)∈ℒ_A.


The important kind of fragments will be countable ones. In particular, we will consider the smallest fragments containing some set of formulas.

For any Γ⊆ℒ_ω_1, there is a smallest (w.r.t. ⊆) distributive fragment frag(Γ) such that Γ⊆frag(Γ). If Γ is countable, then frag(Γ) is also countable. 



 §.§ The Standard Semantics and 𝖦_κ

We now introduce the standard semantics for the language ℒ_κ and the resulting logics of semantic consequence. This standard semantics naturally extends the usual finitary standard semantics for propositional Gödel logics. For Gödel logics, being one of the prime examples of many-valued logics, the first important parameter in that context is that of the truth-value set. We fix this to be [0,1] for the major part of the paper and discuss other choices only in part at the end.

An ℒ_κ-Gödel-evaluation is a function v:ℒ_κ→ [0,1] such that


  * v()=0,

  * v(ϕψ)=min{v(ϕ),v(ψ)},

  * v(ϕψ)=max{v(ϕ),v(ψ)},

  * v(ϕ→ψ)=v(ϕ)⇒ v(ψ) where x⇒ y:=1   if x≤ y,
y   otherwise,

  * v(⋀Φ)=inf{v(ϕ)|ϕ∈Φ},

  * v(⋁Φ)=sup{v(ϕ)|ϕ∈Φ},

for any Φ∪{ϕ,ψ}⊆ℒ_κ.

Given a set of formulas Γ, we write v[Γ]:={v(γ)|γ∈Γ}. The derived notion of semantics consequence is then defined as follows: for Γ∪{ϕ}⊆ℒ_κ, we write Γ_𝖦_κϕ if v[Γ]⊆{1} implies v(ϕ)=1 for any ℒ_κ-Gödel-evaluation v.


We call the set of consequences Γ_𝖦_κϕ the κ-infinitary Gödel logic and denote it by 𝖦_κ. 
For the particular case of 𝖦_ω_1, a main part of the paper is devoted to the study of various proof theoretic formalism for capturing that semantic consequence and we thus continue by introducing the relevant Hilbert-style calculus used later in a corresponding completeness proof.


 §.§ A Proof Calculus for κ=ω_1

The proof calculus for 𝖦_ω_1 which we introduce, denoted by 𝒢_ω_1, is a straightforward combination of a proof calculus for propositional infinitary intuitionistic logic with the (pre-)linearity scheme

    (ϕ→ψ) (ψ→ϕ).

To be concrete, we consider the following system of axiom and rules:


 §.§ The Calculus 𝒢_ω_1



  (IL) a complete set of axioms for propositional intuitionistic logic;[Naturally, we expect the set of axioms to be defined using the connectives ,,→, and to only require modus ponens as an inference rule. For a particular choice, take the schemes -Ax, -Ax, →-Ax, -Ax from <cit.>.]

  (GL) (ϕ→ψ) (ψ→ϕ);

  (ω) ϕ_j→⋁_i∈ωϕ_i, (j∈ω);

  (ω) ⋀_i∈ωϕ_i→ϕ_j, (j∈ω);

  (MP) from ϕ→ψ and ϕ, infer ψ;

  (Rω)_1 from ϕ_i→ψ for all i∈ω, infer ⋁_i∈ωϕ_i→ψ;

  (Rω)_2 from ϕ→ψ_i for all i∈ω, infer ϕ→⋀_i∈ωψ_i.

Further, we consider the extension 𝒢^D_ω_1 which extends the above calculus by the axiom scheme

    D⋀_i∈ω(ϕψ_i)→(ϕ⋀_i∈ωψ_i)

expressing the distributivity of the infinitary operations.
A proof in 𝒢_ω_1 (or 𝒢^D_ω_1) of some ϕ from some assumptions Γ is any function f:α+1→ℒ_ω_1 where α<ω_1 as well as f(α)=ϕ and such that any f(β) is either


  * an instance of an axiom scheme,

  * element of Γ, 

  * the result of (MP) or (Rω)_1, (Rω)_2 with assumptions f(γ) where γ<β.

We write Γ⊢_𝒢_ω_1ϕ (or Γ⊢_𝒢^D_ω_1ϕ, respectively) if there is such a proof.

Relative to some fragment ℒ_A as defined above, we also introduce a restricted notion of derivation: for Γ∪{ϕ}⊆ℒ_A, we write Γ⊢_𝒢_ω_1(ℒ_A)ϕ (or Γ⊢_𝒢^D_ω_1(ℒ_A)ϕ, respectively) if there is a proof f with img(f)⊆ℒ_A.


Note that 𝒢_ω_1(ℒ_A), and thus also 𝒢^D_ω_1(ℒ_A), have the classical Deduction Theorem.

For any Γ∪{ϕ,ψ}⊆ℒ_A, we have 

    Γ∪{ϕ}⊢_𝒢_ω_1(ℒ_A)ψ iff Γ⊢_𝒢_ω_1(ℒ_A)ϕ→ψ.

The same holds for 𝒢^D_ω_1(ℒ_A).



§ FIRST-ORDER INFINITARY GÖDEL LOGICS

For the first-order variant, we assume a standard underlying first-order signature σ consisting of any number of predicate symbols P and functions symbols f. For any such given symbol, we write ar(P) or ar(f), respectively, for its arity (which is assumed to be finite). 

We construct a infinitary language corresponding to cardinals κ≥λ as it is usually done classically as well: assume a set of variables of size κ, given by Var_κ as before, and in that context denote the set of terms over σ and Var_κ by 𝒯_κ(σ). The infinitary language over σ associated with κ,λ is then given by

    ℒ_κ,λ(σ):ϕ::=| P(t_1,…,t_n)| (ϕ→ϕ)| (ϕϕ)|(ϕϕ)|⋀Φ|⋁Φ|∃ Xϕ|∀ Xϕ

where X⊆ Var_κ is a set of size <λ, P∈σ is a predicate symbol with ar(P)=n, t_1,…,t_n∈𝒯_κ(σ) and Φ is a set of formulas of size <κ. We drop the σ if the context is clear or if the choice is arbitrary.

We write free(ϕ) for the set of free variables of ϕ and var(ϕ) for the set of variables of ϕ, free or bound. As before, we write sub(ϕ) for the set of subformulas of ϕ. Further, we write σ(ϕ) for the set of function and predicate symbols occurring in ϕ. These notions straightforwardly extend to sets Γ and we use the same notation there.

Again, the countable case ℒ_ω_1,ω with finite quantifiers will be of particular interest, especially in the context of a completeness theorem, later on. In that case, we consider the existential and universal quantifiers to just quantify one variable at a time and write

    ∃ xϕ or ∀ xϕ

for x∈ Var_ω_1 as usual in that case. Further, we again write ⋀_i∈ωϕ_i for ⋀{ϕ_i| i∈ω} and ⋁_i∈ωϕ_i for ⋁{ϕ_i| i∈ω} where (ϕ_i)_i∈ω is a countable family of formulas. 

On ℒ_κ,λ, we denote the simultaneous substitution of terms t=(t_1,…,t_n) for free variables x=(x_i_1,…,x_i_n) with i_j≠ i_k for j≠ k in a term t by t[t/x] and by ϕ[t/x] for formulas ϕ. Here, we assume that quantifiers are treated by renaming the quantified variable in the sense of

    (Qxϕ)[t/x]:=Qzϕ[(t',z)/(x',x)]

where Q∈{∀,∃} and x' is x with x removed (if it occurs), t' is t with t_j removed when x_i_j=x and z is fresh, i.e. does not occur in ϕ or t.

Similarly to the propositional case, we consider a notion of fragments for ℒ_ω_1,ω by extending the previous properties appropriately to allow for a Lindenbaum-Tarski construction over these fragments also in the first-order case later on.

A (distributive) fragment of ℒ_ω_1,ω is a set ℒ_A⊆ℒ_ω_1,ω together with a set Var_A⊆ Var_ω_1 and a signature σ_A such that 𝒯_A is the set of terms of σ_A using Var_A and


  * ∈ℒ_A,

  * P(t_1,…, t_n)∈ℒ_A for n-ary P∈σ_A and t_i∈𝒯_A,

  * ϕ∈ℒ_A implies sub(ϕ)⊆ℒ_A, var(ϕ)⊆ Var_A and σ(ϕ)⊆σ_A,

  * ϕ,ψ∈ℒ_A implies ϕ∘ψ∈ℒ_A for ∘∈{,,→} and ∃ xϕ,∀ xϕ∈ℒ_A for x∈ Var_A,

  * ϕ∈ℒ_A, t∈𝒯_A implies ϕ[t/x]∈ℒ_A, t[t/x]∈𝒯_A for any t∈(𝒯_A)^n, any x=(x_i_1,…,x_i_n)∈ (Var_A)^n with i_j≠ i_k for j≠ k.

  * ϕ,⋀_i∈ωϕ_i∈ℒ_A implies ⋀_i∈ω(ϕ→ϕ_i)∈ℒ_A,

  * ϕ,⋁_i∈ωϕ_i∈ℒ_A implies ⋀_i∈ω(ϕ_i→ϕ)∈ℒ_A,

  * ϕ,⋀_i∈ωϕ_i∈ℒ_A implies ⋀_i∈ω(ϕϕ_i)∈ℒ_A.

It is additionally assumed that fragments are “saturated" when it comes to variables, in the sense that there are enough variables to find fresh ones given a finite selection of formulas from ℒ_A. More precisely, we want that for any ϕ_1,…,ϕ_n∈ℒ_A, there is a variable y∉var(ϕ_1)∪…∪var(ϕ_n).


For any Γ⊆ℒ_ω_1,ω, there is a smallest (w.r.t. ⊆) distributive fragment frag(Γ) such that Γ⊆frag(Γ). If Γ is countable, then frag(Γ) is also countable.

Note that, for countable Γ, one can even find a countable fragment ℒ_A⊇Γ with a countable Y⊆ Var_A such that var(ϕ)∩ Y is finite for any ϕ∈ℒ_A. So in this case, the saturation of variables is directly satisfied.


 §.§ The Standard Semantics and 𝖦_κ,λ

The standard semantics of infinitary first-order Gödel logics which we want to consider is, like in the propositional case, a straightforward extension of the usual finitary case. Also here, we initially focus on the full real unit interval [0,1] as the corresponding truth-value set.

An ℒ_κ,λ(σ)-Gödel-model is a structure 𝔐 which consists of 


  * a non-empty set M,

  * P^𝔐:M^n→ [0,1] for every n-ary predicate P of σ,

  * f^𝔐:M^n→ M for every n-ary function f of σ.

An ℒ_κ,λ(σ)-Gödel-interpretation is a structure ℑ=(𝔐,v) composed of an ℒ_κ,λ(σ)-Gödel-model 𝔐 together with a function v:Var_κ→ M.

Over such an interpretation ℑ, one naturally defines the value t^ℑ of some term t of 𝒯_κ. Further, we define

    vfX(x):=f(x)   if x∈ X,
    v(x)   otherwise,

for X⊆ Var_κ and functions f:X→ M. We write vmx for the case of X={x} and f(x)=m and also introduce a special notation for finite tuples with

    vmx:=(…(vm_1x_1)…)m_nx_n

where m=(m_1,…,m_n)∈ M^n and x=(x_i_1,…,x_i_n)∈ (Var_κ)^n. We write

    ℑfX:=(𝔐,vfX)

and similarly for singletons and tuples. We also allow empty sets/tuples m, x and set vmx:=v in this case. 

By recursion on ℒ_κ,λ, we construct the evaluation ℑ:ℒ_κ,λ→ [0,1] associated with ℑ:


  * ℑ():=0^𝐀;

  * ℑ(P(t_1,…,t_n)):=P^𝔐(t_1^ℑ,…,t_n^ℑ) for n-ary P;

  * ℑ(ϕψ):=min{ℑ(ϕ),ℑ(ψ)};

  * ℑ(ϕψ):=max{ℑ(ϕ),ℑ(ψ)};

  * ℑ(ϕ→ψ):=ℑ(ϕ)⇒ℑ(ψ);

  * ℑ(⋀Φ):=inf{ℑ(ϕ)|ϕ∈Φ};

  * ℑ(⋁Φ):=sup{ℑ(ϕ)|ϕ∈Φ};

  * ℑ(∀ Xϕ):=inf{ℑfX(ϕ)| f:X→ M};

  * ℑ(∃ Xϕ):=sup{ℑfX(ϕ)| f:X→ M}.

As before, one immediately derives a notion of semantical consequence from the model/interpretation construction and their corresponding evaluations: for Γ∪{ϕ}⊆ℒ_κ,λ, we write Γ_𝖦_κ,λϕ if ℑ[Γ]⊆{1} implies ℑ(ϕ)=1 for any ℒ_κ,λ-Gödel-interpretation ℑ.


We again define the κ,λ-infinitary Gödel logic to be the set of consequences Γ_𝖦_κ,λϕ and in general denote it by 𝖦_κ,λ.


 §.§ A Proof Calculus

The following proof calculus 𝒢_ω_1,ω is obtained by extending the previous proof calculus for the propositional case with appropriate axioms and rules for the quantifiers.


 §.§ The Calculus 𝒢_ω_1,ω



  (IL) a complete set of axiom schemes for propositional intuitionistic logic, in the first-order language;[The same remark as in Section 2.3 applies, in fact one can again just take the schemes -Ax, -Ax, →-Ax, -Ax from <cit.>, now in the first-order language.]

  (GL) (ϕ→ψ) (ψ→ϕ);

  (ω) ϕ_j→⋁_i∈ωϕ_i, (j∈ω);

  (ω) ⋀_i∈ωϕ_i→ϕ_j, (j∈ω);

  (∀ E) ∀ x ϕ→ϕ[t/x];

  (∃ E) ϕ[t/x]→∃ xϕ;

  (MP) from ϕ→ψ and ϕ, infer ψ;

  (Rω)_1 from ϕ_i→ψ for i∈ω, infer ⋁_i∈ωϕ_i→ψ;

  (Rω)_2 from ϕ→ψ_i for i∈ω, infer ϕ→⋀_i∈ωψ_i;

  (∀ I) from ψ→ϕ, infer ψ→∀ xϕ where x∉free(ψ);

  (∃ I) from ϕ→ψ, infer ∃ xϕ→ψ where x∉free(ψ).

As before, we consider an extension 𝒢^D_ω_1,ω obtained by adding the scheme

    D⋀_i∈ω(ϕψ_i)→(ϕ⋀_i∈ωψ_i)

and now additionally also the axiom scheme

    QS∀ x(ψϕ)→ (ψ∀ xϕ) where x∉free(ψ).

The notion of proof immediately transfers to this setting from the propositional case. We write Γ⊢_𝒢_ω_1,ωϕ (or Γ⊢_𝒢^D_ω_1,ωϕ, respectively) if there is such a proof. We define restrictions 𝒢_ω_1,ω(ℒ_A) (or 𝒢^D_ω_1,ω(ℒ_A)) to some fragment ℒ_A of ℒ_ω_1,ω as before.


Note that also both 𝒢_ω_1,ω(ℒ_A) and 𝒢^D_ω_1,ω(ℒ_A) have the classical Deduction Theorem.

For any Γ∪{ϕ,ψ}⊆ℒ_A and ϕ closed, we have 

    Γ∪{ϕ}⊢_𝒢_ω_1,ω(ℒ_A)ψ iff Γ⊢_𝒢_ω_1,ω(ℒ_A)ϕ→ψ.

The same holds for 𝒢^D_ω_1,ω(ℒ_A).



§ L-ALGEBRAS, CHAINS AND ALGEBRAIC SEMANTICS

We follow a similar route to semantic completeness as in the setting of finitary Gödel logics (see in particular <cit.>): we first establish completeness w.r.t. a class of algebras and then construct embeddings from that class into the relevant structures of the intended interpretation. 

More precisely, we first show completeness w.r.t. linearly ordered and sufficiently complete Heyting algebras over countable fragments and then extend this to the Heyting algebra of the real unit interval by embeddings, similar to <cit.>. This approach does not only offer a high degree of modularity but also establishes linear Heyting algebras (with sufficient completeness) as the algebraic semantics for infinitary Gödel logics, in analogy to the finitary case. Once we have established the result with respect to countable fragments, this assumption can be removed over complete algebras like the unit interval.

For that, we need various notions from the theory of Heyting algebras and the next subsection gives a, for reasons of self-containedness, quite detailed account mostly following <cit.> (up to some notation change).


 §.§ Heyting algebras and related notions

A Heyting algebra is a structure 𝐀 = ⟨ A,^𝐀,^𝐀,→^𝐀,0^𝐀,1^𝐀⟩ such that ⟨ A,^𝐀,^𝐀,0^𝐀,1^𝐀⟩ is a bounded lattice with largest element 1^𝐀 and smallest element 0^𝐀 and →^𝐀 is a binary operation with


  * x→^𝐀x=1^𝐀,

  * x^𝐀(x→^𝐀 y)=x^𝐀 y,

  * y^𝐀(x→^𝐀 y)=y,

  * x→^𝐀 (y^𝐀 z)=(x→^𝐀 y)^𝐀(x→^𝐀 z),

where we write a≤^𝐀b for a^𝐀b=a and ^𝐀x:=x→^𝐀0^𝐀. Joins (suprema) and meets (infima) of subsets X are defined as usual and denoted 𝐀 X and 𝐀 X, respectively. If every subset has a join and meet, 𝐀 is called complete. An existing meet 𝐀X is called distributive if

    𝐀x∈ X(y^𝐀x)=y^𝐀𝐀X

for any y∈𝐀 and 𝐀 is called distributive if every meet is distributive.

Two particular types of Heyting algebras, which we will consider in this note are chains, i.e. Heyting algebras where ≤^𝐀 is linear, and L-algebras, i.e. Heyting algebras where (x→^𝐀y)^𝐀(y→^𝐀x)=1^𝐀 for all x,y∈𝐀. We denote the class of all L-algebras by 𝖫, the class of all distributive L-algebras by 𝖣𝖫 and the class of all chains by 𝖢. We write 𝖢𝖢 for the class of countable chains. Naturally, every chain is a distributive L-algebra.


Further, we will need the notion of a filter. A set F⊆𝐀 is a filter for a Heyting algebra 𝐀, if (1) 1∈ F, (2) x,y∈ F implies x^𝐀y∈ F and (3) x∈ F and x≤^𝐀y imply y∈ F. F is called proper if F⊊𝐀 and F is called a prime filter if it is proper and if x^𝐀y∈ F implies x∈ F or y∈ F.


We then can “filter" a Heyting algebra 𝐀 via F: define x≤_F y if x→^𝐀y∈ F for x,y∈𝐀 and x≡_F y if x≤_F y and y≤_Fx. Then ≡_F is a congruence relation on Heyting algebras and thus defines a quotient Heyting algebra 𝐀/F over the set of equivalence classes [a]_F of elements a of 𝐀 over ≡_F.
In particular, “filtering" with a prime filter in L-algebras yields a chain:

If F is a prime filter of some L-algebra 𝐀, then 𝐀/F is a chain. 

The behavior of meets and joins under quotients will be of particular importance later on. For that, we first note the following:

Let 𝐀 be a Heyting algebra. If

    𝐀X and 𝐀Y

exist in 𝐀, then

    𝐀x∈ X(z→^𝐀x)=z→^𝐀𝐀X and 𝐀y∈ Y(y→^𝐀 z)=𝐀Y→^𝐀z

for any z∈𝐀.

A filter F of a Heyting algebra 𝐀 is said to preserve an existing meet

    x=𝐀X

if x∈ F if, and only if x∈ F for all x∈ X.

Further, a homomorphism h:𝐀→𝐁 of Heyting algebras is said to preserve a meet 𝐀X, or a join 𝐀Y, if

    h(𝐀X)=𝐁h[X] or h(𝐀Y)=𝐁h[Y],

respectively.

Suppose 

    𝐀X and 𝐀Y

exist in 𝐀 and F is a filter of 𝐀 which preserves 

    𝐀x∈ X(z→^𝐀x) and 𝐀y∈ Y(y→^𝐀 z)

for any z∈𝐀. Then

    [𝐀X]_F=𝐀/Fx∈ X[x]_F and [𝐀Y]_F=𝐀/Fy∈ Y[y]_F.

Therefore, the canonical map x↦ [x]_F from 𝐀 into 𝐀/F is a Heyting algebra homomorphism which preserves the respective meet and join.


Let 𝐀 be a Heyting algebra and let

    x_n=𝐀X_n

be a sequence of distributive meets in 𝐀. If x,y∈𝐀 with x≰^𝐀y, then there is a prime filter F such that x∈ F, y∉F and such that F preserves the meets given by x_n.

By [0,1]_ℚ and [0,1]_ℝ, we denote the Heyting algebras of all rationals in the unit interval and of the whole unit interval, respectively.

Let 𝐀 be a countable chain. Then there is an embedding, i.e. an injective homomorphism of Heyting algebras

    q:𝐀→[0,1]_ℚ

which preserves all meets and joins of 𝐀.



 §.§ Algebraic Propositional Evaluations for ℒ_ω_1

In this section, we now introduce the actual algebraic generalizations of the ℒ_ω_1-Gödel-evaluations, broadening the domains to fragments and the range to certain Heyting algebras which may be, in a particular way, incomplete. This will be necessary in the approach to completeness chosen here since the Lindenbaum-Tarski algebras later constructed are, in fact, incomplete. 

Let ℒ_A be an arbitrary fragment of ℒ_ω_1 and 𝐀 be a Heyting algebra.

A function v:ℒ_A→𝐀 is an (𝐀-valued) ℒ_A-evaluation if


  * v()=0^𝐀,

  * v(ϕ∘ψ)=v(ϕ)∘^𝐀v(ψ) for ∘∈{→,,},

  * for any ⋀_i∈ωϕ_i,⋁_i∈ωψ_i∈ℒ_A, we have

    v(⋀_i∈ωϕ_i)=𝐀i∈ωv(ϕ_i)

and 

    v(⋁_i∈ωϕ_i)=𝐀i∈ωv(ϕ_i)

such that the corresponding infima/suprema exist.


Given such an evaluation v, we still write v[Γ]:={v(γ)|γ∈Γ} for sets Γ⊆ℒ_A and (𝐀,v)ϕ for v(ϕ)=1^𝐀. We denote the set of all 𝐀-valued ℒ_A-evaluations by 𝖤𝗏(ℒ_A;𝐀).


Using this notion of ℒ_A-evaluations, there is now a natural notion of semantical entailment: let 𝖢𝗅 be a class of Heyting algebras and let Γ∪{ϕ}⊆ℒ_A. We write Γ_𝖢𝗅(ℒ_A)ϕ if

    ∀𝐀∈𝖢𝗅∀ v∈𝖤𝗏(ℒ_A;𝐀)(v[Γ]⊆{1^𝐀} implies v(ϕ)=1^𝐀).

We abbreviate Γ_𝖢𝗅(ℒ_ω_1)ϕ by Γ_𝖢𝗅ϕ.


By transfinite induction on the length of the proof, on quickly verifies the following soundness result:

For any Γ∪{ϕ}⊆ℒ_A:


  * Γ⊢_𝒢_ω_1(ℒ_A)ϕ implies Γ_𝖫(ℒ_A)ϕ,

  * Γ⊢_𝒢^D_ω_1(ℒ_A)ϕ implies Γ_𝖣𝖫(ℒ_A)ϕ.


To form new ℒ_A-evaluations by composition with homomorphisms of Heyting algebras, we now have to additionally require that the existing meets and joins arising from the infinitary connectives are preserved. This is captured in the following lemma.

Let v:ℒ_A→𝐀 be an evaluation of ℒ_A in 𝐀 and let h:𝐀→𝐁 be a Heyting algebra homomorphism which preserves all the meets and joins

    𝐀i∈ωv(ϕ_i) and 𝐀i∈ωv(ψ_i)

for any ⋀_i∈ωϕ_i∈ℒ_A and ⋁_i∈ωψ_i∈ℒ_A. Then h∘ v is an evaluation of ℒ_A in 𝐁.

The proof is rather immediate and thus omitted.


 §.§ Algebraic First-Order Interpretations for ℒ_ω_1,ω

For a similar motivation as in the propositional case, we are also lead to broadening the definitions of models and interpretations for ℒ_ω_1,ω to both arbitrary fragments as domains and Heyting algebras as ranges. For this, let ℒ_A now be a fragment of ℒ_ω_1,ω and 𝐀 again be a Heyting algebra.

An ℒ_A-model is a structure 𝔐 which consists of 


  * a Heyting algebra 𝐀,

  * a non-empty set M,

  * P^𝔐:M^n→𝐀 for every n-ary predicate P of σ_A,

  * f^𝔐:M^n→ M for every n-ary function f of σ_A.

An ℒ_A-interpretation is a structure ℑ=(𝔐,v) where 𝔐 is an ℒ_A-model and v:Var_A→ M.

As before, over some ℒ_A-interpretation ℑ, one naturally defines the value of some term t of 𝒯_A which we still denote by t^ℑ. vmx, vmx and the resulting ℑmx are defined (over Var_A) in the same way as with the standard semantics.

Such a model 𝔐 is called (ℒ_A-)suitable w.r.t. to a variable assignment v:Var_A→ M if for any m∈ M^n, any x∈ (Var_A)^n, corresponding to the interpretation ℑ=(𝔐,vmx) there is a function ℑ:ℒ_A→𝐀 such that


  * ℑ()=0^𝐀,

  * ℑ(P(t_1,…,t_n))=P^𝔐(t_1^ℑ,…,t_n^ℑ) for n-ary P,

  * ℑ(ϕ∘ψ)=ℑ(ϕ)∘^𝐀ℑ(ψ) for ∘∈{,,→},

  * for any ⋀_i∈ωϕ_i,⋁_i∈ωψ_i∈ℒ_A, we have

    ℑ(⋀_i∈ωϕ_i)=𝐀i∈ωℑ(ϕ_i)

and 

    ℑ(⋁_i∈ωϕ_i)=𝐀i∈ωℑ(ϕ_i)

such that the corresponding infima/suprema exist,

  * for any ϕ∈ℒ_A and any x∈ Var_A, we have

    ℑ(∀ xϕ)=𝐀m∈ Mℑmx(ϕ)

and

    ℑ(∃ xϕ)=𝐀m∈ Mℑmx(ϕ)

such that the corresponding infima/suprema exist.


Note that it actually suffices to establish the existence of such an extension only for m and x=(x_i_1,…,x_i_n) where i_j≠ i_k for j≠ k.

We still write ℑ[Γ]:={ℑ(γ)|γ∈Γ} for sets Γ⊆ℒ_A and ℑϕ if ℑ(ϕ)=1^𝐀. 

We denote the class of all models over 𝐀 by 𝖬𝗈𝖽(ℒ_A;𝐀) and if 𝔐 is a model, we write 𝖨𝗇𝗍(ℒ_A;𝔐) for the set of all corresponding interpretations (𝔐,v) such that 𝔐 is suitable for v.


The derived notion of semantic consequence is then given by the following: let 𝖢𝗅 be a class of Heyting algebras and let Γ∪{ϕ}⊆ℒ_A. We write Γ_𝖢𝗅(ℒ_A)ϕ if

    ∀𝐀∈𝖢𝗅∀𝔐∈𝖬𝗈𝖽(ℒ_A;𝐀)∀ℑ∈𝖨𝗇𝗍(ℒ_A;𝔐)(ℑ[Γ]⊆{1^𝐀} implies ℑ(ϕ)=1^𝐀).

It is again straightforward to verify the following soundness result.

For any Γ∪{ϕ}⊆ℒ_A where all formulas from Γ are closed:


  * Γ⊢_𝒢_ω_1,ω(ℒ_A)ϕ implies Γ_𝖫(ℒ_A)ϕ,

  * Γ⊢_𝒢^D_ω_1,ω(ℒ_A)ϕ implies Γ_𝖣𝖫(ℒ_A)ϕ.


As before, we can form new interpretations by composition with Heyting algebra homomorphisms as long as they respect the need meets and joins.

Let 𝔐 be a model over some Heyting algebra 𝐀 which is suitable w.r.t. v:Var_A→ M and let h:𝐀→𝐁 be a Heyting algebra homomorphism which preserves all the meets and joins

    𝐀i∈ωℑ(ϕ_i) and 𝐀i∈ωℑ(ψ_i)

for any ⋀_i∈ωϕ_i∈ℒ_A and ⋁_i∈ωψ_i∈ℒ_A as well as

    𝐀m∈ Mℑmx(ϕ) and 𝐀m∈ Mℑmx(ϕ)

for all ϕ∈ℒ_A and x∈ Var_A and for any interpretation ℑ=(𝔐,vmx) over 𝔐. Then the model h∘𝔐 defined over the same domain with f^h∘𝔐:=f^𝔐 for any function symbol f and P^h∘𝔐:=h∘ P^𝔐 for predicate symbols P is a suitable model w.r.t. v and for any interpretation ℑ=(𝔐,vmx), we have

    h∘ℑ(ϕ)=h(ℑ(ϕ))

for all ϕ∈ℒ_A where h∘ℑ=(h∘𝔐,vmx).



§ A PROPOSITIONAL AND FIRST-ORDER COMPLETENESS THEOREM

We fix a fragment ℒ_A of either ℒ_ω_1 or ℒ_ω_1,ω and all notions, if not explicitly indicated, are to be understood relative to that fragment. Let 𝒢^(D)(ℒ_A) be either 𝒢_ω_1(ℒ_A) or 𝒢^D_ω_1(ℒ_A) in the propositional case or either 𝒢_ω_1,ω(ℒ_A) or 𝒢^D_ω_1,ω(ℒ_A) in the first order case.

We construct, as it is usually done, the Lindenbaum-Tarski algebra of 𝒢^(D)(ℒ_A): given Γ∪{ϕ,ψ}⊆ℒ_A, we write ϕ≼^Γψ if

    Γ⊢_𝒢^(D)(ℒ_A)ϕ→ψ

and write ϕ≡^Γψ if

    ϕ≼^Γψ and ψ≼^Γϕ.

We write [ϕ]^Γ for the equivalence class of ϕ under ≡^Γ and ℒ_A/≡^Γ for the set of all equivalence classes. In the following, we even omit the Γ when the context is clear. The Lindenbaum-Tarski algebra 𝐋𝐓^Γ is defined as

    𝐋𝐓^Γ:=⟨ℒ_A/≡^Γ,^𝐋𝐓,^𝐋𝐓,→^𝐋𝐓,0^𝐋𝐓,1^𝐋𝐓⟩

where we define


  * [ϕ]^𝐋𝐓[ψ]:=[ϕψ],

  * [ϕ]^𝐋𝐓[ψ]:=[ϕψ],

  * [ϕ]→^𝐋𝐓[ψ]:=[ϕ→ψ],

  * 0^𝐋𝐓:=[],

  * 1^𝐋𝐓:=[⊤].

Further, the order induced on 𝐋𝐓^Γ is given by [ϕ]≤^𝐋𝐓[ψ] iff ϕ≼^Γψ

𝐋𝐓^Γ is a well-defined L-algebra with

    𝐋𝐓i∈ω[ϕ_i]=[⋀_i∈ωϕ_i] and 𝐋𝐓i∈ω[ψ_i]=[⋁_i∈ωψ_i]

for ⋀_i∈ωϕ_i,⋁_i∈ωψ_i∈ℒ_A. In the case of 𝒢^D(ℒ_A), the meets

    [χ]→^𝐋𝐓[⋀_i∈ωϕ_i]=𝐋𝐓i∈ω([χ]→^𝐋𝐓[ϕ_i]) and [⋁_i∈ωψ_i]→^𝐋𝐓[χ]=𝐋𝐓i∈ω([ψ_i]→^𝐋𝐓[χ])

are distributive for every additional χ∈ℒ_A. Further, we have

    [∀ xϕ]=𝐋𝐓t∈𝒯_A[ϕ[t/x]] and [∃ xϕ]=𝐋𝐓t∈𝒯_A[ϕ[t/x]].

for ϕ∈ℒ_A and x∈ Var_A in the first-order case and in the case of 𝒢^D_ω_1,ω(ℒ_A), the meets

    [χ]→^𝐋𝐓[∀ xϕ]=𝐋𝐓t∈𝒯_A([χ]→^𝐋𝐓[ϕ[t/x]]) and [∃ xϕ]→^𝐋𝐓[χ]=𝐋𝐓t∈𝒯_A([ϕ[t/x]]→^𝐋𝐓[χ]).

are distributive for every additional χ∈ℒ_A.


We skip the finitary operations. Using the axiom scheme (GL), it is easy to see that 𝐋𝐓^Γ is a well-defined L-algebra. We only show the infinitary claims. For that, let ⋀_i∈ωϕ_i∈ℒ_A and ⋁_i∈ωψ_i∈ℒ_A. Then, we have

    𝒢^(D)(ℒ_A)⊢⋀_i∈ωϕ_i→ϕ_j and 𝒢^(D)(ℒ_A)⊢ψ_j→⋁_i∈ωψ_i

for any j by axioms (ω) and (ω) which gives 

    [⋀_i∈ωϕ_i]≤^𝐋𝐓[ϕ_j] and [ψ_j]≤^𝐋𝐓[⋁_i∈ωψ_i]

for any j. Suppose that [χ]≤^𝐋𝐓[ϕ_j] for any j and [ψ_j]≤^𝐋𝐓[χ'] for any j. Therefore, we have

    Γ⊢_𝒢^(D)(ℒ_A)χ→ϕ_j and Γ⊢_𝒢^(D)(ℒ_A)ψ_j→χ'

for any j which implies

    Γ⊢_𝒢^(D)(ℒ_A)χ→⋀_i∈ωϕ_i and Γ⊢_𝒢^(D)(ℒ_A)⋁_i∈ωψ_i→χ'

by (Rω)_1,2 which is

    [χ]≤^𝐋𝐓[⋀_i∈ωϕ_i] and [⋁_i∈ωψ_i]≤^𝐋𝐓[χ'].

This gives that

    𝐋𝐓i∈ω[ϕ_i]=[⋀_i∈ωϕ_i] and 𝐋𝐓i∈ω[ψ_i]=[⋁_i∈ωψ_i].


Next, we show that all the mentioned meets are distributive. Let χ,ξ∈ℒ_A be arbitrary. We have

    ⋀_i∈ω(ξ(ψ_i→χ))∈ℒ_A and ⋀_i∈ω(ξ(χ→ϕ_i))∈ℒ_A.

by the closure properties of ℒ_A. Write (α_i)_i for either (χ→ϕ_i)_i or (ψ_i→χ)_i. Now, we get

    [ξ]^𝐋𝐓𝐋𝐓i∈ω[α_i]≤^𝐋𝐓[ξ]^𝐋𝐓[α_j]

for any j by axiom (ω) and therefore 

    [ξ]^𝐋𝐓𝐋𝐓i∈ω[α_i]≤^𝐋𝐓𝐋𝐓i∈ω([ξ]^𝐋𝐓[α_i])=[⋀_i∈ω(ξα_i)].

Further, by axiom scheme (D), we have

    Γ⊢_𝒢^D(ℒ_A)⋀_i∈ω(ξα_i)→(ξ⋀_i∈ωα_i)

which gives the converse

    [⋀_i∈ω(ξα_i)]≤^𝐋𝐓[ξ]^𝐋𝐓𝐋𝐓i∈ω[α_i],

i.e. combined we have

    [ξ]^𝐋𝐓𝐋𝐓i∈ω[α_i]=[⋀_i∈ω(ξα_i)].


In the first-order case, the quantifier claims can be proved as outlined in <cit.>. We still sketch the proof here for self-containedness.

For the first two quantifier claims, note that we have

    Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)∀ xϕ→ϕ[t/x] and Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)ϕ[t/x]→∃ xϕ

for any t∈𝒯_A by the axioms (∀ E) and (∃ E). Now, suppose that χ∈ℒ_A is such that

    Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)χ→ϕ[t/x] for all t∈𝒯_A or Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)ϕ[t/x]→χ for all t∈𝒯_A.

Then, pick y∈ Var_A with y∉var(χ)∪var(ϕ). Note that this is possible as fragments are saturated for variables. By assumption, we have

    Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)χ→ϕ[y/x] or Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)ϕ[y/x]→χ

and as y is not free in χ, we get 

    Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)χ→∀ yϕ[y/x] or Γ⊢_𝒢^(D)_ω_1,ω(ℒ_A)∃ yϕ[y/x]→χ

via the rule (∀ I) and (∃ I). As we have

    ⊢_𝒢^(D)_ω_1,ω(ℒ_A)∀ yϕ[y/x]↔∀ xϕ and ⊢_𝒢^(D)_ω_1,ω(ℒ_A)∃ yϕ[y/x]↔∃ xϕ,

the claims follow.


Regarding distributivity, let ϕ∈ℒ_A and x∈ Var_A as well as χ,ξ∈ℒ_A. Further, let y∈ Var_A with y∉var(ϕ)∪var(χ)∪var(ξ) (note again variable saturation). Then, we have

    ⊢_𝒢^(D)_ω_1,ω(ℒ_A)ϕ[t/x]↔ϕ[y/x][t/y]

and therefore, defining ϕ':=ϕ[y/x], we have [ϕ[t/x]]=[ϕ'[t/y]]. Since y does not occur in χ, we have

    χ→ϕ'[t/y]=(χ→ϕ')[t/y]=:α^∀[t/y]

and

    ϕ'[t/y]→χ=(ϕ'→χ)[t/y]=:α^∃[t/y]

and therefore, since y also does not occur in ξ, the previous quantifier claims imply (where we write α for either α^∃ or α^∀):

    𝐋𝐓t∈𝒯_A([ξ]^𝐋𝐓[α[t/y]])   =𝐋𝐓t∈𝒯_A[(ξα)[t/y]]
       =[∀ y(ξα)].

Using the distributivity axiom, as y again does not occur in ξ, we get 

    [∀ y(ξα)]   =[ξ∀ yα]
       =[ξ]^𝐋𝐓𝐋𝐓t∈𝒯_A[α[t/y]]

and finally we have

    𝐋𝐓t∈𝒯_A[ξ]^𝐋𝐓([χ]→^𝐋𝐓[ϕ[t/x]])=[∀ y(ξα^∀)]=[ξ]^𝐋𝐓𝐋𝐓t∈𝒯_A([χ]→^𝐋𝐓[ϕ[t/x]])

and

    𝐋𝐓t∈𝒯_A[ξ]^𝐋𝐓([ϕ[t/x]]→^𝐋𝐓[χ])=[∀ y(ξα^∃)]=[ξ]^𝐋𝐓𝐋𝐓t∈𝒯_A([ϕ[t/x]]→^𝐋𝐓[χ]).


In the propositional case, there is a canonical ℒ_A-evaluation over 𝐋𝐓^Γ, ι:ℒ_A→𝐋𝐓^Γ, which is defined by

    ι(ϕ):=[ϕ].

By Lemma <ref>, ι indeed is a well-defined ℒ_A-evaluation.


In the first-order case, this Lindenbaum-Tarski algebra now forms the algebraic part of the Lindenbaum-Tarski model: define 𝔏𝔗^Γ as a model with 𝐋𝐓^Γ as the underlying Heyting algebra and with 𝒯_A as the domain by setting

    f^𝔏𝔗(t_1,…,t_n):=f(t_1,…,t_n) as well as P^𝔏𝔗(t_1,…,t_n):=[P(t_1,…,t_n)]

for functions symbols f and predicate symbols P of ℒ_A. We define the canonical variable assignment

    ι:Var_A→𝒯_A,  x↦ x

and denote it, for convenience, also by ι but the context will make it clear whether we mean the propositional evaluation or the first-order variable assignment.

First note that 𝔏𝔗^Γ is indeed suitable for ι.

The model 𝔏𝔗^Γ is a suitable model w.r.t. ι. In particular, given some t=(t_1,…,t_n)∈(𝒯_A)^n and x=(x_i_1,…,x_i_n)∈ (Var_A)^n with i_j≠ i_k for j≠ k, it holds that

    (𝔏𝔗^Γ,ιtx)(ϕ)=[ϕ[t/x]].

for any ϕ∈ℒ_A.


Consider (𝔏𝔗^Γ,ιtx) for x and t as required. By Remark <ref>, showing that ϕ↦ [ϕ[t/x]] is the extension of (𝔏𝔗^Γ,ιtx) for those t,x is enough to establish suitability.

Note first that we have 

    s^(𝔏𝔗^Γ,ιtx)=s[t/x]∈𝒯_A

for any s∈𝒯_A as by assumption, 𝒯_A is closed under substitution. The theorem is then proved by induction on ϕ. By the above result for terms, we get

    [P(s_1,…,s_n)[t/x]]=[P(s_1[t/x],…,s_n[t/x])]=P^(𝔏𝔗^Γ,ιtx)(s_1^(𝔏𝔗^Γ,ιtx),…,s_n^(𝔏𝔗^Γ,ιtx)).

Further, we in particular have [[t/x]]=[] and this provides the result for the atomic cases. The cases for ϕ∘ψ∈ℒ_A with ∘∈{,,→} follow just by noting that ·[t/x] distributes over ∘ and by considering the definitions of ∘^𝐋𝐓.

The same also holds true for ⋀_i∈ωϕ_i∈ℒ_A where we have

    [(⋀_i∈ωϕ_i)[t/x]]=[⋀_i∈ωϕ_i[t/x]]=𝐋𝐓i∈ω[ϕ_i[t/x]]

and similarly for ⋁_i∈ωϕ_i∈ℒ_A where we have used Lemma <ref>. This gives the infinitary cases.

Lastly, let ϕ∈ℒ_A and x∈ Var_A. Then, we have

    [(∀ xϕ)[t/x]]=[∀ zϕ[(t',z)/(x',x)]]

where z and x',t' are as in the definition of first-order substitutions. Using Lemma <ref>, we get

    [∀ zϕ[(t',z)/(x',x)]]=𝐋𝐓t∈𝒯_A[ϕ[(t',z)/(x',x)][t/z]]=𝐋𝐓t∈𝒯_A[ϕ[(t',t)/(x',x)]].

Using similar reasoning, one can show 

    [(∃ xϕ)[t/x]]=𝐋𝐓t∈𝒯_A[ϕ[(t',t)/(x',x)]]

in the existential case. This gives the quantifier cases by noting that 

    (ιtx)tx=ι(t',t)(x',x).


This immediately yields completeness theorems for 𝒢_ω_1(ℒ_A) or respectively 𝒢_ω_1,ω(ℒ_A) w.r.t. L-algebras:

Let ℒ_A be any fragment of ℒ_ω_1 or ℒ_ω_1,ω. For any Γ∪{ϕ}⊆ℒ_A (with Γ closed in the first-order case), the following are equivalent:


  * Γ⊢_𝒢(ℒ_A)ϕ;

  * Γ_𝖫(ℒ_A)ϕ.

Here, we write 𝒢 for either 𝒢_ω_1 or 𝒢_ω_1,ω, respectively.


“(1) implies (2)" is contained in Lemma <ref> or Lemma <ref>, respectively. For the converse, suppose Γ⊬_𝒢(ℒ_A)ϕ and construct the Lindenbaum-Tarski algebra 𝐋𝐓^Γ as indicated above. 

Then Lemma <ref> gives that ι is a well-defined 𝐋𝐓^Γ-valued ℒ_A-evaluation in the propositional case and by construction, we have ι[Γ]⊆{1^𝐋𝐓} but ι(ϕ)≠1^𝐋𝐓. Therefore Γ_𝖫(ℒ_A)ϕ as 𝐋𝐓^Γ is an L-algebra.

In the first-order case, we construct the Lindenbaum-Tarski model 𝔏𝔗^Γ as above which is suitable w.r.t. ι by Lemma <ref>. Again by Lemma <ref>, the underlying algebra 𝐋𝐓^Γ is a well-defined L-algebra and for the corresponding ι, we have

    (𝔏𝔗^Γ,ι)[Γ]⊆ 1^𝐋𝐓 but (𝔏𝔗^Γ,ι)(ϕ)=[ϕ]≠ 1^𝐋𝐓

by Lemma <ref> and therefore Γ_𝖫(ℒ_A)ϕ.

However, restricting to countable fragments even yields a further completeness result for 𝒢^D w.r.t. countable chains and thus, by Lemma <ref>, for [0,1] which is what we will outline next.

Let ℒ_A be a countable fragment of ℒ_ω_1 or ℒ_ω_1,ω. For any Γ∪{ϕ}⊆ℒ_A (with Γ closed in the first-order case), the following are equivalent:


  * Γ⊢_𝒢^D(ℒ_A)ϕ;

  * Γ_𝖣𝖫(ℒ_A)ϕ;

  * Γ_𝖢(ℒ_A)ϕ;

  * Γ_𝖢𝖢(ℒ_A)ϕ;

  * Γ_[0,1]_ℚ(ℒ_A)ϕ;

  * Γ_[0,1]_ℝ(ℒ_A)ϕ.

Here, we again write 𝒢^D for either 𝒢^D_ω_1 or 𝒢^D_ω_1,ω, respectively.


“(1) implies (2)" is contained in Lemma <ref> or Lemma <ref>, respectively . “(2) implies (3)" follows from the fact that every chain is a distributive L-algebra. “(3) implies (4)" and “(4) implies (5)" as well as “(6) implies (5)" and “(1) implies (6)" are also immediate.


We thus only show “(5) implies (1)" and for that, suppose Γ⊬_𝒢^D(ℒ_A)ϕ. Also here, we construct the corresponding Lindenbaum-Tarski algebra 𝐋𝐓^Γ and naturally have [ϕ]≠1^𝐋𝐓. Lemma <ref> again guarantees that 𝐋𝐓^Γ is a well-defined L-algebra and that ι is a well-defined evaluation in the propositional case.

In the first-order case, we again construct the Lindenbaum-Tarski model 𝔏𝔗^Γ over the algebra 𝐋𝐓^Γ and by Lemma <ref>, the model 𝔏𝔗^Γ is suitable w.r.t. ι. With ι as the canonical variable assignment, we also get

    (𝔏𝔗^Γ,ι)(ψ) = [ψ]

by the same result.

Lemma <ref> now yields that any of the meets

    𝐋𝐓i∈ω([χ]→^𝐋𝐓[ϕ_i])=[χ]→^𝐋𝐓𝐋𝐓i∈ω[ϕ_i] and 𝐋𝐓i∈ω([ψ_i]→^𝐋𝐓[χ])=𝐋𝐓i∈ω[ψ_i]→^𝐋𝐓[χ]

and additionally, in the first-order case, any of the meets

    𝐋𝐓t∈𝒯_A([χ]→^𝐋𝐓[ϕ[t/x]])=[χ]→^𝐋𝐓[∀ xϕ] and 𝐋𝐓t∈𝒯_A([ϕ[t/x]]→^𝐋𝐓[χ])=[∃ xϕ]→^𝐋𝐓[χ]

are distributive for any χ,⋀_i∈ωϕ_i,⋁_i∈ωψ_i,ϕ∈ℒ_A and x∈ Var_A.

As ℒ_A is countable, we can enumerate all of the above (distributive) meets and by Lemma <ref>, there is a prime filter F with [ϕ]∉F and such that F preserves all the above meets (depending on the propositional or first-order case).

As [χ] reaches every element of 𝐋𝐓^Γ, Lemma <ref> gives that the map 

    p_F:𝐋𝐓^Γ→𝐋𝐓^Γ/F, [χ]↦[χ]_F:=[[χ]]_F

is a homomorphism of Heyting algebras with preserves all the meets/joins 

    𝐋𝐓i∈ω[ϕ_i] and 𝐋𝐓i∈ω[ψ_i]

as well as

    𝐋𝐓t∈𝒯_A[ϕ[t/x]] and 𝐋𝐓t∈𝒯_A[ϕ[t/x]]

for any ⋀_i∈ωϕ_i,⋁_i∈ωψ_i,ϕ∈ℒ_A and x∈ Var_A. Further, 𝐋𝐓^Γ/F is a chain as F is a prime filter and 𝐋𝐓^Γ is an L-algebra. 

In the propositional case, Lemma <ref> implies that p_F∘ι is a well-defined ℒ_A-evaluation into 𝐋𝐓^Γ/F with p_F(ι(ϕ))=[ϕ]_F≠ 1^𝐋𝐓/𝐅 as [ϕ]∉F.

In the first-order case, since ϕ[t/x]∈ℒ_A for any ϕ∈ℒ_A, any t∈(𝒯_A)^n and any x∈ (Var_A)^n with i_j≠ i_k for j≠ k, we in particular have that the map p_F preserves the meets and joins

    𝐋𝐓i∈ω[ϕ_i[t/x]] and 𝐋𝐓i∈ω[ψ_i[t/x]]

as well as

    𝐋𝐓t∈𝒯_A[ϕ[t/x][t/x]] and 𝐋𝐓t∈𝒯_A[ϕ[t/x][t/x]].

Since by Lemma <ref>, we have (𝔏𝔗^Γ,ιtx)(ϕ)=[ϕ[t/x]], the map p_F fulfills the premises of Lemma <ref> and therefore, the model p_F∘𝔏𝔗^Γ is suitable for ι with (p_F∘𝔏𝔗^Γ,ιtx)(ϕ)=[ϕ[t/x]]_F.


Lemma <ref> guarantees the existence of an injective Heyting algebra homomorphism

    q:𝐋𝐓^Γ/F→[0,1]_ℚ

which preserves all the meets and joins existing in 𝐋𝐓^Γ/F.

In the propositional case, by Lemma <ref> we have that q∘ (p_F∘ι) is a well-defined ℒ_A-evaluation with (q∘ (p_F∘ι))(ϕ)≠ 1 by injectivity. Naturally, we have (q∘ (p_F∘ι))[Γ]⊆{1} and therefore Γ_[0,1]_ℚ(ℒ_A)ϕ.

In the first-order case, since p_F∘𝔏𝔗^Γ is suitable for ι, this implies that in particular the conditions of Lemma <ref> are met again and therefore, the model

    q∘(p_F∘𝔏𝔗^Γ)

is suitable for ι as well. In particular, we have

    (q∘(p_F∘𝔏𝔗^Γ),ι)(ϕ)=q([ϕ]_F)≠ 1

as q is injective and as [ϕ]∉F, i.e. [ϕ]_F≠ 1^𝐋𝐓^Γ/F.


Let ℒ_A be an arbitrary fragment of ℒ_ω_1 or ℒ_ω_1,ω but let Γ∪{ϕ}⊆ℒ_A be countable with Γ closed in the first-order case. Then, the following are equivalent:


  * Γ⊢_𝒢^D(ℒ_A)ϕ;

  * Γ_𝖣𝖫(ℒ_A)ϕ;

  * Γ_𝖢(ℒ_A)ϕ;

  * Γ_[0,1]_ℝ(ℒ_A)ϕ.

Here, we again write 𝒢^D for either 𝒢^D_ω_1 or 𝒢^D_ω_1,ω, respectively.


The directions “(1) implies (2)",  “(2) implies (3)" as well as  “(3) implies (4)" follow as before. Suppose Γ⊬_𝒢^D(ℒ_A)ϕ. Then, also

    Γ⊬_𝒢^D(ℒ_B)ϕ

for ℒ_B:=frag(Γ∪{ϕ}) since ℒ_B⊆ℒ_A. Since Γ∪{ϕ} is countable, we have that ℒ_B is countable as well. Theorem <ref> gives Γ_[0,1]_ℝ(ℒ_B)ϕ.

Therefore, in the propositional case there is an ℒ_B-evaluation v:ℒ_B→ [0,1] such that v[Γ]⊆{1} but v(ϕ)≠1. Similarly, in the first-order case, there is an interpretation ℑ=(𝔐,v) such that ℑ[Γ]⊆{1} but ℑ(ϕ)=1.

In [0,1]_ℝ (by completeness), every function v:Var_A→ [0,1] has a single extension to an evaluation which we denote here by v. If we set 

    v':p↦v(p)   if p∈ℒ_B,
    0   otherwise,

for p∈ Var_A, then it is easy to see that v'(ψ)=v(ψ) for ψ∈ℒ_B (as v is an ℒ_B-evaluation) and therefore, we have v'[Γ]=1 but v'(ϕ)≠ 1.

On the first-order side, any model over [0,1]_ℝ (again by completeness) is suitable for any variable assignment. We define 𝔐' by f^𝔐':=f^𝔐 and P^𝔐':=P^𝔐 for function symbols f and predicate symbols P in σ_B and otherwise set f^𝔐' and P^𝔐' arbitrary for symbols from σ_A∖σ_B. Further, we define v'(x):=v(x) if x∈ Var_B and set it arbitrary otherwise for x∈ Var_A∖ Var_B. Again, a simple induction shows that

    (𝔐',v')(ψ)=(𝔐,v)(ψ)

for any ψ∈ℒ_B which results in Γ_[0,1]_ℝ(ℒ_A)ϕ.

In particular, for countable Γ (closed, in the first-order case) in the appropriate language, we have

    Γ⊢_𝒢^D_ω_1ϕ iff Γ_𝖦_ω_1ϕ.

as well as

    Γ⊢_𝒢^D_ω_1,ωϕ iff Γ_𝖦_ω_1,ωϕ.

We will actually see later on that the requirement that the set of premises is countable can not be removed.

In the first-order cases, the formulations of the various completeness results require the set of premises Γ to be closed. This is, however, only needed for the soundness result as can be seen by inspecting the various proofs for the converse direction: both the Lindenbaum-Tarski algebra and model do not rely on Γ to be closed and neither do any remaining parts of the above presented completeness proofs.



§ HYPERSEQUENT CALCULI FOR 𝒢^D_Ω_1 AND 𝒢^D_Ω_1,Ω AND CUT-ELIMINATION

We now want to address structural proof theory for infinitary Gödel logics, both for the propositional and first-order instances with operations of countable length. For that, we lift the usual approach towards structural proof theory for Gödel logics via hypersequent calculi (see <cit.>) to the infinitary case and provide cut-elimination theorems.


 §.§ Sequents, Hypersequents and Related Notions

Hypersequents, as introduced by Avron <cit.>, are multisets of sequents and the rules operating on hypersequents then allow for parallel modification of and for “exchange of information" between sequents (as in particular exemplified by the rule (𝖼𝗈𝗆) given by Avron). More formally, let ℒ be either ℒ_ω_1 or ℒ_ω_1,ω. A sequent is a pair

    ΓΔ

of finite multisets Γ and Δ of ℒ-formulas where Δ contains at most one element. We write Γ,Δ for multiset union and denote the multiset formed by (possibly equal) formulas ϕ_1,…,ϕ_n by [ϕ_1,…,ϕ_n]. We simply write ϕ for [ϕ]. A hypersequent is then a multiset of sequents Γ_iΔ_i (1≤ i≤ n) which we denote by

    Γ_1Δ_1|…|Γ_nΔ_n.

In any other way, we follow the notational conventions of <cit.>. In particular, there is a canonical interpretation ℐ of hypersequents as ℒ-formulas: set ℐ(ΓΔ):=⋀Γ→⋁Δ where ⋀Γ (⋁Δ) is the conjunction (disjunction) over all members of Γ (Δ), with the convention that ⋀∅:=⊤ and ⋁∅:=. This ℐ extends to hypersequents by

    ℐ(Γ_1Δ_1|…|Γ_nΔ_n):=⋁_i=1^nℐ(Γ_iΔ_i).

The hypersequent systems which we consider are based on a hypersequent calculus for finitary propositional Gödel logic introduced by Avron <cit.>. This calculus naturally extends the usual sequent calculus for intuitionistic logic, lifted to the hypersequent setting, by a specific rule emulating the prelinearity axiom scheme (ϕ→ψ) (ψ→ψ). Avron's calculus was extended to first-order Gödel logics by Baaz and Zach in <cit.>.


 §.§ The Systems ℋ𝒢^D_ω_1 and ℋ𝒢^D_ω_1,ω

The range of constituting rules for the various hypersequent calculi can be seen in Figure <ref>. They consist of the rules given in <cit.> for a hypersequent calculus for first-order Gödel logic extended by four additional infinitary rules. Following Baaz and Ciabattoni <cit.>, the version of (𝖼𝗈𝗆) given here differs from the one usually given (see e.g. <cit.>) and (similar to <cit.>) this serves some technical purposes in the following cut-elimination proof. For further context, see in particular Remark 2 from <cit.>. Principal formulas are defined as commonly done.

The rules (∀,𝗅) and (∃,𝗋) are supposed to fulfill the eigenvariable condition: the variable a is free and does not occur in the lower hypersequent. We refer with ℋ𝒢^D_ω_1 to all initial, structural, logical and infinitary rules (over the propositional language) and with ℋ𝒢^D_ω_1,ω to ℋ𝒢^D_ω_1 (now over the first-order language) extended with the quantifier rules.


Deductions in the hypersequent calculi are defined by natural infinitary generalizations of the usual definition: deductions are countable (possibly infinite) rooted trees where every node is labeled with a hypersequent and every edge is labeled with a rule such that the arities of the rules are respected and the applications are correct. If d is such derivation with a root hypersequent H, then we write d⊢_ℋ𝒢^D_ω_1,ωH or d⊢_ℋ𝒢^D_ω_1H (depending on the used language and systems). We omit the system if it is arbitrary or clear from the context and then write d⊢ H. We write ⊢ H if there is any derivation d with d⊢ H.


One quickly verifies that the non-atomic version 

    /ϕϕ

of (𝗂𝖽) for arbitrary ϕ is derivable in the systems and that they are complete w.r.t. to the Hilbert-type systems introduced before in the following sense:

For any ϕ∈ℒ_ω_1, ⊢_ℋ𝒢^D_ω_1ϕ if, and only if ⊢_𝒢^D_ω_1ϕ. Similarly for ℒ_ω_1,ω, ℋ𝒢^D_ω_1,ω and 𝒢^D_ω_1,ω.


The only thing we want to remark is that the infinitary distributivity axiom

    D⋀_i∈ω(ϕψ_i)→(ϕ⋀_i∈ωψ_i).

is derivable in the calculus, akin to the analogous derivation of the first order (QS) axiom e.g. given in <cit.>. Concretely, we have the following derivations

ϕϕ
ψ_iψ_i
(𝖼𝗈𝗆)
ϕψ_i|ψ_iϕ
ϕϕ
(,𝗅)
ϕψ_i|ϕψ_iϕ
ψ_iψ_i
(,𝗅)
ϕψ_iψ_i|ϕψ_iϕ
2x(⋀,𝗅)
⋀_i∈ω(ϕψ_i)ψ_i|⋀_i∈ω(ϕψ_i)ϕ

for any i∈ω. Using those as input for (⋀,𝗋), we get

⋮
(⋀,𝗋)
⋀_i∈ω(ϕψ_i)⋀_i∈ωψ_i|⋀_i∈ω(ϕψ_i)ϕ
(_0,𝗋),(_1,𝗋)
⋀_i∈ω(ϕψ_i)ϕ⋀_i∈ωψ_i|⋀_i∈ω(ϕψ_i)ϕ⋀_i∈ωψ_i
(𝖤𝖢)
⋀_i∈ω(ϕψ_i)ϕ⋀_i∈ωψ_i
(→,𝗋).
⋀_i∈ω(ϕψ_i)→ϕ⋀_i∈ωψ_i


For the upcoming proof of the cut-elimination theorem, we introduce versions of the calculi given above which use sets of formulas for sequents and sets of sequents for hypersequents. With this set-version, we follow both Tait <cit.> as well as Baaz and Ciabattoni <cit.> and the advantage is that we can omit both the internal and external contraction rules in the set-version. We still write  ΓΔ for set-sequents where Δ is still at most a singleton and in this context write Γ,Δ for the ordinary union of Γ and Δ. To emphasize the set-version of the hypersequents, we denote the respective objects by G∪{ΓΔ}. 

All the previously introduced rules (besides external and internal contraction) can be naturally reformulated using the set-hypersequents and we use the same naming in theses cases. We write 𝒮ℋ𝒢^D_ω_1 and 𝒮ℋ𝒢^D_ω_1,ω for these set-versions of the previous calculi. We use the same notion of proof defined via countable trees and write d⊢^s_𝒮ℋ𝒢^D_ω_1,ω H or ⊢^s_𝒮ℋ𝒢^D_ω_1H if d is a derivation tree with H as a root set-hypersequent in the respective systems. Again, if we don't want to be specific about the system, we write d⊢^s H. Also, derivations d⊢^s H with additional set-hypersequent assumptions are defined as always. The notion of substitution naturally carries over to sequents, (set-)hypersequents and derivations and we use the same notation as in formulas and terms.


 §.§ Cut-Elimination in the Schütte-Tait Style

We now turn to cut-elimination. Most cut-elimination methods fall into one of two categories: Gentzen style methods <cit.> which remove highest cuts and Schütte-Tait style methods <cit.> which remove most complex cuts (in the sense of occurring logical symbols or a similar complexity measure). The notion of highest cut does not generally result in terminating procedures with systems which have infinitary rules and it is thus not surprising that we opt for a Schütte-Tait style proof.

For proving cut-elimination, we closely follow the argument given in <cit.> by Baaz and Ciabattoni where the authors provide a Schütte-Tait style cut-elimination proof for the calculus which we have used (together with its propositional fragment) as a basis for our infinitary extensions. Naturally, the finitary notions used there have to be appropriately extended to arbitrary countable ordinals and we do this in a similar vein as in Tait's work <cit.>.


Before moving on to the technical results, we will need to introduce various measures on proofs and formulas. For this, we first give a short primer on the relevant notions regarding ordinals. For a general overview over ordinal arithmetic and further notions, see <cit.>. We write + and · for the usual ordinal addition and multiplication. Given a family of ordinals α_i, we write sup^+_iα_i for the smallest ordinal greater than every α_i and sup_iα_i for the smallest ordinal greater or equal than every α_i.

Further, we will need the natural sum and multiplication on ordinals, also called the Hessenberg sum and multiplication (see <cit.>), which we denote by x⊕ y and x⊗ y, respectively. The precise definition for ⊕ and ⊗ can be given using Cantor normal forms, among others, but we will only need certain properties of ⊕, ⊗ and their interplay with sup^+ which we list in the following remark.

⊕ and ⊗ are commutative, associative and monotone in both arguments. Further, we have α⊕ 1=α+1 for any ordinal α and α⊗ (β⊕γ) = (α⊗β)⊕(α⊗γ). We have sup^(+)_i(β⊕α_i)≤β⊕sup^(+)_iα_i and sup^(+)_i(β⊗α_i) ≤ β⊗sup^(+)_iα_i where sup^(+) is either sup or sup^+.

There is a notion of exponentiation derived from natural multiplication, first considered by de Jongh and Parikh <cit.>, which we denote by α^⊗β and call (super-Jacobsthal) exponentiation, following Altman <cit.>. This exponentiation can be formally defined using transfinite recursion by 


  * α^⊗ 0:=1 for any α,

  * α^⊗ (β+1):=α^⊗β⊗α for any α,β,

  * α^⊗β:=sup_γ <βα^⊗γ for any α and any limit ordinal β,

and has, in particular, the following properties: α^⊗β is strictly increasing and continuous in β and

    α^⊗(β⊕γ)=α^⊗β⊗α^⊗γ.

The first two are immediate by the monotonicity of ⊗ and the definition of exponentiation. A proof of the latter can be found in <cit.>.


Inspired by Tait <cit.>, we define the function χ^0(α):=4^⊗α and derived from that, we define χ^z as the function enumerating the common fixed points of χ^w for all w<z. These χ^z are the Veblen iterations of χ^0 which exist (for all countable ordinals) by <cit.> as χ^0 is continuous and strictly increasing. Further, all χ^z are also continuous and strictly increasing.


We define the complexity |ϕ| of ϕ∈ℒ_ω_1 recursively by


  * |ϕ| := 0 for atomic ϕ,

  * |ϕ∘ψ| := max{|ϕ|,|ψ|}+1,

  * |⋀_i∈ωϕ_i|:=|⋁_i∈ωϕ_i|:=sup^+_i∈ω|ϕ_i|.

|·| is extended to ℒ_ω_1,ω by adding the clause



  * | Qxϕ|:=|ϕ|+1,

for Q∈{∀,∃}.


Let d be a derivation (of normal or set-hypersequents) with d_i, i<k≤ω, as its direct predecessors (i.e., those subderivations proving the assumptions of the last rule in d as the direct subderivations from <cit.>). As natural generalizations of the notions defined in <cit.> (and in some way akin to <cit.>) we set | d|:=sup^+_i<k| d_i| if the last rule was not a weakening and | d| :=| d_0| otherwise. We define w(d):=sup_i<kw(d_i) if the last rules was not an internal weakening and w(d):=w(d_0)+1 otherwise. Similarly, we define W(d) by using external instead of internal weakenings. 

Lastly, we recursively define ρ(d) by


  * ρ(d):=0 if d is cut-free,

  * ρ(d):=sup_i<kρ(d_i) if the last inference is not a cut,

  * ρ(d):=max{|ϕ|+1,ρ(d_0),ρ(d_1)} if the last inference is a cut with cut-formula ϕ.

| d| is called the rank of d and ρ(d) is called the cut-degree of d. All of these naturally extend to derivations with assumptions.

If d⊢^s H, then d[t/x]⊢^s H[t/x] with | d[t/x]|=| d| and ρ(d[t/x])=ρ(d).

It is straightforward to check that d[t/x] is a correct proof since d is. Both d[t/x]⊢^s H[t/x] and the other properties are then immediate.


It is clear that ⊢ and ⊢^s prove essentially the same theorems (modulo applications of contractions) and using the above notions, we can state the following result on the impact of change between ℋ𝒢 and 𝒮ℋ𝒢 on the rank of derivations. For that, we write H^s for the set-hypersequent obtained from a hypersequent H by removing all multiplicities of formulas and sequents (and treating the resulting objects as sets).

Following <cit.>, we call a hypersequent H (1-1-)reduced if no formula occurs more than once in any multiset and if no sequent occurs more than once in the hypersequent. These hypersequents can be naturally seen as set-hypersequents.

Let H be a reduced hypersequent. If d'⊢^s H^s, then there is a d⊢ H with | d|≤ (2⊗| d'|)⊕ w(d') and ρ(d')=ρ(d). Conversely, if d⊢ H, then there is a d'⊢^s H^s with | d'|≤| d| and ρ(d')=ρ(d).

We omit the proof as it is a natural generalization of the respective finitary result of Baaz and Ciabattoni <cit.>.


The proofs which we give in the following rely on a (formal) tracking of the cut formula through the proof based on so-called decorations as introduced by Baaz and Ciabattoni in <cit.>, extended to the infinitary case. 

Given d⊢^s H and given a decoration of H, that is H where some (but not necessarily all) occurrences of a formula ϕ are decorated, denoted by ϕ^*, the decorated version of d is defined by recursion on the tree: if we have a decoration of an occurring hypersequent H', then the premises are decorated according to which rule was used to derive H'. The definitions for the rules (𝖤𝖶), (𝗐,𝗅), (𝗐,𝗋), (𝖼𝗈𝗆) and (𝖼𝗈𝗆) are exactly as in <cit.>. Suppose the rule used is a (possibly infinitary) logical rule with arity k≤ω, i.e. we have

    G∪{Γ_iΔ_i| i<k}/G∪{ΓΔ}.

Then if


  * ϕ is the principal formula of the rule: if ϕ^*∈Γ then ϕ is decorated in Γ_i iff ϕ already occurs in Γ_i.

  * ϕ is not the principal formula of the rule then ϕ is decorated in Γ_i or Δ_i iff it is decorated in Γ or Δ, respectively. 

Further, in both cases, G∖{Γ_iΔ_i| i<k} is decorated as in the conclusion.


The following inversions are valid:


  (i) If d⊢^s G∪{Γ,ϕψΔ}, then there are proofs d_0⊢^s G∪{Γ,ϕΔ} and d_1⊢^s G∪{Γ,ψΔ}.

  (ii) If d⊢^s G∪{Γ,ϕψΔ}, then there is a proof d_0⊢^s G∪{Γ,ϕ,ψΔ}.

  (iii) If d⊢^s G∪{Γϕψ}, then there are proofs d_0⊢^s G∪{Γϕ} and d_1⊢^s G∪{Γψ}.

  (iv) If d⊢^s G∪{Γϕ→ψ}, then there is a proof d_0⊢^s G∪{Γ,ϕψ}.

  (v) If d⊢^s G∪{Γ,∃ xϕΔ}, then there is a proof d_0⊢^s G∪{Γ,ϕ[a/x]Δ}.

  (vi) If d⊢^s G∪{Γ∀ xϕ}, then there is a proof d_0⊢^s G∪{Γϕ[a/x]}.

  (vii) If d⊢^s G∪{Γ,⋁_i∈ωϕ_iΔ}, then there are proofs d_j⊢^s G∪{Γ,ϕ_jΔ} for each j∈ω.

  (viii) If d⊢^s G∪{Γ⋀_i∈ωϕ_i}, then there are proofs d_j⊢^s G∪{Γϕ_j} for each j∈ω.

In any case, we respectively have ρ(d_i)≤ρ (d) and | d_i|≤| d|.


The proof for items (i) to (vi) follows exactly the reasoning of <cit.> for the respective finitary result (see Lemma 4 there). We give the proofs for (vii) and (viii) in the same spirit.


  (vii) We consider a decoration of d starting with G∪{Γ,(⋁_i∈ωϕ_i)^*Δ}. Replace every occurring Γ',(⋁_i∈ωϕ_i)^*Δ' by Γ',ϕ_jΔ'. Delete all the subderivations but the j-th one above any application of (⋁,𝗅) where (⋁_i∈ωϕ_i)^* occurs as a decorated formula and is principle. As all initial hypersequents are atomic, correctness of the resulting d_j can be shown by an induction over | d|⊕ w(d)⊕ W(d). Clearly | d_j|≤| d| and ρ(d_j)≤ρ(d).

  (viii) We consider a decoration of d starting from G∪{Γ(⋀_i∈ωϕ_i)^*}. Replace every occurring Γ'(⋀_i∈ωϕ_i)^* by Γ'ϕ_j and delete all subderivations but the j-th one above any application of (⋀,𝗋) in which (⋀_i∈ωϕ_i)^* occurs decorated and is principle. Again, the correctness of d_j follows by a straightforward induction on | d|⊕ w(d)⊕ W(d) and we have | d_j|≤| d| and ρ(d_j)≤ρ (d) already by construction.



Suppose d⊢^s G∪{Γ,ϕΔ} where ϕ is atomic and not the cut-formula of any cut in d. Then for any Σ, there is a d' with assumption G∪{Σϕ} such that d'⊢ G∪{Γ,ΣΔ} with | d'|≤| d| and ρ(d')≤ρ(d).


The proof can be easily obtained by generalizing the proof of the respective finitary result from <cit.>: Decorate d, starting from G∪{Γ,ϕ^*Δ}, replace any occurring {Γ',ϕ^*Δ'} by {Γ',ΣΔ'} and add G to every set-hypersequent. This tree now needs to be corrected to yield a correct proof. As in <cit.>, weakenings which produce decorated ϕ^* are replaced by (potentially more) weakenings producing Σ. Initial sequents

    /ψψ(𝗂𝖽) and /()

which don't introduce ϕ^* are respectively replaced by 

    /ψψ/G∪{ψψ} and //G∪{}

where we added sufficiently many weakenings to introduce G,
while initial sequents introducing ϕ^* are replaced by G∪{Σϕ} which is an allowed assumption for d'. That proof is now correct as ϕ is not the cut-formula of any cut in d. As weakenings do not lengthen | d|, we get | d'|≤| d| and as we didn't introduce any new cut, we get ρ(d')≤ρ(d).


Suppose d_0⊢^s G∪{Γϕ} and d_1⊢^s G∪{Γ,ϕΔ} with ρ(d_i)≤|ϕ| for i=0,1. Then there is a d⊢^s G∪{ΓΔ} with ρ(d)≤|ϕ| and | d|≤ 2⊗(| d_0|⊕| d_1|).


The proof is a natural extension of the corresponding finitary result from <cit.>. Note that since ρ(d_i)≤|ϕ|, ϕ is not the cut-formula of any cut in d_i.


For ϕ=, decorate d_0 starting from G∪{Γ^*} and replace any {Γ'^*} by {Γ'Δ}. We now have to correct the proof at the points where ^* originates. In this simple case, ^* arises by either an internal or external weakening. The internal weakenings can be either removed if Δ is empty or replaced by an internal weakening with Δ if Δ is nonempty. Similarly, the external weakenings get appropriately replaced.


For atomic ϕ≠, note first that ρ(d_i)≤|ϕ|=0 implies that d_1 and d_0 are cut-free. In particular, ϕ is not the cut-formula of any cut in d_1 and thus, there is a derivation d_1' with assumption G∪{Γϕ} such that

    d_1'⊢^s G∪{ΓΔ}

as well as | d'_1|≤| d_1| and ρ(d_1')=0. We form d by replacing every assumption G∪{Γϕ} with the proof d_0. It is straightforward to check that | d|≤| d_0|⊕| d_1| ≤ 2⊗ (| d_0|⊕| d_1|) and we have ρ(d)=0 by Lemma <ref>.


For ϕ=⋁_i∈ωϕ_i, consider a decoration of d_0 starting from G∪{Γ(⋁_i∈ωϕ_i)^*}. Replace any occurring {Σ(⋁_i∈ωϕ_i)^*} by {Γ,ΣΔ} and add G to every set-hypersequent and Γ to every premise of any sequent. This resulting tree is not a correct proof anymore and we consider the following correction steps on the initial rules and on the rules which introduce a decorated instance of ϕ:


  * Replace any initial rule 

    /ψψ(𝗂𝖽) or /()

by


(𝗂𝖽)
ψψ
G∪{Γ,ψψ}

or


()

G∪{Γ,}

respectively, using sufficiently many applications of (𝖤𝖶).

  * Suppose (⋁_i∈ωϕ_i)^* originates as the principal formula of a logical rule. Then, replace any part of the form

⋮
G'∪{Γ'ϕ_j}
(⋁,𝗋)
G'∪{Γ' (⋁_i∈ωϕ_i)^*}

occurring in the decorated version of d_0 by

⋮
G∪ (G'∪{Γ,Γ'ϕ_j})[Δ/(⋁_i∈ωϕ_i)^*]
⋮  d_1^-1
G∪G'∪{Γ,Γ',ϕ_jΔ}
(𝖼𝗎𝗍)
G∪G'∪{Γ,Γ'Δ}

where d_1^-1 is obtained by Lemma <ref> from d_1⊢ G∪{Γ,⋁_i∈ωϕ_iΔ}. Here, G' is the set-hypersequent G' after the possible internal replacements. In the above presentation, we have suppressed the needed external and internal weakenings as they have no effect on the resulting rank.

  * If (⋁_i∈ωϕ_i)^* originates from an internal weakening, replace any such

⋮
G'∪{Γ'}
(𝗐,𝗋)
G'∪{Γ'(⋁_i∈ωϕ_i)^*}

by 

⋮
G'∪ G∪{Γ'}
(𝗐,𝗋)
G'∪ G∪{Γ,Γ'Δ}

if Δ is nonempty and remove them otherwise.

  * If (⋁_i∈ωϕ_i)^* originates from an external weakening, replace any 

⋮
G'
(𝖤𝖶)
G'∪{Γ'(⋁_i∈ωϕ_i)^*}

by 

⋮
G'∪ G
(𝖤𝖶).
G'∪ G∪{Γ,Γ'Δ}


The resulting proof d is correct as can be verified by transfinite induction on | T|⊕ w(T)⊕ W(T) for subderivations T of d_0. Here, it is important that ϕ is not the cut-formula of any cut.

Furthermore, any newly introduced cut uses one of the ϕ_i as a cut-formula. We thus get, using ρ(d_1^-1)≤ρ(d_1) from Lemma <ref>, that

    ρ(d)≤max{ρ(d_0),ρ(d_1),sup_i∈ω(|ϕ_i|+1)}=max{ρ(d_0),ρ(d_1),^+sup_i∈ω|ϕ_i|}≤|ϕ|

as ρ(d_i)≤|ϕ| for i=0,1 by assumption and |ϕ|=sup^+_i∈ω|ϕ_i| by definition.


Regarding the rank, let T' be the replacement of any rooted sub derivation T of d_0 after the replacement and correction procedure. Then we can prove, by transfinite induction on | T|⊕ w(T)⊕ W(T), that | T'|≤ 2⊗ (| d_1^-1|⊕| T|). 


  * If T is just a single initial rule, then | T'|=| T| as only weakenings were added.

  * If T ends with an application of (⋁,𝗋) which introduces ϕ^* in the annotation, let T_0 be its preceding derivation. Note that T' ends with an application of cut with preceding derivations T_0' and d_1^-1 (modulo additional weakenings). We get

    | T'|   =max{| T_0'|,| d_1^-1|}+1
       ≤max{2⊗(| T_0|⊕| d_1^-1|),| d_1^-1|}+1
       ≤ 2⊗((| T_0|+1)⊕| d_1^-1|)
       =2⊗(| T|⊕| d_1^-1|)

which completes this case. Here, the first inequality follows from the induction hypothesis.

  * If T ends with a weakening which introduces ϕ^*, then we still have | T_0|⊕ w(T_0)⊕ W(T_0)<| T|⊕ w(T)⊕ W(T) and thus, we get

    | T'|=| T_0'|≤ 2⊗ (| d_1^-1|⊕| T_0|)=2⊗ (| d_1^-1|⊕| T|)

as by definition | T_0| =| T| and as only weakenings were added.

  * If the last rule of T does not introduce ϕ^* and is not a weakening, then for the preceding derivations T'_i of T', we have

    | T'|=^+sup_i∈ω| T'_i|≤^+sup_i∈ω2⊗ (| d_1^-1|⊕| T_i|)≤ 2⊗ (| d_1^-1|⊕^+sup_i∈ω| T_i|)=2⊗ (| d_1^-1|⊕| T|).


  * If the last rules does not introduce ϕ^* but is a weakening, then the reasoning is as in case (3).

We in particular thus have (taking d=d_0')

    | d|≤ 2⊗(| d_1^-1|⊕| d_0|)≤2⊗(| d_1|⊕| d_0|)

as | d_1|≤| d_1^-1| by Lemma <ref>.


For ϕ=⋀_i∈ωϕ_i, consider a decoration of d_1 starting from G∪{Γ,(⋀_i∈ωϕ_i)^*Δ}. Replace any occurring {Γ',(⋀_i∈ωϕ_i)^*Δ'} by {Γ',ΓΔ'}, add G to every set-hypersequent and add Γ to the premise of every sequent. This resulting tree is not a correct proof anymore and we consider the following correction steps:


  * For initial rules, this is the same as the previous correction step (1).

  * If (⋀_i∈ωϕ_i)^* originates as the principal formula of a logical rule, then replace any part of the form

⋮
G'∪{Γ',ϕ_jΔ'}
(⋁,𝗋)
G'∪{Γ',(⋀_i∈ωϕ_i)^*Δ'}

of the current proof by

⋮
G∪ (G'∪{Γ,Γ',ϕ_jΔ'}[Γ/(⋀_i∈ωϕ_i)^*]
⋮  d_0^-1
G∪G'∪{Γ,Γ'ϕ_j}
(𝖼𝗎𝗍)
G∪G'∪{Γ,Γ'Δ}

where d_0^-1 is obtained via Lemma <ref> from d_0⊢ G∪{Γ⋀_i∈ωϕ_i}.

  * If (⋀_i∈ωϕ_i)^* originates from an internal weakening, replace any such

⋮
G'∪{Γ'Δ'}
(𝗐,𝗋)
G'∪{Γ',(⋀_i∈ωϕ_i)^*Δ'}

by 

⋮
G'∪ G∪{Γ'Δ'}
G'∪ G∪{Γ',ΓΔ'}

using stepwise internal weakenings for members of Γ.

  * If (⋀_i∈ωϕ_i)^* originates from an external weakening, replace any 

⋮
G'
(𝖤𝖶)
G'∪{Γ',(⋀_i∈ωϕ_i)^*Δ'}

by 

⋮
G'∪ G
(𝖤𝖶)
G'∪ G∪{Γ',ΓΔ'}


As ϕ is again not the cut-formula of any cut in d_1, one can verify the correctness of the resulting proof d by transfinite induction on | T|⊕ w(T)⊕ W(T) of subdervations T of d_1.

Using the same reasoning as before, we also again derive ρ(d)≤|ϕ| as well as | T'|≤ 2⊗ (| d_0^-1|⊕| T|) where T' is the replacement of any rooted subderivation T of d_1 after the replacement and correction procedure, as before. The latter implies | d|≤ 2⊗ (| d_0|⊕| d_1|) as before.


The cases of ϕ=ϕ_0ϕ_1 and ϕ=∃ xϕ_0 are similar to that of ϕ=⋁_i∈ωϕ_i (see <cit.> for the latter). The quantifier case in particular uses Lemma <ref>.

Similarly, the cases of ϕ=ϕ_0ϕ_1, ϕ=∀ xϕ_0 and ϕ=ϕ_0→ϕ_1 are analogous to that of ϕ=⋀_i∈ωϕ_i (see again <cit.> for the last). As with ∃, the ∀-case uses Lemma <ref>.


Let d⊢^s H with ρ(d)≤ v+ω^z. Then there is a derivation d'⊢^s H with | d'|≤χ^z(| d|) and ρ(d')≤ v.


The theorem is proved by induction on the lexicographically ordered pair (z,| d|). So assume the claim for any (ẑ,|d̂|) with ẑ<z or ẑ=z and |d̂|<| d|. We divide the proof on whether the last inference rule of d was a cut, a weakening or neither.


Suppose the last rule was not a cut and not a weakening. Let k≤ω be the arity of the last rule and let d_i, i<k, be the direct predecessors with d_i⊢^sH_i. Naturally, | d_i| <| d| for all i<k as the last rule was not a weakening and also

    v+ω^z≥ρ(d)≥ρ(d_i)

for all i<k by definition. Using the induction hypothesis on d_i, we get derivations d_i'⊢^sH_i with | d_i'|≤χ^z(| d_i|) and ρ(d_i')≤ v. Using the same last rule as in d, we combine the d_i' to a proof d'⊢ H. First, we have ρ(d')≤ v as the last rule was not a cut. Further, we get

    | d_i'|≤χ^z(| d_i|)<χ^z(| d|)

using that | d_i|<| d| and that χ^z is increasing. As | d'| is the least ordinal α with | d'_i| <α for all i, as the last rule was not a weakening, we get | d'|≤χ^z(| d|).


Suppose the last rule was a cut. Then we get two preceding derivations

    d_0⊢^s G∪{Γϕ} and d_1⊢^s G∪{Γ,ϕΔ}

and by definition, we have

    v+ω^z≥ρ(d)=max{|ϕ|+1,ρ(d_0),ρ(d_1)}.

and, as the last rule was not a weakening, we get | d_i| <| d|. We can apply the induction hypothesis to d_0,d_1 to get derivations d'_0⊢^s G∪{Γϕ} and d_1'⊢^s G∪{Γ,ϕΔ} with | d_i'|≤χ^z(| d_i|) and ρ(d_i')≤ v.

If z=0, then ρ(d)≤ v+ω^z=v+1 and therefore |ϕ|≤ v.  Now, either


  (i) max{ρ(d_0'),ρ(d_1')}≤|ϕ|, or 

  (ii) max{ρ(d_0'),ρ(d_1')}>|ϕ|.

For (i), we may apply Lemma <ref> to get a derivation

    d'⊢ G∪{ΓΔ}

with ρ(d')≤|ϕ|≤ v and

    | d'|   ≤ 2⊗(χ^0(| d_0|)⊕χ^0(| d_1|))
       ≤ 2⊗(4^⊗| d_0|⊕ 4^⊗| d_1|)
       ≤ 2⊗ (2⊗ 4^⊗max{| d_0|,| d_1|})
       ≤ 4^⊗(max{| d_0|,| d_1|}+1)
       =4^⊗| d|=χ^0(| d|)

where we in particular used that ⊕ and ⊗ are increasing in both arguments as well as commutative, associative and distributive, that χ^0 is increasing, that α⊕ 1=α+1,  and that max{| d_0|,| d_1|}+1=| d| by definition.

For (ii), we combine d_0' and d_1' using cut on ϕ to a derivation d'⊢ G∪{ΓΔ}. Now, we get

    ρ(d)=max{|ϕ|+1,ρ(d_0'),ρ(d_1')}=max{ρ(d_0'),ρ(d_1')}≤ v

as |ϕ|+1≤max{ρ(d_0'),ρ(d_1')} by the assumption (ii) and as ρ(d_i')≤ v from the induction hypothesis. Further, we have

    | d'|=max{| d_0'|,| d_1'|}+1≤max{4^⊗| d_0|,4^⊗| d_1|}+1≤ 4^⊗| d|=χ^0(| d|)

which completes the case for (ii).


If z≠ 0, then there are y<z and k∈ℕ such that |ϕ|≤ v+ω^y· k. We can combine d_0' and d_1' using cut to a derivation d̂⊢^s G∪{ΓΔ}.

This immediately gives |d̂|≤max{χ^z(| d_0|),χ^z(| d_1|)}+1 and ρ(d̂)≤ v+ω^y· k. As y<z, we can apply the induction hypothesis k-times and get a derivation d'⊢^s G∪{ΓΔ} with ρ(d')≤ v as well as

    | d'|≤ (χ^y)^(k)(max{χ^z(| d_0|),χ^z(| d_1|)}+1)

We have | d_i| <| d| and thus χ^z(| d_i|)<χ^z(| d|) which implies χ^z(| d_i|)+1≤χ^z(| d|). This gives max{χ^z(| d_0|),χ^z(| d_1|)}+1≤χ^z(| d|). 

Now, assuming α≤χ^z(β) and y<z, then

    χ^y(α)≤χ^y(χ^z(β))=χ^z(β)

where the first inequality follows from χ^y being increasing and the latter equality follows from the definition of χ^z(β) being the β-th simultaneous solution for γ=χ^x(γ) for all x<z. This implies, in combination with the above, that

    | d'|≤ (χ^y)^(k)(max{χ^z(| d_0|),χ^z(| d_1|)}+1)≤χ^z(| d|).


From Lemma <ref>, cut elimination immediately follows:

For any derivation d⊢ H, there exists a cut-free derivation d'⊢ H.

Further, we of course get a bound on | d'| which, in the case of finitary proofs with finitary formulas, matches that of Baaz and Ciabattoni <cit.>.


§ THE RANGE OF THE RESULTS AND EXTENSIONS

We want to use this section to give an overview of some other topics extending the previous ones and some initial observations, at varying depth, regarding those.




 §.§ Extensions of the Completeness Results

At first, it should be noted that the completeness theorems for 𝖦_ω_1 and 𝖦_ω_1,ω do not generalize to uncountable sets Γ. Consider the following two notions of compactness from <cit.>:

Let ⊩⊆𝒫(ℒ_κ,λ)×ℒ_κ,λ or ⊩⊆𝒫(ℒ_κ)×ℒ_κ be a relation. Then ⊩ is called


  * weakly compact if for every Γ,ϕ with at most κ many different atomics, there is a Δ with size <κ such that Γ⊩ϕ implies Δ⊩ϕ,

  * compact if for every Γ,ϕ, there is a Δ with size <κ such that Γ⊩ϕ implies Δ⊩ϕ.


Indeed, the relations ⊢_𝒢^(D)_ω_1 and ⊢_𝒢^(D)_ω_1,ω are compact as any proof only involves countably many formulas.

However, as Aguilera shows in <cit.>, the consequence relation _𝖦_ω_1,ω (i.e. _[0,1]_ℝ) is not even weakly compact. This follows from the following general result:

If _𝖦_κ,ω is weakly compact, then κ is weakly compact, i.e. it is strongly inaccessible and any tree of size κ, such that every level has <κ nodes, has a branch of length κ.

As ω_1 is not strongly inaccessible, it is not weakly compact and therefore _𝖦_ω_1,ω is not either.


It turns out that Aguilera's proof is, in itself, “propositional" and can be straightforwardly adapted to 𝖦_κ. We therefore have the following result which implies the same limitation for 𝒢^D_ω_1:

If _𝖦_κ is weakly compact, then κ is weakly compact.

We omit the proof as it is, as hinted above, literally that of Aguilera <cit.>, rephrased in the propositional language.

Before moving on to other topics, we want to mention a peculiar application of the above result of Aguilera and its propositional version. Although we don't dive into the rich (and difficult) topic of interpolation for Gödel logics, we can use the impossibility of a proof calculus for uncountable premises to show the following negative result.

There is no countable Δ⊆ℒ_ω_1,ω such that for any ϕ,ψ∈ℒ_ω_1,ω, _𝖦_ω_1,ωϕ→ψ implies that there is a δ∈Δ with _𝖦_ω_1,ωϕ→δ and _𝖦_ω_1,ωδ→ψ. Similarly for ℒ_ω_1 and 𝖦_ω_1.


Suppose such a Δ would exist. Constructing the Lindenbaum-Tarski algebra over ℒ_ω_1,ω, the set {[δ]|δ∈Δ} would form a countable dense subset of 𝐋𝐓^Γ, even for uncountable Γ. As 𝐋𝐓^Γ is therefore separable, it embeds into [0,1]_ℝ with an embedding preserving infima and suprema. If we assume Γ⊬_𝒢^D_ω_1,ωϕ with said uncountable Γ, then this embedding would provide a countermodel by Lemma <ref>, verifying Γ_𝖦_ω_1,ωϕ. Thus, we would have completeness of 𝒢^D_ω_1,ω for 𝖦_ω_1,ω w.r.t. uncountable Γ which is a contradiction to Proposition <ref>.

The argument works similarly also for the propositional 𝖦_ω_1.

Although it is probably expected that there is no countable set of interpolants in this infinitary case (as we already work over an uncountable language), it is maybe still instructive to note how cardinality considerations can have an impact on these type of questions.


In a similar vein, a generalization of the results to ℒ_ω_1,ω_1 is problematic. As is well-known by a theorem of Scott (and Karp, see <cit.>[As Karp remarks, the proof of hers is based on an outline circulated by Scott in 1960 which was not published.]), the set of classical validities over ℒ_ω_1,ω_1 is not definable in H(ω_1), the collection of hereditarily countable sets, and thus in particular not Σ_1 on H(ω_1), a property which would, however, be implied by the existence of a complete classical proof calculus with proofs of countable lengths. These results should generalize to the Gödel case:

Is the set of theorems of 𝖦_ω_1,ω_1 non-definable over H(ω_1)?

We also want to note that there is a different definition of consequence common in the context of Gödel logics, which we may define by

    Γ^≤_𝖦_κϕ if inf v[Γ]≤ v(ϕ) for any evaluation v

for the propositional infinitary case and similarly in the first-order case by

    Γ^≤_𝖦_κ,λϕ if infℑ[Γ]≤ℑ(ϕ) for any interpretation ℑ.

In a finitary context, it can be easily seen that ^≤ is equivalent to  and we can show a similar statement here if we restrict to countable sets. The following results are thereby natural generalizations of the finitary cases as given in <cit.> and the proofs for both results are essentially the same (and thus omitted).

Let 𝐀 be a complete linear Heyting algebra, x∈ A, and let v:ℒ_κ→𝐀 be any evaluation. Then, for

    v_x(p):=v(p)   if v(p)<^𝐀x,
    1^𝐀   otherwise,

with p∈ Var_κ, the unique extension v_x:ℒ_κ→𝐀 to an evaluation satisfies:

    x∉v[sub(ϕ)] implies v_x(ϕ)=v(ϕ)   if v(ϕ)<^𝐀x,
    1^𝐀   otherwise,

for any ϕ∈ℒ_κ.

The following first-order version is rather intricate to formulate if one wants to guarantee a similar level of generality as in the finitary case. We give it here in its full strength but will, in the following, mostly use the special case with κ=ω_1 and λ=ω where the conditions simplify considerably (in particular the definition of Val_ℑ(ϕ)).

Let 𝐀 be a complete linear Heyting algebra, x∈ A, and let 𝔐 be an 𝐀-valued model. Define 𝔐_x from 𝔐 by replacing P^𝔐 with

    P^𝔐_x(m_1,…,m_n):=P^𝔐(m_1,…,m_n)   if P^𝔐(m_1,…,m_n)<^𝐀x,
    1^𝐀   otherwise,

where P is an n-ary predicate. We write 𝔍_x=(𝔐_x,w) and

    Val_𝔍(ϕ):={𝔍'(ψ)|ψ∈sub(ϕ) and 𝔍'=(…(𝔍f_1X_1)f_2X_2…)f_nX_n
                    where  X_i⊆ Var_κ∩sub(ϕ) with | X_i| <λ and f_i:X_i→ M}.

given an interpretation 𝔍=(𝔐,w). 

Then, for a given v:Var_κ→ M and ℑ=(𝔐,v), we have

    x∉Val_ℑ'(ϕ) implies ℑ'_x(ϕ)=ℑ'(ϕ)   if ℑ'(ϕ)<^𝐀x,
    1^𝐀   otherwise,

for any ϕ∈ℒ_κ,λ and any interpretation

    ℑ'=(…(ℑf_1X_1)f_2X_2…)f_nX_n

where X_i⊆ Var_κ with | X_i| <λ and f_i:X_i→ M.

As a direct consequence, we obtain the following result:

For any countable Γ∪{ϕ}⊆ℒ_ω_1, Γ^≤_𝖦_ω_1ϕ iff Γ_𝖦_ω_1ϕ. Similarly, for any countable Γ∪{ϕ}⊆ℒ_ω_1,ω, we have Γ^≤_𝖦_ω_1,ωϕ iff Γ_𝖦_ω_1,ωϕ.



 §.§ Other Sets of Variables

As common in propositional and first-order Gödel logics, one could consider closed sets V with {0,1}⊆ V⊊ [0,1] instead of [0,1] as truth-value sets, thereby forming the propositional variants 𝖦^V_κ and the first-order variants 𝖦^V_κ,λ by extending the semantic definitions from before. The most common instances of V are among

    V_ℝ:=[0,1],
       V_0:={0}∪[1/2,1],
       V_↓:={1/k| k≥ 1}∪{0},
       V_↑:={1-1/k| k≥ 1}∪{1},
       V_n:={1-1/k| 1≤ k≤ n-1}∪{1} with n≥ 2,

following the selection from <cit.>. In that notation, we have 𝖦_κ=𝖦^V_ℝ_κ and 𝖦_κ,λ=𝖦^V_ℝ_κ,λ. A few easy observations from <cit.> directly carry over to the infinitary case.

Let 𝖦^V be either 𝖦^V_κ or 𝖦^V_κ,λ for arbitrary κ,λ (for λ≤κ). The following relations hold:


  * 𝖦^V_ℝ=⋂_V𝖦^V

  * 𝖦^V_n⊋𝖦^V_n+1

  * 𝖦^V_n⊋𝖦^V_↑⊋𝖦^V_ℝ

  * 𝖦^V_n⊋𝖦^V_↓⊋𝖦^V_ℝ

  * 𝖦^V_0⊋𝖦^V_ℝ.


We omit the proof as it is essentially a replica of the analogous result in the finitary first-order case (see <cit.>). Still, we want to emphasize the following differences to the finitary case: already in the finitary propositional case, 𝖦^V_↑_ω, 𝖦^V_↓_ω and 𝖦^V_0_ω differ in entailment (see <cit.>) while they coincide, as observed first by Dummett <cit.>, in tautologies unlike the finitary first-order versions. So, it is natural that in this infinitary case the propositional (and first-order) versions differ in entailment as well.

But, in the infinitary case, the propositional variants already differ with respect to tautologies and, moreover, the witnessing (non-)tautologies are natural analogues of the finitary first-order examples: consider C^↑:=⋁_i∈ω(p_i→⋀_j∈ωp_j), C^↓:=⋁_i∈ωp_i(⋁_j∈ωp_j→ p_i) and 𝖨𝖲𝖮_0:=⋀_i∈ω p_i→⋀_i∈ωp_i. 

Then C^↑ is valid in 𝖦^V_↑ but not in 𝖦^V_↓.  C^↓ is valid in 𝖦^V_↑ and 𝖦^V_↓. Both are not valid in 𝖦^V_0 and 𝖦^V_ℝ. 𝖨𝖲𝖮_0 is valid in 𝖦^V_0 but not in 𝖦^V_ℝ.


Further, we can give the following analogy of the relationship between 𝖦^V_↑ and the finite-valued 𝖦^V_n.

We have

    𝖦^V_↑_κ=⋂_n≥ 2𝖦^V_n_κ and 𝖦^V_↑_κ,λ=⋂_n≥ 2𝖦^V_n_κ,λ.



Again, let 𝖦^V be either 𝖦^V_κ or 𝖦^V_κ,λ. Item (3) of Proposition <ref> gives

    𝖦^V_↑⊆⋂_n≥ 2𝖦^V_n.

For the converse, suppose that Γ_𝖦^V_↑ϕ, i.e. there is an evaluation v such that v[Γ]⊆{1} but v(ϕ)<1 in the propositional case or an interpretation ℑ such that ℑ[Γ]⊆{1} but ℑ(ϕ)<1 in the first-order case. As v/ℑ evaluate into V_↑, there is a k such that v(ϕ)=1-1k or ℑ(ϕ)=1-1k. Let x∈ [0,1] be such that 1-1k<x<1-1k+1 and

    x∉v[sub(Γ∪{ϕ})]

in the propositional case or such that

    x∉Val_ℑ(Γ∪{ϕ})

in the first-order case. We form v_x or ℑ_x by Lemma <ref> or Lemma <ref>, respectively. The above choice of x is such that v_x[Γ]⊆{1} but v_x(ϕ)<1 in the propositional case and ℑ_x[Γ]⊆{1} but ℑ_x(ϕ)<1 in the first-order case by the previous lemmas. But, by the choice of x, we have that v_x or ℑ_x evaluate into V_k+1 which gives Γ_𝖦^V_k+1ϕ.

By the results of <cit.>, the status quo on complete proof calculi in the finitary setting in very clear cut: 𝖦^V_ω,ω is axiomatizable iff V is finite or uncountable with either 0 contained in the perfect kernel of V or isolated. In particular, already the tautologies of 𝖦^V_↑_ω,ω and 𝖦^V_↓_ω,ω are not recursively enumerable. On the propositional side, while the tautologies of all 𝖦^V_ω are axiomatizable (again, see<cit.>), the only axiomatizable entailment relations are 𝖦^V_n_ω and 𝖦^V_ℝ_ω (see <cit.>).


Now, the situation is different in the infinitary cases. In the following, we will obtain analogous axiomatizations for the instances of V which were axiomatizable already in the finite but we further obtain infinitary axiomatizations of 𝖦^V_↑_ω_1,ω and 𝖦^V_↑_ω_1.

We don't now the state of 𝖦^V_↓_ω_1,ω, 𝖦^V_↓_ω_1 or any other V in particular but in the finitary, as shown by Hájek <cit.>, the tautologies of 𝖦^V_↓_ω,ω are not arithmetical. So we leave with the following question regarding the other truth-value sets:

Have any 𝖦^V_ω_1 or 𝖦^V_ω_1,ω (countable) infinitary axiomatizations for any V not considered here?

To approach these axiomatizability questions, we follow the general route of <cit.> which relies on tools from the theory of Polish spaces, like the Cantor-Bendixson theorem, which we briefly want to recall. In the following, we write 𝐀_V for the Heyting algebra associated with a Gödel set V. Note that every V, as a closed subset of ℝ, is a Polish space. A subset P of ℝ is perfect if it is closed and every point is a limit point in the topology induced by ℝ.

Any Polish space X can be partitioned as P∪ C with P perfect and C countable and open.

The following result is then the central connection between the Cantor-Bendixson theorem and evaluations over Gödel sets.

Let M⊆[0,1] be countable and P⊆ [0,1] be perfect. Then there is a strictly monotone h:M→ P which preserves any infima and suprema existing in M and if inf M∈ M, then h(inf M)=inf P.



  §.§.§ V is finite

We consider the axiom scheme

    𝖥𝖨𝖭(n):=(ϕ_0→ϕ_1)(ϕ_1→ϕ_2)…(ϕ_n-1→ϕ_n)

as in the finitary axiomatizations.

For any countable Γ∪{ϕ}⊆ℒ_ω_1, we have

    Γ⊢_𝒢^D_ω_1+𝖥𝖨𝖭(n)ϕ iff Γ_𝖦^V_n_ω_1ϕ.

Similarly, for any countable Γ∪{ϕ}⊆ℒ_ω_1,ω where all formulas of Γ are closed, we have

    Γ⊢_𝒢^D_ω_1,ω+𝖥𝖨𝖭(n)ϕ iff Γ_𝖦^V_n_ω_1,ωϕ.

In fact, 𝖥𝖨𝖭(n) can, in both cases, be replaced by 𝖥𝖨𝖭^a(n): all atomic instances of 𝖥𝖨𝖭(n).


Soundness is routine. For the converse, define ℒ_A:=frag(Γ∪{ϕ}) and write ℒ^a_A for the atomics of ℒ_A. We consider

    Π:={(ϕ_0→ϕ_1)(ϕ_1→ϕ_2)…(ϕ_n-1→ϕ_n)|ϕ_i∈ℒ^a_A}.

Π is countable as Γ, and therefore ℒ_A, is countable. Now suppose Γ⊬_(𝒢^D_ω_1+𝖥𝖨𝖭(n))(ℒ_A)ϕ. Then clearly Γ∪Π⊬_𝒢^D_ω_1(ℒ_A)ϕ and by strong completeness of 𝒢^D_ω_1(ℒ_A), we have Γ∪Π_[0,1]_ℝ(ℒ_A)ϕ, i.e. there is an evaluation v:ℒ_A→ [0,1] with

    v[Γ∪Π]⊆{1} but v(ϕ)<1.

Now, the set v[ℒ^a_A] contains at most n elements. If not, then there are formulas ϕ_0,…,ϕ_n∈ℒ^a_A with v(ϕ_i)>v(ϕ_i+1). In that case, we have

    v((ϕ_0→ϕ_1)(ϕ_1→ϕ_2)…(ϕ_n-1→ϕ_n))<1

which is a contradiction to v[Π]⊆{1}. Thus, we can write v[ℒ^a_A]⊆{0,v_1,…,v_n-2,1} with v_i<v_i+1. By induction on the structure of formulas, we also get v[ℒ_A] ⊆ {0,v_1,…,v_n-2,1}. We define a function h:v[ℒ_A]→ V_n by setting h(0):=0, h(1):=1 and h(v_i):=1-1i+1. v[ℒ_A] is, with its order by <, a Heyting algebra and therefore h is an isomorphism of Heyting algebras and in particular preserves infima and suprema. Lemma <ref> gives that h∘ v is a ℒ_A-evaluation with

    (h∘ v)[Γ]⊆{1} but (h∘ v)(ϕ)<1.

As h∘ v evaluates into V_n, we get Γ_𝐀_V_n(ℒ_A)ϕ. Therefore also Γ_𝖦^V_n_ω_1ϕ, as 𝐀_V_n is complete.


For the first-order instances, we instead consider

    Π:={∀ x_i_1…∀ x_i_m((ϕ_0→ϕ_1)…(ϕ_n-1→ϕ_n))|ϕ_j∈ℒ^a_A, var(ϕ_j)⊆{x_i_1,…,x_i_m}}.

similar to <cit.> where ℒ_A^a now represents the atomic formulas of the first-order fragment ℒ_A.

For countable fragments ℒ_A, Π is countable and as every atomic formulas has only a finite number of variables, we have that every formula in Π is closed. Then apply Lemma <ref> in place of Lemma <ref> as in <cit.>.



  §.§.§ V is V_↑

The strength of infinitary logics is of course that we have infinitary disjunctions available which we can use to combine the various finitary axioms 𝖥𝖨𝖭(n). More precisely, we define the scheme 𝖥𝖨𝖭 by

    ⋁_n≥ 2⋀_k∈ω⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1).

In the first-order case, we will additionally consider a seemingly weakened version 𝖥𝖨𝖭^a given by

    ⋁_n≥ 2⋀_k∈ω⋁_i=0^n-1∀ x^n,k_j_1…∀ x^n,k_j_m(ϕ^n,k_i→ϕ^n,k_i+1)

where all ϕ^n,k_i are atomic with var(ϕ^n,k_i)⊆{x^n,k_j_1,…,x^n,k_j_m}. Now, 𝖥𝖨𝖭 can be used to obtain an axiomatization of ⋂_n≥ 2𝖦^V_n_ω_1 or ⋂_n≥ 2𝖦^V_n_ω_1,ω for countable sets. In combination with the previous Proposition <ref>, we then obtain an axiomatization of V_↑.

For any countable Γ∪{ϕ}⊆ℒ_ω_1, we have

    Γ⊢_𝒢^D_ω_1+𝖥𝖨𝖭ϕ iff Γ_𝖦^V_↑_ω_1ϕ.

Similarly, for countable Γ∪{ϕ}⊆ℒ_ω_1,ω where all formulas in Γ are closed, we have

    Γ⊢_𝒢^D_ω_1,ω+𝖥𝖨𝖭ϕ iff Γ_𝖦^V_↑_ω_1,ωϕ.



𝖥𝖨𝖭 is valid in V_↑: suppose v:ℒ_ω_1→ V_↑ is such that 

    v(⋁_n≥ 2⋀_k∈ω⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1))<1.

Thus, for some α, we have 

    v(⋀_k∈ω⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1))≤α<1

for any n≥ 2. Let k be such that v(⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1))<1. Such a k exists as α<1. For such a k, we get

    v(ϕ_0^n,k)>v(ϕ_1^n,k)>…>v(ϕ^n,k_n)

and as v evaluates into V_↑, we have

    v(ϕ_0^n,k)≥ 1-1n+1 and v(ϕ_1^n,k)≥ 1-1n

and therefore v(ϕ_0^n,k→ϕ_1^n,k)≥ 1-1n. This yields

    v(⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1))≥ 1-1n

for any such k and we get

    v(⋀_k∈ω⋁_i=0^n-1ψ^n,k)   =min{inf_v(ψ^n,k)<1v(ψ^n,k),inf_v(ψ^n,k)=1v(ψ^n,k)}
       =inf_v(ψ^n,k)<1v(ψ^n,k)
       ≥ 1-1n

for any n≥ 2 where we write ψ^n,k:=⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1). But this implies

    v(⋁_n≥ 2⋀_k∈ω⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1))=1

in contradiction to our assumption.

For the converse, suppose Γ⊬_𝒢^D_ω_1+𝖥𝖨𝖭ϕ. Then, we have

    Γ⊬_𝒢^D_ω_1+𝖥𝖨𝖭(n)ϕ

for some n as if Γ⊢_𝒢^D_ω_1+𝖥𝖨𝖭(n)ϕ for all n, then there are countably many instances

    ⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1)   (k∈ω)

of 𝖥𝖨𝖭(n), such that

    Γ⊢_𝒢^D_ω_1⋀_k∈ω⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1)→ϕ

for any n and thus

    Γ⊢_𝒢^D_ω_1⋁_n≥ 2⋀_k∈ω⋁_i=0^n-1(ϕ^n,k_i→ϕ^n,k_i+1)→ϕ

by (Rω)_1. The premise is an instance of 𝖥𝖨𝖭 which implies that Γ⊢_𝒢^D_ω_1+𝖥𝖨𝖭ϕ, a contradiction. Therefore, there is an n with Γ⊬_𝒢^D_ω_1+𝖥𝖨𝖭(n)ϕ and thus, using that Γ is countable, we get

    (Γ,ϕ)∉⋂_n≥ 2𝖦^V_n_ω_1

by Theorem <ref> which implies Γ_𝖦^V_↑_ω_1ϕ by Proposition <ref>.


The first order case is very similar. Soundness follows in the same way and the converse follows by the following slightly modified argument: supposing Γ⊬_𝒢^D_ω_1,ω+𝖥𝖨𝖭ϕ, we of course also have Γ⊬_𝒢^D_ω_1,ω+𝖥𝖨𝖭^aϕ. As in the propositional case, we get Γ⊬_𝒢^D_ω_1,ω+𝖥𝖨𝖭^a(n)ϕ for some n where it is essential that all instances of 𝖥𝖨𝖭^a are closed to be able to use the deduction theorem. We get Γ_𝖦^V_↑_ω_1,ωϕ using Proposition <ref>.



  §.§.§ 0 contained in the perfect kernel

We obtain the following infinitary version of the well-known finitary result from <cit.>.

Let V be a Gödel set and P its perfect Kernel and W=V∪[inf P,1]. For any fragment ℒ_A (of ℒ_ω_1 or ℒ_ω_1,ω) and any countable Γ∪{ϕ}⊆ℒ_A, we have

    Γ_𝐀_V(ℒ_A)ϕ iff Γ_𝐀_W(ℒ_A)ϕ.



We only present the propositional case which is essentially contained in <cit.>. The first order case is the same with Lemma <ref> replaced by Lemma <ref> and Lemma <ref> replaced by Lemma <ref>, respectively

Since V⊆ W, we have that Γ_𝐀_W(ℒ_A)ϕ implies Γ_𝐀_V(ℒ_A)ϕ. 

Let v:ℒ_A→𝐀_W be such that v[Γ]⊆{1} but v(ϕ)<1. As Γ is countable, there is an x∈ [0,1] with v(ϕ)<x<1 and where x∉v[sub(Γ∪{ϕ})]. With v_x as in Lemma <ref>, we have

    v_x(ψ)=v(ψ)   if v(ψ)<x,
    1   otherwise,

for any ψ∈Γ∪{ϕ}. Set M:={v_x(ψ)|ψ∈ℒ_A}∪{1} and 

    M_0:=M∩ [0,inf P) as well as M_1:=(M∩ [inf P,x])∪{inf P}.

Lemma <ref> gives a strictly monotone h:M_1→ P preserving all infima and suprema such that h(inf M_1)=inf P. We define

    g:y↦y   if y∈ [0,inf P],
    h(y)   if y∈ [inf P,x],
    1   if y=1,

for y∈ M. g preserves infima, suprema and is strictly monotone with g(0)=0 and g(1)=1. g therefore is a homomorphism of Heyting algebras preserving infima and suprema and by Lemma <ref>, g∘ v_x is an evaluation. But g∘ v_x maps into V and (g∘ v_x)[Γ]⊆{1} but g(v_x(ϕ))=g(v(ϕ))<1.

This immediately yields the following completeness result.

Let V be a Gödel set where 0 is contained in the perfect Kernel. For any fragment ℒ_A (of ℒ_ω_1 or ℒ_ω_1,ω) and countable Γ∪{ϕ}⊆ℒ_A where Γ is closed in the first-order case, we have

    Γ⊢_𝒢^D(ℒ_A)ϕ iff Γ_𝐀_V(ℒ_A)ϕ.

Here, we write 𝒢^D(ℒ_A) for 𝒢^D_ω_1(ℒ_A) or 𝒢^D_ω_1,ω(ℒ_A), respectively, depending the choice of language.



  §.§.§ V uncountable and 0 isolated

We now turn to the case of an isolated 0. For the first-order case, we have to additionally consider the quantifier version 𝖰𝖨𝖲𝖮_0 of 𝖨𝖲𝖮_0 (from which it was derived) as e.g. seen in <cit.>:

    ∀ xϕ→∀ xϕ.

The following lemma is an easy adaption of the finitary first-order case from <cit.>, which only mentions the latter statement regarding the quantifiers.

For any ϕ_i, we have ⊢_𝒢^D_ω_1+𝖨𝖲𝖮_0⋀_i∈ωϕ_i→⋁_i∈ωϕ_i. Similarly for 𝒢^D_ω_1,ω. In the first-order case, we additionally have ⊢_𝒢^D_ω_1,ω+𝖰𝖨𝖲𝖮_0∀ xϕ→∃ xϕ for any ϕ and x.


Let V be an uncountable Gödel set with 0 isolated. Let ℒ_A be a countable fragment of ℒ_ω_1 or ℒ_ω_1,ω where ⋀_i∈ωϕ_i∈ℒ_A iff ⋁_i∈ωϕ_i∈ℒ_A and where ⋁_i∈ωϕ_i∈ℒ_A implies ⋁_i∈ωϕ_i∈ℒ_A. 

For any Γ∪{ϕ}⊆ℒ_A, we have

    Γ⊢_(𝒢^D_ω_1+𝖨𝖲𝖮_0)(ℒ_A)ϕ iff Γ_𝐀_V(ℒ_A)ϕ

in the propositional case and

    Γ⊢_(𝒢^D_ω_1,ω+𝖨𝖲𝖮_0+𝖰𝖨𝖲𝖮_0)(ℒ_A)ϕ iff Γ_𝐀_V(ℒ_A)ϕ

in the first-order case where Γ is assumed to be closed.


Soundness is clear. For the other direction, note that we know by Lemma <ref> that

    Γ_𝐀_V(ℒ_A)ϕ iff Γ_𝐀_V∪[inf P,1](ℒ_A)ϕ

where P is the perfect kernel of V. We thus assume that [inf P,1]⊆ V. We define

    Π:={⋀_i∈ωϕ_i→⋁_i∈ωϕ_i|⋀_i∈ωϕ_i∈ℒ_A}.

By the assumptions on ℒ_A, we have Π⊆ℒ_A and in particular, Π is countable. Suppose that Γ⊬_(𝒢^D_ω_1+𝖨𝖲𝖮_0)(ℒ_A)ϕ.

We now either have Π∪Γ_[0,1]_ℝ(ℒ_A)ϕ or Π∪Γ_[0,1]_ℝ(ℒ_A)ϕ. For the former, we get

    Π∪Γ⊢_𝒢^D_ω_1(ℒ_A)ϕ

by completeness. As by Lemma <ref>, (𝒢^D_ω_1+𝖨𝖲𝖮_0)(ℒ_A) proves every element of Π, we have

    Γ⊢_(𝒢^D_ω_1+𝖨𝖲𝖮_0)(ℒ_A)ϕ

which is a contradiction to our assumption. Therefore we have Π∪Γ_[0,1]_ℝ(ℒ_A)ϕ, i.e. there is a v:ℒ_A→ [0,1] with v[Π]∪ v[Γ]⊆{1} and v(ϕ)<1. We define

    h:x↦0   if x=0,
    inf P+x/1-inf P   otherwise.

Note that (h∘ v)[ℒ_A]⊆ V. Uniquely extend v_h:x↦ h(v(x)) for x∈ Var_ω_1∩ℒ_A to v_h on ℒ_A. Then we have

    v_h(ψ)=h(v(ψ))

for any ψ∈ℒ_A which gives the claim. This can be proven by induction on ψ, see in particular <cit.> for the similar finitary case, where v[Π]⊆{1} is used to handle the ⋀-case.

The proof in the first-order case is very similar. We then consider

    Π:={∀x(⋀_i∈ωϕ_i→⋁_i∈ωϕ_i)|⋀_i∈ωϕ_i∈ℒ_A,x∈ (Var_A)^n,n∈ℕ}
                   ∪{∀y(∀ xϕ→∃ xϕ)|ϕ∈ℒ_A, x∈ Var_A, y∈ (Var_A)^n,n∈ℕ}

and one proceeds as above and obtains a ℑ with ℑ[Π]∪ℑ[Γ]⊆{1} but ℑ(ϕ)<1. As Π is not closed, note in particular Remark <ref> in that closedness is not needed for both directions of the completeness results, only for the soundness direction. Note that Π is countable.

With the same h defined as before, one similarly defines ℑ'_h for ℑ'=ℑmx by changing P^𝔐 to h∘ P^𝔐 for predicates P in the underlying model 𝔐 and the key point is to now establish 

    ℑ'_h(ψ)=h(ℑ'(ψ))

for any ψ∈ℒ_A for any such ℑ' where, for the ⋀- and ∀-cases, it is important that ℑ[Π]⊆{1} and that any element of Π is universally quantified with arbitrary but finitely many quantifiers such that ℑ[Π]⊆{1} implies 

    ℑ'(⋀_i∈ωϕ_i→⋁_i∈ωϕ_i)=1

and 

    ℑ'(∀ xϕ→∃ xϕ)=1

even for any ℑ' as above.

As before, we can now lift the above result to arbitrary ℒ_A if we restrict to countably many assumptions.

Let V be an uncountable Gödel set with 0 isolated and let ℒ_A be an arbitrary fragment of ℒ_ω_1 or ℒ_ω_1,ω with the same additional closure conditions as in Theorem <ref> but let Γ∪{ϕ}⊆ℒ_A be countable with Γ closed in the first-order case.

For any Γ∪{ϕ}⊆ℒ_A, we have

    Γ⊢_(𝒢^D_ω_1+𝖨𝖲𝖮_0)(ℒ_A)ϕ iff Γ_𝐀_V(ℒ_A)ϕ

in the propositional case and

    Γ⊢_(𝒢^D_ω_1,ω+𝖨𝖲𝖮_0+𝖰𝖨𝖲𝖮_0)(ℒ_A)ϕ iff Γ_𝐀_V(ℒ_A)ϕ

in the first-order case.

The proof follows the same type of argument as in Corollary <ref> where we now consider the smallest fragment containing Γ∪{ϕ} with the additional closure properties. The important point is here that for a countable Γ, this fragment is again countable.


Again, the above gives in particular

    Γ⊢_𝒢^D_ω_1+𝖨𝖲𝖮_0ϕ iff Γ_𝖦^V_ω_1ϕ

for countable Γ and

    Γ⊢_𝒢^D_ω_1,ω+𝖨𝖲𝖮_0+𝖰𝖨𝖲𝖮_0ϕ iff Γ_𝖦^V_ω_1,ωϕ
 
for countable and closed Γ where 0 is isolated in V.


 §.§ Acknowledgments

I want to thank Matthias Baaz for helpful discussions of the topics of this paper.

plain


