A sequent calculus for 1-backtracking
Stefano Berardi and Yoriyuki Yamagata
A sequent calculus for 1-backtracking – p. 1
Background : LCM
Susumu Hayashi and N. Nakata (2001)
Analogy of Constructive Mathematics (realized by recursive functions)
Realized by learnable (limit recursive) functions
Covers large parts of classical elementary mathematics
A sequent calculus for 1-backtracking – p. 2
Background : LCM
Susumu Hayashi and N. Nakata (2001)
Analogy of Constructive Mathematics (realized by recursive functions)
Realized by learnable (limit recursive) functions
Covers large parts of classical elementary mathematics
A sequent calculus for 1-backtracking – p. 2
Background : LCM
Susumu Hayashi and N. Nakata (2001)
Analogy of Constructive Mathematics (realized by recursive functions)
Realized by learnable (limit recursive) functions
Covers large parts of classical elementary mathematics
A sequent calculus for 1-backtracking – p. 2
Background : LCM is quasi-classical
Excluded middle holds only for Σ01-formulas. i.e.
EM1(P ) ≡ ∀x(∃yP xy ∨ ∀y¬P xy) P : decidable
EM1 suffices for elementary classical mathematics.
A sequent calculus for 1-backtracking – p. 3
Background : LCM is quasi-classical
Excluded middle holds only for Σ01-formulas. i.e.
EM1(P ) ≡ ∀x(∃yP xy ∨ ∀y¬P xy) P : decidable
EM1 suffices for elementary classical mathematics.
A sequent calculus for 1-backtracking – p. 3
Background : LCM is quasi-classical
Excluded middle holds only for Σ01-formulas. i.e.
EM1(P ) ≡ ∀x(∃yP xy ∨ ∀y¬P xy) P : decidable
EM1 suffices for elementary classical mathematics.
A sequent calculus for 1-backtracking – p. 3
Background : 1-backtracking game
two person game with A and E.
E can retract her moves,
but cannot retract retraction itself.
We will look at this more closely ...
A sequent calculus for 1-backtracking – p. 4
Background : 1-backtracking game
two person game with A and E.
E can retract her moves, but cannot retract retraction itself.
We will look at this more closely ...
A sequent calculus for 1-backtracking – p. 4
Background : 1-backtracking game
two person game with A and E.
E can retract her moves,
but cannot retract retraction itself.
We will look at this more closely ...
A sequent calculus for 1-backtracking – p. 4
Background : 1-backtracking game
two person game with A and E.
E can retract her moves,
but cannot retract retraction itself.
We will look at this more closely ...
A sequent calculus for 1-backtracking – p. 4
Background : Fact
Berardi, Tierry Coquand, Hayashi (2005)
Formula A is valid (realized) in LCM
⇔ E has a winning strategy of bck1(TA), where TA is Tarski game of A.
A sequent calculus for 1-backtracking – p. 5
Background : Fact
Berardi, Tierry Coquand, Hayashi (2005)
Formula A is valid (realized) in LCM
⇔ E has a winning strategy of bck1(TA), where TA is Tarski game of A.
A sequent calculus for 1-backtracking – p. 5
Our contribution : P A
1E has a winning strategy σ of bck1(TA),
⇔ There is a proof π(σ) of A in P A1,
where P A1 is a sequent calculus without Exchange,
and π(σ) is tree-isomorphic to σ.
A sequent calculus for 1-backtracking – p. 6
Our contribution : P A
1E has a winning strategy σ of bck1(TA),
⇔ There is a proof π(σ) of A in P A1, where P A1 is a sequent calculus without
Exchange,
and π(σ) is tree-isomorphic to σ.
A sequent calculus for 1-backtracking – p. 6
Our contribution : P A
1E has a winning strategy σ of bck1(TA),
⇔ There is a proof π(σ) of A in P A1,
where P A1 is a sequent calculus without Exchange,
and π(σ) is tree-isomorphic to σ.
A sequent calculus for 1-backtracking – p. 6
Our contribution : P A
1E has a winning strategy σ of bck1(TA),
⇔ There is a proof π(σ) of A in P A1,
where P A1 is a sequent calculus without Exchange,
and π(σ) is tree-isomorphic to σ.
A sequent calculus for 1-backtracking – p. 6
backtracking play
m0 m1
A sequent calculus for 1-backtracking – p. 7
backtracking play
m0 m1 m2
A sequent calculus for 1-backtracking – p. 7
backtracking play
m0 m1 m2 m’1
A sequent calculus for 1-backtracking – p. 7
backtracking play
m0 m1 m2 m’1
m1, m2 are cancelled and E replies m0.
A sequent calculus for 1-backtracking – p. 7
1-backtracking play
m0 m1
A sequent calculus for 1-backtracking – p. 8
1-backtracking play
m0 m1 m2
A sequent calculus for 1-backtracking – p. 8
1-backtracking play
m0 m1 m2 m’1
A sequent calculus for 1-backtracking – p. 8
1-backtracking play
m0 m1 m2 m’1 m’2
A sequent calculus for 1-backtracking – p. 8
1-backtracking play
m0 m1 m2 m’1 m’2 m1
This is allowed
A sequent calculus for 1-backtracking – p. 8
1-backtracking play
m0 m1 m2 m’1 m’2 m3
This is not allowed
A sequent calculus for 1-backtracking – p. 8
1-backtracking play
m0 m1 m2 m’1 m’2 m3
inaccessible after m01
A sequent calculus for 1-backtracking – p. 8
1-excluded middle
1-excluded middle EM1 is a schema
∀x(∃yP xy ∨ ∀y¬P xy) P : decidable
A sequent calculus for 1-backtracking – p. 9
1-excluded middle
1-excluded middle EM1 is a schema
∀x(∃yP xy ∨ ∀y¬P xy) P : decidable
A sequent calculus for 1-backtracking – p. 9
Tarski game G of EM
1A sequent calculus for 1-backtracking – p. 10
Tarski game G of EM
1(2)
There is no recursive winning strategy for G,
because E must choose ∃yP xy or ∀y¬P xy
A sequent calculus for 1-backtracking – p. 11
Tarski game G of EM
1(2)
There is no recursive winning strategy for G,
because E must choose ∃yP xy or ∀y¬P xy
A sequent calculus for 1-backtracking – p. 11
Tarski game G of EM
1(3)
But there is a recursive winning strategy for 1-bck play of G
A sequent calculus for 1-backtracking – p. 12
1-bck play of G
A sequent calculus for 1-backtracking – p. 13
1-bck play of G
A sequent calculus for 1-backtracking – p. 13
1-bck play of G
A sequent calculus for 1-backtracking – p. 13
1-bck play of G
A sequent calculus for 1-backtracking – p. 13
1-bck play of G
A sequent calculus for 1-backtracking – p. 13
P A
1Γ, p
Γ, A(0) . . . Γ, A(n) . . . Γ, ∀xA(x), ∆ ∀ Γ, ∃xA(x), A(n)
Γ, ∃xA(x), ∆ ∃
A sequent calculus for 1-backtracking – p. 14
Remarks
No Exchange (Sequents are lists) Weakening and Contractions are
merged to logical rules ω-rules
A sequent calculus for 1-backtracking – p. 15
Remarks
No Exchange (Sequents are lists) Weakening and Contractions are merged to logical rules
ω-rules
A sequent calculus for 1-backtracking – p. 15
Remarks
No Exchange (Sequents are lists) Weakening and Contractions are merged to logical rules
ω-rules
A sequent calculus for 1-backtracking – p. 15
A proof of EM
1. . .
A, ∃yP ny, P nm true A, ∃yP ny ∃
A, ¬P nm ∨
. . . A, ∀y¬P ny ∀
∃yP ny ∨ ∀y¬P ny ∨
A sequent calculus for 1-backtracking – p. 16
Interpretation of sequent
B1, B2, . . . , Bn, C C: current position
B1, . . . , Bn: possible positions to backtrack
A sequent calculus for 1-backtracking – p. 17
Interpretation of sequent
B1, B2, . . . , Bn, C C: current position
B1, . . . , Bn: possible positions to backtrack
A sequent calculus for 1-backtracking – p. 17
Interpretation of sequent
B1, B2, . . . , Bn, C C: current position
B1, . . . , Bn: possible positions to backtrack
A sequent calculus for 1-backtracking – p. 17
Isomorphic Theorem
There is a tree isomorphism between a proof tree of formula A
a winning strategy (as a tree of move) of bck1(TA)
A sequent calculus for 1-backtracking – p. 18
Isomorphic Theorem
There is a tree isomorphism between a proof tree of formula A
a winning strategy (as a tree of move) of bck1(TA)
A sequent calculus for 1-backtracking – p. 18
Conclusion
We introduce a proof system P A1, an ω-logic without Exchange
We show a proof of formula A in P A1 and a winning strategies of bck1(TA) has a tree-isomorphism
A sequent calculus for 1-backtracking – p. 19
The End
A sequent calculus for 1-backtracking – p. 20
