Can FPA really prove its consistency?

Question

I will ask the question first and then explain.

QUESTION: FPA can prove its own consistency in the Godelian sense. But can it really prove its consistency?

FPA is a multi-sorted first-order theory, with lower-case or small letters (for numbers) and upper-case or big letters for relations of n-arity (n >= 1). (Practically, I think one can limit the theory to relations where n = 1, 2, or 3.)

Full comprehension is assumed.

FPA has a constant symbol 0, a 1-ary relationship N (natural number), and a 2-ary relationship symbol S (successoring).

In this context the Peano Axioms can be written:

(PA1) N0
(PA2) $\forall$n (Nn $\Rightarrow$ $\exists$m (Nm & Sn,m))
(PA3) $\forall$n$\forall$m$\forall$m' (Nn & Nm & Nm' & Sn,m & Sn,m' $\Rightarrow$ m = m')
(PA4) $\forall$n$\forall$m$\forall$n' (Nn & Nm & Nn' & Sn,m & Sn',m $\Rightarrow$ n = n')
(PA5) $\forall$n (Nn $\Rightarrow$ $\neg$ Sn,0)
(PA6) $\forall$P (P0 & $\forall$n$\forall$m(Pn & Sn,m $\Rightarrow$ Pm) $\Rightarrow$ $\forall$n(Nn $\Rightarrow$ Pn))

FPA assumes all the Peano Axioms except (PA2), that is, everything except the totality of the successor relationship. It has as its standard models all the initial segments as well as the standard model of the natural numbers. {0} is a model. It is therefore agnostic as to whether the natural numbers go on and on.

In FPA it is possible to define formula for addition, multiplication, less than, exponentiation, and, except obviously for totality and any related property, prove the usual properties. Intuitively, the existence of a natural number n implies that every number less than n exists.

Predicates for numbers can be defined:
one(n) if and only if S0,n & Nn,
two(n) if and only if $\exists$x (one(x) & Sx,n) & Nn
Obviously one cannot prove there exists any n such that one(n). But if such an n exists, then one can show it has all the usual properties of 1. Similarly for two, three, etc.

FPA proves the Fundamental Theorem of Arithmetic.

Recursion is available and it is possible to define formula expressing syntax in the Godel fashion. For instance, Term1(n) ("n is a lower-case term") might be defined as: seven(n) $\vee$ $\exists$y$\exists$z (+(y,y,n) & eleven(z) & z >= n). (Seven(n) expresses n is 0, and the lower-case variables are the even numbers >= eleven.)

One can continue and define a formula GProof(n,x) which says that n is the Godel number of a proof in FPA of a wff whose Godel number is x. Letting $\mathcal{F}$ be "$\neg$ 0 = 0", then GCons(FPA) is the formula:
$\neg$ $\exists$p (GProof(p,$\mathcal{F}$))

But FPA proves GCons(FPA). Intuitively the reasoning goes like this. Suppose $\neg$ GCons(FPA). Then there is a number p such that GProof(p,$\mathcal{F}$). But, because of the nature of Godelization, and its use of a single number to represent sequences of numbers via exponentiation, this is a very big number, easily bigger than what is required to define "true in {0}" for all propositions of length smaller than the propositions in the purported proof. FPA can show the axioms are true in {0}, that the deduction rules preserve truth in {0} for all steps in the proof, but of course $\mathcal{F}$ is not true in {0}. Contradiction, so FPA proves GCons(FPA).

Well this does seem like a bit of a cheat, because it uses the fact that Godelization, by using numbers to represent sequences, needs very big numbers. Instead of lower-case numbers to code a sequence, one can use upper-case letters: R is a sequence if and only if dom(R) is {x : x <= n} for some natural number n. One can then redefine a formula RProof(R,S) which says that R is a sequence representing a proof of the proposition represented by the sequence S. And define a new formula RCons(FPA).

The question is: does FPA prove RCons(FPA)?

The proof for the Godelization formula doesn't go through because now only a small number (the length of the proof) is implied, and this is not enough, at least prime facie, to construct a model of true-in-{0} for the propositions in the proof. To show that FPA proves RCons(FPA), it would suffice to show that any proof of an inconsistency would have to be very, very long. To show that FPA doesn't prove RCons(FPA), maybe Godel's original proof would go through, but this makes me nervous, because of the problem with GCons(FPA).

Sorry for the long question, but any help appreciated!

Answer 1

In principle, the answer can depend on the proof system, but as long as you stick to some of the usual Hilbert-style or sequent proof systems, this shouldn’t matter.

First, as explained in https://mathoverflow.net/questions/120106, the question is equivalent to provability of the consistency of FPA in $I\Delta_0+\Omega_1$. (The fact that you are using second order objects to encode proofs and formulas corresponds to using all numbers instead of just the logarithmically small ones in $I\Delta_0+\Omega_1$, hence you end up with the usual consistency statement.)

Now, working in $I\Delta_0+\Omega_1$ (or equivalently, Buss’s $S_2$), the consistency of FPA is equivalent to the consistency of the second-order theory of the model with one-element first-order universe (in whatever finite language, it’s all equivalent), since the two theories are interpretable in each other. This in turn can be reduced to the quantified propositional calculus: since there is only one first-order element (and only one $n$-tuple of elements for every $n$), you can ignore first-order quantifiers and variables, and replace second-order variables with propositional variables both in second-order quantifiers and in atomic formulas. (Purely first-order atomic formulas such as $t=s$ can be replaced with the constant $\top$ for truth.) Thus, the question becomes whether $I\Delta_0+\Omega_1$ proves the consistency of the quantified propositional calculus ($G$).

