I claim the answer is "Yes," that is, FPA (and $IΔ_0+Ω_1$) can prove the consistency of $G$.
Consider the proof system $G$ as found in Logical Foundations of Proof Complexity by Stephen Cook and Phuong Nguyen, with two simplifications: axioms $A→A$ must have $A$ atomic; and the target formula for existential-right or universal-left must be either $⊤$ or $⊥$.
$<e>$ represents the unary sequence listing precisely one element, $<e_1,e_2>$ or just $e_1,e_2$ is a sequence listing two elements, etc. and if $s_1,s_2$ are sequences, then let their concatenation be $s_1⌢s_2$. In $IΔ_0+Ω_1$ the usual properties of sequences and concatenations can be proved and shall be assumed here.
Atomic formula are constants $⊤$ and $⊥$, and variables $A, B, C, .... , x, y, z, ...$ If $ϕ$ and $ψ$ are formula, and $X$ is a variable, $¬ϕ, (ϕ∨ψ), (ϕ∧ψ), ∃Xϕ,$ and ∀Xϕ are also formulas. A bounded variable is not allowed to occur free outside the scope of the quantifier - e.g. $((X∧A)∨∀Xϕ)$ is not permitted - nor is it allowed to be in the scope of a quantifier using it again - e.g. $∀X(ϕ∧∃Xψ)$ is not permitted. Sequences of formula (perhaps empty) will be represented by capital Greek letters such as $Γ$ and $Δ$. Sequents are of the form $Γ→Δ$, i.e. in effect sequents are a sequence of two elements, both elements being sequences of formulas. Bounded and free variables in a formula are defined as usual. Let $free(ϕ)$ and $bnd(ϕ)$ be the set of all free and all bounded, respectively, variables of a formula $ϕ$. By the condition previously stated, $bnd(ϕ)∩free(ϕ)=∅$.
Axioms are:
$A→A$, $→⊤$, $⊥→$
As already noted $A$ must be an atomic formula.
Where A and B are any formulas, the rules of deduction are:
Weakening
Left: ${\dfrac{\Gamma\rightarrow \Delta}{A,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow \Delta}{\Gamma\rightarrow\Delta,A}}$
Exchange
Left: ${\dfrac{\Gamma_1 ,A,B,\Gamma_2\rightarrow\Delta}{\Gamma_1 ,B,A,\Gamma_2\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta_1 ,A,B, \Delta_2}{\Gamma \rightarrow\Delta_1 ,B,A, \Delta_2}}$
Contraction
Left: ${\dfrac{\Gamma ,A,A\rightarrow\Delta}{\Gamma ,A\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta ,A,A}{\Gamma\rightarrow\Delta,A}}$
¬
Left: ${\dfrac{\Gamma\rightarrow\Delta,A}{\neg A,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{A,\Gamma\rightarrow\Delta}{\Gamma\rightarrow\Delta,\neg A}}$
∧
Left: ${\dfrac{A,B,\Gamma\rightarrow\Delta}{(A \land B),\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A\qquad\Gamma\rightarrow \Delta,B}{\Gamma\rightarrow\Delta,(A\land B)}}$
∨
Left: ${\dfrac{A,\Gamma\rightarrow\Delta\qquad B,\Gamma\rightarrow \Delta}{(A \lor B),\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A,B}{\Gamma\rightarrow\Delta,(A \lor B)}}$
Cut
${\dfrac{\Gamma\rightarrow \Delta,A\qquad A,\Gamma\rightarrow\Delta}{\Gamma\rightarrow\Delta}}$
∀
Left: ${\dfrac{A(c),\Gamma\rightarrow\Delta}{\forall x\, A(x) ,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A(p)}{\Gamma\rightarrow\Delta,\forall x\,A(x)}}$
∃
Left: ${\dfrac{A(p), \Gamma\rightarrow\Delta}{\exists xA(x) ,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A(c)}{\Gamma\rightarrow\Delta,\exists x\,A(x)}}$
In the last rules $p$ is a free variable, called an eigenvariable, which must not occur in the bottom sequent, and $c$ is called a target formula, which as already noted is restricted to $⊤$ and $⊥$.
A $G$ proof $π$ of length $n$ of a sequent $q$ is a sequence of sequents such that for all $i≤n$, $π(i)$ is either an axiom or $∃j,k<i$ s.t. $π(i)$ can be deduced from $π(j)$ and perhaps $π(k)$ using one of the Rules of Deduction, and such that $π(n)=q$. Since $n$ can be inferred from context or is unimportant, its mention will be dropped, and since all proofs will be $G$ proofs, mention of $G$ will be dropped, so we will simply speak of a proof $π$ of a sequent $q$. If $π$ is a proof, then for every sequent $q$ appearing in the sequence, there exists a sub-sequence of $π$ which is a proof of $q$.
Let $free(π)$ be the set of variables appearing free somewhere in a proof $π$, $eigen(π)$ the set of eigenvariables removed by $∀$ Right or $∃$ Left in $π$, and $var(π)$ the variables, free or bound, appearing in $π$. Clearly, $eigen(π)⊆free(π)⊆var(π)$.
In $IΔ_0+Ω_1$ it is easy to count the total number of characters in a formula $ϕ$, a sequent $q$, or a proof $π$, and this ability and certain properties about this function $tlen$ will be assumed without proof. For instance, it will be assumed without proof that if $π$ is the proof $π'$ with the sequent $q$ inferred as an additional step, i.e. if $π=π'⌢q$, then $tlen(π)≥tlen(π')+tlen(q)$.
Def 1. Define the negation normal form $ϕ^*$ of a formula $ϕ$ by recursion:
$ϕ^*=ϕ$ if $ϕ$ is atomic
$(ϕ∧ψ)^*=ϕ^*∧ψ^*$
$(ϕ∨ψ)^*=ϕ^*∨ψ^*$
$(∃xϕ(x))^*=∃x(ϕ(x))^*$
$(∀xϕ(x))^*=∀x(ϕ(x))^*$
$(¬ϕ)^*=¬ϕ$ if $ϕ$ is atomic
$(¬¬ϕ)^*$=$ϕ$
$(¬(ϕ∧ψ))^*=((¬ϕ)^*∨(¬ψ^*))$
$(¬(ϕ∨ψ))^*=((¬ϕ)^*∧(¬ψ^*))$
$(¬∃xϕ(x))^*=∀x(¬ϕ(x))^*$
$(¬∀xϕ(x))^*=∃x(¬ϕ(x))^*$
If $ϕ^*=ϕ$, then we say $ϕ$ is in negation normal form. A negation sign in $ϕ^*$ must appear directly in front of an atomic formula.
Because the $^*$ operation at most adds a negation sign before every variable, it at most doubles the total number of characters of a formula. Thus $tlen(ϕ^*)≤2(tlen(ϕ))$.
Observations 2. For any formula $ϕ$
1/ $(ϕ^* )^*=ϕ^*$
2/ $(¬(¬ϕ)^* )^*=ϕ^*$
Note the free and bound barriers do not change under $^*$, so for any formula $ϕ$, the free (or bound) variables are all the same in: $ϕ, ¬ϕ, ϕ^*,$ and $(¬ϕ)^*$.
Def 3. For a sequence of formulas $Γ=ϕ_1,ϕ_2,...,ϕ_k$ define
$¬Γ=¬ϕ_1,¬ϕ_2,...,¬ϕ_k$
$Γ^*=ϕ_1^*,ϕ_2^*,...,ϕ_k^*$
Thus $(¬Γ)^*=(¬ϕ_1 )^*,(¬ϕ_2 )^*,...,(¬ϕ_k )^*$.
When $Γ$ is the empty sequence (i.e. $k=0$), then $¬Γ$ and $Γ^*$ are also the empty sequences.
For a sequent $Γ→Δ$ define $(Γ→Δ)^*=(¬Γ)^*⌢Δ^*$.
Some basic facts will be assumed about labelled binary trees, which as with sequences can be easily represented and proved in $IΔ_0+Ω_1$. For instance, when $T_1$ and $T_2$ are finite binary trees, new finite binary trees can be formed with root $η$ and children either both $T_1$ and $T_2$, or just $T_1$. $T_1$ and (if present) $T_2$ are called child trees of the new tree. In the first case, we represent the new tree by $[η;T_1;T_2]$ and in the second $[η;T_1]$. If a tree consists just of a root $η$ and no children, represent this as $[η]$. If $η$ is labelled $ϕ$, we may abuse notation and write $[ϕ;T_1;T_2]$ and $[ϕ;T_1]$ and $[ϕ]$. We say that the size of a binary tree $T$ is the number of its nodes and write $size(T)$.
Def 4. A semantical tree or semtree $T$ is a finite binary tree labelled with formulas such that:
1/ The root of $T$ is labelled with a formula $ϕ$ in negative normal form
2/ The leaves of $T$ are each labelled with some atomic formula or its negation
3/ The possible branches with their labels are as follows:
Split: Parent: $ψ$ Children: $ψ$ and $ψ$
$∧$ : Parent: $(ψ_1∧ψ_2)$ Children: $ψ_1$ and $ψ_2$
$∨$ : Parent: $(ψ_1∨ψ_2)$ Children: $ψ_1$ and $ψ_2$
$∃$ : Parent: $∃xψ(x)$ Child: $ψ(c)$, where $c$ is either $⊤$ or $⊥$
$∀$ : Parent: $∀xψ(x)$ Child: $ψ(E)$, where $E$ is some variable
4/ If a variable $E$ is introduced via a $∀$ branch, it is so introduced in the entire tree exactly once, and does not occur (free or bounded) in $ϕ$
Set $root(T)$ to the formula labelling the root of $T$. $T$ is said to be a semtree for $ϕ$ if $root(T)=ϕ^*$.
Observe no explanation is given for a parent of the form $¬ψ$, since in formulas in negation normal form, $¬$ may only occur before an atomic formula. This omission forces formulas of the form $¬ψ$ to be the labels of leaves.
If a variable appears in a semtree $T$, it must appear either free in the formula labelling the root, or be introduced (once and only once) via a $∀$ branch, or be a dummy variable appearing after a quantification sign. Set $free(T)$ to be the set of the first, $intro(T)$ for the second, and $bnd(T)$ for the third. By condition 4/ and the condition on free and bounded variables in formulas, $free(T)$, $intro(T)$, and $bnd(T)$ must be pairwise disjoint. Also set $var(T)=free(T)∪intro(T)$ and $var^+ (T)=var(T)∪bnd(T)$. Clearly, if a variable appears in a leaf, it must belong to $var(T)$.
Prop 5. Let $ϕ$ be a formula in negation normal form, $v$ a set of variables such that $(free(ϕ)∪bnd(ϕ))∩v=∅$. Suppose the number $n$ of elements of $v$ equals the number of universal quantifiers in $ϕ$. Then there exists a semtree $T$ for $ϕ$ with size $≤tlen(ϕ)$ such that $intro(T)=v$. Also, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ)$.
Proof:
Suppose $ϕ$ is an atomic formula or its negation. Then $n=0$ and $v=∅$. Set $T=[ϕ]$.
Suppose $ϕ$ is of the form $(ϕ_1∨ϕ_2)$ or $(ϕ_1∧ϕ_2)$, and partition $v$ into two sets $v_1$ and $v_2$ in any way, such that for both $i=1,2$ the number $n_i$ of elements of $v_i$ equals the number of quantifiers in $ϕ_i$. By the induction hypothesis, for both $i=1,2$ there exists a semtree $T_i$ for $ϕ_i$ with size $≤tlen(ϕ_i)$ such that $intro(T_i)=v_i$ and, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ_i)$. Then set $T=[ϕ;T_1;T_2]$.
Suppose $ϕ$ is of the form $∃xϕ_1(x)$. Then $ϕ_1(⊤)$ will have the same number of universal quantifiers as $ϕ$. By the induction hypothesis, there exists a semtree $T_1$ for $ϕ_1(⊤)$ with size $≤tlen(ϕ_1(⊤))$ such that $intro(T_1)=v$ and, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ_1(⊤))$. Then set $T=[ϕ;T_1]$.
Finally suppose $ϕ$ is of the form $∀xϕ_1 (x)$. Choose any element $E∈v$, and set $v^-=v∖{E}$. Then the number of elements of $v^-$ equals the number of universal quantifiers in $ϕ_1 (E)$, so by the induction hypothesis, there exists a semtree $T_1$ for $ϕ_1(E)$ with size $≤tlen(ϕ_1(E))$ such that $intro(T_1)=v^-$ and, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ_1(E))$. Then set $T=[ϕ;T_1]$ and note $intro(T)=intro(T')∪\{E\}=v$. //
Call some tree guaranteed by the previous proposition $\mathcal{B}(ϕ,v)$.
Def 6. An assignment $σ$ on a set of variables $v$ (perhaps empty) is a function from $v∪\{⊥,⊤\}$ to ${0,1}$ where $σ(⊤)=1$ and $σ(⊥)=0$. Let $ι$ be the assignment on the empty set, so $ι(⊤)=1$ and $ι(⊥)=0$.
An assignment $σ$ extends to the negations of atomic formulas in a natural way, using
$σ(¬ϕ)=1-σ(ϕ)$
Thus any assignment on a set $v$ with $var(T)⊆v$ can be extended to all the leaves of a semtree $T$. It can then be extended to the entire tree as follows, where $ϕ$ is the parent and $ψ_1$ and $ψ_2$ are the children (in the case of Split, $∨$, and $∧$) or $ψ$ is the child (in the case of $∃$ and $∀$).
Split$: σ(ϕ)=σ(ψ_1)+σ(ψ_2)-σ(ψ_1)σ(ψ_2)$
$∧ : σ(ϕ)=σ(ψ_1)σ(ψ_2)$
$∨ : σ(ϕ)=σ(ψ_1)+σ(ψ_2)-σ(ψ_1)σ(ψ_2)$
$∃ : σ(ϕ)=σ(ψ)$
$∀ : σ(ϕ)=σ(ψ)$
When $η$ is a node of $T$ and $σ$ is an assignment, set $σ_T(η)$ to the value assigned to that node when $σ$ is extended as just described. Set $val_σ(T)=σ_T(η)$, where $η$ is the root node of $T$.
Observation 7. Let $T$ be a semtree, and let $σ,σ'$ be assignments on $v_1,v_2$ respectively, where $var(T)⊆v_1,v_2$. Suppose $σ↾var(T)=σ'↾var(T)$. Then $σ_T(η)=σ'_T(η)$ for any node $η$ of $T$ and in particular $val_σ(T)=val_{σ' }(T)$.
Def 8. Let $T$ and $T'$ be semtrees. We say $T$ and $T'$ are separate if $free(T)∪free(T')$, $intro(T)$, and $intro(T')$ are pairwise disjoint.
Observations 9.
(1) If $[η;T_1;T_2]$ is a semtree, then $T_1,T_2$ are separate.
(2) If $T$ and $[η;T_1]$ are separate, then so are $T,T_1$. And if $T$ and $[η;T_1;T_2]$ are separate, then so are both $T,T_1$ and $T,T_2$.
(3) If $T$ and $T'$ are separate, then $var(T)∩var(T')=free(T)∩free(T')$.
Def 10. Write $ϕ∼ψ$ if $ϕ^*=(¬ψ)^*$.
Def 11. Let $T$ and $T'$ be semtrees. Write $T∼T'$ if $root(T)∼root(T')$.
Observations 12. If $T∼T'$, then $free(T)=free(T')$. So if in addition $T$ and $T'$ are separate, then $var(T)∩var(T')=free(T)$.
Def 13. Let $T$ be a semtree, $X∈free(T)$, and $c$ a constant. Write $T[X/c]$ for the tree $T$ with every free occurrence of $X$ replaced by $c$.
Observations 14. If $T$ is a semtree, $X∈free(T)$, and $c$ a constant, then $T[X/c]$ is a semtree. If in addition $root(T)=ϕ(X)$, then $root(T[X/c])=ϕ(c)$.Suppose further $σ$ is an assignment on $var(T)$ and that $i=σ(X)$. $i=0$ or $1$, so there exists a constant $c$ such that $ι(c)=σ(X)$. For this $c$, $val_σ(T)=val_σ (T[X/c])$.
Def 15. Let $T$ and $T'$ be semtrees with $free(T)=free(T')$. $T$ and $T'$ are jointly satisfiable if there exists an assignment $σ$ on $var(T)∪var(T')$ such that for all assignments $τ$ on $var(T)∪var(T')$, if $τ↾free(T)=σ↾free(T)$, then $val_τ(T)=val_τ(T')=1$.
Observation 16. Suppose $T$ and $T'$ are jointly satisfiable. Then there exists an assignment $σ$ on $var(T)∪var(T')$ such that $val_σ(T)=val_σ(T')=1$.
Def 17. Let $T$ be a semtree, and let U $= U_0,U_1,...,U_k$ be a sequence of semtrees where $U_0=T, U_k$ is a branchless tree (i.e. has only one node), and for all $i$ with $0≤i<k$ either:
$U_{i+1}$ is a child tree of $U_i$, or
$∃V$ such that $V$ is a child tree of $U_i$ and for some free variable $E$ and some constant $c$, $U_{i+1} =V[E/c]$.
Call U a root-to-leaf analysis of $T$. Say that a subsequence $S_0,S_1,...,S_j$ of U is Split-cleaned if for all $i$ with $0≤i≤k, U_i$ does not appear in the sub-sequence if and only if the root of $U_i$ is a Split branch.
Observation 18. In the context of the previous definition, the root of $U_k$ cannot be a Split branch, so $S_j=U_k$.
Theorem 19. Let $T$ and $T'$ be separate semtrees with $T∼T'$. And suppose $T$ and $T'$ are jointly satisfiable. Then there exist a root-to-leaf analysis U = $U_0,U_1,...,U_k$ of $T$ and a root-to-leaf analysis U' $= U'_0,U'_1,...,U'_{k' }$ of $T'$, and Split-cleaned subsequences $S_0,S_1,...,S_j$ of U and $S'_0,S'_1,...,S'_j$ of U' such that for all $i$ with $0≤i≤j$
1/ $S_i$ and $S'_i$ are separate
2/ $S_i ∼ S'_i$
3/ $S_i$ and $S'_i$ are jointly satisfiable.
Pf:
If $T$ and $T'$ are branchless trees (i.e. with only one node), the conclusion is obvious.
Split branch.
Suppose the root of either $T$ or $T'$ is a Split branch, WLOG the root of $T$. Then $T$ is of the form $[ϕ;T_1;T_2]$, where $T_1$ and $T_2$ are also semtrees with roots labelled $ϕ$. Set $f=free(T)$. Note for both $i=1,2$, $free(T_i)=f$, so $var(T_i)=f∪intro(T_i)$, and $T_i,T'$ are separate.
Let $σ$ be an assignment on $var(T)∪var(T')$ such that for all assignments $τ$ on $var(T)∪var(T')$ with $τ↾f=σ↾f$, $val_τ(T)=val_τ(T')=1$.
Suppose $T_1$ and $T'$ are not jointly satisfiable. Then there exists assignment $μ$ on $var(T_1)∪var(T')$ with $μ↾f=σ↾f$ but $val_μ(T_1)=0$ or $val_μ(T')=0$. Since $μ↾f=σ↾f$, $val_μ(T')=1$. This forces $val_μ(T_1)=0$.
Let $τ'$ be an assignment on $var(T_2)∪var(T')$ with $τ'↾f=σ↾f$.
Set
$σ'=ι∪τ'↾(f∪intro(T_2)∪intro(T'))∪μ↾intro(T_1)$.
Because of separateness $σ'$ is a well-defined assignment on $var(T)∪var(T')$. $σ'↾f=τ'↾f=σ↾f=μ↾f$, so $val_{σ'}(T)=val_{σ'}(T')=1$. Since $σ'↾intro(T_1)=μ↾intro(T_1)$ also $val_{σ' }(T_1)=0$. By the definition of assignment on a Split branch, $val_{σ'}(T_2)=1$. Thus $val_{τ'}(T_2)=1$. Hence $T_2$ and $T'$ are jointly satisfiable.
So either $T_1,T'$ or $T_2,T'$ are jointly satisfiable. The other conditions are trivial, so one of these pairs satisfies the conditions of the theorem, with one less node, so apply the induction hypothesis, and prefix $T$ to the unprimed root-to-leaf analysis. The Split-cleaned subsequences remain the same since the root of $T$ is a Split branch.
Henceforth, suppose the roots of both $T$ and $T'$ are not Split branches.
$∨$ branch.
Suppose the root of $T$ is a $∨$ branch. Then $T$ is of the form $[(ϕ_1∨ϕ_2);T_1;T_2]$, where $T_1$ and $T_2$ are also semtrees, with roots labelled $ϕ_1,ϕ_2$ respectively, and $T'$ is of the form $[(ψ_1∧ψ_2);T'_1;T'_2]$, where $T'_1$ and $T'_2$ are also semtrees, with roots labelled $ψ_1,ψ_2$ respectively, such that $ϕ_1∼ψ_1$ and $ϕ_2∼ψ_2$. Note $T_i,T'_j$ are separate for any $i,j=1,2$.
Set $f=free(T)$, $f_1=free(T_1)$, and $f_2=free(T_2)$. Note $f=free(T')$, $f_1=free(T'_1)$, $f_2=free(T'_2)$, and $f=f_1∪f_2$.
Let $σ$ be an assignment on $var(T)∪var(T')$ such that for all assignments $τ$ on $var(T)∪var(T')$ with $τ↾f=σ↾f$, $val_τ(T)=val_τ(T')=1$.
If $T_1, T'_1$ are jointly satisfiable, apply the induction hypothesis, and prefix $T_1$ and $T'_1$ to the resulting sequences.
Otherwise assume $T_1,T'_1$ are not jointly satisfiable. Then there exists assignment μ on $var(T_1)∪var(T'_1)$ with $μ↾f_1=σ↾f_1$ but $val_μ(T_1)=0$ or $val_μ (T'_1)=0$. Let $τ'$ be an assignment on $var(T_2)∪var(T'_2)$ with $τ'↾f_2=σ↾f_2$. Note $μ↾(f_1∩f_2)=τ'↾(f_1∩f_2)$.
Set $σ'=ι∪μ∪τ'$, which is well-defined since by separateness,
$(var(T_1)∪var(T'_1))∩(var(T_2)∪var(T'_2)))=f_1∩f_2$.
$σ'↾(f_1∪f_2)=σ↾(f_1∪f_2)$, so $val_{σ'}(T)=val_{σ'}(T')=1$. By the definition of an assignment on an $∧$ branch, both $val_{σ'}(T'_1)=1$ and $val_{σ'}(T'_2)=1$. Thus $val_μ(T'_1)=1$, which forces $val_μ(T_1)=0$, and so $val_{σ'}(T_1)=0$. By the definition of an assignment on an $∨$ branch, this forces $val_{σ'}(T_2)=1$. Thus $val_{τ'}(T_2)=1$. Hence $T_2$ and $T'_2$ are jointly satisfiable. Apply now the induction hypothesis, and prefix $T_2$ and $T'_2$ to the resulting sequences.
$∧$ branch.
By symmetry.
$∃$ branch.
Suppose the root of $T$ is an $∃$ branch. Then $T$ is of the form $[∃xϕ(x);T_1]$, where $T_1$ is a semtree, with root labelled $ϕ(c)$ for some constant $c$, and $T'$ is of the form $[∀xψ(x);T'_1]$, where $T'_1$ is a semtree, with root labelled $ψ(E)$ for some variable $E∈intro(T')$ where $E∉free(ψ(x))$ and $E∉var(T)$. Clearly, $ϕ(c)∼ψ(c)$.
Set $f=free(T)$ and $v=var(T)∪var(T')$ and $v-=v∖{E}$. Note $f=free(T')$ and $f=free(T_1)$ and $f∪{E}=free(T'_1)$, where $E∉f$.
Since $T,T'$ are jointly satisfiable, there is an assignment $σ$ on $v$ s.t. for all assignments $τ$ on $v$ with $τ↾f=σ↾f$, $val_τ(T)=val_τ(T')=1$. Set $T''_1=T'_1[E/c]$ and $σ'=ι∪σ↾v-$. Note $f=free(T''_1)$ and $v-=var(T_1)∪var(T''_1)$ and $σ'$ is an assignment on $v-$. Let $τ'$ be an assignment on $v-$ s.t. $τ'↾f=σ'↾f$. Set $τ''$ to $τ'∪\{(E,ι(c))\}$. Then $τ''$ is an assignment on $v$ s.t. $τ''↾f=σ↾f$. So $val_{τ''}(T)=val_{τ''}(T')=1$. But then $val_{τ''}(T_1)=1$ and $val_{τ''}(T'_1)=1$. The latter conjunct, along with the observation that $τ''(E)=ι(c)$, implies $val_{τ''}(T''_1)=1$, so $val_{τ'} (T_1)=1$ and $val_{τ'}(T''_1)=1$. Thus $T_1$ and $T''_1$ are jointly satisfiable, and clearly $T_1∼T''_1$. Apply now the induction hypothesis, and prefix $T_1$ and $T''_1$ to the resulting sequences.
$∀$ branch.
By symmetry. //
Corollary 20. Let $T,T'$ be separate semtrees with $T∼T'$. Then $T,T'$ are not jointly satisfiable.
Pf:
Suppose they were jointly satisfiable. By the previous theorem there are semtrees $U,U'$ s.t. both are branchless, $U∼U'$, and $U,U'$ are jointly satisfiable. By the first and second conditions, the roots of $U$ and $U'$ must be labelled by $E$ and $¬E$, for some atomic formula $E$. By the third condition there exists $σ$ on $free(U)$ such that $val_σ(U)=val_σ(U')=1$. But this is impossible. //
Def 21. Let $t = T_1,...,T_k$ be a sequence of semtrees. Set $val_σ(t)=1$ if $∃i(val_σ(T_i)=1)$, and $=0$ otherwise. If $val_σ(t)=1$ for all assignments $σ$ on $∪_{i=1}^m var(T_i)$, write $val(t)=1$.
Note if $k=0$, then $val(t)=0$.
Theorem 22. Suppose $π$ is a tree-like proof where every instance of a free variable is as an eigenvariable. Let $w$ be the number of applications of weakening in $π$, let $β_i$ be the formula introduced by the $i$th weakening according to some fixed ordering, and let $w_i$ be the number of universal quantifiers in $β_i$ ($1≤i≤w$). Let $z_1,...,z_w$ be a set of pairwise disjoint sets of variables such that the number of elements in each $z_i$ equals $w_i$ and such that $z_i∩var(π)=∅$. For any sub-proof $π'$ of $π$, set $weak(π') =⋃z_i$, where the union is taken over every $i$ such that the $i$th weakening occurs in $π'$.
Let $q$ be a sequent in the proof sequence of $π$, where $q=Γ→Δ=ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$. And let $q*=ψ_1,...,ψ_m$. Also let $π_1$ be the sub-proof of $q$ in $π$. Then there exists a sequence of semtrees $t=T_1,T_2,...,T_m$ such that:
1/ each $T_i$ is a semtree for $ψ_i$
2/ $val(t)=1$
3/ $∑_{i=1}^m size(T_i)≤tlen(π_1)$
4/ For all $i,j(i≠j)$, $T_i$ and $T_j$ are separate
5/ $intro(T_i)⊆eigen(π_1)∪weak(π_1)$ for all $i$
6/ If $ϕ$ is a label of a node of $T_i$ then $tlen(ϕ)≤tlen(ψ_i)$ for all $i$
Proof:
We show how to construct a semtree satisfying the six conditions for each axiom and rule of deduction, by induction on the steps of $π_1$ bounded by the proof $π$.
Case 1. $q=A→A$, for atomic formula $A$. Note $(A→A)*=<¬A,A>$. Let $T_1$ be the semtree with root labelled $¬A$ and no children, $T_2$ the semtree with root labelled $A$ and no children. Setting $t=T_1,T_2$, clearly $val_σ (t)=1$ for all assignments on $var(T_1)$. If $π_1$ is a proof of $q$, $π_1$ must contain $q$, so $tlen(π_1)≥3≥(1+1)=size(T_1)+size(T_2)$. Finally, $T_1, T_2$ are vacuously separate.
Case 2. $q=⊥→$ or $q=→⊤$. Then $q*=<¬⊥>$ or $q*=<⊤>$. Both have trivial semtrees of size 1 with only a root, the root labelled either $¬⊥$ or $⊤$. All conditions 1/ through 6/ are easily seen to hold.
For the induction cases, by appropriate substitutions which do not increase the length of the number of characters in the proof, we may assume that every eigenvariable appearing in $π$ is eliminated exactly once via $∀$-left or $∃$-right.
Case 3. Weakening Left. Suppose $π_1=π_1'⌢<A,Γ→Δ>$, where $π_1'$ contains the sequent $Γ→Δ$. Let this be the $k$th weakening.
Obviously, the $k$th weakening is not present in $π_1'$.
Let $q'=Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$. Note $q^*=<(¬A)^*>⌢(q')^*$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Set $T_0=\mathcal{B}((¬A)^*,z_k)$ from Proposition 5 and $t=T_0⌢t'$.
Trivially $val(t)=1$ since $val(t')=1$.
$size(T_0)≤tlen((¬A)^*)$, so
$∑_{i=0}^m size(T_i)≤tlen(π_1')+tlen((¬A)^*)≤tlen(π_1)$.
$intro(T_i)⊆eigen(π_1')∪weak(π_1')$ for all $i(1≤i≤m). intro(T_0)=z_k$, and by assumption $z_k∩var(π)=∅$. So $z_k∩eigen(π_1')=∅$. And since the $k$th weakening is not present in $π_1'$, $z_k∩weak(π_1')=∅$. Thus $intro(T_0)∩intro(T_i)=∅$ for all $i(1≤i≤m)$. Moreover, $z_k∩free(ϕ_i)=∅$ for all $i(1≤i≤m)$, since $free(ϕ_i)⊆var(π)$.Finally, suppose $E∈free(T_0)∩intro(T_i)$ for some $i(1≤i≤m)$. $E∈free(T_0)$ implies $E∈free(A)$, so $E$ appears in the last step of the sub-proof $π_1$. By assumption this instance of $E$ must as an eigenvariable. So if $E∈eigen(π_1')$, then $E$ is eliminated twice as an eigenvariable in $π$, a contradiction. Hence $E∈weak(π_1')$, but this contradicts each of the $z_i$ being disjoint from $var(π)$. Thus $T_0$ and $T_i$ are separate for all $i≠0$.
If $ϕ$ is the label of a node of $T_0$, then $tlen(ϕ)≤tlen((¬A)^*)$.
Case 4. Weakening Right.
As Weakening Left.
Case 5. Exchange.
Trivial.
Case 6. Contraction Left. Suppose $π_1=π_1'⌢<Γ,A→Δ>$, where $π_1'$ contains the sequent $Γ,A,A→Δ$.
Let $q'=Γ,A,A→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_{k-1}=ϕ_k=A$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Define $T'=[(¬A)^*;T_{k-1};T_k]$ with $(¬A)^*$ being a Split branch, and set $t=T_1,...,T_{k-2},T',T_{k+1},...,T_m$.
Case 7. Contraction Right.
As Contraction Left.
Case 8. $¬$ Left.
Trivial since $(¬¬A)^*=A^*$, so $(¬A,Γ→Δ)^*$ simply reorganizes the order of the sequence $(Γ→Δ,A)^*$.
Case 9. $¬$ Right.
Also trivial.
Case 10. $∧$ Left. Suppose $π_1=π_1'⌢<(A∧B),Γ→Δ>$, where $π_1'$ contains the sequent $A,B,Γ→Δ$.
Let $q'=A,B,Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_1=A$ and $ϕ_2=B$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Define $T'=[(¬(A∧B))^*;T_1;T_2]$, where the root is an $∨$ Branch, and set $t=T',T_3,...T_m$.
Case 11. $∧$ Right. Suppose $π_1=π_A'⌢π_B'⌢Γ→Δ,(A∧B)$, where $π_A'$ contains the sequent $Γ→Δ,A$ and $π_B'$ the sequent $Γ→Δ,B$.
Because $π$ is a tree-like proof, $π_A'$ and $π_B'$ are disjoint.
Let $q_A'=Γ→Δ,A = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},A$ and let $q_B'=Γ→Δ,B = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},B$. Also let $q_A^*=ψ_1,...,ψ_{m-1},A^*$ and $q_B^*=ψ_1,...,ψ_{m-1},B^*$. Suppose $u=U_1,U_2,...,U_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_A',u$. Further suppose $v=V_1,V_2,...,V_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_B',v$. For $1≤i≤m-1$ set $T_i=[ψ_i;U_i;V_i]$ where the root is a Split Branch, and set $T_m=[(A^*∧B^*);U_m;V_m]$. The number of new nodes is $m$, less than the length of the sequent. By assumption $intro(U_i)⊆eigen(π_A')∪weak(π_A')$ and $intro(V_i)⊆eigen(π_B')∪weak(π_B')$, for $i(1≤i≤m)$. But $π_A',π_B'$ are disjoint, so $eigen(U_i)∩eigen(V_j)=∅$ to prevent eigenvariables being eliminated twice in the proof $π$. Also because $π_A',π_B'$ are disjoint, $weak(π_A')∩weak(π_B')=∅$. $eigen(π_A')∩weak(π_B')=∅$ by construction of the $z_i$, and similarly $eigen(π_B')∩weak(π_A')=∅$. Thus $intro(U_i)∩intro(V_j)=∅$ for all $i,j(1≤i,j≤m)$. If $E∈free(V_i)$ for some $i(1≤i≤m)$, then $E∈free(π_B')$ and must then be an instance of an eigenvariable in $π$. But then $E∉eigen(π_A')$. Also $E∉weak(π_B')$ by construction of the $z_i$. So $E∉intro(U_i)$ for any $i$. Thus all the $U_i,V_j$ are pairwise separate, and so the $T_i$ are pairwise separate.
Case 12. $∨$ Left and Right.
As $∧$ Right and Left.
Case 13. Cut. Suppose $π_1=π_1'⌢Γ→Δ$, where $π_R'$ contains the sequent $Γ→Δ,A$ and $π_L'$ contains the sequent $A,Γ→Δ$.
Let $q_R'=Γ→Δ,A = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},A$ and let $q_L'=A,Γ→Δ = A,ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1}$. Also let $q_R^*=ψ_1,...,ψ_{m-1},A^*$ and $q_L^*=(¬A)^*,ψ_1,...,ψ_{m-1}$. Suppose $u=U_1,...,U_{m-1},U_R$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_R',u$. And suppose $v=V_L,V_1,...,V_{m-1}$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_L',v$. Note that $U_R∼V_L$ and the pair $U_R,V_L$ are separate by the same argument as used in $∧$ Right. For $1≤i≤m-1$ set $T_i=[ψ_i;U_i;V_i]$ where the root is a Split Branch, and set $t=T_1,T_2,...,T_{m-1}$. Set $v=∪_{i=1}^{m-1} var(T_i)$, $v'=var(U_R)∪var(V_L)$, $v+=v∪v'$, and $f=free(U_R)$. $f=free(V_L)$, so $v'=f∪intro(U_R)∪intro(V_L)$. By separateness, $(intro(U_R)∪intro(V_L))∩v=∅$, so
$intro(U_R)∪intro(V_L)⊆v+∖v⊆v+$.
Suppose $val(t)≠1$. Then $val_μ (t)=0$ for some assignment $μ$ on $v$. Extend $μ$ to $v+$ in any way and call this new assignment $σ$. Still $val_σ(t)=0$. But $val(u)=val(v)=1$, so $val_σ(u)=val_σ(v)=1$, so $val_σ(U_R)=val_σ(V_L)=1$. Let $τ$ be an assignment on $v+$ such that $τ↾f=σ↾f$. Set τ'=ι∪τ↾(v+∖v)∪σ↾v, an assignment on v+. So val_(τ' ) (u)=val_(τ' ) (v)=1. Obviously $τ'↾v=σ↾v$, so $val_(τ')(t)=0$. Thus $val_(τ')(U_R)=val_(τ')(V_L)=1$. By construction $τ'↾v'=τ↾v'$, so $val_τ (U_R)=val_τ (V_L)=1$. Therefore $U_R,V_L$ are jointly satisfiable, contradicting Corollary 20. Thus $val(t)=1$.
Case 14. ∀ Left. Suppose $π_1=π_1'⌢∀xA(x),Γ→Δ$, where $π_1'$ contains the sequent $A(c),Γ→Δ$ with $c$ a constant.
Let $q'=A(c),Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_1=A(c)$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Set $T'=[(¬∀xA(x))*;T_1]$ and $t=T',...,T_m$. Note $(¬∀xA(x))^*=∃x(¬A(x))^*$, so the root of $T'$ is a $∃$ branch, and so $T'$ is indeed a semtree.
Case 15. $∀$ Right. Suppose $π_1=π_1'⌢Γ→Δ,∀xA(x)$, where $π_1'$ contains the sequent $Γ→Δ,A(p)$ with $p$ a variable not appearing in $Γ$ or $Δ$.
Let $q'=Γ→Δ,A(p)=ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_m=A(p)$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Set $T'=[(∀xA(x))^*;T_m]$ and $t=T_1,...,T_{m-1},T'$. Note $(∀xA(x))^*=∀x(A(x))^*$, so the root of $T'$ is a $∀$ branch, and so $T'$ is indeed a semtree. $p$ can only be used as an eigenvariable once, so $p∉eigen(π_1')$. Let $1≤i≤m-1$. $p∉weak(π_1')$ by construction of the $z_i$, so $p∉intro(T_i)$. Also $p∉free(T_i)$ because $free(T_i)=free(ϕ_i)$.Thus $T'$ is separate from each of the $T_i$ (where $1≤i≤m-1$).
Set $v=∪_{j=1}^m var(T_j)$. Note $v=∪_{j=1}^{m-1} var(T_j)∪var(T')$ since $var(T_m)=var(T')$. Let $σ$ be an assignment on $v$. Then by assumption, $val_σ(t')=1$. If $val_σ(T_j)=1$ for some $j(1≤j≤m-1)$, then $val_σ(t)=1$. Otherwise $val_σ(T_m)=1$, so by the definition of an assignment on a $∀$ branch, $val_σ(T')=1$, in which case again $val_σ(t)=1$.
Case 16. $∃$ Left and Right.
As $∀$ Right and Left. //
Take the contradictory sequent to be the empty sequent,$ → $.
Corollary 23. There is no proof of a contradiction.
Pf:
Suppose $π$ is a proof. It may be assumed that all free variables are eigenvariables, because if a free variable were not an eigenvariable, it would have to be eliminated by Cut. But then it could be replaced throughout the proof by a constant.
Let $e$ be the empty sequence. Then $( → )^* = e$. By the theorem, $val(e)=1$. But $val(e)=0$. //
EDIT: I retract. See comments.
I claim the answer is "Yes," that is, FPA (and $IΔ_0+Ω_1$) can prove the consistency of $G$.
Consider the proof system $G$ as found in Logical Foundations of Proof Complexity by Stephen Cook and Phuong Nguyen, with two simplifications: axioms $A→A$ must have $A$ atomic; and the target formula for existential-right or universal-left must be either $⊤$ or $⊥$.
$<e>$ represents the unary sequence listing precisely one element, $<e_1,e_2>$ or just $e_1,e_2$ is a sequence listing two elements, etc. and if $s_1,s_2$ are sequences, then let their concatenation be $s_1⌢s_2$. In $IΔ_0+Ω_1$ the usual properties of sequences and concatenations can be proved and shall be assumed here.
Atomic formula are constants $⊤$ and $⊥$, and variables $A, B, C, .... , x, y, z, ...$ If $ϕ$ and $ψ$ are formula, and $X$ is a variable, $¬ϕ, (ϕ∨ψ), (ϕ∧ψ), ∃Xϕ,$ and ∀Xϕ are also formulas. A bounded variable is not allowed to occur free outside the scope of the quantifier - e.g. $((X∧A)∨∀Xϕ)$ is not permitted - nor is it allowed to be in the scope of a quantifier using it again - e.g. $∀X(ϕ∧∃Xψ)$ is not permitted. Sequences of formula (perhaps empty) will be represented by capital Greek letters such as $Γ$ and $Δ$. Sequents are of the form $Γ→Δ$, i.e. in effect sequents are a sequence of two elements, both elements being sequences of formulas. Bounded and free variables in a formula are defined as usual. Let $free(ϕ)$ and $bnd(ϕ)$ be the set of all free and all bounded, respectively, variables of a formula $ϕ$. By the condition previously stated, $bnd(ϕ)∩free(ϕ)=∅$.
Axioms are:
$A→A$, $→⊤$, $⊥→$
As already noted $A$ must be an atomic formula.
Where A and B are any formulas, the rules of deduction are:
Weakening
Left: ${\dfrac{\Gamma\rightarrow \Delta}{A,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow \Delta}{\Gamma\rightarrow\Delta,A}}$
Exchange
Left: ${\dfrac{\Gamma_1 ,A,B,\Gamma_2\rightarrow\Delta}{\Gamma_1 ,B,A,\Gamma_2\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta_1 ,A,B, \Delta_2}{\Gamma \rightarrow\Delta_1 ,B,A, \Delta_2}}$
Contraction
Left: ${\dfrac{\Gamma ,A,A\rightarrow\Delta}{\Gamma ,A\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta ,A,A}{\Gamma\rightarrow\Delta,A}}$
¬
Left: ${\dfrac{\Gamma\rightarrow\Delta,A}{\neg A,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{A,\Gamma\rightarrow\Delta}{\Gamma\rightarrow\Delta,\neg A}}$
∧
Left: ${\dfrac{A,B,\Gamma\rightarrow\Delta}{(A \land B),\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A\qquad\Gamma\rightarrow \Delta,B}{\Gamma\rightarrow\Delta,(A\land B)}}$
∨
Left: ${\dfrac{A,\Gamma\rightarrow\Delta\qquad B,\Gamma\rightarrow \Delta}{(A \lor B),\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A,B}{\Gamma\rightarrow\Delta,(A \lor B)}}$
Cut
${\dfrac{\Gamma\rightarrow \Delta,A\qquad A,\Gamma\rightarrow\Delta}{\Gamma\rightarrow\Delta}}$
∀
Left: ${\dfrac{A(c),\Gamma\rightarrow\Delta}{\forall x\, A(x) ,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A(p)}{\Gamma\rightarrow\Delta,\forall x\,A(x)}}$
∃
Left: ${\dfrac{A(p), \Gamma\rightarrow\Delta}{\exists xA(x) ,\Gamma\rightarrow\Delta}}$ Right: ${\dfrac{\Gamma\rightarrow\Delta,A(c)}{\Gamma\rightarrow\Delta,\exists x\,A(x)}}$
In the last rules $p$ is a free variable, called an eigenvariable, which must not occur in the bottom sequent, and $c$ is called a target formula, which as already noted is restricted to $⊤$ and $⊥$.
A $G$ proof $π$ of length $n$ of a sequent $q$ is a sequence of sequents such that for all $i≤n$, $π(i)$ is either an axiom or $∃j,k<i$ s.t. $π(i)$ can be deduced from $π(j)$ and perhaps $π(k)$ using one of the Rules of Deduction, and such that $π(n)=q$. Since $n$ can be inferred from context or is unimportant, its mention will be dropped, and since all proofs will be $G$ proofs, mention of $G$ will be dropped, so we will simply speak of a proof $π$ of a sequent $q$. If $π$ is a proof, then for every sequent $q$ appearing in the sequence, there exists a sub-sequence of $π$ which is a proof of $q$.
Let $free(π)$ be the set of variables appearing free somewhere in a proof $π$, $eigen(π)$ the set of eigenvariables removed by $∀$ Right or $∃$ Left in $π$, and $var(π)$ the variables, free or bound, appearing in $π$. Clearly, $eigen(π)⊆free(π)⊆var(π)$.
In $IΔ_0+Ω_1$ it is easy to count the total number of characters in a formula $ϕ$, a sequent $q$, or a proof $π$, and this ability and certain properties about this function $tlen$ will be assumed without proof. For instance, it will be assumed without proof that if $π$ is the proof $π'$ with the sequent $q$ inferred as an additional step, i.e. if $π=π'⌢q$, then $tlen(π)≥tlen(π')+tlen(q)$.
Def 1. Define the negation normal form $ϕ^*$ of a formula $ϕ$ by recursion:
$ϕ^*=ϕ$ if $ϕ$ is atomic
$(ϕ∧ψ)^*=ϕ^*∧ψ^*$
$(ϕ∨ψ)^*=ϕ^*∨ψ^*$
$(∃xϕ(x))^*=∃x(ϕ(x))^*$
$(∀xϕ(x))^*=∀x(ϕ(x))^*$
$(¬ϕ)^*=¬ϕ$ if $ϕ$ is atomic
$(¬¬ϕ)^*$=$ϕ$
$(¬(ϕ∧ψ))^*=((¬ϕ)^*∨(¬ψ^*))$
$(¬(ϕ∨ψ))^*=((¬ϕ)^*∧(¬ψ^*))$
$(¬∃xϕ(x))^*=∀x(¬ϕ(x))^*$
$(¬∀xϕ(x))^*=∃x(¬ϕ(x))^*$
If $ϕ^*=ϕ$, then we say $ϕ$ is in negation normal form. A negation sign in $ϕ^*$ must appear directly in front of an atomic formula.
Because the $^*$ operation at most adds a negation sign before every variable, it at most doubles the total number of characters of a formula. Thus $tlen(ϕ^*)≤2(tlen(ϕ))$.
Observations 2. For any formula $ϕ$
1/ $(ϕ^* )^*=ϕ^*$
2/ $(¬(¬ϕ)^* )^*=ϕ^*$
Note the free and bound barriers do not change under $^*$, so for any formula $ϕ$, the free (or bound) variables are all the same in: $ϕ, ¬ϕ, ϕ^*,$ and $(¬ϕ)^*$.
Def 3. For a sequence of formulas $Γ=ϕ_1,ϕ_2,...,ϕ_k$ define
$¬Γ=¬ϕ_1,¬ϕ_2,...,¬ϕ_k$
$Γ^*=ϕ_1^*,ϕ_2^*,...,ϕ_k^*$
Thus $(¬Γ)^*=(¬ϕ_1 )^*,(¬ϕ_2 )^*,...,(¬ϕ_k )^*$.
When $Γ$ is the empty sequence (i.e. $k=0$), then $¬Γ$ and $Γ^*$ are also the empty sequences.
For a sequent $Γ→Δ$ define $(Γ→Δ)^*=(¬Γ)^*⌢Δ^*$.
Some basic facts will be assumed about labelled binary trees, which as with sequences can be easily represented and proved in $IΔ_0+Ω_1$. For instance, when $T_1$ and $T_2$ are finite binary trees, new finite binary trees can be formed with root $η$ and children either both $T_1$ and $T_2$, or just $T_1$. $T_1$ and (if present) $T_2$ are called child trees of the new tree. In the first case, we represent the new tree by $[η;T_1;T_2]$ and in the second $[η;T_1]$. If a tree consists just of a root $η$ and no children, represent this as $[η]$. If $η$ is labelled $ϕ$, we may abuse notation and write $[ϕ;T_1;T_2]$ and $[ϕ;T_1]$ and $[ϕ]$. We say that the size of a binary tree $T$ is the number of its nodes and write $size(T)$.
Def 4. A semantical tree or semtree $T$ is a finite binary tree labelled with formulas such that:
1/ The root of $T$ is labelled with a formula $ϕ$ in negative normal form
2/ The leaves of $T$ are each labelled with some atomic formula or its negation
3/ The possible branches with their labels are as follows:
Split: Parent: $ψ$ Children: $ψ$ and $ψ$
$∧$ : Parent: $(ψ_1∧ψ_2)$ Children: $ψ_1$ and $ψ_2$
$∨$ : Parent: $(ψ_1∨ψ_2)$ Children: $ψ_1$ and $ψ_2$
$∃$ : Parent: $∃xψ(x)$ Child: $ψ(c)$, where $c$ is either $⊤$ or $⊥$
$∀$ : Parent: $∀xψ(x)$ Child: $ψ(E)$, where $E$ is some variable
4/ If a variable $E$ is introduced via a $∀$ branch, it is so introduced in the entire tree exactly once, and does not occur (free or bounded) in $ϕ$
Set $root(T)$ to the formula labelling the root of $T$. $T$ is said to be a semtree for $ϕ$ if $root(T)=ϕ^*$.
Observe no explanation is given for a parent of the form $¬ψ$, since in formulas in negation normal form, $¬$ may only occur before an atomic formula. This omission forces formulas of the form $¬ψ$ to be the labels of leaves.
If a variable appears in a semtree $T$, it must appear either free in the formula labelling the root, or be introduced (once and only once) via a $∀$ branch, or be a dummy variable appearing after a quantification sign. Set $free(T)$ to be the set of the first, $intro(T)$ for the second, and $bnd(T)$ for the third. By condition 4/ and the condition on free and bounded variables in formulas, $free(T)$, $intro(T)$, and $bnd(T)$ must be pairwise disjoint. Also set $var(T)=free(T)∪intro(T)$ and $var^+ (T)=var(T)∪bnd(T)$. Clearly, if a variable appears in a leaf, it must belong to $var(T)$.
Prop 5. Let $ϕ$ be a formula in negation normal form, $v$ a set of variables such that $(free(ϕ)∪bnd(ϕ))∩v=∅$. Suppose the number $n$ of elements of $v$ equals the number of universal quantifiers in $ϕ$. Then there exists a semtree $T$ for $ϕ$ with size $≤tlen(ϕ)$ such that $intro(T)=v$. Also, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ)$.
Proof:
Suppose $ϕ$ is an atomic formula or its negation. Then $n=0$ and $v=∅$. Set $T=[ϕ]$.
Suppose $ϕ$ is of the form $(ϕ_1∨ϕ_2)$ or $(ϕ_1∧ϕ_2)$, and partition $v$ into two sets $v_1$ and $v_2$ in any way, such that for both $i=1,2$ the number $n_i$ of elements of $v_i$ equals the number of quantifiers in $ϕ_i$. By the induction hypothesis, for both $i=1,2$ there exists a semtree $T_i$ for $ϕ_i$ with size $≤tlen(ϕ_i)$ such that $intro(T_i)=v_i$ and, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ_i)$. Then set $T=[ϕ;T_1;T_2]$.
Suppose $ϕ$ is of the form $∃xϕ_1(x)$. Then $ϕ_1(⊤)$ will have the same number of universal quantifiers as $ϕ$. By the induction hypothesis, there exists a semtree $T_1$ for $ϕ_1(⊤)$ with size $≤tlen(ϕ_1(⊤))$ such that $intro(T_1)=v$ and, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ_1(⊤))$. Then set $T=[ϕ;T_1]$.
Finally suppose $ϕ$ is of the form $∀xϕ_1 (x)$. Choose any element $E∈v$, and set $v^-=v∖{E}$. Then the number of elements of $v^-$ equals the number of universal quantifiers in $ϕ_1 (E)$, so by the induction hypothesis, there exists a semtree $T_1$ for $ϕ_1(E)$ with size $≤tlen(ϕ_1(E))$ such that $intro(T_1)=v^-$ and, if $ψ$ labels a node of the tree, $tlen(ψ)≤tlen(ϕ_1(E))$. Then set $T=[ϕ;T_1]$ and note $intro(T)=intro(T')∪\{E\}=v$. //
Call some tree guaranteed by the previous proposition $\mathcal{B}(ϕ,v)$.
Def 6. An assignment $σ$ on a set of variables $v$ (perhaps empty) is a function from $v∪\{⊥,⊤\}$ to ${0,1}$ where $σ(⊤)=1$ and $σ(⊥)=0$. Let $ι$ be the assignment on the empty set, so $ι(⊤)=1$ and $ι(⊥)=0$.
An assignment $σ$ extends to the negations of atomic formulas in a natural way, using
$σ(¬ϕ)=1-σ(ϕ)$
Thus any assignment on a set $v$ with $var(T)⊆v$ can be extended to all the leaves of a semtree $T$. It can then be extended to the entire tree as follows, where $ϕ$ is the parent and $ψ_1$ and $ψ_2$ are the children (in the case of Split, $∨$, and $∧$) or $ψ$ is the child (in the case of $∃$ and $∀$).
Split$: σ(ϕ)=σ(ψ_1)+σ(ψ_2)-σ(ψ_1)σ(ψ_2)$
$∧ : σ(ϕ)=σ(ψ_1)σ(ψ_2)$
$∨ : σ(ϕ)=σ(ψ_1)+σ(ψ_2)-σ(ψ_1)σ(ψ_2)$
$∃ : σ(ϕ)=σ(ψ)$
$∀ : σ(ϕ)=σ(ψ)$
When $η$ is a node of $T$ and $σ$ is an assignment, set $σ_T(η)$ to the value assigned to that node when $σ$ is extended as just described. Set $val_σ(T)=σ_T(η)$, where $η$ is the root node of $T$.
Observation 7. Let $T$ be a semtree, and let $σ,σ'$ be assignments on $v_1,v_2$ respectively, where $var(T)⊆v_1,v_2$. Suppose $σ↾var(T)=σ'↾var(T)$. Then $σ_T(η)=σ'_T(η)$ for any node $η$ of $T$ and in particular $val_σ(T)=val_{σ' }(T)$.
Def 8. Let $T$ and $T'$ be semtrees. We say $T$ and $T'$ are separate if $free(T)∪free(T')$, $intro(T)$, and $intro(T')$ are pairwise disjoint.
Observations 9.
(1) If $[η;T_1;T_2]$ is a semtree, then $T_1,T_2$ are separate.
(2) If $T$ and $[η;T_1]$ are separate, then so are $T,T_1$. And if $T$ and $[η;T_1;T_2]$ are separate, then so are both $T,T_1$ and $T,T_2$.
(3) If $T$ and $T'$ are separate, then $var(T)∩var(T')=free(T)∩free(T')$.
Def 10. Write $ϕ∼ψ$ if $ϕ^*=(¬ψ)^*$.
Def 11. Let $T$ and $T'$ be semtrees. Write $T∼T'$ if $root(T)∼root(T')$.
Observations 12. If $T∼T'$, then $free(T)=free(T')$. So if in addition $T$ and $T'$ are separate, then $var(T)∩var(T')=free(T)$.
Def 13. Let $T$ be a semtree, $X∈free(T)$, and $c$ a constant. Write $T[X/c]$ for the tree $T$ with every free occurrence of $X$ replaced by $c$.
Observations 14. If $T$ is a semtree, $X∈free(T)$, and $c$ a constant, then $T[X/c]$ is a semtree. If in addition $root(T)=ϕ(X)$, then $root(T[X/c])=ϕ(c)$.Suppose further $σ$ is an assignment on $var(T)$ and that $i=σ(X)$. $i=0$ or $1$, so there exists a constant $c$ such that $ι(c)=σ(X)$. For this $c$, $val_σ(T)=val_σ (T[X/c])$.
Def 15. Let $T$ and $T'$ be semtrees with $free(T)=free(T')$. $T$ and $T'$ are jointly satisfiable if there exists an assignment $σ$ on $var(T)∪var(T')$ such that for all assignments $τ$ on $var(T)∪var(T')$, if $τ↾free(T)=σ↾free(T)$, then $val_τ(T)=val_τ(T')=1$.
Observation 16. Suppose $T$ and $T'$ are jointly satisfiable. Then there exists an assignment $σ$ on $var(T)∪var(T')$ such that $val_σ(T)=val_σ(T')=1$.
Def 17. Let $T$ be a semtree, and let U $= U_0,U_1,...,U_k$ be a sequence of semtrees where $U_0=T, U_k$ is a branchless tree (i.e. has only one node), and for all $i$ with $0≤i<k$ either:
$U_{i+1}$ is a child tree of $U_i$, or
$∃V$ such that $V$ is a child tree of $U_i$ and for some free variable $E$ and some constant $c$, $U_{i+1} =V[E/c]$.
Call U a root-to-leaf analysis of $T$. Say that a subsequence $S_0,S_1,...,S_j$ of U is Split-cleaned if for all $i$ with $0≤i≤k, U_i$ does not appear in the sub-sequence if and only if the root of $U_i$ is a Split branch.
Observation 18. In the context of the previous definition, the root of $U_k$ cannot be a Split branch, so $S_j=U_k$.
Theorem 19. Let $T$ and $T'$ be separate semtrees with $T∼T'$. And suppose $T$ and $T'$ are jointly satisfiable. Then there exist a root-to-leaf analysis U = $U_0,U_1,...,U_k$ of $T$ and a root-to-leaf analysis U' $= U'_0,U'_1,...,U'_{k' }$ of $T'$, and Split-cleaned subsequences $S_0,S_1,...,S_j$ of U and $S'_0,S'_1,...,S'_j$ of U' such that for all $i$ with $0≤i≤j$
1/ $S_i$ and $S'_i$ are separate
2/ $S_i ∼ S'_i$
3/ $S_i$ and $S'_i$ are jointly satisfiable.
Pf:
If $T$ and $T'$ are branchless trees (i.e. with only one node), the conclusion is obvious.
Split branch.
Suppose the root of either $T$ or $T'$ is a Split branch, WLOG the root of $T$. Then $T$ is of the form $[ϕ;T_1;T_2]$, where $T_1$ and $T_2$ are also semtrees with roots labelled $ϕ$. Set $f=free(T)$. Note for both $i=1,2$, $free(T_i)=f$, so $var(T_i)=f∪intro(T_i)$, and $T_i,T'$ are separate.
Let $σ$ be an assignment on $var(T)∪var(T')$ such that for all assignments $τ$ on $var(T)∪var(T')$ with $τ↾f=σ↾f$, $val_τ(T)=val_τ(T')=1$.
Suppose $T_1$ and $T'$ are not jointly satisfiable. Then there exists assignment $μ$ on $var(T_1)∪var(T')$ with $μ↾f=σ↾f$ but $val_μ(T_1)=0$ or $val_μ(T')=0$. Since $μ↾f=σ↾f$, $val_μ(T')=1$. This forces $val_μ(T_1)=0$.
Let $τ'$ be an assignment on $var(T_2)∪var(T')$ with $τ'↾f=σ↾f$.
Set
$σ'=ι∪τ'↾(f∪intro(T_2)∪intro(T'))∪μ↾intro(T_1)$.
Because of separateness $σ'$ is a well-defined assignment on $var(T)∪var(T')$. $σ'↾f=τ'↾f=σ↾f=μ↾f$, so $val_{σ'}(T)=val_{σ'}(T')=1$. Since $σ'↾intro(T_1)=μ↾intro(T_1)$ also $val_{σ' }(T_1)=0$. By the definition of assignment on a Split branch, $val_{σ'}(T_2)=1$. Thus $val_{τ'}(T_2)=1$. Hence $T_2$ and $T'$ are jointly satisfiable.
So either $T_1,T'$ or $T_2,T'$ are jointly satisfiable. The other conditions are trivial, so one of these pairs satisfies the conditions of the theorem, with one less node, so apply the induction hypothesis, and prefix $T$ to the unprimed root-to-leaf analysis. The Split-cleaned subsequences remain the same since the root of $T$ is a Split branch.
Henceforth, suppose the roots of both $T$ and $T'$ are not Split branches.
$∨$ branch.
Suppose the root of $T$ is a $∨$ branch. Then $T$ is of the form $[(ϕ_1∨ϕ_2);T_1;T_2]$, where $T_1$ and $T_2$ are also semtrees, with roots labelled $ϕ_1,ϕ_2$ respectively, and $T'$ is of the form $[(ψ_1∧ψ_2);T'_1;T'_2]$, where $T'_1$ and $T'_2$ are also semtrees, with roots labelled $ψ_1,ψ_2$ respectively, such that $ϕ_1∼ψ_1$ and $ϕ_2∼ψ_2$. Note $T_i,T'_j$ are separate for any $i,j=1,2$.
Set $f=free(T)$, $f_1=free(T_1)$, and $f_2=free(T_2)$. Note $f=free(T')$, $f_1=free(T'_1)$, $f_2=free(T'_2)$, and $f=f_1∪f_2$.
Let $σ$ be an assignment on $var(T)∪var(T')$ such that for all assignments $τ$ on $var(T)∪var(T')$ with $τ↾f=σ↾f$, $val_τ(T)=val_τ(T')=1$.
If $T_1, T'_1$ are jointly satisfiable, apply the induction hypothesis, and prefix $T_1$ and $T'_1$ to the resulting sequences.
Otherwise assume $T_1,T'_1$ are not jointly satisfiable. Then there exists assignment μ on $var(T_1)∪var(T'_1)$ with $μ↾f_1=σ↾f_1$ but $val_μ(T_1)=0$ or $val_μ (T'_1)=0$. Let $τ'$ be an assignment on $var(T_2)∪var(T'_2)$ with $τ'↾f_2=σ↾f_2$. Note $μ↾(f_1∩f_2)=τ'↾(f_1∩f_2)$.
Set $σ'=ι∪μ∪τ'$, which is well-defined since by separateness,
$(var(T_1)∪var(T'_1))∩(var(T_2)∪var(T'_2)))=f_1∩f_2$.
$σ'↾(f_1∪f_2)=σ↾(f_1∪f_2)$, so $val_{σ'}(T)=val_{σ'}(T')=1$. By the definition of an assignment on an $∧$ branch, both $val_{σ'}(T'_1)=1$ and $val_{σ'}(T'_2)=1$. Thus $val_μ(T'_1)=1$, which forces $val_μ(T_1)=0$, and so $val_{σ'}(T_1)=0$. By the definition of an assignment on an $∨$ branch, this forces $val_{σ'}(T_2)=1$. Thus $val_{τ'}(T_2)=1$. Hence $T_2$ and $T'_2$ are jointly satisfiable. Apply now the induction hypothesis, and prefix $T_2$ and $T'_2$ to the resulting sequences.
$∧$ branch.
By symmetry.
$∃$ branch.
Suppose the root of $T$ is an $∃$ branch. Then $T$ is of the form $[∃xϕ(x);T_1]$, where $T_1$ is a semtree, with root labelled $ϕ(c)$ for some constant $c$, and $T'$ is of the form $[∀xψ(x);T'_1]$, where $T'_1$ is a semtree, with root labelled $ψ(E)$ for some variable $E∈intro(T')$ where $E∉free(ψ(x))$ and $E∉var(T)$. Clearly, $ϕ(c)∼ψ(c)$.
Set $f=free(T)$ and $v=var(T)∪var(T')$ and $v-=v∖{E}$. Note $f=free(T')$ and $f=free(T_1)$ and $f∪{E}=free(T'_1)$, where $E∉f$.
Since $T,T'$ are jointly satisfiable, there is an assignment $σ$ on $v$ s.t. for all assignments $τ$ on $v$ with $τ↾f=σ↾f$, $val_τ(T)=val_τ(T')=1$. Set $T''_1=T'_1[E/c]$ and $σ'=ι∪σ↾v-$. Note $f=free(T''_1)$ and $v-=var(T_1)∪var(T''_1)$ and $σ'$ is an assignment on $v-$. Let $τ'$ be an assignment on $v-$ s.t. $τ'↾f=σ'↾f$. Set $τ''$ to $τ'∪\{(E,ι(c))\}$. Then $τ''$ is an assignment on $v$ s.t. $τ''↾f=σ↾f$. So $val_{τ''}(T)=val_{τ''}(T')=1$. But then $val_{τ''}(T_1)=1$ and $val_{τ''}(T'_1)=1$. The latter conjunct, along with the observation that $τ''(E)=ι(c)$, implies $val_{τ''}(T''_1)=1$, so $val_{τ'} (T_1)=1$ and $val_{τ'}(T''_1)=1$. Thus $T_1$ and $T''_1$ are jointly satisfiable, and clearly $T_1∼T''_1$. Apply now the induction hypothesis, and prefix $T_1$ and $T''_1$ to the resulting sequences.
$∀$ branch.
By symmetry. //
Corollary 20. Let $T,T'$ be separate semtrees with $T∼T'$. Then $T,T'$ are not jointly satisfiable.
Pf:
Suppose they were jointly satisfiable. By the previous theorem there are semtrees $U,U'$ s.t. both are branchless, $U∼U'$, and $U,U'$ are jointly satisfiable. By the first and second conditions, the roots of $U$ and $U'$ must be labelled by $E$ and $¬E$, for some atomic formula $E$. By the third condition there exists $σ$ on $free(U)$ such that $val_σ(U)=val_σ(U')=1$. But this is impossible. //
Def 21. Let $t = T_1,...,T_k$ be a sequence of semtrees. Set $val_σ(t)=1$ if $∃i(val_σ(T_i)=1)$, and $=0$ otherwise. If $val_σ(t)=1$ for all assignments $σ$ on $∪_{i=1}^m var(T_i)$, write $val(t)=1$.
Note if $k=0$, then $val(t)=0$.
Theorem 22. Suppose $π$ is a tree-like proof where every instance of a free variable is as an eigenvariable. Let $w$ be the number of applications of weakening in $π$, let $β_i$ be the formula introduced by the $i$th weakening according to some fixed ordering, and let $w_i$ be the number of universal quantifiers in $β_i$ ($1≤i≤w$). Let $z_1,...,z_w$ be a set of pairwise disjoint sets of variables such that the number of elements in each $z_i$ equals $w_i$ and such that $z_i∩var(π)=∅$. For any sub-proof $π'$ of $π$, set $weak(π') =⋃z_i$, where the union is taken over every $i$ such that the $i$th weakening occurs in $π'$.
Let $q$ be a sequent in the proof sequence of $π$, where $q=Γ→Δ=ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$. And let $q*=ψ_1,...,ψ_m$. Also let $π_1$ be the sub-proof of $q$ in $π$. Then there exists a sequence of semtrees $t=T_1,T_2,...,T_m$ such that:
1/ each $T_i$ is a semtree for $ψ_i$
2/ $val(t)=1$
3/ $∑_{i=1}^m size(T_i)≤tlen(π_1)$
4/ For all $i,j(i≠j)$, $T_i$ and $T_j$ are separate
5/ $intro(T_i)⊆eigen(π_1)∪weak(π_1)$ for all $i$
6/ If $ϕ$ is a label of a node of $T_i$ then $tlen(ϕ)≤tlen(ψ_i)$ for all $i$
Proof:
We show how to construct a semtree satisfying the six conditions for each axiom and rule of deduction, by induction on the steps of $π_1$ bounded by the proof $π$.
Case 1. $q=A→A$, for atomic formula $A$. Note $(A→A)*=<¬A,A>$. Let $T_1$ be the semtree with root labelled $¬A$ and no children, $T_2$ the semtree with root labelled $A$ and no children. Setting $t=T_1,T_2$, clearly $val_σ (t)=1$ for all assignments on $var(T_1)$. If $π_1$ is a proof of $q$, $π_1$ must contain $q$, so $tlen(π_1)≥3≥(1+1)=size(T_1)+size(T_2)$. Finally, $T_1, T_2$ are vacuously separate.
Case 2. $q=⊥→$ or $q=→⊤$. Then $q*=<¬⊥>$ or $q*=<⊤>$. Both have trivial semtrees of size 1 with only a root, the root labelled either $¬⊥$ or $⊤$. All conditions 1/ through 6/ are easily seen to hold.
For the induction cases, by appropriate substitutions which do not increase the length of the number of characters in the proof, we may assume that every eigenvariable appearing in $π$ is eliminated exactly once via $∀$-left or $∃$-right.
Case 3. Weakening Left. Suppose $π_1=π_1'⌢<A,Γ→Δ>$, where $π_1'$ contains the sequent $Γ→Δ$. Let this be the $k$th weakening.
Obviously, the $k$th weakening is not present in $π_1'$.
Let $q'=Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$. Note $q^*=<(¬A)^*>⌢(q')^*$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Set $T_0=\mathcal{B}((¬A)^*,z_k)$ from Proposition 5 and $t=T_0⌢t'$.
Trivially $val(t)=1$ since $val(t')=1$.
$size(T_0)≤tlen((¬A)^*)$, so
$∑_{i=0}^m size(T_i)≤tlen(π_1')+tlen((¬A)^*)≤tlen(π_1)$.
$intro(T_i)⊆eigen(π_1')∪weak(π_1')$ for all $i(1≤i≤m). intro(T_0)=z_k$, and by assumption $z_k∩var(π)=∅$. So $z_k∩eigen(π_1')=∅$. And since the $k$th weakening is not present in $π_1'$, $z_k∩weak(π_1')=∅$. Thus $intro(T_0)∩intro(T_i)=∅$ for all $i(1≤i≤m)$. Moreover, $z_k∩free(ϕ_i)=∅$ for all $i(1≤i≤m)$, since $free(ϕ_i)⊆var(π)$.Finally, suppose $E∈free(T_0)∩intro(T_i)$ for some $i(1≤i≤m)$. $E∈free(T_0)$ implies $E∈free(A)$, so $E$ appears in the last step of the sub-proof $π_1$. By assumption this instance of $E$ must as an eigenvariable. So if $E∈eigen(π_1')$, then $E$ is eliminated twice as an eigenvariable in $π$, a contradiction. Hence $E∈weak(π_1')$, but this contradicts each of the $z_i$ being disjoint from $var(π)$. Thus $T_0$ and $T_i$ are separate for all $i≠0$.
If $ϕ$ is the label of a node of $T_0$, then $tlen(ϕ)≤tlen((¬A)^*)$.
Case 4. Weakening Right.
As Weakening Left.
Case 5. Exchange.
Trivial.
Case 6. Contraction Left. Suppose $π_1=π_1'⌢<Γ,A→Δ>$, where $π_1'$ contains the sequent $Γ,A,A→Δ$.
Let $q'=Γ,A,A→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_{k-1}=ϕ_k=A$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Define $T'=[(¬A)^*;T_{k-1};T_k]$ with $(¬A)^*$ being a Split branch, and set $t=T_1,...,T_{k-2},T',T_{k+1},...,T_m$.
Case 7. Contraction Right.
As Contraction Left.
Case 8. $¬$ Left.
Trivial since $(¬¬A)^*=A^*$, so $(¬A,Γ→Δ)^*$ simply reorganizes the order of the sequence $(Γ→Δ,A)^*$.
Case 9. $¬$ Right.
Also trivial.
Case 10. $∧$ Left. Suppose $π_1=π_1'⌢<(A∧B),Γ→Δ>$, where $π_1'$ contains the sequent $A,B,Γ→Δ$.
Let $q'=A,B,Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_1=A$ and $ϕ_2=B$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Define $T'=[(¬(A∧B))^*;T_1;T_2]$, where the root is an $∨$ Branch, and set $t=T',T_3,...T_m$.
Case 11. $∧$ Right. Suppose $π_1=π_A'⌢π_B'⌢Γ→Δ,(A∧B)$, where $π_A'$ contains the sequent $Γ→Δ,A$ and $π_B'$ the sequent $Γ→Δ,B$.
Because $π$ is a tree-like proof, $π_A'$ and $π_B'$ are disjoint.
Let $q_A'=Γ→Δ,A = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},A$ and let $q_B'=Γ→Δ,B = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},B$. Also let $q_A^*=ψ_1,...,ψ_{m-1},A^*$ and $q_B^*=ψ_1,...,ψ_{m-1},B^*$. Suppose $u=U_1,U_2,...,U_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_A',u$. Further suppose $v=V_1,V_2,...,V_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_B',v$. For $1≤i≤m-1$ set $T_i=[ψ_i;U_i;V_i]$ where the root is a Split Branch, and set $T_m=[(A^*∧B^*);U_m;V_m]$. The number of new nodes is $m$, less than the length of the sequent. By assumption $intro(U_i)⊆eigen(π_A')∪weak(π_A')$ and $intro(V_i)⊆eigen(π_B')∪weak(π_B')$, for $i(1≤i≤m)$. But $π_A',π_B'$ are disjoint, so $eigen(U_i)∩eigen(V_j)=∅$ to prevent eigenvariables being eliminated twice in the proof $π$. Also because $π_A',π_B'$ are disjoint, $weak(π_A')∩weak(π_B')=∅$. $eigen(π_A')∩weak(π_B')=∅$ by construction of the $z_i$, and similarly $eigen(π_B')∩weak(π_A')=∅$. Thus $intro(U_i)∩intro(V_j)=∅$ for all $i,j(1≤i,j≤m)$. If $E∈free(V_i)$ for some $i(1≤i≤m)$, then $E∈free(π_B')$ and must then be an instance of an eigenvariable in $π$. But then $E∉eigen(π_A')$. Also $E∉weak(π_B')$ by construction of the $z_i$. So $E∉intro(U_i)$ for any $i$. Thus all the $U_i,V_j$ are pairwise separate, and so the $T_i$ are pairwise separate.
Case 12. $∨$ Left and Right.
As $∧$ Right and Left.
Case 13. Cut. Suppose $π_1=π_1'⌢Γ→Δ$, where $π_R'$ contains the sequent $Γ→Δ,A$ and $π_L'$ contains the sequent $A,Γ→Δ$.
Let $q_R'=Γ→Δ,A = ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1},A$ and let $q_L'=A,Γ→Δ = A,ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_{m-1}$. Also let $q_R^*=ψ_1,...,ψ_{m-1},A^*$ and $q_L^*=(¬A)^*,ψ_1,...,ψ_{m-1}$. Suppose $u=U_1,...,U_{m-1},U_R$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_R',u$. And suppose $v=V_L,V_1,...,V_{m-1}$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q_L',v$. Note that $U_R∼V_L$ and the pair $U_R,V_L$ are separate by the same argument as used in $∧$ Right. For $1≤i≤m-1$ set $T_i=[ψ_i;U_i;V_i]$ where the root is a Split Branch, and set $t=T_1,T_2,...,T_{m-1}$. Set $v=∪_{i=1}^{m-1} var(T_i)$, $v'=var(U_R)∪var(V_L)$, $v+=v∪v'$, and $f=free(U_R)$. $f=free(V_L)$, so $v'=f∪intro(U_R)∪intro(V_L)$. By separateness, $(intro(U_R)∪intro(V_L))∩v=∅$, so
$intro(U_R)∪intro(V_L)⊆v+∖v⊆v+$.
Suppose $val(t)≠1$. Then $val_μ (t)=0$ for some assignment $μ$ on $v$. Extend $μ$ to $v+$ in any way and call this new assignment $σ$. Still $val_σ(t)=0$. But $val(u)=val(v)=1$, so $val_σ(u)=val_σ(v)=1$, so $val_σ(U_R)=val_σ(V_L)=1$. Let $τ$ be an assignment on $v+$ such that $τ↾f=σ↾f$. Set τ'=ι∪τ↾(v+∖v)∪σ↾v, an assignment on v+. So val_(τ' ) (u)=val_(τ' ) (v)=1. Obviously $τ'↾v=σ↾v$, so $val_(τ')(t)=0$. Thus $val_(τ')(U_R)=val_(τ')(V_L)=1$. By construction $τ'↾v'=τ↾v'$, so $val_τ (U_R)=val_τ (V_L)=1$. Therefore $U_R,V_L$ are jointly satisfiable, contradicting Corollary 20. Thus $val(t)=1$.
Case 14. ∀ Left. Suppose $π_1=π_1'⌢∀xA(x),Γ→Δ$, where $π_1'$ contains the sequent $A(c),Γ→Δ$ with $c$ a constant.
Let $q'=A(c),Γ→Δ= ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_1=A(c)$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Set $T'=[(¬∀xA(x))*;T_1]$ and $t=T',...,T_m$. Note $(¬∀xA(x))^*=∃x(¬A(x))^*$, so the root of $T'$ is a $∃$ branch, and so $T'$ is indeed a semtree.
Case 15. $∀$ Right. Suppose $π_1=π_1'⌢Γ→Δ,∀xA(x)$, where $π_1'$ contains the sequent $Γ→Δ,A(p)$ with $p$ a variable not appearing in $Γ$ or $Δ$.
Let $q'=Γ→Δ,A(p)=ϕ_1,...,ϕ_k→ϕ_{k+1},...,ϕ_m$, with $ϕ_m=A(p)$. Suppose $t'=T_1,...,T_m$ is a sequence of semtrees satisfying conditions 1/ through 6/ for $q',t'$. Set $T'=[(∀xA(x))^*;T_m]$ and $t=T_1,...,T_{m-1},T'$. Note $(∀xA(x))^*=∀x(A(x))^*$, so the root of $T'$ is a $∀$ branch, and so $T'$ is indeed a semtree. $p$ can only be used as an eigenvariable once, so $p∉eigen(π_1')$. Let $1≤i≤m-1$. $p∉weak(π_1')$ by construction of the $z_i$, so $p∉intro(T_i)$. Also $p∉free(T_i)$ because $free(T_i)=free(ϕ_i)$.Thus $T'$ is separate from each of the $T_i$ (where $1≤i≤m-1$).
Set $v=∪_{j=1}^m var(T_j)$. Note $v=∪_{j=1}^{m-1} var(T_j)∪var(T')$ since $var(T_m)=var(T')$. Let $σ$ be an assignment on $v$. Then by assumption, $val_σ(t')=1$. If $val_σ(T_j)=1$ for some $j(1≤j≤m-1)$, then $val_σ(t)=1$. Otherwise $val_σ(T_m)=1$, so by the definition of an assignment on a $∀$ branch, $val_σ(T')=1$, in which case again $val_σ(t)=1$.
Case 16. $∃$ Left and Right.
As $∀$ Right and Left. //
Take the contradictory sequent to be the empty sequent,$ → $.
Corollary 23. There is no proof of a contradiction.
Pf:
Suppose $π$ is a proof. It may be assumed that all free variables are eigenvariables, because if a free variable were not an eigenvariable, it would have to be eliminated by Cut. But then it could be replaced throughout the proof by a constant.
Let $e$ be the empty sequence. Then $( → )^* = e$. By the theorem, $val(e)=1$. But $val(e)=0$. //