Implementability of proof assistants for Infinitary logics with finite many terms

Question

Infinitary logic is a natural consequence of extending the length of proofs of first-order logic to a infinite ordinal level.

By definition, since proof lengths are infinitely long, one should not expect to implement a proof assistant that can check proofs on an Infinitary logic...

But what if one only needs to check proofs of finite terms in Infinitary logic?

Can we have decidable checkers to check the proofs in the following Infinitary logic:

• $\mathcal{L}_{\omega_1,\omega}$, Countable infinite logical connectives and finite quantifiers which use only finitely many terms.

This is the simplest infinitary logic, enjoying the downward Löwenheim-Skolem theorem and the Barwise Compactness Theorem.

• $\mathcal{L}_{\infty,\omega}$, Any ordinal number of logical connectives and finite quantifiers which use only finitely many terms.

• $\mathcal{L}_{\omega_1,\omega_1}$, Countable infinite logical connectives and Countable infinite quantifiers which use only finitely many terms.

It is dangerous and powerful enough to define genuine wellorderings:

$$ \forall x_0 ...\forall x_n...(\neg(\bigwedge\limits_{n<\omega}x_{n+1}< x_n)) $$

Answer 1

I don't think this question is well formed for the following reasons. As stated in the answer to a similar math stack exchange question, there are uncountable many $\mathcal{L}_{\omega_1, \omega}$ sentences, so it wouldn't make sense to talk about a finite proof of a given sentence. Not only would the proof not be checkable in finite time, but it wouldn't even be possible in general to express the statement you are trying to prove in finite time.

Now, one can certainly talk about a countable fragment of $\mathcal{L}_{\omega_1, \omega}$. (Note, just restricting the number of variables doesn't make the number of sentences countable. For example, consider the infinite sentence $(1 > 0) \land (1 + 1 > 0) \land (1 + 1 + 1 > 0) \land \ldots$. It encodes the sequence 1, 2, 3, ... and similarly, all sequences of natural numbers can be encoded into infinite sentences as such.).

In computability theory, one such countable fragment is the fragment of computable infinitary formulas. This is well-studied. I doubt this version has a nice finite proof theory though. Consider the following example: $$\bigwedge_n \text{$1=1$ if $\phi_{e}(0)$ doesn't halt in $n$ steps, else $1=0$}$$ This can be made into a valid computable $\mathcal{L}_{\omega_1, \omega}$ sentence, but proving it is true for an arbitrary $e$ would be the same as a proof that the program $\phi_e(0)$ doesn't halt. Now, note, if $\phi_e(0)$ doesn't halt, this formula is deducible with an infinite proof, and even a computable one at that, namely check that the $n$th term is $1=1$ and give a trivial proof of that. So whatever you mean by "decidable checkers to check the proofs in the following Infinitary logic", you can't ask for a finite deduction method for this fragment of $\mathcal{L}_{\omega_1, \omega}$ which can be used to prove any computable infinite statement that has an infinite proof, even a computable one. Otherwise, you could solve the halting problem by searching for a finite proof of the corresponding infinite formula.

Maybe there is some nice proof-theoretic fragment of $\mathcal{L}_{\omega_1, \omega}$ with a nice form of finite deduction. I'm not an expert in this field. But as my above example shows, it is not clear what "nice" means, and it isn't clear it is going to agree with the usual infinite deduction of $\mathcal{L}_{\omega_1, \omega}$.

---

Since this is a proof assistant forum, let me mention that almost all common proof assistants can handle infinite conjunctions and can prove any reasonable statement in $\mathcal{L}_{\omega_1, \omega}$. An infinite conjunction is just a form of universal quantification. Here is one of the above examples in Lean:

def f : Nat -> Nat
| 0 => 1
| n+1 => (f n) + 1

-- This expresses /\_n 1 + ... + 1 > 0 
theorem foo (n : Nat) : f n > 0 := by
  induction n with
  | zero =>
      rw [f]
      norm_num
  | succ n ih =>
    rw [f]
    calc
    f n + 1 ≥ f n := by norm_num
    _      > 0    := ih

Indeed, Lean can talk about every computable $\mathcal{L}_{\omega_1, \omega}$ sentence (using the axiom of choice), but for the same argument above there are going to be sentences with infinite proofs (even computable ones) for which Lean has no (finite) proof.

Update: Further, handling infinite quantifiers is just as easy. Instead of quantifying over a type A infinitely many times, you quantify over sequences $\{x_i\}_{i\in I}$ of elements in A for some index set $I$. This is equivalent to quantifying over the type I -> A of functions from I to A. So your well-order example becomes:

theorem nat_wellordered : ∀ (x : Nat -> Nat), ¬ ∀ (n : Nat), x (n + 1) < x n := sorry

Similarly, you can show Int is not well ordered:

theorem int_not_wellordered : ∃ (x : Nat -> Int), ∀ (n : Nat), x (n + 1) < x n := sorry

One can even work with infinite conjunctions and infinite quantifiers much larger than countable. In this example, we can express that any universe Type u doesn't have an increasing chain of cardinalities of size Ordinal.{u+1} (which is the ordinal corresponding to the size of the next higher universe Type (u+1). The details are particular to Lean, but you can do similar things in other theorem provers.

theorem bar : ∀ (X : Ordinal.{u+1} -> Type u), ¬ ∀ (α β : Ordinal.{u+1}),
  α < β -> Cardinal.mk (X α) < Cardinal.mk (X β) := sorry