4

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.

Greg Nisbet
  • 11,657
  • 1
    "ill-founded" and "controlled" really don't go well together, especially in set theory/logic context. While I don't see a reason it is not possible, and I have few ideas of how to define a logic that allows such proofs, you are losing the idea that a proof is a "procedure" made out of steps starting from a base assumption – ℋolo Feb 04 '22 at 16:49
  • 1
    Here is an idea of such logic: let ${\cal W}_κ$ be logic that allows statements of length $β$ such that $\aleph(β)<κ$, and similarly to the set of variables, with proofs defined as: if $(I,<_I)$ is a linearly ordered set, and $(A_i\mid i\in I)$ is a set of statements such that (1) $A_j$ follows from ${A_i\mid i<j}$, (2) for each $p<j$ such that $p$ is not the minimum we have that $A_j$ does not follows from ${A_i\mid p\le i<j}$, and (3) ${i\mid i\in I\land A_i\text{ is an assumption or a tautology}}$ is cofinal in $(I,<_I)^*$(that is, $I$ with reverse orderer)... – ℋolo Feb 04 '22 at 16:58
  • 1
    ... then we say that $(A_i\mid i\in I)$ is a proof for each $A_j$ – ℋolo Feb 04 '22 at 16:59
  • 1
    Condition (1) is just to make it works similarly to our normal notion of proof, condition (2) is so we cannot prove everything using non-well ordered set, and condition (3) is so that the proof is not "out of nothing" – ℋolo Feb 04 '22 at 17:01
  • 1
    Is this "controlled" enough for what you want? – ℋolo Feb 04 '22 at 17:02
  • Okay, so my statements are linearly ordered; everything follows from earlier statements; if I take a proper suffix of my proof, none of the statements hold based on earlier ones ... and my open assumptions / instances of axioms are sprinkled throughout the proof? Interesting. Does allowing this kind of proof alongside the normal wellfounded proof-tree proofs in $\mathcal{L}_{\kappa,\lambda}$ lead to more things being provable? – Greg Nisbet Feb 04 '22 at 17:32
  • @ℋolo, I think your construction would make a good answer, thanks. When I wrote this question, I was envisioning restrictions on what inference rules could be used where to avoid circularity/spurious-proofs ... and not so much restrictions on the structure on the proof itself. – Greg Nisbet Feb 04 '22 at 17:34
  • 1
    Let me write a full answer, and I will add the relation to well-ordered proofs in there – ℋolo Feb 04 '22 at 17:55

1 Answers1

2

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:

  1. $B_j$ follows from $\{B_i\mid i\in I\land i<j\}$
  2. 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\}$
  3. 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:

  1. 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.
  2. I used linearly ordered set, but I can imagine that there exists variations that allow arbitrary posets, or some other class of posets
  3. 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")
ℋolo
  • 10,006