Logical Foundations of Computer Science, LFCS 2020

Preface......Page 6
Organization......Page 7
Contents......Page 9
 1 Introduction......Page 11
  1.1 Preliminaries......Page 12
 3 Lower Bounds for Quantifier-Free Formulas......Page 15
 4 Boolean Combinations of n-Formulas......Page 18
 References......Page 21
 1 Preliminaries......Page 22
  1.1 Motivations......Page 23
 2 Observable Models......Page 24
 3 On the Structure of Induced Observable Models......Page 25
 4 Derivations from Hypotheses in Modal Logic......Page 26
 5 Canonical Models for S5 with a single letter......Page 27
 6 From Observable Models to Kripke Models......Page 29
  7.1 Common Knowledge and Necessitation......Page 30
  7.2 Canonical Models of Sets of Assumptions......Page 31
  8.1 Ignorant Agent Example......Page 33
 9 Intuitionistic Observable Models......Page 34
 10 Findings and Suggestions......Page 35
 References......Page 36
 1 Introduction......Page 37
 2 Non-normal Modal Logics......Page 39
 3 Hypersequent Calculi......Page 41
 4 Complexity of Proof Search......Page 44
 5 Countermodel Extraction......Page 46
 6 Extensions with Axioms T, P, and D......Page 50
 7 Conclusion......Page 52
 References......Page 56
 1 Introduction......Page 57
 2 Syntax, Deduction, Computability......Page 59
  2.2 Deduction Systems......Page 60
  2.3 Synthetic Computability......Page 61
  3.1 Tarski Semantics......Page 62
  3.2 Kripke Semantics......Page 66
 4 On Markov's Principle......Page 70
 5 Algebraic Semantics......Page 72
 6 Game Semantics......Page 74
 7 Discussion......Page 75
  7.2 Future Work......Page 76
 A  Overview of Deduction Systems......Page 77
 B  Notes on the Coq Formalisation......Page 78
 References......Page 81
 1 Introduction......Page 85
 2 The Constant Sentences of Peano Arithmetic......Page 86
 3 Generalized `Constructive' Liar Sentences and Rosser Sentences......Page 89
 4 `Extremely' Independent Sentences......Page 92
 5 Concluding Remark......Page 93
 References......Page 94
 1 Introduction......Page 95
 2 Syntax......Page 97
 3 Semantics......Page 99
 4 Soundness......Page 103
 5 Basic Properties......Page 104
 References......Page 106
 1 Introduction......Page 108
  2.1 Finite Partial Functions......Page 109
  2.3 Basic-Terms and Accessibility......Page 110
  2.4 A Formal Language......Page 111
  2.5 Definable Classes of Fp-Structures......Page 112
  3.2 The Theory FST0......Page 113
  3.3 Some Derived Schemas......Page 114
  4.2 Imperative Programs for Generic PR Computing......Page 116
 5 An Abstract Form of Parson's Theorem......Page 118
 References......Page 119
 1 Introduction......Page 121
 2 Need of Easier Programming with Logic......Page 122
 3 DA Logic......Page 125
 4 Formal Definition of Semantics of DA Logic......Page 128
 5 Additional Examples......Page 132
 References......Page 135
 1 Introduction......Page 138
 2 The Derivation of First-Order Rules from Second-Order Rule Macros: A First Approach......Page 140
 3 LK++: A Globally Sound Calculus, Cf. aguilera2016unsound......Page 143
 4 The Analytic Sequent Calculus LH++......Page 145
 5 Soundness, Completeness and Cut-Elimination for LH++......Page 149
 References......Page 153
 1 Introduction......Page 154
 2 Background on O......Page 155
 3 Strict Feedback Hyperjump......Page 156
 4 Loose Feedback Hyperjump......Page 161
 References......Page 165
 1 Introduction......Page 166
 2 Logical Preliminaries......Page 168
 3 Soundness and Completeness of LNIF......Page 171
 4 Proof-Theoretic Properties of LNIF......Page 173
 5 Conclusion......Page 183
 References......Page 184
 1 Introduction......Page 187
  2.1 The Labelled Calculi G3Int and G3IntQC......Page 189
  2.2 The Nested Calculi NInt and NIntQC......Page 191
 3 Translating Notation: Labelled and Nested......Page 192
 4 Deriving NInt from G3Int......Page 195
 5 Deriving NIntQC from G3IntQC......Page 200
 6 Conclusion......Page 202
 References......Page 203
 1 Introduction......Page 205
 2 Preliminaries......Page 208
  2.1 Base Independence......Page 213
 3 Complexity Results for Abductive Reasoning......Page 214
  3.2 Parameter `Number of Explanations' |E|......Page 217
  3.3 Parameter `Number of Manifestations' |M|......Page 218
 4 Conclusion......Page 220
 References......Page 221
 1 Introduction......Page 224
 2 Preliminaries......Page 225
 3 The LGPAC......Page 226
 4 Tracking Computability......Page 230
 5 Computability of the Input-Output Operator......Page 233
 6 Computability of LGPAC-Generable Functions......Page 235
 7 Some Applications of Theorem 1......Page 238
 8 Discussion......Page 240
 References......Page 244
 1 Introduction......Page 246
 2 Motivation......Page 247
 3 Typed Lambda-Calculus Based on IEL-......Page 250
 4 Relation with the Monadic Metalanguage......Page 255
 References......Page 257
 1 Introduction......Page 259
  2.1 Reverse Mathematics......Page 260
  2.2 Some Axioms of Higher-Order RM......Page 263
  3.1 Specker Nets......Page 264
  3.2 Compactness of Metric Spaces......Page 268
  3.3 Rado Selection Lemma......Page 271
  3.4 Fields and Order......Page 272
  4.2 Implications and Interpretations......Page 274
 References......Page 276
 1 Introduction......Page 278
 2 Revisiting Some Intuitions of Gödel and Hilbert......Page 280
 3 Main Notation and Background Literature......Page 281
 4 Main Theorems and Related Notation......Page 284
 5 Intuition Behind Theorem 1......Page 287
 6 Summary of the Justification For Theorem 2......Page 289
 7 On the Significance of Theorems 1 and 2......Page 290
 References......Page 294
Author Index......Page 297