of Buss’s S1 2 and S2, S1 2 S2 (?) As a corollary, P = NP (?!) I do not believe it at all, but it may contain interesting techniques or conjectures Draft: https://www.dropbox.com/s/g22x84rfdqmyx82/
PIND for Σb i -formula plus axioms Ax. 1 Ax is ﬁnite, 2 all formulas in Ax are true in the standard interpretation, 3 all formulas in Ax is quantiﬁer free, 4 Ax implies all BASICe axioms in [Buss and Ignjatovi´ c, 1995] 5 Ax implies formulas corresponding P = NP in [Takeuti, 1996] if P = NP. S2 := i=1,2,... Si 2
functions Identity axioms Substitution axiom Induction axiom PV− is a system obtained from PV by dropping induction axiom PV− 1 = PV− + ﬁrst order logic PV− 1 (D) is the restriction of PV− 1 in which the number of quantiﬁers and equations is bounded by D.
PV− with ﬁnite number D of Henkin-like quantiﬁers 2 Prove consistency of PV− q (D) in S2 3 Embed PV− 1 (D) to PV− 1 (D) in S2 4 Prove embedded PV− 1 (D) + Ax is consistent in S2 5 Prove consistency of PV− 1 (D) + Ax is not provable in S1 2 5. is modiﬁcation of [Buss and Ignjatovi´ c, 1995] Our tasks are 1-4
of 1 x(x1, . . . , xn) 2 {x}(x1, . . . , xn) in which all x are diﬀerent (but x1, . . . , xn may have overlap) x(x1, . . . , xn) is a existential quantiﬁcation which depends on x1, . . . , xn {x}(x1, . . . , xn) is a universal quantiﬁcation which depends on x1, . . . , xn A dependency matrix is almost like a Henkin quantiﬁer [Krynicki and Mostowski, 1995], but the order has meaning (to construct a semantics)
S2 plus Boolean variables and terms Additional functions bit(x, y): |y|-th bit of x p is the if-then-else function p(⊥, x, y) = x and p( , x, y) = y Boolean functions !, &, ||, →, ↔ A formula of PV− q is a form Q =⇒ φ where Q is a dependency matrix and φ is an equation Deﬁnition PV− q (D)-proofs are tree of PV− q (D)-formulas built by the following axioms and rules
Q =⇒ φ(y) Q =⇒ φ(t) Q, x(FV(t)) =⇒ φ(x) if y is not a bound variable of Q and y is a free variables of Q =⇒ φ(y) Q1, {x}(x) =⇒ φ(x) Q1 =⇒ φ(t) if FV(t) ⊆ {x}
. . Q =⇒ t = u is interpreted as a constraction of a “computation” of ξ(u) from a “computation” of ξ(t) and reverse direction, where quantiﬁers Q is interpreted by substitutions ξ
computation can be exponential, e.g. 2#2#2# · · · #2 Therefore, the proof cannot construct a computation of the lefthand from the righthand proj1 2 (0, 2#2#2# · · · #2) = 0 Solution Introduce unknown value ∗
bit(∗, ∗)? We want to interpret the value of a Boolean term as a real Boolean, not, for example, a three-valued logic, so that we can prove that ⊥ = is never derived Solution We choose the value of bit(∗, ∗) randomly, yet consistently across the same computation. For this purpose, we incorporate the evaluation of bit(∗, ∗) into an evaluation environment ρ
| ∗ | 0v | 1v Approximate relation is deﬁned as: ε ε, v ∗, v w =⇒ bv bw for b = 0, 1, If v w then w is often written as v∗. G-numerals and Boolean values are called g-values
t is a map uW → v ∈ W uB → b ∈ B = {⊥, } for subformulas of t t ∈ dom(ρ) ⇐⇒ ρ(t) is deﬁned. Deﬁnition A computational statement is a form t, ρ ↓ v where t is a term, ρ is an environment and v is a g-value.
rules: tW, ρ ↓ ∗ ∗ x, ρ ↓ v∗ Env where v = ρ(x) v, ρ ↓ v∗ v where v is a numeral t, ρ ↓ v bt, ρ+ ↓ bv∗ b where b is either 0 or 1 and t is not a numeral.
w bit(t, u), ρ ↓ b bit where b is determined by bit(ε, w) = ⊥ if w = ∗ bit(bv, ε) = b bit(bv, b w) = bit(v, w). If bit(v, w) function is undeﬁned, we often write bit(v, w) = ∗. If bit(v, w) = ∗, we put b = ρ(bit(t, u)).
have the following rules. gε(x1, . . . , xn), ξ ↓ z t, ρ ↓ ε ( ti , ρ ↓ vi )i=1,...,n f (t, t1, . . . , tn), ρ+ ↓ z∗ rec-ε where ξ(xi ) = vi for i = 1, . . . , n. gb(x0, y, x), ξ ↓ z t, ρ ↓ bv0 f (x0, x), ν ↓ w ( tj , ρ ↓ vj )j=1,...,n f (t, t1, . . . , tn), ρ+ ↓ z∗ where b = 0, 1 and x = x1, . . . , xn. The environment ν is deﬁned by ν(xj ) = vj for j = 1, . . . , n and ν(x0) = v0 while ξ is deﬁned by ξ(xj ) = vj , ξ(x0) = v0, ξ(y) = w.
If ε, ρ ↓ v is contained in a computation σ, then either v ≡ ε or v ≡ ∗. If bt, ρ ↓ v where t is not a numeral, is contained in σ, then either v ≡ bv0 for some g-value v0 or v ≡ ∗. If v ≡ bv0, then σ contains t, ρ∗ ↓ v0 and v0 v0. Proof. Induction on σ
a term of type W, we deﬁne V (t, ρ) = {v | σ t, ρ ↓ v, C(σ) ≤ nodes(t) · U} vals(t, ρ) = {v ∈ V (t, ρ) | v ∈ V (t, ρ), v v =⇒ v = v} ρ is maximal if ρ(t) ∈ vals(t, ξ) and ρ(bit(a, b)) = bit(ρ(a), ρ(b)) if bit(ρ(a), ρ(b)) = ∗. Env(ρ, t, U) ⇐⇒ ρ is a maximal environment . Env(ρ, t, U) is a bounded formula.
w ⇐⇒ either v w or w v ρ1 ρ2 ⇐⇒ ρ1(t) ρ2(t) for any t ∈ dom(ρ1) ∩ dom(ρ2) For Boolean b1, b2, deﬁne b1 b2 ⇐⇒ b1 = b2 Lemma (S2: Compatibility lemma) Let ρ1 and ρ2 be maximal environments which satisfy ρ1 ρ2, t be the term. If both of t, ρ1 ↓ v and t, ρ2 ↓ w are contained in computations σ and τ respectively, then v w.
I) Let ρ be a maximal environment and σ be a computation with conclusions t1(u1, . . . , un), ρ ↓ v1, . . . , tm(u1, . . . , un), ρ ↓ vm. Let ρ be the maximal environment which extends ρ by ρ (xi ) = v(ui , ρ, σ) and ρ (bit(a(x), b(x))) = ρ(bit(a(u), b(u))). Then, there is a computation τ with conclusions t1(x), ρ ↓ v1, . . . , tm(x), ρ ↓ vm. such that C(τ) ∈ C(σ) + m j=1 size(tj (ε, . . . , ε))
II) Let ρ be a maximal environment and ρ is the maximal extension of ρ such that ρ (xi ) = wi and ρ (bit(r(x), s(x))) = ρ(bit(r(u), s(u))). Assume that size(tj (u1, . . . , un)) ≤ C, j = 1, . . . , m. Then for any computation σ with conclusions tj (x1, . . . , xn), ρ ↓ vj for j = 1, . . . , m such that ρ(xi ) = v(ui , ρ, σ), there is a computation τ such that τ has all conclusions of σ plus tj (u1, . . . , un), ρ ↓ vj for j = 1, . . . , m as conclusions and C(τ) ≤ max(C(σ) + m j=1 size(tj (ε, . . . , ε)), C).
I) Let f (u(r)) = t(r) is a substitution instance of the deﬁning axiom f (u(y)) = t(y). Let ρ be a maximal environment and α judgements. If σ is a computation of f (u(r)), ρ ↓ v, α, there is a computation τ of t(r), ρ ↓ v, α such that C(τ) ≤ C(σ) + size(f (u(r)) = t(r)) Further, τ derives α from the same assumptions using the same rule to σ.
II) Let f (u(r)) = t(r) is a substitution instance of the deﬁning axiom f (u(y)) = t(y). Let ρ be a maximal environment and α judgements. If σ is a computation of t(r), ρ ↓ v, α, there is a computation τ of f (u(r)), ρ ↓ v, α such that C(τ) ≤ C(σ) + size(f (u(r)) = t(r)) Further, τ derives α from the same assumptions using the same rule to σ.
t(r) = u(r) (1) a substitution instance of a valid Boolean axiom t(y) = u(y). Let ρ be a maximal environment and α judgements. If σ is a computation of t(r), ρ ↓ b, α, there is a computation τ of u(r), ρ ↓ b, α such that C(τ) ≤ C(σ) + size(t(r) = u(r)) (2)
/xd ], d ≤ D is called substitution sequence if x1, . . . , xd are all diﬀerent dom(ξ) = {x1, . . . , xd } ξ(t) ≡ t[qd /xd ] · · · [q1/x1] B(ξ) = max{size(ξ(xi )) | i = 1, . . . , d} ξ : η is the concatenation of ξ and η Env(ρ, t, U): ρ is a maximal environment or t. U is the same U in the deﬁnittion of maximal environments.
χ of PV− q (D) of S ≡ Q =⇒ φ an integer U s.t. U ≥ 2size(χ) a substitution sequence η ≡ [q1/x1] · · · [qd /xd ] s.t. B(η) ≤ (U − size(χ))d a sequence of statements α s.t. M(α) ≤ (U − size(χ))D+2 where M(α) is the maximum size of terms appearing in α. Then, Sat(U, size(χ), η, ρ, α, S) holds.
built by following axioms and rules. The subsystem PV1(D) is a system in which for all sequents Γ =⇒ ∆, the number of quantiﬁers plus the number of equations is bounded by D. t = u =⇒ t = u =⇒ t = t t = u =⇒ u = t t = u, u = s =⇒ t = s t1 = u1, . . . , tm = um =⇒ f (t1, . . . , tm) = f (u1, . . . , um) if f (x1, . . . , xm) = t is a deﬁning axiom, =⇒ f (u1, . . . , um) = t(u1, . . . , um)
be the universal closure of conjunction of Ax. If A1 can be written in the language of PV− 1 (D), S2 proves the consistency of PV− 1 (D) + A1. To prove the theorem, we use the following lemma. Lemma (S1 2 ) Let t(x1, . . . , xn) be a term of type and ρ be an exact maximal environment. Assume that t(ρ(x1), . . . , ρ(xn)) = d in the standard interpretation. Then, there is a computation σ such that σ t, ρ ↓ d and nodes(σ) ≤ Pt(B(ρ)) for a polynomial Pt. Let P be a polynomial such that P(|n1| + · · · + |nm|) ≤ |t(n1, . . . , nm)| for any term t which appears in Ax.
inside S2. A is embedded into PV− q (D) as tA1 = . If PV− 1 (D) + Ax is inconsistent, we have PV− q (D) i1, . . . , ik =⇒ tA1 (i1, . . . , ik) = ⊥ Soundness of PV− q (D) and by deﬁnition of Sat, Sat(2size(π), size(π), [ ], tA1 (u1, . . . , uk) = ⊥) Therefore, there is a computation σ of tA1 (u1, . . . , uk), [ ] ↓ ⊥. By Substititon Lemma I, there is a maximal environment ρ and a computation σ0 of tA1 (x), ρ ↓ ⊥. Let ρ ρ be an exact environment. Then, there is a computation σ1 of tA1 (x), ρ ↓ ⊥. By previous lemma, we can build a computation τ of tA1 (x), ρ ↓ with enough large C(τ), which is against Compatibility Lemma.
consistency statements in fragments of bounded arithmetic. Annals of pure and applied Logic, 74:221–244. Krynicki, M. and Mostowski, M. (1995). Henkin quantiﬁers. In Quantiﬁers: logics, models and computation, pages 193–262. Springer. Takeuti, G. (1996). Incompleteness theorems and Si 2 versus Si+1 2 . In Logic Colloquium ’96: Proceedings of the Colloquium held in San Sebasti´ an, Spain, July 9-15, 1996, volume 12 of Lecture notes in logic, pages 247–261.