Are there infinite logics that permit non-well-founded proofs in a controlled way? Are there any infinite logics that permit infinite, non-well-founded proofs in a controlled way?

SEP's article on infinitary logic has a nice definition of the family of infinitary logics. There are logics like $\mathcal{L}_{\kappa,\lambda}$. $\kappa$ and $\lambda$ are cardinals constrained to satisfy $\lambda \le \kappa$.
Let's assume for the moment that free and bound variables are disjoint sets.
A quantifier must introduce a set of bound variables strictly smaller than $\lambda$. (I think we could equivalently just impose the condition that the set of bound variables is strictly smaller than $\lambda$ because the is-a-proper-subexpression-of relation is still well-founded in $\mathcal{L}_{\kappa,\lambda}$).
$\kappa$ is strictly greater than the size of the largest set of variables that we can join together in an infinitary conjunction $\bigwedge \Phi$.
In section 2, they list an infinite inference rule for conjunction.
$$ \frac{\varphi_1, \varphi_2 \cdots}{\bigwedge \Phi} \;\; \text{is infinite conjunction introduction in $\mathcal{L}_{\omega_1, \omega}$} $$
This results in an infinite proof. In an instance of this inference rule, there are infinitely many open assumptions.
However, a proof containing this rule can still be "unfolded" in a graph that's a tree with a directed edge going from premises to conclusions ... that's still well-founded. (The graph isn't a hypergraph so it loses information about the struture of the proof).
Equivalently, if we start at the conclusion of a proof and work our way backwards picking premises to jump to, we'll always reach the end after a finite number of jumps ... because there aren't any infinite paths through the proof.
 A: Here are 2 different ideas of logics with non-well ordered proofs:

Working with either ZF (if you want some really weird proofs/statements), or ZFC as a meta theory, let $κ$ be any linearly ordered set, then let ${\cal W}_κ$ be the logic that allows the following statements:
If $(I, <_I)$ is an linearly ordered set such that $κ$ does not embed into $(I,<_I)$, and $A=\{A_i\mid i\in I\}$ is a set of statements, so is $\bigvee A$ and $\bigwedge A$ are.
Similarly, if $V=\{V_i\mid i\in I\}$ is a set of variables, $∃_{i\in I}V_i(A)$ and $\forall_{i\in I} V_i(A)$ are statements.
We define a proof as follows:
Let $B=\{B_i\mid i\in I\}$ be a set of statements indexed by $I$ such that:

*

*$B_j$ follows from $\{B_i\mid i\in I\land i<j\}$

*if $k<j$ and there exists $q<k$, then $B_j$ does not follows from $\{B_i\mid i\in I\land k<i<j\}$

*the set $\{i\in I\mid A_i\text{ is an assumption or a tautology}\}$ is cofinal in $I$ with the reverse order.

Then we say that $B$ is a proof of $B_j$ for each $j\in I$.
The second idea with the same but replace 3 with:
3*.  there exists $k\in I$ such that $\{B_i\mid i\in I\land i<k\}$ is made only from assumptions or tautology.

The idea of (1) is clear.
(2) has 2 parts, first $B_j$ does not follows from $\{B_i\mid i\in I\land k<i<j\}$. That is because otherwise, let $φ$ be any statement, and $ψ$ be tautology, and then $I=ℤ$, and letting $B_{2n}=ψ$ and $B_{2n+1}=φ$ is a proof of $φ$.
The second part, of "there exists $q<k$" is to allow well ordered proofs (in the usual sense) to work.
The 2 options for the third condition is to guarantee that a proof "comes out" of true statements, and not from nothing.
(3*) probably behaves better, but (3) will give you more freedom on "what we can conclude".


3 final words:

*

*Notice that I defined ${\cal W}_κ$, but in reality I we can make $\cal W$ depends on more than 1 ordered set, just like in infinitary logic.

*I used linearly ordered set, but I can imagine that there exists variations that allow arbitrary posets, or some other class of posets

*And I have no idea if anything meaningful can come from the above definition, or even if the above definitions or in some sense "reduced to normal proofs", it is just an idea to show that "well order" in the definitions of infinitary logic/higher order logics are just by product of using cardinals/ordinals (which makes sense intuitively), but there is no reason to stick to those (at least I don't see a reason immediately, apart from getting further away from our intuition of "proof")