The answer is that this is one of the major open problems in the area, but it is conjectured to be false. There is a kind of correspondence of subsystems of bounded arithmetic to propositional proof systems; in particular, the fragments $T^i_2$ of $S_2$ (${}=I\Delta_0+\Omega_1$) correspond to the fragments $G_i$ of the quantified propositional calculus, obtained by restricting all formulas in the proof (or alternatively, all cut formulas in the sequent calculus formulation) to $\Sigma^q_i$ or $\Pi^q_i$ formulas (= formulas in prenex form with at most $i$ quantifier blocks). This means:

• $T^i_2$ proves the consistency (and even some form of reflection principle) of $G_i$.

• Conversely, $\mathrm{Con}_{G_i}$ implies over a weak base theory all $\forall\Delta^b_1$-consequences of $T^i_2$ (and more complex consequences of $T^i_2$ can be axiomatized by an appropriate reflection principle). A related fact is that if $T^i_2$ proves a $\forall\Sigma^b_i$ statement, one can translate it into a sequence of quantified propositional tautologies which will have polynomially bounded proofs in $T^i_2$.

• If $P$ is any propositional proof system whose consistency is provable in $T^i_2$, then $G_i$ polynomially simulates $P$.

$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.

The correspondence of theories and propositional proof systems also extends to complexity classes. Sets definable by $\Sigma^b_i$ formulas in the standard model of arithmetic are exactly those computable in the $i$-level $\Sigma^P_i$ of the polynomial hierarchy. The theories $T^i_2$ have induction for $\Sigma^b_i$ formulas, and their provably total $\Sigma^b_{i+1}$-definable functions are $\mathrm{FP}^{\Sigma^P_i}$, so these theories correspond to levels of the polynomial hierarchy. On the propositional side, satisfiability of $\Sigma^q_i$ formulas is a $\Sigma^P_i$-complete problem. Taking the union, $S_2$ corresponds to the full polynomial hierarchy $\mathrm{PH}$. However, the complexity class corresponding to $G$ is $\mathrm{PSPACE}$, as satisfiability of unrestricted quantified propositional formulas is $\mathrm{PSPACE}$-complete. Thus, asking $S_2$ to prove the consistency of $G$ is in the same spirit as collapsing $\mathrm{PSPACE}$ to $\mathrm{PH}$ (and therefore to some its fixed level). (Don’t quote me on this. While the collapse of the $T^i_2$ hierarchy does imply the collapse of $\mathrm{PH}$, for propositional proof systems this becomes only a loose analogy.)

In order to give also an upper bound on the consistency strength, the consistency of $G$, and therefore of FPA, is provable in theories corresponding to $\mathrm{PSPACE}$. The best known such theory is Buss’s theory $U^1_2$, which is a “second-order” extension of $S_2$ with comprehension for bounded sets defined by bounded formulas without second-order quantifiers, and length induction for bounded $\Sigma^1_1$-formulas. Notice that things get really messy here, as the first-order objects of $U^1_2$ correspond to second-order objects of FPA, and second-order objects of $U^1_2$ have no analogue in FPA. Alan Skelley formulated an equivalent (technically, RSUV-isomorphic) theory $W^1_1$. This is syntactically a third-order arithmetic, and it is more directly comparable to FPA (as numbers of one theory correspond to numbers of the other, and sets correspond to sets). $W^1_1$ proves the consistency of $G$, and thus of FPA. 

Answer 2

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$. //

Answer 3

This is too long as a comment, but can be viewed as an Answer in that it gives a better partial answer to the question (although there won't be any justification). To best understand it you might consult my previous answer and read the comments to it.

Relax the restriction that the target formula of $\exists$-Right and $\forall$-Left must be $\top$ or $\bot$ as follows. Consider the rule

${\dfrac{\Gamma\rightarrow\Delta,A(t)}{\Gamma\rightarrow\Delta,\exists x\,A(x)}}$

provided any variable in $t$ does not occur in $\Gamma$ or $\Delta$. (Similarly for $\forall$-Left.) Notice this rule includes the cases when $t$ is $\top$ or $\bot$, since there isn't any variable in $\top$ or $\bot$. Call this new system $G-$.

I claim (not justified here) one can still establish a separability condition for semtrees for formula provable in $G-$, and so $I\Delta_0 + \Omega_1$ proves the consistency of $G-$.

The relaxation does not appear completely trivial, since variables in $t$ may occur in $\exists x\,A(x)$. So for instance, one can infer:

${\dfrac{\rightarrow x \iff x}{\rightarrow\exists y (x \iff y)}}$

So $G-$ allows the straightfoward proof of Emil's example $A_n$, so apparently $G$[where the target formula is restricted to $\top$ or $\bot$] does not polynomially simulate $G-$.

Unfortunately, Exercise VII.3.6 seems to fail irremediably, or at least I cannot see a way to repair it meaningfully. So I cannot make any claim about the strength of $G-$ compared to $G$.