Index

acceptance predicate, 230

accepted justification, see justification, accepted, 223

accessibility relation, 48

annotated formula, 93

application, 14

arithmetic example, 225

arithmetical completeness, 165, 172 arithmetical incompleteness, see

incompleteness, 219

arithmetical interpretation, 159

arithmetical semantics, 212

arithmetical soundness, 160, 218 awareness logic, 9

!! Condition, 56

! Condition, 55, 56, 73

Barcan formula, 218

basic model, 32-36

LP, 42

positive and negative introspection, 38

BHK, 4, 5, 174-176

block tableau, see tableau, block, 96

Brouwer-Heyting-Kolmogorov, see BHK, 4 ButFirst, 149

c condition, 59

canonical modal logic, see modal logic, canonical, 60

canonical model

decidable, 161

Fitting, 63, 202, 204

modal, 61

completion lemma, 163

conclusive evidence, 52

condensing, 120, 121 conjoinability of proofs, 159 consequence, 18

consistency, 25, 62

constant specification, 16, 17, 101 axiomatically appropriate, 18, 201 condition, 51

empty, 17

extension, 201

finite, 17, 218

FOLP, 195

schematic, 17

single-conclusion, 101, 102, 104, 107, 109 total, 17

counterpart, 112

Curry-Howard isomorphism, 7, 103

cut, 77

cut elimination, 172

D constant, 194

D formula, 194

deduction, 185

density condition, 59

domain constant, 194

• condition, 50

E-complete, 204

epistemic logic, 1

essential family, 105

evidence condition, 50

minimum, 50

evidence function, 49, 195

universal, 197

exact, 226

explicit proofs, 6

fact checker, 25

factivity, 24, 54

fair, 226

filtered

arithmetical interpretation, 217 derivation, 214

proof, 214

finiteness of proofs, 159

First, 149

first-order logic of proofs, see justification logic, FOLP, 181

first-order modal logic, see modal logic,

FOS4, 182

Fitting model, 49, 50

FOLP, 195

forgetful functor, 112, 187

formula translation

sequent, 76

tableau, 89

frame, 48

based on, 49

underlying, 49

frame condition, 50

fully explanatory, 51, 64, 208

Godel translation, 6, 190

Godel's translation, 191

Geach condition, 59

Gettier examples, 223

global variable, 212

Gbdel-Lbb logic, see modal logic, GL, 62

hyperintensional, 8, 9

incompleteness, 219

internalization, 21, 102, 186

property, 20

strong, 20

intuitionistic propositional calculus, see IPC, 6

IPC, 6

JAM, 223, 227, 228, 233

justification

accepted, 223, 226 constant, 12

formula, 13 knowledge-producing, 223, 226 master, 231

proof variable, 100

term, 12

variable, 12

justification awareness models, see JAM, 223

justification logic

FOLP, 181, 182

axiomatization, 184

formula, 183

language, 183

proof term, 183

FOLP0, 184

J, 24

J(CS), 52, 53

J0, 14

J4, 55

J4³, 28, 55, 66, 141

JT, 55

JT4, 26, 55

JT4.2, 29, 58, 68, 74, 142, 152

JT45, 28, 56, 66, 142

JX4, 30, 59, 70, 142

LP, 7, 26, 54, 55, 65, 100, 159

LP⁰, 73

LP0, 101

justification sound, 127

Justification Yields Belief, see JYB, 45

JYB, 45,51

Kleenerealizability, 7, 175 knowledge-producing justification, see justification, knowledge-producing, 223

knowledge-producing predicate, 230

Kreisel second clause, 179, 190

Kreisel theory of constructions, 7, 175 Kuznets' Theorem, 180

Lemmon-Scott logics, see modal logic, Geach logics, 142

lifting lemma, 22, 102, 129, 145

lives in, 195

local variable, 212

logic of proofs, see justification logic, LP, 7 master justification, see justification, master,

231

Mkrtychev model, 39-41

FOLP, 210

LP, 42

modal condition, 50

modal logic, 11

canonical, 60

FOS4,182

Geachlogics, 142, 143, 147, 149

GL, 62

K, 12, 90

K4³,27, 55, 141

KX4, 30, 59, 70, 142

normal, 12

54, 5, 6, 79

S4.2, 29, 58, 68, 74, 142, 152

55, 28, 56, 142

modal model, 48

modular model, 42, 44

monotonic, 194 monotonicity condition, 55, 73

Moore sentence, 179

non-deterministic, 86

PA, see Peano arithmetic, 158 paraconsistency, 10

Peano arithmetic, 158

+ condition, 50

polarity, 94

positive introspection, 25, 54

possible world, 48 potential quasi-realizer, see quasi-realizer,

potential, 117

potential realizer, see realizer, potential, 114 precise model, 225, 226

primitive recursive formula, 213, 214

provably, 214

primitive recursive term, 158

proof checker, 25

proof polynomial, 100

proof predicae, 158

proof predicate

normal, 158

provability completeness, 176

provably Δ₁, 158

provisional variable, 105

quasi-realization, 111, 116

nonconstructively, 135

quasi-realization tree, 126

quasi-realizer

potential, 117

? condition, 56

realization, 113, 186, 187

Geach logics, 152

LP₀, 103

nonconstructively, 138

normal, 104, 113, 186

S4, 108

realizer

potential, 114, 115

red barn example, 2-4, 223

refutation system, 85

related occurrence, 105

relevant evidence, 50, 52

Russell Prime Minister example, 222-228, 231

Russell true premises example, 224

Sahlqvist formula, 29, 57, 67, 142

saturated, 161

saturation lemma, 162

Schwichtenberg paradox, 190 self-referentiality, 179

direct, 179 semantic tableau, see tableau, 84 sequent, 76

admissible, 82

antecedent, 76

consistent, 82

saturated, 82

succedent, 76

sequent calculus, 76

atomic axiomatization, 78, 87 classical, 76

completeness, 81

Gcl, 76

Gci^,77

GFOS4, 187

GS4, 79

GS4,'/9

modal, 79

soundness, 81

sharp operation

justification, 63 modal, 60

∑1 formula, 158 signed formula, 85 skeleton, 193 state, 48

strong evidence condition, 56 strong evidence function, 51, 59, 64 structural rule, 77

subformula property, 77 substitution, 22, 118, 184, 185

lives away from, 119

lives on, 119

no new variable, 119 substitution closure, 23 sum, 14

tableau

annotated block, 98 atomic closure, 87 block, 96, 97 classical, 84

closed, 86

modal, 90, 91

open, 86

] operation, 90, 91

single use rule, 87

tableau calculus

classical, 85, 87

modal, 90

truth lemma

FOLP, 207 justification, 63 modal, 61 sequent, 83

valid

FOLP, 196 in a frame, 49

modal, 49

variable renaming, 201 variable variant, 201 variant closed, 201 weakening, 77 witness variable, 200

Yu's Theorem, 180