Self-referentiality in Justification Logic

Nathan Sebastian Gass; Thomas Studer

arXiv:1902.01106·math.LO·January 28, 2020

Self-referentiality in Justification Logic

Nathan Sebastian Gass, Thomas Studer

PDF

Open Access

TL;DR

This paper investigates the role of self-referential justifications in justification logic, showing that prehistoric cycles are necessary but not sufficient for self-referential theorems unless the definition is expanded.

Contribution

It clarifies the conditions under which prehistoric cycles lead to self-referential theorems in justification logic, resolving an open problem.

Findings

01

Prehistoric cycles are not sufficient under the standard definition.

02

An expanded definition makes prehistoric cycles sufficient.

03

Self-referentiality is crucial for realizing S4 in LP.

Abstract

The Logic of Proofs, LP, and other justification logics can have self-referential justifications of the form t:A. Such self-referential justifications are necessary for the realization of S4 in LP. Yu discovered prehistoric cycles in a particular Gentzen system as a necessary condition for S4 theorems that can only be realized using self-referentiality. It was an open problem whether prehistoric cycles also are a sufficient condition. The main results of this paper are: First, with the standard definition of self-referential theorems, prehistoric cycles are not a sufficient condition. Second, with an expansion on that definition, prehistoric cycles become sufficient for self-referential theorems.

Tables3

$P, Γ \supset Δ, P$ $(A x)$ ( $P$ atomic)	$⊥, Γ \supset Δ$ $(⊥ \supset)$
$Γ \supset Δ, A$ $(\neg \supset)$ $\neg A, Γ \supset Δ$	$A, Γ \supset Δ$ $(\supset \neg)$ $Γ \supset Δ, \neg A$
$A, B, Γ \supset Δ$ $(\land \supset)$ $A \land B, Γ \supset Δ$	$Γ \supset Δ, A$ $Γ \supset Δ, B$ $(\supset \land)$ $Γ \supset Δ, A \land B$
$A, Γ \supset Δ$ $B, Γ \supset Δ$ $(\lor \supset)$ $A \lor B, Γ \supset Δ$	$Γ \supset Δ, A, B$ $(\supset \lor)$ $Γ \supset Δ, A \lor B$
$Γ \supset Δ, A$ $B, Γ \supset Δ$ $(\to \supset)$ $A \to B, Γ \supset Δ$	$A, Γ \supset Δ, B$ $(\supset \to)$ $Γ \supset Δ, A \to B$
$A, □ A, Γ \supset Δ$ $(□ \supset)$ $□ A, Γ \supset Δ$	$□ Γ \supset ◇ Δ, A$ $(\supset □)$ $Γ^{'}, □ Γ \supset ◇ Δ, Δ^{'}, □ A$
$A, □ Γ \supset ◇ Δ$ $(◇ \supset)$ $◇ A, Γ^{'}, □ Γ \supset ◇ Δ, Δ^{'}$	$Γ \supset Δ, A, ◇ A$ $(\supset ◇)$ $Γ \supset Δ, ◇ A$

P, \neg □ ​ P, □ ​ (P \land \neg □ ​ P) \supset P

(\land \supset)

P \land \neg □ ​ P, □ ​ (P \land \neg □ ​ P) \supset P

(□ \supset)

□ ​ (P \land \neg □ ​ P) \supset P

(\supset □)

P, □ ​ (P \land \neg □ ​ P) \supset □ ​ P

(\neg \supset)

P, \neg □ ​ P, □ ​ (P \land \neg □ ​ P) \supset

(\land \supset)

P \land \neg □ ​ P, □ ​ (P \land \neg □ ​ P) \supset

(□ \supset)

□ ​ (P \land \neg □ ​ P) \supset

(\supset \neg)

\supset \neg □ ​ (P \land \neg □ ​ P)

P, \neg t \cdot x : P, x : (P \land \neg t \cdot x : P) \supset P

P \land \neg t \cdot x : P, x : (P \land \neg t \cdot x : P) \supset P

x : (P \land \neg t \cdot x : P) \supset P

P, x : (P \land \neg t \cdot x : P) \supset t \cdot x : P

P, \neg t \cdot x : P, x : (P \land \neg t \cdot x : P) \supset

P \land \neg t \cdot x : P, x : (P \land \neg t \cdot x : P) \supset

x : (P \land \neg t \cdot x : P) \supset

\supset \neg x : (P \land \neg t \cdot x : P)

$\supset A$ ${(\supset :)}_{c}$ ( $A$ an axiom of LP) $Γ \supset Δ, c : A$	$t : A \supset A$ ${(\supset :)}_{t}$ $t : A, Γ \supset Δ, t : A$
$A, t : A, Γ \supset Δ$ $(: \supset)$ $t : A, Γ \supset Δ$	$Γ \supset Δ, t : A,! t : t : A$ $(\supset!)$ $Γ \supset Δ,! t : t : A$
$Γ \supset Δ, s : A, t : A, (s + t) : A$ $(\supset +)$ $Γ \supset Δ, (s + t) : A$	$Γ \supset Δ, s : (A \to B), s \cdot t : B$ $Γ \supset Δ, t : A, s \cdot t : B$ $(\supset \cdot)$ $Γ \supset Δ, s \cdot t : B$

Equations54

R := {(S_{i}, S_{j}) \in T \times T ∣ S_{i} is the conclusion of a rule which has S_{j} as a premise} .

R := {(S_{i}, S_{j}) \in T \times T ∣ S_{i} is the conclusion of a rule which has S_{j} as a premise} .

x : A \to t (x) : B

x : A \to t (x) : B

A := {c_{0} : A (c_{1}), \dots, c_{n - 1} : A (c_{0})} .

A := {c_{0} : A (c_{1}), \dots, c_{n - 1} : A (c_{0})} .

≺_{L} := ⋃ {≺_{L}^{S} ∣ S is a leaf} ≺_{R} := ⋃ {≺_{R}^{S} ∣ S is a leaf}

≺_{L} := ⋃ {≺_{L}^{S} ∣ S is a leaf} ≺_{R} := ⋃ {≺_{R}^{S} ∣ S is a leaf}

Γ \supset Δ, □ A, □ B

Γ \supset Δ, □ A, □ B

G3s + (□ Cut) ⊢ Γ \supset Δ \Rightarrow G3s + (Cut) ⊢ Γ \supset Δ \Rightarrow G3s ⊢ Γ \supset Δ.

G3s + (□ Cut) ⊢ Γ \supset Δ \Rightarrow G3s + (Cut) ⊢ Γ \supset Δ \Rightarrow G3s ⊢ Γ \supset Δ.

G3s ⊢ Γ \supset Δ, A and G3s ⊢ A, Γ \supset Δ,

G3s ⊢ Γ \supset Δ, A and G3s ⊢ A, Γ \supset Δ,

i_{0} ≺ \dots ≺ i_{n - 1} ≺ i_{0}

i_{0} ≺ \dots ≺ i_{n - 1} ≺ i_{0}

i_{k} ≺ i_{k + 1 mod n}

i_{k} ≺ i_{k + 1 mod n}

G3s ⊢ Γ \supset Δ, □ A, □ B and G3s ⊢ Γ \supset Δ, □ (A \to B), □ B,

G3s ⊢ Γ \supset Δ, □ A, □ B and G3s ⊢ Γ \supset Δ, □ (A \to B), □ B,

Γ \subset Δ \in G 3 s^{\otimes}

Γ \subset Δ \in G 3 s^{\otimes}

(G3s + (□ Cut))^{\otimes} \subseteq (G3s + (Cut))^{\otimes} \subseteq G3s^{\otimes}

(G3s + (□ Cut))^{\otimes} \subseteq (G3s + (Cut))^{\otimes} \subseteq G3s^{\otimes}

G3s^{\otimes} = (G3s + (Cut))^{\otimes} = (G3s + (□ Cut))^{\otimes} \qed

G3s^{\otimes} = (G3s + (Cut))^{\otimes} = (G3s + (□ Cut))^{\otimes} \qed

i_{0} ≺ \dots ≺ i_{n} ≺ i_{0} in T^{\circ}

i_{0} ≺ \dots ≺ i_{n} ≺ i_{0} in T^{\circ}

