Poster - Paula Henk

A Bimodal Provability Logic –
Towards an Interpretability Logic with a Supremum Operator
Paula Henk
supervised by Dick de Jongh, Volodya Shavrukov, and Albert Visser
ILLC, University of Amsterdam, The Netherlands
[email protected]
le:
p
m
a
Ex
A
P
ZFC
Interpretability
T S :
S ` A ⇒ T ` Aτ , for some structure–preserving translation τ
A Nonstandard Provability Predicate
Let 4A := ¬O¬A. Then
Two perspectives on interpretability:
Notion for comparing theories
Generalisation of provability
⇓
1
where Πn+1
(Π0 1 ) stands for provability in IΣn+1 (I∆0 + exp) with a Π1–oracle.
⇓
Lattice of Degrees
1
4A = ∃x (xA ∧ ¬Πx−1
⊥)
V 4 expresses a strong notion of provability, call it s–provability
Interpretability Logic
The axioms and rules of provability logic (GL) are valid for s–provability in PA:
1. `PA A ⇒ `PA 4A
Degree of T : {S | S T & T S}
Theorem (Sˇvejdar): The degrees of finite extensions of Peano
Arithmetic (PA) form a lattice.
Meaning in LPA
Modal Language
A:
A B:
A is provable in PA
PA + A interprets PA + B
Axioms of ILM:
L1 (A → B) → (A → B)
[A] : the degree of PA + A
L2 (A → A) → A
J1 (A → B) → A B
[⊥]
..
..
sup([A], [B])
J2 (A B) ∧ (B C) → (A C)
J3 (A C) ∧ (B C) → (A ∨ B) C
J4 A B → (3A → 3B)
[A]
J5 3A A
[B]
M A B → (A ∧ C) (B ∧ C)
Rules: modus ponens, necessitation for [A ∨ B]
..
..
[>]
Theorem (Shavrukov, Berarducci):
`ILM A ⇔ `PA A∗ for all translations A∗ of
A into the language LPA of arithmetic
2. `PA 4(A → B) → (4A → 4B)
3. `PA 4(4A → A) → 4A
A Bimodal Provability Logic
1
#
n
o
i
at
t
e
r
A
p
P
r
n
e
i
t
e
n
l
I
ab
v
o
r
p
s
i
A
ble
a
:
v
o
r
p
A
A is s
4A :
GLT, a first step towards adding 4 to ILM:
T1 4(A → B) → (4A → 4B)
T2 4(4A → A) → 4A
T3 (A → B) → (A → B)
2
#
n
A.
o
i
r
t
e
f
a
t
n
i
e
,
r
Interp ule: from A
’s r
h
k
i
ule
r
r
a
s
P
’
h
k
i
ar
P
+
A
P
PA
n
i
n
i
e
l
e
l
b
b
a
va
ov
o
r
r
p
p
s
i
s
i
A
A : A
4A :
T4 4A → A
T5 A → 4A
T6 A → 4A
T7 4A → A
Rules: modus ponens, and necessitation for 4
Standard Semantics
Lindstr¨
om’s Semantics
Aim of Current Work
Model: hW, Q, R, i with
Model: hW, Q, i with
1. Q conversely well–founded & transitive
`ILM “A ∨ B is an infimum of A and B in the lattice of degrees.”
1. R, Q conversely well–founded &
transitive
2. R ⊆ Q
3. w A ⇔ x A whenever
{u | wQuQx} = ∞
On the other hand:
3. Q ◦ R ⊆ R, R ◦ Q ⊆ R
Fact: There exist A, B with [A ∧ B] 6= sup([A], [B]).
4. R ⊆ R ◦ Q
Fact: The existence of sup([A], [B]) is not expressible in LILM.
5. Q, R accessibility relations for 4, V add to ILM a new modality whose arithmetical interpretation is the supremum
...
xn . . . x2
2. Q accessibility relation for 4
x1
x0
x0
x1
w 3B, x0 B
...
w 3B, x0 B
First Approach
Add to ILM a binary modality ?, together with the axiom
C A ∧ C B ↔ C A ? B.
Intended arithmetical meaning of A ? B: a sentence in sup([A], [B]).
An example (Sˇvejdar): θ with
`PA θ ↔ ∀x(3xθ → 3xA ∧ 3xB),
where 0 stands for provability in I∆0 + exp, and n+1 for provability in IΣn+1.
w
x2
..
..
xn
..
..
w
Soundness and Completeness
Theorem (Lindstr¨om):
1. GLT is arithmetically sound and complete with respect to Interpretation #2.
2. GLT is modally sound and complete with respect to Lindstr¨om’s semantics.
Theorem :
GLT is modally sound and complete with respect to the standard semantics.
A Discovery
Shavrukov: there is a formula O of LPA with one free variable, such that for all sentences
A, B, and C of LPA,
Future Work
`PA C A ∧ C B ↔ C OA ∧ OB
1. Arithmetical completeness of GLT w.r.t. Interpretation #1
V it suffices to add a unary modality O to ILM
2. Adding 4 to ILM; arithmetical completeness (w.r.t. Int. #1) of the resulting system
References
Lindstro¨m, P.: On Parikh Provability - an Exercise in Modal Logic. Modality Matters: Twenty-Five Essays in Honour of Krister Segerberg. Henrik Lagerlund and Sten Lindstr¨om and Rysiek
Sliwinski (eds). Uppsala Philosophical Studies 53, pp.279–288, 2006.
LATEX Tik Zposter

Download Report