A := {t_{0} : A (t_{1}), \dots, t_{n - 1} : A (t_{0}) .

A := {t_{0} : A (t_{1}), \dots, t_{n - 1} : A (t_{0}) .

i_{0} ≺ i_{1} ≺ \dots ≺ i_{n - 1} ≺ i_{0} .

i_{0} ≺ i_{1} ≺ \dots ≺ i_{n - 1} ≺ i_{0} .

y : (P \land \neg y \cdot x : P \to P) ⊢_{LPG_{0}} \neg x : (P \land \neg y \cdot x : P)

y : (P \land \neg y \cdot x : P \to P) ⊢_{LPG_{0}} \neg x : (P \land \neg y \cdot x : P)

G 3 s ⊢\supset □ (P \land \neg □ P \to P) \to \neg □ (P \land \neg □ P)

G 3 s ⊢\supset □ (P \land \neg □ P \to P) \to \neg □ (P \land \neg □ P)

G 3 s ⊢ □ (P \land \neg □ P \to P), □ (P \land \neg □ P) \supset .

G 3 s ⊢ □ (P \land \neg □ P \to P), □ (P \land \neg □ P) \supset .

P \land \neg □ P, □ (P \land \neg □ P \to P), □ (P \land \neg □ P) \supset,

P \land \neg □ P, □ (P \land \neg □ P \to P), □ (P \land \neg □ P) \supset,

□ (P \land \neg □ P \to P) \supset P

□ (P \land \neg □ P \to P) \supset P

□ (P \land \neg □ P \to P) \to P

□ (P \land \neg □ P \to P) \to P

W := w, v a l (P) := \emptyset, R := {(w, w)} .

W := w, v a l (P) := \emptyset, R := {(w, w)} .

w ⊩ \neg (P \land \neg □ P) .

w ⊩ \neg (P \land \neg □ P) .

□ (P \land \neg □ P \to P), □ (P \land \neg □ P) \supset

□ (P \land \neg □ P \to P), □ (P \land \neg □ P) \supset

\neg □ (P \land \neg □ P)

\neg □ (P \land \neg □ P)

B := y : (P \land \neg y \cdot x : P \to P) \to \neg x : (P \land \neg y \cdot x : P)

B := y : (P \land \neg y \cdot x : P \to P) \to \neg x : (P \land \neg y \cdot x : P)

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Logic, programming, and type systems

Full text

Self-referentiality in Justification Logic

Nathan Sebastian Gass

Thomas Studer

Abstract

The Logic of Proofs, LP, and other justification logics can have self-referential justifications of the form $t{:}A(t)$ . Such self-referential justifications are necessary for the realization of S4 in LP. Yu discovered prehistoric cycles in a particular Gentzen system as a necessary condition for S4 theorems that can only be realized using self-referentiality. It was an open problem whether prehistoric cycles also are a sufficient condition.

The main results of this paper are: First, with the standard definition of self-referential theorems, prehistoric cycles are not a sufficient condition. Second, with an expansion on that definition, prehistoric cycles become sufficient for self-referential theorems.

Disclaimer. This paper contains several mistakes. A revised version is under progress.

Note, however, that the counterexample in Section 4.3 is valid. It is correct that prehistoric cycles in G3s are not sufficient for needing a self-referential CS.

1 Introduction

Sergei Artemov [1, 2] first introduced the Logic of Proofs, LP. He replaced the $\Box$ -modality of S4 with explicit proof terms to obtain a classical provability semantics for intuitionistic logic. Later more applications of this explicit notations were discovered for different epistemic logics [4]. So Artemov [3] introduced the more general notion of justification logics where justification terms take over the role of the proof terms in LP. In any justification logic $t{:}A$ is read as $t$ is a justification of $A$ , leaving open what exactly that entails. Using different axioms and different operators, various different justification logic counterparts where developed for the different modal systems used in epistemic logic (K, T, K4, S4, K45, KD45, S5, etc.).

In justification logics it is possible for a term $t$ to be a justification for a formula $A(t)$ containing $t$ itself, i.e. for the assertion $t{:}A(t)$ to hold. Prima facie this seems suspicious from a philosophical standpoint as well for more formal mathematical reasons. Such a self-referential sentence is for example impossible with an arithmetic proof predicate using standard Gödel numbers as the Gödel number of a proof is always greater than any number referenced in it as discussed by Roman Kuznets [12]. In the same paper, the author argues that there is nothing inherently wrong with self-referential justifications if we understand the justifications as valid reasoning templates or schemes, which of course then can be used on themselves.

Kuznets studied the topic of self-referentiality at the logic-level. He discovered theorems of S4, D4, T and K4 that need a self-referential constant specification to be realized in their justification logic counterparts [12]. Junhua Yu on the other hand studied self-referentiality at the theorem level. He discovered prehistoric cycles as a necessary condition for self-referential S4 theorems [16] and later expanded that results to the modal logics T and K4 [17]. He also conjectured that the condition is actually sufficient for self-referential S4 theorems. In this paper we will concentrate on that topic, that is prehistoric cycles as necessary and sufficient condition for self-referential theorems in S4.

This paper is divided in three parts. In the first part we introduce the modal logic S4 and its justification counterpart LP. The second part restates Yu’s main theorem, i.e. that prehistoric cycles are a necessary condition for self-referential theorems in S4. The third part goes beyond Yu’s original paper by adapting the notion of prehistoric cycles to Gentzen systems with cut rules and finally to a Gentzen system for LP. This allows to study prehistoric cycles directly in LP, which leads to the two main results of this paper. First, with the standard definition of self-referential theorems, prehistoric cycles are not a sufficient condition. Second, with an expansion on the definition of self-referential theorems, prehistoric cycles become sufficient for self-referential theorems.

2 LP and S4

2.1 Preliminaries

As the results and concepts in this paper are mostly purely syntactical, we will also limit this brief introduction to the modal logic S4 and its justification counterpart LP to the syntactic side.

Definition 1 (Syntax of S4).

The language of S4 is given by $A:=\bot\mid P\mid A_{0}\land A_{1}\mid A_{0}\lor A_{1}\mid A_{0}\to A_{1}\mid\Box A\mid\Diamond A$ . By using the known abbreviations for $\land$ , $\lor$ and $\Diamond$ we can reduce that to the minimal language $A:=\bot\mid P\mid A_{0}\to A_{1}\mid\Box A$ .

Definition 2 (Syntax of LP).

The language of LP consists of terms given by $t:=c\mid x\mid t_{0}\cdot t_{1}\mid t_{0}+t_{0}\mid\>!t$ and formulas given by $A:=\bot\mid P\mid A_{0}\to A_{1}\mid t{:}A$ .

A Hilbert style system for LP is given by the following Axioms and the rules modus ponens and axiom necessitation [2]

•

$A0$ : Finite set of axiom schemes of classical propositional logic

•

$A1$ : $t{:}F\to F$ (Reflection)

•

$A2$ : $s{:}(F\to G)\to(t{:}F\to(s\cdot t){:}G)$ (Application)

•

$A3$ : $t{:}F\to\;!t{:}(t{:}F)$ (Proof Checker)

•

$A4$ : $s{:}F\to(s+t){:}F$ , $t{:}F\to(s+t){:}F$ (Sum)

•

$R1$ : $F\to G,F\vdash G$ (Modus Ponens)

•

$R2$ : $A\vdash c{:}A$ , if $A$ is an axiom $A0-A4$ and $c$ a constant (Axiom Necessitation)

A Hilbert style derivation $d$ from a set of assumptions $\Gamma$ is a sequence of formulas $A_{0},\ldots,A_{n}$ such that any formula is either an instance of an axiom A0–A4, a formula $A\in\Gamma$ or derived from earlier formulas by a rule R1 or R2. The notation $\Gamma\vdash_{\operatorname{LP}}A$ means that a LP derivation from assumptions $\Gamma$ ending in $A$ exists. We also write $\vdash_{\operatorname{LP}}A$ or $\operatorname{LP}\vdash A$ if a LP derivation for $A$ without any assumptions exists.

When formulating such derivations, we will introduce propositional tautologies without derivation and use the term propositional reasoning for any use of modus ponens together with a propositional tautology. This is of course correct as axioms A0 together with the modus ponens rule R1 are a complete Hilbert style system for classical propositional logic. Its easy to see by a simple complete induction on the proof length that this derivations do not use any new terms not already occurring in the final propositional tautology.

Definition 3 (Constant Specification).

A constant specification CS is a set of of formulas of the form $c{:}A$ with $c$ a constant and $A$ an axiom A0-A4.

Every LP derivation naturally generates a finite constant specification of all formulas derived by axiom necessitation (R2). For a given constant specification CS, LP(CS) is the logic with axiom necessitation restricted to that CS. $\operatorname{LP}_{0}:=\operatorname{LP}(\emptyset)$ is the logic without axiom necessitation. A constant specification CS is injective if for each constant $c$ there is at most one formula $c{:}A\in\operatorname{CS}$ .

2.2 Gentzen Systems

In the following, capital greek letters $\Gamma$ , $\Delta$ are used for multisets of formulas, latin letters $P$ , $Q$ for atomic formulas and latin letters $A$ , $B$ for arbitrary formulas. We also use the following short forms:

•

$\Box\Gamma:=\{\Box A|A\in\Gamma\}$

•

$\Gamma,A:=\Gamma\cup\{A\}$

•

$\Gamma,\Delta:=\Gamma\cup\Delta$

•

$\bigwedge\Gamma:=A_{0}\land\cdots\land A_{n}$ and $\bigvee\Gamma:=A_{0}\lor\cdots\lor A_{n}$ for the formulas $A_{i}\in\Gamma$ in an arbitrary but fixed order.

Throughout this paper, we will use the G3s calculus from Troelstra and Schwichtenberg [15] for our examples with additional rules $(\lnot\supset)$ and $(\supset\lnot)$ as we are only concerned with classical logic (see figure 1). For proofs, on the other hand, we use a minimal subset of that system consisting only of $(Ax)$ , $(\bot\supset)$ , $(\to\supset)$ , $(\supset\to)$ , $(\Box\supset)$ , and $(\supset\Box)$ using the standard derived definitions for $\lnot$ , $\lor$ , $\land$ and $\Diamond$ .

In Artemov [2], a Gentzen-Style system LPG is introduced for the logic of proofs LP using explicit contraction and weakening rules, i.e. based on G1c as defined in Troelstra and Schwichtenberg [15]. Later we will follow Cornelia Pulver [14] instead and use G3lp with the structural rules absorbed.

In all rules, arbitrary formulas which occur in the premises and the conclusion (denoted by repeated multisets $\Gamma$ , $\Box\Gamma$ , $\Delta$ and $\Diamond\Delta$ ) are called side formulas. Arbitrary formulas which only occur in the conclusion (denoted by new multisets $\Gamma$ , $\Delta$ , $\Gamma^{\prime}$ , $\Delta^{\prime}$ ) are called weakening formulas.111Notice that weakening formulas only occur in axioms and the rules $(\supset\Box)$ and $(\Diamond\supset)$ , which are also the only rules that restrict the possible side formulas. The remaining single new formula in the conclusion is called the principal formula of the rule. The remaining formulas in the premises are called active formulas. Active formulas are always used as subformulas of the principal formula. Active formulas which are also strict subformulas of other active formulas of the same rule as used in $(:\supset)$ and $(\Box\supset)$ are contraction formulas.

Formally, a Gentzen style proof is denoted by $\mathcal{T}=(T,R)$ , where $T:=\{S_{0},\ldots,S_{n}\}$ is the set of occurrences of sequents, and

[TABLE]

The only root sequent of $\mathcal{T}$ is denoted by $S_{r}$ . A leaf sequent $S$ is a sequent without any premises, i.e $S\not{R}S^{\prime}$ for all $S^{\prime}\in T$ .

A path in a proof tree is a list of related sequent occurrences $S_{0}R\ldots RS_{n}$ . A root path is a path starting at the root sequent $S_{r}$ . A root-leaf path is a root path ending in a leaf sequent.222Yu uses the term path for a root path and branch for a root-leaf path. As this terminology is ambiguous we adopted the slightly different terminology given here. A root path is fully defined by the last sequent $S$ . So we will use root path $S$ to mean the unique path $S_{r}RS_{0}R\ldots RS$ from the root $S_{r}$ to the sequent $S$ . $T\mathord{\upharpoonright}S$ denotes the subtree of $T$ with root $S$ . The transitive closure of $R$ is denoted by $R^{+}$ and the reflexive-transitive closure is denoted by $R^{*}$ .

Consistent with the notation for the Hilbert style system LP, the notation $G\vdash\Gamma\subset\Delta$ is used if there exists a Gentzen style proof tree with the sequent $\Gamma\subset\Delta$ as root in the system $G$ .

Definition 4 (Correspondence).

The subformula (symbol) occurrences in a proof correspond to each other as follows:

•

Every subformula (symbol) occurrence in a side formula of a premise directly corresponds to the same occurrence of that subformula (symbol) in the same side formula in the conclusion.

•

Every active formula of a premise directly correspond to the topmost subformula occurrence of the same formula in the principal formula of the conclusion.

•

Every subformula (symbol) occurrence in an active formula of a premise directly corresponds to the same occurrence of that subformula (symbol) in the corresponding subformula in the principal formula of the rule.

•

Two subformulas (symbols) correspond to each other by the transitive reflexive closure of direct correspondence.

As by definition correspondence is reflexive and transitive, we get the following definition for the equivalence classes of correspondence:

Definition 5 (Family).

A family is an equivalence class of $\Box$ occurrences which respect to correspondence.

For the following lemma and all the other results in this paper concerning correspondence, we fix a proof tree $\mathcal{T}=(T,R)$ and consider correspondence according to this complete proof tree even when talking about subtrees $T\mathord{\upharpoonright}S$ of $\mathcal{T}$ .

As usual, we have the subformula property.

Lemma 6 (Subformula Property).

Any subformula (symbol) occurrence in a partial Gentzen style (pre-)proof $T\mathord{\upharpoonright}S$ in G3s corresponds to at least one subformula (symbol) occurrence of the sequent $S$ of $T\mathord{\upharpoonright}S$ .

Any subformula (symbol) occurrence in a complete Gentzen style (pre-)proof $T$ in G3s corresponds to exactly one subformula (symbol) occurrence in the root sequent $S_{r}$ of $T$ .

2.3 Annotated S4

As we have already seen, all symbol occurrences in a Gentzen style proof can be divided in disjoint equivalence classes of corresponding symbol occurrences. In this text we will be mainly concerned with the equivalence classes of $\Box$ occurrences, called families, and their polarities as defined below. We will therefore define annotated formulas, sequents and proof trees in this section which make the families and polarities of $\Box$ occurrences explicit in the notation and usable in definitions.

Definition 7 (Polarity).

Assign positive or negative polarity relative to $A$ to all subformulas occurrences $B$ in $A$ as follows:

•

The only occurrence of $A$ in $A$ has positive polarity.

•

If an occurrence $B\to C$ in $A$ already has a polarity, then the occurrence of $C$ in $B\to C$ has the same polarity and the occurrence of $B$ in $B\to C$ has the opposite polarity.

•

If an occurrence $\Box B$ already has a polarity, then the occurrence of $B$ in $\Box B$ has the same polarity.

Similarly all occurrences of subformulas in a sequent $\Gamma\supset\Delta$ get assigned a polarity as follows:

•

An occurrence of a subformula $B$ in a formula $A$ in $\Gamma$ has the opposite polarity relative to the sequent $\Gamma\supset\Delta$ as the same occurrence $B$ in the formula $A$ has relative to $A$ .

•

An occurrence of a subformula $B$ in a formula $A$ in $\Delta$ has the same polarity relative to the sequent $\Gamma\supset\Delta$ as the same occurrence $B$ in the formula $A$ has relative to $A$ .

This gives the subformulas of a sequent $\Gamma\supset\Delta$ the same polarity as they would have in the equivalent formula $\bigwedge\Gamma\to\bigvee\Delta$ . Also notice that for the derived operators all subformulas have the same polarity, except for $\lnot$ which switches the polarity for its subformula.

The rules of S4 respect the polarities of the subformulas, so that all corresponding occurrences of subformulas have the same polarity throughout the proof. We therefore assign positive polarity to families of positive occurrences and negative polarity to families of negative occurrences. Moreover, positive families in a S4 proof which have occurrences introduced by a $(\supset\Box)$ rule are called principal positive families or simply principal families. The remaining positive families are called non-principal positive families.333This is the same terminology as used in Yu [16]. In many papers principal families are called essential families following the original text [2].

The following definition of an annotated proof as well as the definition of a realization function are heavily inspired by Fittings use of explicit annotations in Fitting [8]. Other than Fitting, we allow ourselves to treat symbols $\boxplus_{i}$ , $\boxminus_{i}$ directly as mathematical objects and define functions on them, instead of encoding the symbols as natural numbers.

For the following definition, we use an arbitrary fixed enumeration for all different classes of families. That is, we enumerate all principal positive families as $p_{0},\ldots,p_{n_{p}}$ , all non-principal positive families as $o_{0},\ldots,o_{n_{o}}$ and all negative families as $n_{0},\ldots,n_{n_{n}}$ . Given a S4 proof $T$ we then annotate the formulas $A$ in the proof in the following way:

Definition 8 (Annotated Proof).

$\operatorname{\mathsf{an}}_{T}(A)$ is defined recursively on all occurrences of subformulas $A$ in a proof $T$ as follows:

•

If $A$ is the occurrence of an atomic formula $P$ or $\bot$ , then $\operatorname{\mathsf{an}}_{T}(A):=A$ .

•

If $A=A_{0}\to A_{1}$ , then $\operatorname{\mathsf{an}}_{T}(A):=\operatorname{\mathsf{an}}_{T}(A_{0})\to\operatorname{\mathsf{an}}_{T}(A_{1})$

•

If $A=\Box A_{0}$ and the $\Box$ belongs to a principal positive family $p_{i}$ , then $\operatorname{\mathsf{an}}_{T}(A):=\boxplus_{i}\operatorname{\mathsf{an}}_{T}(A_{0})$ .

•

If $A=\Box A_{0}$ and the $\Box$ belongs to a non-principal positive family $o_{i}$ , then $\operatorname{\mathsf{an}}_{T}(A):=\boxdot_{i}\operatorname{\mathsf{an}}_{T}(A_{0})$ .

•

If $A=\Box A_{0}$ and the $\Box$ belongs to a negative family $n_{i}$ , then $\operatorname{\mathsf{an}}_{T}(A):=\boxminus_{i}\operatorname{\mathsf{an}}_{T}(A_{0})$ .

2.4 Realization

LP and S4 are closely related and LP can be understood as an explicit version of S4. The other way around, S4 can be seen as a version of LP with proof details removed or forgotten. We will establish this close relationship in this section formally by two main theorems translating valid LP formulas into valid S4 formulas and vice versa. The former is called forgetful projection, the latter is more complex and called realization.

Definition 9 (Forgetful Projection).

The forgetful projection $A^{\circ}$ of a LP formula $A$ is the following S4 formula:

•

if $A$ is atomic or $\bot$ , then $A^{\circ}:=A$ .

•

if $A$ is the formula $A_{0}\to A_{1}$ then $A^{\circ}:=A_{0}^{\circ}\to A_{1}^{\circ}$

•

if $A$ is the formula $t{:}A_{0}$ then $A^{\circ}:=\Box A_{0}$

The definition is expanded to sets, multisets and sequents of LP formulas in the natural way.

The forgetful projection maps LP theorems to S4 theorems.

Theorem 10.

If $\operatorname{LP}\vdash A$ then $S4\vdash A^{\circ}$ .

In the other direction, one can realize S4 formulas in LP by replacing the $\Box$ occurrences by explicit justification terms as defined below. Of course most of this realizations will not transform a theorem of S4 into a theorem of LP. So the realization theorem will only assert the existence of a specific realization producing a theorem of LP from a theorem of S4. The constructive proof for the realization theorem also provides us with an algorithm to generate one such realization. However, that realization is not necessarily the only possible realization or the simplest one.

Definition 11 (Realization Function).

A realization function $r_{T}$ for a proof $T$ is a mapping from the set of different $\Box$ symbols used in $\operatorname{\mathsf{an}}_{T}(T)$ to arbitrary LP terms.

Definition 12 (LP-Realization).

By an LP-realization of a modal formula $A$ we mean an assignment of proof polynomials to all occurrences of the modality in $A$ along with a constant specification of all constants occurring in those proof polynomials. By $A^{r}$ we understand the image of $A$ under a realization $r$ .

An LP-realization of $A$ is fully determined by a realization function $r_{T}$ relative to a proof tree for $\supset A$ and a constant specification of all constants occurring in $r_{T}$ with $A^{r}:=r_{T}(\operatorname{\mathsf{an}}_{T}(A))$ .

If we read $\Box A$ as there exists a proof for $A$ and $t{:}A$ as $t$ is a proof for $A$ , this process seems immediately reasonable. For the formula $\lnot\Box A$ , read as there is no proof of $A$ , and its realization $\lnot t{:}A$ , read as $t$ is not a proof of $A$ , on the other hand, that process seems wrong at first. But justification logic without any quantifications over proofs is still enough to capture the meaning of $\lnot\Box A$ by using Skolem’s idea of replacing quantifiers with functions. That is, we realize $\lnot\Box A$ using an implicitly all quantified justification variable $\lnot x{:}A$ . The same example formulated without the derived connective $\lnot$ is $x{:}A\to\bot$ . That formula can be read as function which produces a contradiction from a given proof $x$ for $A$ .

This last interpretation also hints at the role of complex justification terms using variables in a realization. They define functions from input proofs named by the variables to output proofs for different formulas. So a realization

[TABLE]

of an S4 formula $\Box A\to\Box B$ actually defines a function $t(x)$ producing a proof for $B$ from a proof $x$ for $A$ . This then is the Skolem style equivalent of the quantified formula $\exists(x)x{:}A\to\exists(y)y{:}B$ which is the direct reading of $\Box A\to\Box B$ (cf Artemov [3]). This discussion implies that we should replace $\Box$ with negative polarity with justification variables, which leads to the following definition of a normal realization:

Definition 13 (Normal).

A realization function is normal if all symbols for negative families and non-principal positive families are mapped to distinct variables. A LP-realization is normal if the corresponding realization function is normal and the CS is injective.

We are now ready to complete the connection between S4 and LP by the following realization theorem giving a constructive way of producing the necessary proof functions to realize a S4 theorem in LP:

Theorem 14 (Realization).

If $S4\vdash A$ then $\operatorname{LP}\vdash A^{r}$ for some normal LP-realization $r$ .

There are many proofs of the realization theorem available. Artemov [2] already established it in his original paper on the Logic of Proofs. Fitting [8] introduces a different proof-theoretic realization method. Adapting his method to nested sequent systems yields a modular realization theorem that covers many modal logics [11]. There is also a semantic proof of the realization theorem available [7] and Fitting [10] develops a general realization method that uses the model existence theorem. A realization theorem can sometimes be obtained using a translation from one logic into another [6, 9].

3 Prehistoric Relations in

G3s

3.1 Self-referentiality

As already mentioned in the introduction, the formulation of LP allows for terms $t$ to justify formulas $A(t)$ about themselves. We will see that such self-referential justification terms are not only possible, but actually unavoidable for realizing S4 even at the basic level of justification constants. That is to realize all S4 theorems in LP, we need self-referential constant specifications defined as follows:

Definition 15 (Self-Referential Constant Specification).

A constant specification CS is

•

directly self-referential if there is a constant $c$ such that $c{:}A(c)\in\operatorname{CS}$ .

•

self-referential if there is a subset $A\subseteq\operatorname{CS}$ such that

[TABLE]

A constant specification which is not directly self-referential is denoted by $\operatorname{CS}^{*}$ . Similarly a constant specification which is not self-referential at all is denoted by $\operatorname{CS}^{\odot}$ . So $\operatorname{CS}^{*}$ and $\operatorname{CS}^{\odot}$ stand for a class of constant specifications and not a single specific one. Following Yu [16], we use the notation $\operatorname{LP}(\operatorname{CS}^{\odot})\vdash A$ if there exists any non-self-referential constant specification CS such that $\operatorname{LP}(\operatorname{CS})\vdash A$ . There does exist a single maximal constant specification $\operatorname{CS}_{nds}$ that is not directly self-referential and for any theorem $A$ we have $\operatorname{LP}(\operatorname{CS}^{*})\vdash A$ iff $\operatorname{LP}(\operatorname{CS}_{nds})\vdash A$ .

Given that any S4 theorem is realizable in LP with some constant specification, we can carry over the definition of self-referentiality to S4 with the following definition:

Definition 16 (Self-Referential Theorem).

An S4 theorem $A$ is (directly) self-referential iff for any LP-realization $A^{r}$ we have that $\operatorname{LP}(\operatorname{CS}^{\odot})\not{\vdash}A^{r}$ (respectively $\operatorname{LP}(\operatorname{CS}^{*})\not{\vdash}A^{r}$ ).

Expanding on a first result for S4 in Brezhnev and Kuznets [5], Kuznets [12] explores the topic of self-referentiality on the level of individual modal logics and their justification counterparts. He gives theorems for the modal logics S4, D4, T, and K4 which can only be realized in their justification logic counterpart using directly self-referential constant specifications, i.e. directly self-referential theorems by the above definition. So for S4 in particular, Kuznets gives the theorem $\lnot\Box\lnot(S\to\Box S)$ and shows that it is directly self-referential.

We will not reproduce this result but use the logically equivalent formula $\lnot\Box(P\land\lnot\Box P)$ as an example for a self-referential S4 theorem. Notice that it does not directly follow from the above theorem that $\lnot\Box(P\land\lnot\Box P)$ can only be realized with a self-referential constant specification, as justification terms do not necessary apply to logically equivalent formulas. Still it should be fairly straightforward to show that $\lnot\Box(P\land\lnot\Box P)$ is self-referential by translating justification terms for the outer $\Box$ occurrences in the formulas $\lnot\Box(P\land\lnot\Box P)$ and $\lnot\Box\lnot(S\to\Box S)$ using the logical equivalence of $P\land\lnot\Box P$ and $\lnot(S\to\Box S)$ .

Looking at the G3s proof for $\lnot\Box(P\land\lnot\Box P)$ and a realization of that proof in figure 2, we can see why a self referential term like $t$ for the propositional tautology $P\land\lnot t\cdot x{:}P\to P$ is necessary. In order to prove $\lnot\Box(P\land\lnot\Box P)$ one needs to disprove $P\land\lnot\Box P$ at some point which means one has to prove $\Box P$ . The only way to prove $\Box P$ is using $\Box(P\land\lnot\Box P)$ as an assumption on the left. This leads to the situation that the proof introduces $\Box$ by a $(\supset\Box)$ rule where the same family already occurs on the left. In the following, we will see that such a situation is actually necessary for the self-referentiality of any S4 formula.

3.2 Prehistoric Relations

In his paper “Prehistoric Phenomena and Self-referentiality” [16], Yu gives a formal definition for the situation described in the last section, which he calls a prehistoric loop. In the later paper [18], Yu adopts the proper graph theoretic term cycle as we do here. Beside that change we will reproduce his definitions of prehistoric relation, prehistoric cycle as well as some basic lemmas about this new notions exactly as they were presented in the original paper.

To work with the $(\supset\Box)$ rules introducing occurrences of principal families in a G3s proof, we will use the following notation: we enumerate all $(\supset\Box)$ rules introducing an occurrence of the principal family $p_{i}$ as $R_{i,0},\ldots R_{i,l_{i}-1}$ and use $I_{i,0},\ldots I_{i,l_{i}-1}$ to denote the premises of those rules and $O_{i,0},\ldots O_{i,l_{i}-1}$ to denote their conclusions, see Yu [16]

Definition 17 (History).

In a root-leaf path $S$ of the form $S_{r}R^{*}O_{i,j}RI_{i,j}R^{*}S$ in a G3s-proof $T$ , the path $S_{r}R^{*}O_{i,j}$ is called a history of the family $p_{i}$ in the root-leaf path $S$ . The path $I_{i,j}R^{*}S$ is called a pre-history of $p_{i}$ in the root-leaf path $S$ .

So intuitively every $(\supset\Box)$ rule divides a root-leaf path of the proof tree into two parts. The first part from the root of the tree to the conclusion of the $(\supset\Box)$ rule of sequents having a copy of that $\Box$ symbol, i.e. the history of that $\Box$ symbol from its formation up to the root sequent. And the second part which predates the formation of that $\Box$ symbol, i.e. all sequents from the leaf up to the premise of that $(\supset\Box)$ rule, which do not have a copy of that symbol. The informal notion of “having a copy of that symbol” is not the same as correspondence, as it is not transitively closed. It is possible to have corresponding $\boxplus_{i}$ occurrences of a family $p_{i}$ in a prehistory of that same family. The proof in figure 2 of our example theorem exhibits this case.

As we are especially interested in these cases, that is occurrences of principal families in prehistoric periods, the following definition and lemma give that concept a precise meaning and notation:

Definition 18 (Prehistoric Relation).

For any principal positive families $p_{i}$ and $p_{h}$ and any root-leaf path $S$ of the form $S_{r}R^{*}O_{i,j}RI_{i,j}R\ast S$ in a S4 proof $\mathcal{T}=(T,R)$ :

(1)

If $\operatorname{\mathsf{an}}_{T}(I_{i,j})$ has the form $\boxminus_{k_{0}}B_{k_{0}},\ldots,\boxminus_{k}B_{k}(\boxplus_{h}C),\ldots,\boxminus_{k_{q}}B_{k_{q}}\supset A$ , then $p_{h}$ is a left prehistoric family of $p_{i}$ in $S$ with notation $h\prec^{S}_{L}i$ . 2. (2)

If $\operatorname{\mathsf{an}}_{T}(I_{i,j})$ has the form $\boxminus_{k_{0}}B_{k_{0}},\ldots,\boxminus_{k_{q}}B_{k_{q}}\supset A(\boxplus_{h}C)$ then $p_{h}$ is a right prehistoric family of $p_{i}$ in $S$ with notation $h\prec^{S}_{R}i$ . 3. (3)

The relation of prehistoric family in $S$ is defined by: $\prec^{S}:=\prec^{S}_{L}\cup\prec^{S}_{R}$ . The relation of (left, right) prehistoric family in $T$ is defined by:

[TABLE]

and $\prec:=\prec_{L}\cup\prec_{R}$ .

Even though both definitions so far use the notion of a prehistory, they do not directly refer to each other. But the following lemma provides the missing connection between these two definitions and therefore explains the common terminology:

Lemma 19.

There is an occurrence of $\boxplus_{h}$ in a pre-history of $p_{i}$ in the root-leaf path $S$ iff $h\prec^{S}i$ .

Proof.

( $\Rightarrow$ ): $\boxplus_{h}$ occurs in a sequent $S^{\prime}$ in a pre-history of $p_{i}$ in the root-leaf path $S$ , so $S$ has the form $S_{r}R^{*}O_{i,j}RI_{i,j}R^{*}S^{\prime}R^{*}S$ for some $j<l_{i}$ . By the subformula property, there is an occurrence of $\boxplus_{h}$ in $I_{i,j}$ as $S^{\prime}$ is part of $T\mathord{\upharpoonright}I_{i,j}$ . If this occurrence is on the left we have $h\prec^{S}_{L}i$ , if it is on right we have $h\prec^{S}_{R}i$ . In both cases $h\prec^{S}i$ holds.

( $\Leftarrow$ ): By definition there is a $I_{i,j}$ in $S$ , where $\boxplus_{h}$ occurs either on the left (for $h\prec^{S}_{L}i$ ) or on the right (for $h\prec^{S}_{R}i$ ). $I_{i,j}$ is part of the pre-history of $R_{i,j}$ in $S$ . ∎

Having introduced the concepts of prehistoric periods and prehistoric relations, we are now ready to define the concept of prehistoric cycles used in Yu’s theorem:

Definition 20 (Prehistoric Cycle).

In a G3s-proof $T$ , the ordered list of principal positive families $p_{i_{0}},\ldots,p_{i_{n-1}}$ with length $n$ is called a prehistoric cycle or left prehistoric cycle respectively, if we have: $i_{0}\prec i_{2}\prec\cdots\prec i_{n-1}\prec i_{0}$ or $i_{0}\prec_{L}i_{2}\prec_{L}\cdots\prec_{L}i_{n-1}\prec_{L}i_{0}$ .

In our example formula, we have a prehistoric cycle consisting of a single principal family which has a left prehistoric relation to itself. The following lemma shows that if a proof has a prehistoric cycle, then it also has a left prehistoric cycle:

Lemma 21.

$T$ * has a prehistoric cycle iff $T$ has a left prehistoric cycle.*

Finally, Yu [16] showed that left prehistoric cycles are necessary for self-referentiality

Theorem 22 (Necessity of Left Prehistoric Cycle for

Self-referentiality).

If a S4-theorem $A$ has a left-prehistoric-cycle-free G3s-proof, then there is a LP-formula $B$ s.t. $B^{\circ}=A$ and $\operatorname{LP}(\operatorname{CS}^{\odot})\vdash B$

4 Prehistoric Relations in

G3lp

4.1 Cut Rules

In this section we will prepare our discussion of prehistoric relations for LP, by first expanding the notion of families and prehistoric relations to the systems G3s + (Cut) and G3s + ( $\Box$ Cut) using cut rules. The (context sharing) cut rule has the following definition:

Definition 23 ((Cut) Rule).

$\Gamma\supset\Delta,A$ $A,\Gamma\supset\Delta$

(Cut)

$\Gamma\supset\Delta$

It is necessary to expand the definition of correspondence (def. 4) to (Cut) rules as follows:

Definition 24 (Correspondence for (Cut)).

The active formulas (and their symbols) in the premises of a (Cut) rule correspond to each other.

The classification and annotations for families of $\Box$ do not carry over to G3s + (Cut), as the (Cut) rule uses the cut formula in different polarities for the two premises. We therefore will consider all $\Box$ families for prehistoric relations in G3s + (Cut) proofs. This leads to the following expanded definition of prehistoric relation:

Definition 25 (Local Prehistoric Relation in G3s + (Cut)).

A family $\Box_{i}$ has a prehistoric relation to another family $\Box_{j}$ , in notation $i\prec j$ , if there is a $(\supset\Box)$ rule introducing an occurrence of $\Box_{j}$ with premise $S$ , such that there is an occurrence of $\Box_{i}$ in $S$ .

Notice that there can be prehistoric relations with $\Box$ families which locally have negative polarity, as the family could be part of a cut formula and therefore also occur with positive polarity in the other branch of the cut. On the other hand, adding prehistoric relations with negative families in a cut free G3s proof does not introduce prehistoric cycles, as in G3s a negative family is never introduced by a $(\supset\Box)$ rule and therefore has no prehistoric families itself. In G3s + (Cut) proofs, the subformula property and therefore also lemma 19 no longer hold. That means we can have an occurrence of a family $\Box$ as part of a cut formula in the global prehistory of a $(\supset\Box)$ rule, which by the local definition is not a local prehistoric family.

To handle terms $s\cdot t$ in the next section an additional rule for modus ponens under $\Box$ is necessary. We therefore introduce here the new rule ( $\Box$ Cut) as follows:

Definition 26 (( $\Box$ Cut) Rule).

[TABLE]

Again it is also necessary to expand the definition of correspondence (def. 4) for this rule:

Definition 27 (Correspondence for ( $\Box$ Cut)).

•

The topmost $\Box$ occurrence in the active formulas and the principal formula correspond to each other.

•

The subformulas $A$ in the active formulas of the premises correspond to each other.

•

The subformulas $B$ correspond to each other.

Notice that with this expansion $\Box$ occurrences of the same family no longer are always part of the same subformula $\Box C$ . Also similar to the (Cut) rule, correspondence is expanded to relate negative and positive occurrences of $\Box$ symbols as $A$ is used with different polarities in the two premises.

With the following lemmas and theorems we will establish a constructive proof for

[TABLE]

Moreover there will be corollaries showing that the constructions do not introduce prehistoric cycles by the new definition 25. As all prehistoric relations by the first definition 18 are included in the new definition, the final proof in G3s will be prehistoric-cycle-free by any definition if the original proof in G3s +( $\Box$ Cut) was prehistoric-cycle-free by the new definition.

We need the following standard result, which we mention without proof.

Lemma 28.

Weaking, inversion, and contraction are admissible in G3s. Moreover, for any annotation the constructed proofs do not introduce any new prehistoric relations.

It is important to note, that the second part of the lemma is not restricted to the annotations $\operatorname{\mathsf{an}}_{T}$ of the proofs $\mathcal{T}=(T,R)$ given by the premise of the lemma but still hold for arbitrary annotations $\operatorname{\mathsf{an}}$ . That means there is no implicit assumption that the families have only a single occurrence in the root sequents used in the lemma or theorem and the results can also be used in subtrees $T\mathord{\upharpoonright}S$ together with an annotation $\operatorname{\mathsf{an}}_{T}$ for the complete tree.

In the case for weakening, the second part of the lemma also follows from the fact 2.8 in Yu [18]. There, Yu looks at prehistoric relations locally, i.e. taking only correspondence up to the current sequent in consideration. That means the graph of prehistoric relations has to be updated going up the proof tree as new rules add new correspondences and therefore unify vertices in the prehistoric relations graph which were still separate in the premise. To work with such changing graphs, Yu introduces the notion of isolated families. He shows that all $\Box$ occurrences introduced by weakening are isolated. That means they have no prehistoric relations themselves, which globally means that they can not add any prehistoric relations from adding correspondences later in the proof. This is exactly what the second part asserts for weakening.

Theorem 29 (Cut Elimination for G3s).

If

[TABLE]

then $\operatorname{G3s}\vdash\Gamma\supset\Delta$ .

Proof.

By a simultaneous induction over the depths of the proof trees $\mathcal{T}_{L}$ for $\Gamma\supset\Delta,A$ and $\mathcal{T}_{R}$ for $A,\Gamma\supset\Delta$ as well as the rank of $A$ .

For us, the only interesting case is:

$A$ is a side formula in the last rule of $\mathcal{T}_{R}$ , which is a $(\supset\Box)$ rule and a principal formula in the last rule of $\mathcal{T}_{L}$ . Then $A$ has the form $\Box A_{0}$ as it is a side formula of a $(\supset\Box)$ on the right. So the last rule of $\mathcal{T}_{L}$ is also a $(\supset\Box)$ rule and the proof has the following form:

$\mathcal{T}_{L}$

$\Box\Gamma_{L}\supset A_{0}$

$(\supset\Box)$

$\Gamma^{\prime}_{L},\Box\Gamma_{L}\supset\Delta^{\prime},\Box B,\Box A_{0}$

$\mathcal{T}_{R}$

$\Box A_{0},\Box\Gamma_{R}\supset B$

$(\supset\Box)$

$\Gamma^{\prime}_{R},\Box A_{0},\Box\Gamma_{R}\supset\Delta^{\prime},\Box B$

(Cut)

$\Gamma\supset\Delta^{\prime},\Box B$

where $\Delta=\Delta^{\prime},\Box B$ and $\Gamma=\Gamma^{\prime}_{L},\Box\Gamma_{L}=\Gamma^{\prime}_{R},\Box\Gamma_{R}$ .

The cut can be moved up on the right using weakening as follows:

$\mathcal{T}_{L}$

$\Box\Gamma_{L}\supset A_{0}$

$(\supset\Box)$

$\Box\Gamma_{R},\Box\Gamma_{L}\supset B,\Box A_{0}$

$\mathcal{T}^{\prime}_{R}$

$\Box A_{0},\Box\Gamma_{R},\Box\Gamma_{L}\supset B$

(Cut)

$\Box\Gamma_{R},\Box\Gamma_{L}\supset B$

$(\supset\Box)$

$\Gamma,\Box\Gamma_{R},\Box\Gamma_{L}\supset\Delta^{\prime},\Box B$

By the induction hypothesis and a contraction we get the required proof for $\Gamma\supset\Delta$ as $\Box\Gamma_{L}\subseteq\Gamma$ and $\Box\Gamma_{R}\subseteq\Gamma$ . ∎

Corollary 30.

For any annotation $\operatorname{\mathsf{an}}$ the constructed proof for $\Gamma\supset\Delta$ only introduces new prehistoric relations $i\prec j$ between families $\Box_{i}$ and $\Box_{j}$ occurring in $\Gamma\supset\Delta$ where there exists a family $\Box_{k}$ in $A$ such that $i\prec k\prec j$ in the original proof.

Proof.

The only place where new prehistoric relations get introduced is by the new $(\supset\Box)$ in the case shown above. All prehistoric relations from $\Box\Gamma_{R}$ are already present from the $(\supset\Box)$ rule on the right in the original proof. So only prehistoric relations from $\Box\Gamma_{L}$ are new. For all families $\Box_{i}$ in $\Box\Gamma_{L}$ we have $i\prec k$ for the family $\Box_{k}$ in the cut formula introduced by the $(\supset\Box)$ rule on the left. Moreover $k\prec j$ for the same family because of the occurrence of $\Box A_{0}$ on the right. ∎

Corollary 31.

For any annotation $\operatorname{\mathsf{an}}$ the constructed proof for $\Gamma\supset\Delta$ does not introduce prehistoric cycles.

Proof.

Assume for contradiction that there exists a prehistoric cycle

[TABLE]

in the new proof. By the previous lemma for any prehistoric relation

[TABLE]

in the cycle either $i_{k}\prec i_{k+1\mod n}$ in the original proof or there is a family $i^{\prime}_{k}$ in the cut formula such that $i_{k}\prec i^{\prime}_{k}\prec i_{k+1\mod n}$ in the original proof. Therefore we also have a prehistoric cycle in the original proof. ∎

Theorem 32 (( $\Box$ Cut) Elimination).

If

[TABLE]

then $\operatorname{G3s}\vdash\Gamma\supset\Delta,\Box B$

Proof.

By a structural induction over the proof trees $\mathcal{T}_{L}$ for $\Gamma\supset\Delta,\Box A,\Box B$ and $\mathcal{T}_{R}$ for $\Gamma\supset\Delta,\Box(A\to B),\Box B$ .

1. case: $\Box(A\to B)$ or $\Box A$ is a weakening formula of the last rule. Then removing them from that proof gives the required proof. This includes the case when $\Box B$ is the principal formula of the last rule of either proof, as then the last rule is $(\supset\Box)$ which has no side formulas on the right.

2. case: $\Box(A\to B)$ or $\Box A$ is a side formula of the last rule. Then also $\Box B$ is a side formula of that rule. Use the induction hypothesis on the premises of that rule with the other proof and append the same rule.

3. case: $\Box(A\to B)$ and $\Box A$ are the principal formula of the last rule. Then the last rules have the following form:

$\mathcal{T}_{L}$

$\Box\Gamma_{L}\supset A$

$(\supset\Box)$

$\Gamma_{L}^{\prime},\Box\Gamma_{L}\supset\Delta,\Box A,\Box B$

$\mathcal{T}_{R}$

$\Box\Gamma_{R}\supset A\to B$

$(\supset\Box)$

$\Gamma^{\prime}_{R},\Box\Gamma_{R}\supset\Delta,\Box(A\to B),\Box B$

( $\Box$ Cut)

$\Gamma\supset\Delta,\Box B$

where $\Delta=\Delta^{\prime},\Box B$ and $\Gamma=\Gamma^{\prime}_{L},\Box\Gamma_{L}=\Gamma^{\prime}_{R},\Box\Gamma_{R}$ .

By inversion for $(\supset\to)$ we get a proof $\mathcal{T}^{\prime}_{R}$ for $A,\Box\Gamma_{R}\supset B$ from the first premise $\Box\Gamma_{R}\supset A\to B$ . Using weakening and a normal cut on the formula $A$ we get the following proof:

$\mathcal{T}^{\prime}_{L}$

$\Box\Gamma_{L},\Box\Gamma_{R}\supset A$

$\mathcal{T}^{\prime\prime}_{R}$

$A,\Box\Gamma_{L},\Box\Gamma_{R}\supset B$

(Cut)

$\Box\Gamma_{L},\Box\Gamma_{R}\supset B$

$(\supset\Box)$

$\Gamma,\Box\Gamma_{L},\Box\Gamma_{R}\supset\Delta,\Box B$

By contraction and a cut elimination we get the required G3s proof for $\Gamma\supset\Delta,\Box B$ as $\Box\Gamma_{L}\subseteq\Gamma$ and $\Box\Gamma_{R}\subseteq\Gamma$ . ∎

Corollary 33.

For any annotation $\operatorname{\mathsf{an}}$ the constructed proof for $\Gamma\supset\Delta,\Box B$ does not introduce prehistoric cycles.

Proof.

Removing weakening or side formulas $\Box(A\to B)$ or $\Box A$ as in case 1 and 2 does not introduce new prehistoric relations.

Any prehistoric relation because of the new $(\supset\Box)$ rule in case 3 already exists in the original proof, as every $\Box$ occurrence in $\Box\Gamma_{L}$ or $\Box\Gamma_{R}$ also occurs in one of the two $(\supset\Box)$ rules in the original proof, which both introduce a $\Box$ of the same family as $\Box B$ by the definition of correspondence for ( $\Box$ Cut).

So the new proof with ( $\Box$ Cut) rules replaced by (Cut) rules does not introduce new prehistoric relations and therefore also no new prehistoric cycles. By corollary 31, the cut elimination to get a G3s proof does not introduce prehistoric cycles. ∎

Definition 34.

The cycle-free fragment of a system $Y$ , denoted by $Y^{\otimes}$ , is the collection of all sequents that each have a prehistoric-cycle-free $Y$ -proof.

Theorem 35.

The cycle-free fragments of G3s + ( $\Box$ Cut), G3s + (Cut) and G3s are identical.

Proof.

A prehistoric-cycle-free proof in G3s by the original definition 18 is also prehistoric-cycle-free by the new definition 25 as a negative family can not have any prehistoric families itself in a G3s-proof . So any sequent

[TABLE]

is trivially also provable prehistoric-cycle-free in G3s + (Cut) and G3s + ( $\Box$ Cut) and we have $\operatorname{G3s}^{\otimes}\subseteq(\operatorname{G3s}+(\Box\operatorname{Cut}))^{\otimes}$ and $\operatorname{G3s}^{\otimes}\subseteq(\operatorname{G3s}+(\operatorname{Cut}))^{\otimes}$ . Moreover $(\operatorname{G3s}+(\operatorname{Cut}))^{\otimes}\subseteq\operatorname{G3s}^{\otimes}$ by corollary 31 and

[TABLE]

by corollary 33. All together we get

[TABLE]

Yu [18, th. 2.21] shows that non-self-referentiality is not normal in T, K4, and S4. The results in this section hint at an explanation for this fact for S4 and at the possibility to still use modus ponens with further restrictions in the non-self-referential subset of S4. Namely, to consider the global aspects of self-referentiality coming from correspondence of occurrences, it is necessary when combining two proofs, that the two proofs together with the correct correspondences added are prehistoric-cycle-free. So we can only use modus ponens on two non-self-referential S4 theorems $A$ and $A\to B$ if there are proofs of $A$ and $A\to B$ such that the prehistoric relations of these proofs combined, together with identifying the occurrences of $A$ in both proofs, are prehistoric-cycle-free. In that case we get a prehistoric-cycle-free G3s proof for $B$ using cut elimination and corollary 30, which shows that $B$ is also non-self-referential.

4.2 A sufficient condition for self-referentiality

Cornelia Pulver [14] introduces the system LPG3 by expanding G3c with rules for the build up of justification terms as well as the new axioms (Axc) and (Axt). To ensure that the contraction lemma holds, all rules have to be invertible, which is the reason why contracting variants of all the justification rules are used for LPG3. Our variant G3lp will use the same rules to build up terms, but replace the axioms with rules $(\supset:)_{c}$ and $(\supset:)_{t}$ to keep the prehistoric relations of the proof intact. As there is a proof for $\supset A$ for any axiom $A$ and also for $A\supset A$ for any formula $A$ , these two rules are equivalent to the two axioms and invertible.

As we already did with G3s, we will use the full system with all classical operators for examples, but only the minimal subset with $\to$ and $\bot$ for proofs. So these two systems use the classical rules from G3s as well as the new LP rules in figure 3.

This system is adequate for the logic of proofs LP as shown in corollary 4.37 in Pulver [14]. It also allows for weakening, contraction and inversion. By corollary 4.36 in the same paper, G3lp without the $(\supset:)_{c}$ rule is equivalent to $\operatorname{LP}_{0}$ . Neither Pulver [14] nor Artemov [2] define Gentzen systems for a restricted logic of proofs LP(CS), perhaps because it seems obvious that restricting whatever rule is used for introducing proof constants to CS gives a Gentzen system for LP(CS).

To work with prehistoric relations in G3lp proofs we need the following new or adapted definitions:

Definition 36 (Subformula).

The set of subformulas $\operatorname{sub}(A)$ of a LP formula $A$ is inductively defined as follows:

$\operatorname{sub}(P)=\{P\}$ for any atomic formula $P$ 2. 2.

$\operatorname{sub}(\bot)=\{\bot\}$ 3. 3.

$\operatorname{sub}(A_{0}\to A_{1})=\operatorname{sub}(A_{0})\cup\operatorname{sub}(A_{1})\cup\{A_{0}\to A_{1}\}$ 4. 4.

$\operatorname{sub}(s+t{:}A_{0})=\operatorname{sub}(A_{0})\cup\{s{:}A_{0},t{:}A_{0},s+t{:}A_{0}\}$ 5. 5.

$\operatorname{sub}(t{:}A_{0})=\operatorname{sub}(A_{0})\cup\{t{:}A_{0}\}$

Definition 37 (Subterm).

The set of subterms $\operatorname{sub}(t)$ of a LP justification term $t$ is inductively defined as follows:

$\operatorname{sub}(x)=\{x\}$ for any variable $x$ 2. 2.

$\operatorname{sub}(c)=\{c\}$ for any constant $c$ 3. 3.

$\operatorname{sub}(!t)=\operatorname{sub}(t)\cup\{!t\}$ 4. 4.

$\operatorname{sub}(s+t)=\operatorname{sub}(s)\cup\operatorname{sub}(t)\cup\{s+t\}$ 5. 5.

$\operatorname{sub}(s\cdot t)=\operatorname{sub}(s)\cup\operatorname{sub}(t)\cup\{s\cdot t\}$

The set of subterms $\operatorname{sub}(A)$ of a LP formula $A$ is the union of all sets of subterms for all terms occurring in $A$ .

We use the symbol $\operatorname{sub}$ for all definitions of subterms and subformulas, as it will be clear from context which of the definitions is meant. Notice that by this definition $s{:}A$ is a subformula of $s+t{:}A$ .

We expand the definition of correspondence to G3lp proofs as follows:

Definition 38 (Correspondence in G3lp).

All topmost terms in active or principal formulas in the rules $(\supset\cdot)$ , $(\supset+)$ $(\supset!)$ and $({:}\supset)$ correspond to each other.

Notice that in the $(\supset!)$ rule, the topmost term $t$ in the contraction formula therefore corresponds to the topmost proof term $!t$ in the principal formula. The term $t$ of the other active formula $!t{:}t{:}A$ on the other hand corresponds to the same term $t$ in the principal formula.

By this definition, families of terms in G3lp consist not of occurrences of a single term $t$ but of occurrences of subterms $s$ of a top level term $t$ . We will use $\bar{t}$ for the family of occurrences corresponding to the top level term $t$ , i.e. seen as a set of terms instead of term occurrences we have $\bar{t}\subseteq\operatorname{sub}(t)$ . So for any term occurrence $s$ , $\bar{s}$ is not necessarily the full family of $s$ in the complete proof tree as $s$ could be a subterm of the top level term $t$ of the family. For any occurrence $s$ in a sequent $S$ of the proof tree though, $\bar{s}$ is the family of $s$ relative to the subtree $T\mathord{\upharpoonright}S$ as all related terms in the premises of G3lp rules are subterms of the related term in the conclusion.

We also see that most rules of G3lp only relate terms to each other used for the same subformula $A$ . The two exceptions are the $(\supset\cdot)$ rule and the $(\supset!)$ rule. Similar to the cut rules from the previous section, $(\supset\cdot)$ relates subformulas and symbols of different polarities as well as terms used for different formulas. So we will use the same approach to define prehistoric relations of term families for any polarity:

Definition 39 (Prehistoric Relation in G3lp).

A family $\bar{t_{i}}$ has a prehistoric relation to another family $\bar{t_{j}}$ , in notation $i\prec j$ , if there is a $(\supset:)$ rule introducing an occurrence belonging to $\bar{t_{j}}$ with premise $S$ , such that there is an occurrence belonging to $\bar{t_{i}}$ in $S$ .

Given that we now have defined families of terms and prehistoric relations between them in G3lp, it is interesting to see what happens with this relations if we look at the forgetful projection of a G3lp proof. That is, what happens on the G3s side if we construct a proof tree with the forgetful projections of the original sequents. Of course we do not get a pure G3s proof as most of the G3lp rules have no direct equivalent in G3s. We will therefore define new rules, which are the forgetful projection of a G3lp rule denoted for example by $(\supset!)^{\circ}$ for the forgetful projection of a $(\supset!)$ rule. The following two lemmas show that all this new rules are admissible in G3s + $(\Box\operatorname{Cut})$ .

Lemma 40.

$\operatorname{G3lp}\vdash\Gamma\supset\Delta,\Box A$ * iff $\operatorname{G3lp}\vdash\Gamma\supset\Delta,\Box\Box A$ .*

Proof.

The ( $\Leftarrow$ ) direction is just inversion for $(\supset\Box)$ . The ( $\Rightarrow$ ) direction is proven by the following structural induction:

1. case: $\Box A$ is a weakening formula of the last rule. Just weaken in $\Box\Box A$ .

2. case: $\Box A$ is a side formula of the last rule. Use the induction hypothesis on the premises and append the same last rule.

3. case: $\Box A$ is the principal formula of the last rule. Then the last rule is a $(\supset\Box)$ rule and has the following form:

$\Box\Gamma\supset A$

$(\supset\Box)$

$\Gamma^{\prime},\Box\Gamma\supset\Delta,\Box A$

Use an additional $(\supset\Box)$ rule to get the necessary proof as follows:

$\Box\Gamma\supset A$

$(\supset\Box)$

$\Box\Gamma\supset\Box A$

$(\supset\Box)$

$\Gamma^{\prime},\Box\Gamma\supset\Delta,\Box\Box A$

∎

Lemma 41.

The forgetful projection of all rules in G3lp are admissible in G3s + ( $\Box$ Cut).

Proof.

The subset G3c is shared by G3lp and G3s and is therefore trivially admissible. The forgetful projection of the rule $(\supset+)$ is just a contraction and therefore also admissible. The forgetful projection of the rules $(\supset:)_{t}$ and $(\supset:)_{c}$ are $(\supset\Box)$ rules in G3s. The forgetful projection of $(\supset\cdot)$ is a $(\Box\operatorname{Cut})$ . Finally the forgetful projection of a $(\supset!)$ rule has the following form:

$\Gamma\supset\Delta,\Box A,\Box\Box A$

$(\supset!)^{\circ}$

$\Gamma\supset\Delta,\Box\Box A$

That rule is admissible by lemma 40 and a contraction. ∎

Instead of working with a G3s system with all this extra rules included, we will define a forgetful projection from a G3lp proof to a G3s + $(\Box\operatorname{Cut})$ proof by eliminating all contractions using the algorithm implicitly defined in the proof of contraction admissibility and eliminating the $(\supset!)^{\circ}$ rules by the algorithm implicitly described in the proof for lemma 40.

For the following lemmas and proofs we fix an arbitrary G3lp proof $\mathcal{T}=(T,R)$ and its forgetful projection $\mathcal{T}^{\circ}=(T^{\prime},R^{\prime})$ as defined below.

Definition 42 (Forgetful Projection of a G3lp Proof).

The forgetful projection of a G3lp proof $\mathcal{T}=(T,R)$ for a LP sequent $\Gamma\supset\Delta$ is the G3s + $(\Box\operatorname{Cut})$ proof $\mathcal{T}^{\circ}=(T^{\prime},R^{\prime})$ for $\Gamma^{\circ}\supset\Delta^{\circ}$ inductively defined as follows:

case: The last rule of $\mathcal{T}$ is an axiom. Then $\mathcal{T}^{\circ}$ is just $\Gamma^{\circ}\supset\Delta^{\circ}$ which is an axiom of G3s.
case: The last rule of $\mathcal{T}$ is a $(\supset\to)$ or a $(\to\supset)$ rule with premises $S_{i}$ . Then $\mathcal{T}^{\circ}$ has the same last rule with $(\mathcal{T}\mathord{\upharpoonright}S_{i})^{\circ}$ as proofs for the premises $S_{i}^{\circ}$ .
case: The last rule of $\mathcal{T}$ is a $(\supset:)_{c}$ or $(\supset:)_{t}$ rule with premise $S$ . Then $\mathcal{T}^{\circ}$ has a $(\supset\Box)$ as last rule with $(\mathcal{T}\mathord{\upharpoonright}S)^{\circ}$ as proof for the premise $S^{\circ}$ .
case: The last rule of $\mathcal{T}$ is a $(\supset+)$ rule with premise $S$ . Then $\mathcal{T}^{\circ}$ is $(\mathcal{T}\mathord{\upharpoonright}S)^{\circ}$ with the necessary contraction applied.
case: The last rule of $\mathcal{T}$ is a $(\supset\cdot)$ rule with premises $S_{0}$ and $S_{1}$ . Then $\mathcal{T}^{\circ}$ has a $(\Box\operatorname{Cut})$ as last rule with $(\mathcal{T}\mathord{\upharpoonright}S_{i})^{\circ}$ as proofs for the premises $S_{i}^{\circ}$ .
case: The last rule of $\mathcal{T}$ is a $(\supset!)$ rule with premise $S$ . Then we get a G3s + $(\Box\operatorname{Cut})$ proof for $\Gamma^{\circ}\supset\Delta^{\circ},\Box\Box A$ from the proof $(\mathcal{T}\mathord{\upharpoonright}S)^{\circ}$ by lemma 40. $\mathcal{T}^{\circ}$ is that proof with the additional $\Box\Box A$ removed by contraction as $\Box\Box A\in\Delta^{\circ}$ .

To reason about the relations between a G3lp proof $\mathcal{T}$ and its forgetful projection $\mathcal{T}^{\circ}$ , the following algorithm to construct $\mathcal{T}^{\circ}$ is useful:

Replace all sequents by their forgetful projection. 2. 2.

Add the additional $(\supset\Box)$ rules and prepend additional $\Box$ where necessary, so that the forgetful projections of $(\supset!)$ reduce to simple contractions. 3. 3.

Eliminate all contractions to get a G3s + $(\Box\operatorname{Cut})$ proof.

It is not immediately clear that contracting formulas only removes occurrences as the proof uses inversion which in turn also adds weakening formulas. But all the deconstructed parts weakened in this way get contracted again in the next step of the contraction. In the end the contracted proof tree is always a subset of the original proof tree.

That means that also $\mathcal{T}^{\circ}$ is a subset of the tree constructed in step 2 of the algorithm. From this we see that all $\Box$ occurrences in $\mathcal{T}^{\circ}$ have a term occurrence in $\mathcal{T}$ mapped to them if we consider the extra $\Box$ occurrences introduced in step 2 (resp. in case 6 of the definition) as replacements of the same term as the $\Box$ occurrences they are contracted with and also consider the extra sequents $\Box\Gamma\supset\Box A$ introduced in step 2 as copies of the same formulas in the original sequent $\Gamma^{\prime},\Box\Gamma\supset\Delta,\Box A$ derived by the original $(\supset\Box)$ rule.

Lemma 43.

For any family $f_{i}$ of $\Box$ occurrences in $\mathcal{T}^{\circ}$ there is a unique proof term family $\bar{t}_{\tilde{i}}$ in $\mathcal{T}$ such that $s\in\bar{t}_{\tilde{i}}$ for all proof term occurrences $s$ mapped to $\Box$ occurrences in $f_{i}$ .

Proof.

For any two directly corresponding $\Box$ occurrences we show that the two mapped term occurrences correspond directly or by reflexive closure:

1. case: The two $\Box$ occurrences are added in step 2 of the algorithm. Then the mapped term occurrences are the same occurrence and correspond by reflexive closure.

2. case: The two $\Box$ occurrence correspond directly by a rule which is the forgetful projection of a rule in $\mathcal{T}$ . Then the mapped term occurrences also correspond as all G3lp rules with a direct equivalent in G3s have the same correspondences. Notice that lemma 40 only removes weakening formulas from existing $(\supset\Box)$ rules. So this still holds for $(\supset\Box)$ rules and their corresponding $(\supset:)$ rules even after applying lemma 40.

3. case: The two $\Box$ occurrences correspond directly by a $(\supset\Box)$ rule added in step 2 of the algorithm. Then the rule together with the previous rule has the following form:

$\Box\Gamma\supset A$

$(\supset\Box)$

$\Box\Gamma\supset\Box A$

$(\supset\Box)$

$\Gamma^{\prime},\Box\Gamma\supset\Delta,\Box\Box A$

As the formulas in $\Box\Gamma\supset\Box A$ are considered copies of the original sequent $\Gamma^{\prime},\Box\Gamma\supset\Delta,\Box A$ , and the sequent $\Gamma^{\prime},\Box\Gamma\supset\Delta,\Box\Box A$ is considered the same sequent with an additional $\Box$ symbol, the mapped term occurrences are actually the same and therefore correspond by reflexive closure.

As direct correspondence in the G3s proof is a subset of correspondence in the G3lp proof, so is its transitive and reflexive closure. So for any two corresponding $\Box$ occurrences of a family $f_{i}$ the mapped term occurrences also correspond and therefore belong to the same family $\bar{t}_{\tilde{i}}$ . ∎

Lemma 44.

If $i\prec j$ in $\mathcal{T}^{\circ}$ then either $\tilde{i}=\tilde{j}$ or $\tilde{i}\prec\tilde{j}$ in $\mathcal{T}$ for the term families $\bar{t}_{\tilde{i}}$ and $\bar{t}_{\tilde{j}}$ from the previous lemma.

Proof.

$i\prec j$ in $\mathcal{T}^{\circ}$ , so there is a $(\supset\Box)$ rule in $\mathcal{T}^{\circ}$ introducing an occurrence $\Box_{j}$ of $f_{j}$ with an occurrence $\Box_{i}$ of $f_{i}$ in the premise. For the mapped term occurrences $s_{i}$ and $s_{j}$ in $\mathcal{T}$ we have $s_{i}\in\bar{t}_{\tilde{i}}$ and $s_{j}\in\bar{t}_{\tilde{j}}$ by the previous lemma. From this it follows that $\tilde{i}\prec\tilde{j}$ or $\tilde{i}=\tilde{j}$ by an induction on the proof height:

1. case: The $(\supset\Box)$ rule is the forgetful projection of a $(\supset:)$ rule. Then we have $\tilde{i}\prec\tilde{j}$ directly by the definition of prehistoric relations for G3lp proofs using the occurrences $s_{i}$ in the premise of the rule $(\supset:)$ introducing the occurrence $s_{j}$ .

2. case: The $(\supset\Box)$ rule is added in step 2 of the algorithm. Then the rule together with the previous rule has the following form:

$\Box\Gamma\supset A$

$(\supset\Box)$

$\Box\Gamma\supset\Box_{k}A$

$(\supset\Box)$

$\Gamma^{\prime},\Box\Gamma\supset\Delta,\Box_{j}\Box_{k}A$

For the term occurrence $s_{k}$ mapped to the occurrence $\Box_{k}$ we have $s_{j}=!s_{k}$ and $s_{k}\in\bar{t}_{\tilde{j}}$ as $s_{j}$ is the top level term of the principal formula of a $(\supset!)$ rule. If the occurrence $\Box_{i}$ is the occurrence $\Box_{k}$ then $\tilde{i}=\tilde{j}$ and we are finished. If the occurrence $\Box_{i}$ is not the occurrence $\Box_{k}$ then there is a corresponding occurrence $\Box^{\prime}_{i}$ with a corresponding mapped term $s^{\prime}_{i}$ in the sequent $\Box\Gamma\supset A$ and we have $i\prec k$ from the previous $(\supset\Box)$ . As $\bar{t}_{\tilde{j}}$ is also the term family of $s_{k}$ we get $\tilde{i}\prec\tilde{j}$ or $\tilde{i}=\tilde{j}$ by induction hypothesis on the shorter proof up to the that $(\supset\Box)$ rule with the occurrences $\Box^{\prime}_{i}$ , $s^{\prime}_{i}$ , $\Box_{k}$ and $s_{k}$ . ∎

Corollary 45.

If $\mathcal{T}$ is prehistoric-cycle-free then also $\mathcal{T}^{\circ}$ is prehistoric-cycle-free.

Proof.

The contraposition follows directly from the lemma as for any cycle

[TABLE]

we get a cycle in $\mathcal{T}$ by removing duplicates in the list $\tilde{i}_{0},\ldots,\tilde{i}_{n}$ of mapped term families $\bar{t}_{\tilde{i}_{0}},\ldots\bar{t}_{\tilde{i}_{n}}$ . ∎

We will now come back to our example formula $\lnot\Box(P\land\lnot\Box P)$ from section 3.1. Figure LABEL:g3lpproof contains a proof of the same realization $\lnot x{:}(P\land\lnot t\cdot x{:}P)$ in G3lp as well as the forgetful projection of that proof in G3s + ( $\Box$ Cut). For simplicity we assumed that $(A\land B\to A)$ is an axiom A0 and therefore $t$ is a constant.

This proofs display the logical dependencies that make the formula self-referential in quite a different way than the original G3s proof in figure 2. There are three families of $\Box$ in the G3s + ( $\Box$ Cut) proof. Two are the same families as in the G3s proof, occur in the root sequent and have a consistent polarity throughout the proof. We therefore simply use the symbols $\boxplus$ and $\boxminus$ for this families. The third one is part of the cut formula and therefore does not occur in the final sequent and does not have consistent polarity throughout the proof. We use $\Box$ for occurrences of this family in the proof.

All left prehistoric relations of the proof are from left branch of the cut where we have $\boxminus\prec_{L}\boxplus$ and the cycle $\boxplus\prec_{L}\boxplus$ . Other than in the G3s proof, the two $\boxplus$ occurrences are used for different formulas $P$ and $P\land\lnot\Box P$ and the connection between the two is established by the ( $\Box$ Cut) with $\Box(P\land\lnot\Box P\to P)$ . A similar situation is necessary for any prehistoric cycle in a G3lp proof as we will show formally.

Lemma 46.

All occurrences belonging to a term family $\bar{t}$ in a premise $S$ of any $(\supset:)$ rule are occurrences of the top level term $t$ itself.

Proof.

All G3lp rules only relate different terms if they are top level terms on the right. All occurrences of $s\in\bar{t}$ in a premise $S$ of a $(\supset:)$ rule correspond either as part of a strict subformula on the right or as part of a subformula on the left of the conclusion. A formula on the left can only correspond to a subformula on the right as a strict subformula. Therefore all corresponding occurrences of $s$ on the right in the remaining path up to the root are part of a strict subformula and so all corresponding occurrences of $s$ , left or right, in the remaining path are occurrences of the same term $s$ . As $t$ itself is a corresponding occurrence of $s$ in that path, we get $t=s$ . ∎

Corollary 47.

If $i\prec j$ for two term families $\bar{t_{i}}$ and $\bar{t_{j}}$ of a G3lp proof, then there is $(\supset:)$ rule introducing an occurrence $s\in\bar{t_{j}}$ in a formula $s{:}A$ such that there is an occurrence of $t_{i}$ in $s{:}A$ (as a term, not as a family, i.e. the occurrence of $t_{i}$ is not necessary in $\bar{t_{i}}$ ).

Proof.

Follows directly from the lemma and the definition of prehistoric relations for G3lp. ∎

The last corollary gives us a close relationship between prehistoric relations in G3lp and occurrences of terms in $(\supset:)$ rules. But it does not differentiate between the two variants $(\supset:)_{c}$ and $(\supset:)_{t}$ used for introducing elements from CS and input formulas $t{:}A$ . It is therefore necessary to expand the definition of self-referentiality by considering all basic justifications and not only the justification constants:

Definition 48 (Inputs).

The inputs IN of a G3lp proof are all LP formulas that are the principal formula of a $(\supset:)_{t}$ or $(\supset:)_{c}$ rule.

Notice that the used constant specifications CS is a subset of the inputs IN. The interpretation here is that $(\supset:)_{t}$ introduces arguments to Skolem style functions by proving the trivial identity function $t{:}A\to t{:}A$ . So we have two different clearly marked sources of basic proofs in G3lp, on the one hand there are the constants justifying known axioms, on the other hand there are presupposed existing proofs or arguments to proof functions. Based on this expanded notion, we can also expand the definition of self-referentiality to input sets:

Definition 49 (Self-Referential Inputs).

A input set IN is

•

directly self-referential if there is a term $t$ such that $t{:}A(t)\in\operatorname{IN}$ .

•

self-referential if there is a subset $A\subseteq\operatorname{IN}$ such that

[TABLE]

With this definitions we finally arrive at our main result, a counterpart to Yu’s theorem.

Theorem 50.

If the input set IN of a G3lp proof is non-self-referential, then the proof is prehistoric-cycle-free.

Proof.

We show the contraposition. Assume there is a prehistoric cycle

[TABLE]

By corollary 47 there exists formulas $s_{k}{:}A_{k}$ in IN such that $t_{i_{k}}\in\operatorname{sub}(A_{k})$ and $s_{k}\in\operatorname{sub}(t_{i_{k^{\prime}}})$ with $k^{\prime}:=k+1\mod n$ . From the latter and $t_{i_{k^{\prime}}}\in\operatorname{sub}(A_{k^{\prime}})$ follows $s_{k}\in\operatorname{sub}(A_{k^{\prime}})$ . So $\{s_{k}{:}A_{k}\ |0\leq k<n\}\subseteq\operatorname{IN}$ is a self-referential subset of IN. ∎

Corollary 51.

The forgetful projection $A^{\circ}$ of an LP formula $A$ provable with a non-self-referential input set IN is provable prehistoric-cycle-free in G3s.

Proof.

Suppose that $\mathcal{T}$ is a proof of $A$ from non-self-referential inputs IN. Then $\mathcal{T}$ is prehistoric-cycle-free as proven above. So by corollary 45 $\mathcal{T}^{\circ}$ is a prehistoric-cycle-free proof of $A^{\circ}$ in $\operatorname{G3s}+(\Box\operatorname{Cut})$ . Finally there is a prehistoric-cycle-free proof of $A^{\circ}$ in G3s by corollary 33. ∎

4.3 Counterexample

The main result of the last section does not exactly match Yu’s result. We have shown that prehistoric cycles in G3s are sufficient for self-referentiality but only for the expanded definition of self-referentiality considering the set of all inputs IN. The question arises if this expansion is actually necessary. The following counterexample shows that indeed, prehistoric cycles in G3s are not sufficient for needing a self-referential CS.

Lemma 52.

The S4 formula $A\equiv\Box(P\land\lnot\Box P\to P)\to\lnot\Box(P\land\lnot\Box P)$ has a realization in $\operatorname{LPG}_{0}$ .

Proof.

Set $A^{r}\equiv y{:}(P\land\lnot y\cdot x{:}P\to P)\to\lnot x{:}(P\land\lnot y\cdot x{:}P)$ . We have

[TABLE]

by the same derivation as for $\operatorname{LP}\vdash\lnot x{:}(P\land\lnot t\cdot x{:}P)$ replacing the introduction of $t{:}(P\land\lnot t\cdot x{:}P\to P)$ by the assumption $y{:}(P\land\lnot y\cdot x{:}P\to P)$ and $t$ by $y$ . So by the deduction theorem $\operatorname{LPG}_{0}\vdash y{:}(P\land\lnot y\cdot x{:}P\to P)\to\lnot x{:}(P\land\lnot y\cdot x{:}P)$ .444If we assume that $P\land\lnot y\cdot x{:}P\to P$ is an axiom A0, this matches the more general result in corollary 7.2 in Artemov [2]: $\operatorname{LP}(\operatorname{CS})\vdash F$ if and only if $\operatorname{LPG}_{0}\vdash\operatorname{CS}\supset F$ . ∎

Lemma 53.

The S4 formula $\Box(P\land\lnot\Box P\to P)\to\lnot\Box(P\land\lnot\Box P)$ has no prehistoric-cycle-free proof.

Proof.

By inversion for G3s in one direction and an easy deduction in the other, we have

[TABLE]

iff

[TABLE]

In both directions the proofs remain prehistoric-cycle-free if the other proof was prehistoric-cycle-free. For a proof of $\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset$ we have two possibilities for the last rule:

1. case: The last rule is a $(\Box\supset)$ rule with $\Box(P\land\lnot\Box P\to P)$ as the principal formula. Then the following proof tree shows that we need a proof for the sequent $P,\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset$ which is just the original sequent weakened by $P$ on the left:

$P\land\lnot\Box P,\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset P\land\lnot\Box P$

$(\Box\supset)$

$\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset P\land\lnot\Box P$

$P,\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset$

$(\to\supset)$

$P\land\lnot\Box P\to P,\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset$

$(\Box\supset)$

$\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset$

So for the remaining of the proof we will have to check if weakening $P$ on the left helps to construct a prehistoric-cycle-free proof.

2. case: The last rule is a $(\Box\supset)$ rule with $\Box(P\land\lnot\Box P)$ as the principal formula. We get as premise the sequent

[TABLE]

which again by inversion and an easy deduction is provable prehistoric-cycle-free iff $P,\Box(P\land\lnot\Box P\to P),\Box(P\land\lnot\Box P)\supset\Box P$ is provable prehistoric-cycle-free. It is clear that using $(\Box\supset)$ rules on this sequent just adds additional copies of the existing formulas by the same arguments. So by contraction if there is a prehistoric-cycle-free proof for this sequent, then there is also one ending in a $(\supset\Box)$ rule. The premise of this rule has to have the form

[TABLE]

to avoid a prehistoric cycle. But the following Kripke model shows that

[TABLE]

is not a theorem of S4 and therefore not provable at all:

[TABLE]

We have $w\Vdash P\land\lnot\Box P\to P$ because $w\Vdash\lnot P$ and therefore also

[TABLE]

As $w$ is the only world we get $w\Vdash\Box(P\land\lnot\Box P\to P)$ which leads to the final $w\Vdash\lnot(\Box(P\land\lnot\Box P\to P)\to P)$ again because $w\Vdash\lnot P$ .

As all possibilities for a prehistoric-cycle-free proof of

[TABLE]

are exhausted, there is no such proof and therefore also no prehistoric-cycle-free proof of $\supset\Box(P\land\lnot\Box P\to P)\to\lnot\Box(P\land\lnot\Box P)$ ∎

Theorem 54.

There exists a S4-theorem $A$ and a LP-formula $B$ such that $A$ has no prehistoric-cycle-free G3s-proof, $B^{\circ}=A$ and $\operatorname{LP}(\operatorname{CS}^{\odot})\vdash B$

Proof.

$A:=\Box(P\land\lnot\Box P\to P)\to\lnot\Box(P\land\lnot\Box P)$ is a theorem of S4, as

[TABLE]

already is a theorem of S4. By the previous lemma, there is no prehistoric-cycle-free proof for $A$ and by the first lemma

[TABLE]

is a realization of $A$ provable in $\operatorname{LP}_{0}$ and therefor also in $\operatorname{LP}(\operatorname{CS}^{\odot})$ . ∎

Finally the question arises if prehistoric cycles are also a necessary condition on self-referential S4 theorems under the expanded definition. For this it is necessary to clarify the term inputs for Hilbert style proofs used in the original definition of LP and in the realization theorem (thm. 14) as there is no direct equivalent for $(\supset:)_{t}$ rules in the Hilbert style LP calculus as there is for $(\supset:)_{c}$ rules. Looking at the adequacy proof for G3lp, $(\supset:)_{t}$ is used only for the base cases $A\supset A$ in proofing axioms of LP. In the other direction, a $(\supset:)_{t}$ rule is translated first to the trivial proof for $t{:}A\vdash_{\operatorname{LP}}t{:}A$ , but the usage of deduction theorem could change that to a different proof for example for $\vdash_{\operatorname{LP}}t{:}A\to t{:}A$ .

So far, the situation seems pretty clear cut, and we have inputs as assumptions or as subformulas with negative polarity of formulas proven by the deduction theorem. This also matches the notion that $(\supset:)_{t}$ rules introduce the arguments of Skolem functions used in the LP realization. Unfortunately the deductions as constructed in the deduction theorem sometimes use existing formulas with swapped polarities. That is, in a deduction constructed by the deduction theorem, subformulas can occur with negative polarity which only occurred with positive polarity in the original deduction. Moreover formulas can be necessary to derive the final formula without occurring in that formula. So there is no guarantee that all necessary inputs actually occur in the final formula or that a formula occurring with negative polarity somewhere in the proof is an input.

So we have no clear definition of inputs in the original definition of LP matching the definition of inputs in G3lp, and therefore also currently no way to expand Yu’s result to all inputs. But we can stipulate that the inputs of a derivation $d$ as constructed by the realization theorem are exactly the realizations of formulas $\boxminus_{i}A$ with negative polarity in the original G3s proof. As G3s enjoys the subformula property, that means all inputs used in the proof thus constructed are actually also inputs in the final formula of the proof, a property which does not necessarily hold for all derivations as discussed above. We have to assume without proof that this definition of inputs somehow matches the exact definition given in the context of G3lp proofs. That is, there exists a G3lp proof for a G3s proof where only realizations of formulas with negative polarity are introduced by $(\supset:)_{t}$ . Given this stipulations and assumptions, the following sketch of a proof tries to argue for the necessity of prehistoric cycles for the expanded definition of self-referentiality:

Conjecture 55.

If a S4-theorem $A$ has a left-prehistoric-cycle-free G3s-proof, then there is a LP-formula $B$ s.t. $B^{\circ}=A$ and $\operatorname{LP}(\operatorname{IN}^{\odot})\vdash B$ .

Proof idea. Given a left-prehistoric-cycle-free G3s-proof $\mathcal{T}=(T,R)$ for $A$ , use the realization theorem to construct a realization function $r_{T}^{N}$ and a constant specification $\operatorname{CS}^{N}$ such that $B:=r_{T}^{N}(\operatorname{\mathsf{an}}_{T}(A))$ is a realization of $A$ and $\operatorname{LP}\vdash B$ by the constructed deduction $d$ . To simplify the following, we do not enforce a injective constant specification here and allow multiple proof constants for the same formula. From this it follows that any constant $c_{i,j,k}$ is exclusively used when handling the $(\supset\Box)$ rule $R_{i,j}$ .

Assume for a contradiction that the set of inputs IN used for $d$ is self-referential. That is there is a subset $\{t_{0}{:}A_{0}(t_{1}),\ldots,t_{n-1}{:}A_{n-1}(t_{0})\}$ of IN. The occurrences of $t_{k+1\mod n}$ in $t_{k}{:}A_{i}$ have to be a subterm of realization term for a principal family $i_{k}$ as the construction of such realization terms are the only place where the constants and variables of IN can get reused. For every consecutive pair of principal families $i_{k}$ and $i_{k^{\prime}}$ thus given, there is a constant or variable $t_{k^{\prime}}$ such that $t_{k^{\prime}}$ occurs in the realization term for $i_{k}$ and there is a subterm of the realization term for $i_{k^{\prime}}$ occurring in $t_{k^{\prime}}{:}A_{k^{\prime}}\in\operatorname{IN}$ . We distinguish the following cases:

1. case: $t_{k^{\prime}}$ is a variable $x_{j}$ . Then the formula $t_{k^{\prime}}{:}A_{k^{\prime}}$ is the realization of an annotated S4 formula $\boxminus_{j}A(\boxplus_{i_{k^{\prime}}})$ . That formula occurs on the left of a $(\supset\Box)$ rule introducing an occurrence of $\boxplus_{k}$ as $x_{j}$ is in the realization term of $\boxplus_{k}$ . Therefore we have $i_{k^{\prime}}\prec i_{k}$ .

2. case: $t_{k^{\prime}}$ is a constant $c_{j,l,m}$ . Then the formula $t_{k^{\prime}}{:}A_{k^{\prime}}$ is added to the CS when handling a $(\supset\Box)$ rule $R_{j,l}$ introducing an occurrence of $\boxplus_{j}$ . $c_{j,l,m}$ is in the realization term of $\boxplus_{k}$ so $R_{j,l}$ lies in a prehistory of $\boxplus_{k}$ . At the same time, the term $t_{k^{\prime}}$ occurs in the formula $c_{j,l,m}{:}A_{k^{\prime}}$ as part of a term $t$ used in the construction of the realization of $\boxplus_{k^{\prime}}$ . As $c_{j,l,m}{:}A_{k^{\prime}}$ is introduced when realizing $R_{j,l}$ , $A_{k^{\prime}}$ occurs in the proof of the premise and there has to be an occurrence of $\boxplus_{k^{\prime}}$ in the prehistory of $R_{j,l}$ . Together we get that $\boxplus_{k^{\prime}}$ occurs in a prehistory of $\boxplus_{k}$ and therefore $i_{k^{\prime}}\prec i_{k}$ by lemma 19.-

So for all $k<n$ we get $i_{k^{\prime}}\prec i_{k}$ and the list of principal families $i_{0},\ldots,i_{n-1}$ is therefore a prehistoric cycle in $\mathcal{T}$ .

5 Conclusion

We defined prehistoric relations for Gentzen systems with cut rules and finally for a Gentzen system G3lp for the logic of proofs LP. This makes it possible to study prehistoric relations directly in LP and leads to a negative answer on Yu’s conjecture that prehistoric cycles are sufficient for self-referential S4 theorems. It also leads to an expanded definition of self-referentiality considering all inputs used to construct justification terms. With that expanded definition of self-referentiality prehistoric cycles are sufficient for self-referential theorems in S4, which is the main result of this paper.

Given this expansion, the question goes back to the other direction. That is, are prehistoric cycles also necessary for the expanded definition of self-referentiality? Unfortunately this question is not easy to answer, as already transferring the definitions of inputs to the original Hilbert style calculus poses problems. A more detailed discussion of Skolem style functions and their role in LP realizations will hopefully help to clear this up. It is possible that the definition of input variables relative to a subformula occurrence and the machinery used to work with input variables in [13] already provides a part of the answer.

Yu [17] expanded his result to modal logics T and K4 and their justification counterparts. Another open question is whether the same generalization can be done with the results of this paper. That is, if there are Gentzen style systems without structural rules for T and K4 together with a consistent definition of term correspondence and prehistoric relations and a translation to some variant of G3s.

Acknowledgments

This work was supported by the grant 200021_165549 of the Swiss National Science Foundation.

Bibliography18

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1] Sergei Artemov. Operational modal logic. Technical Report MSI 95–29, Cornell University, 1995.
2[2] Sergei Artemov. Explicit provability and constructive semantics. Bulletin of Symbolic Logic , 7(1):1–36, 2001.
3[3] Sergei Artemov. The logic of justification. The Review of Symbolic Logic , 1(4):477–513, 2008.
4[4] Vladimir Brezhnev. On the logic of proofs. In Kristina Striegnitz, editor, Proceedings of the sixth ESSLLI Student Session, 13th European Summer School in Logic, Language and Information (ESSLLI’01) , pages 35–46. Fo LLI, 2001.
5[5] Vladimir Brezhnev and Roman Kuznets. Making knowledge explicit: How hard it is. Theoretical Computer Science , 357(1–3):23–34, 2006.
6[6] Samuel Bucheli, Roman Kuznets, and Thomas Studer. Realizing public announcements by justifications. Journal of Computer and System Sciences , 80(6):1046–1066, 2014.
7[7] Melvin Fitting. The logic of proofs, semantically. Annals of Pure and Applied Logic , 132(1):1–25, 2005.
8[8] Melvin Fitting. Realizations and LP. Annals of Pure and Applied Logic , 161(3):368–387, 2009.

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

Self-referentiality in Justification Logic

Abstract

1 Introduction

2 LP and S4

2.1 Preliminaries

Definition 1** (Syntax of S4).**

Definition 2** (Syntax of LP).**

Definition 3** (Constant Specification).**

2.2 Gentzen Systems

Definition 4** (Correspondence).**

Definition 5** (Family).**

Lemma 6** (Subformula Property).**

2.3 Annotated S4

Definition 7** (Polarity).**

Definition 8** (Annotated Proof).**

2.4 Realization

Definition 9** (Forgetful Projection).**

Theorem 10**.**

Definition 11** (Realization Function).**

Definition 12** (LP-Realization).**

Definition 13** (Normal).**

Theorem 14** (Realization).**

3 Prehistoric Relations in

3.1 Self-referentiality

Definition 15** (Self-Referential Constant Specification).**

Definition 16** (Self-Referential Theorem).**

3.2 Prehistoric Relations

Definition 17** (History).**

Definition 18** (Prehistoric Relation).**

Lemma 19**.**

Proof.

Definition 20** (Prehistoric Cycle).**

Lemma 21**.**

Theorem 22** **(Necessity of Left Prehistoric Cycle for

4 Prehistoric Relations in

4.1 Cut Rules

Definition 23** ((Cut) Rule).**

Definition 24** (Correspondence for (Cut)).**

Definition 25** (Local Prehistoric Relation in G3s + (Cut)).**

Definition 26** ((□\Box□Cut) Rule).**

Definition 27** (Correspondence for (□\Box□Cut)).**

Lemma 28**.**

Theorem 29** (Cut Elimination for G3s).**

Proof.

Corollary 30**.**

Proof.

Corollary 31**.**

Proof.

Theorem 32** ((□\Box□Cut) Elimination).**

Proof.

Corollary 33**.**

Proof.

Definition 34**.**

Theorem 35**.**

Proof.

4.2 A sufficient condition for self-referentiality

Definition 36** (Subformula).**

Definition 37** (Subterm).**

Definition 38** (Correspondence in G3lp).**

Definition 39** (Prehistoric Relation in G3lp).**

Lemma 40**.**

Proof.

Lemma 41**.**

Proof.

Definition 42** (Forgetful Projection of a G3lp Proof).**

Lemma 43**.**

Proof.

Lemma 44**.**

Proof.

Corollary 45**.**

Proof.

Lemma 46**.**

Proof.

Definition 1 (Syntax of S4).

Definition 2 (Syntax of LP).

Definition 3 (Constant Specification).

Definition 4 (Correspondence).

Definition 5 (Family).

Lemma 6 (Subformula Property).

Definition 7 (Polarity).

Definition 8 (Annotated Proof).

Definition 9 (Forgetful Projection).

Theorem 10.

Definition 11 (Realization Function).

Definition 12 (LP-Realization).

Definition 13 (Normal).

Theorem 14 (Realization).

Definition 15 (Self-Referential Constant Specification).

Definition 16 (Self-Referential Theorem).

Definition 17 (History).

Definition 18 (Prehistoric Relation).

Lemma 19.

Definition 20 (Prehistoric Cycle).

Lemma 21.

Theorem 22 (Necessity of Left Prehistoric Cycle for

Definition 23 ((Cut) Rule).

Definition 24 (Correspondence for (Cut)).

Definition 25 (Local Prehistoric Relation in G3s + (Cut)).

Definition 26 (( $\Box$ Cut) Rule).

Definition 27 (Correspondence for ( $\Box$ Cut)).

Lemma 28.

Theorem 29 (Cut Elimination for G3s).

Corollary 30.

Corollary 31.

Theorem 32 (( $\Box$ Cut) Elimination).

Corollary 33.

Definition 34.

Theorem 35.

Definition 36 (Subformula).

Definition 37 (Subterm).

Definition 38 (Correspondence in G3lp).

Definition 39 (Prehistoric Relation in G3lp).

Lemma 40.

Lemma 41.

Definition 42 (Forgetful Projection of a G3lp Proof).

Lemma 43.

Lemma 44.

Corollary 45.

Lemma 46.

Corollary 47.

Definition 48 (Inputs).

Definition 49 (Self-Referential Inputs).

Theorem 50.

Corollary 51.

Lemma 52.

Lemma 53.

Theorem 54.

Conjecture 55.