-
-
Notifications
You must be signed in to change notification settings - Fork 18
Expand file tree
/
Copy pathFoundation.lean
More file actions
537 lines (536 loc) · 28.8 KB
/
Foundation.lean
File metadata and controls
537 lines (536 loc) · 28.8 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
module -- shake: keep-all
public import Foundation.FirstOrder.Arithmetic.Basic
public import Foundation.FirstOrder.Arithmetic.Basic.Hierarchy
public import Foundation.FirstOrder.Arithmetic.Basic.Misc
public import Foundation.FirstOrder.Arithmetic.Basic.Model
public import Foundation.FirstOrder.Arithmetic.Basic.Monotone
public import Foundation.FirstOrder.Arithmetic.Definability
public import Foundation.FirstOrder.Arithmetic.Definability.Absoluteness
public import Foundation.FirstOrder.Arithmetic.Definability.BoundedDefinable
public import Foundation.FirstOrder.Arithmetic.Definability.Definable
public import Foundation.FirstOrder.Arithmetic.Definability.Hierarchy
public import Foundation.FirstOrder.Arithmetic.Exponential
public import Foundation.FirstOrder.Arithmetic.Exponential.Bit
public import Foundation.FirstOrder.Arithmetic.Exponential.Exp
public import Foundation.FirstOrder.Arithmetic.Exponential.Log
public import Foundation.FirstOrder.Arithmetic.Exponential.PPow2
public import Foundation.FirstOrder.Arithmetic.Exponential.Pow2
public import Foundation.FirstOrder.Arithmetic.HFS
public import Foundation.FirstOrder.Arithmetic.HFS.Basic
public import Foundation.FirstOrder.Arithmetic.HFS.Coding
public import Foundation.FirstOrder.Arithmetic.HFS.Fixpoint
public import Foundation.FirstOrder.Arithmetic.HFS.PRF
public import Foundation.FirstOrder.Arithmetic.HFS.Seq
public import Foundation.FirstOrder.Arithmetic.HFS.Vec
public import Foundation.FirstOrder.Arithmetic.IOpen.Basic
public import Foundation.FirstOrder.Arithmetic.Induction
public import Foundation.FirstOrder.Arithmetic.Omega1.Basic
public import Foundation.FirstOrder.Arithmetic.Omega1.Nuon
public import Foundation.FirstOrder.Arithmetic.PeanoMinus.Basic
public import Foundation.FirstOrder.Arithmetic.PeanoMinus.Functions
public import Foundation.FirstOrder.Arithmetic.PeanoMinus.Q
public import Foundation.FirstOrder.Arithmetic.Q.Basic
public import Foundation.FirstOrder.Arithmetic.R0.Basic
public import Foundation.FirstOrder.Arithmetic.R0.Representation
public import Foundation.FirstOrder.Arithmetic.Schemata
public import Foundation.FirstOrder.Arithmetic.TA.Basic
public import Foundation.FirstOrder.Arithmetic.TA.Nonstandard
public import Foundation.FirstOrder.Basic
public import Foundation.FirstOrder.Basic.AesopInit
public import Foundation.FirstOrder.Basic.BinderNotation
public import Foundation.FirstOrder.Basic.Calculus
public import Foundation.FirstOrder.Basic.Calculus2
public import Foundation.FirstOrder.Basic.Coding
public import Foundation.FirstOrder.Basic.Definability
public import Foundation.FirstOrder.Basic.Eq
public import Foundation.FirstOrder.Basic.Model
public import Foundation.FirstOrder.Basic.Operator
public import Foundation.FirstOrder.Basic.Padding
public import Foundation.FirstOrder.Basic.Semantics.Elementary
public import Foundation.FirstOrder.Basic.Semantics.Semantics
public import Foundation.FirstOrder.Basic.Soundness
public import Foundation.FirstOrder.Basic.Syntax.Formula
public import Foundation.FirstOrder.Basic.Syntax.Rew
public import Foundation.FirstOrder.Basic.Syntax.Theory
public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D1
public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D2
public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.D3
public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.EquationalTheory
public import Foundation.FirstOrder.Bootstrapping.DerivabilityCondition.PeanoMinus
public import Foundation.FirstOrder.Bootstrapping.FixedPoint
public import Foundation.FirstOrder.Bootstrapping.Syntax
public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Basic
public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Coding
public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Functions
public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Iteration
public import Foundation.FirstOrder.Bootstrapping.Syntax.Formula.Typed
public import Foundation.FirstOrder.Bootstrapping.Syntax.Language
public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Basic
public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Coding
public import Foundation.FirstOrder.Bootstrapping.Syntax.Proof.Typed
public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Basic
public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Coding
public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Functions
public import Foundation.FirstOrder.Bootstrapping.Syntax.Term.Typed
public import Foundation.FirstOrder.Bootstrapping.Syntax.Theory
public import Foundation.FirstOrder.Completeness.Coding
public import Foundation.FirstOrder.Completeness.Completeness
public import Foundation.FirstOrder.Completeness.Corollaries
public import Foundation.FirstOrder.Completeness.SearchTree
public import Foundation.FirstOrder.Completeness.SubLanguage
public import Foundation.FirstOrder.Hauptsatz
public import Foundation.FirstOrder.Incompleteness.Consistency
public import Foundation.FirstOrder.Incompleteness.Dense
public import Foundation.FirstOrder.Incompleteness.Examples
public import Foundation.FirstOrder.Incompleteness.First
public import Foundation.FirstOrder.Incompleteness.GödelRosser
public import Foundation.FirstOrder.Incompleteness.Halting
public import Foundation.FirstOrder.Incompleteness.Jeroslow
public import Foundation.FirstOrder.Incompleteness.Löb
public import Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Basic
public import Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Height
public import Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Refutability
public import Foundation.FirstOrder.Incompleteness.RestrictedProvability
public import Foundation.FirstOrder.Incompleteness.RosserProvability
public import Foundation.FirstOrder.Incompleteness.Second
public import Foundation.FirstOrder.Incompleteness.StandardProvability
public import Foundation.FirstOrder.Incompleteness.Tarski
public import Foundation.FirstOrder.Incompleteness.WitnessComparison
public import Foundation.FirstOrder.Incompleteness.Yablo
public import Foundation.FirstOrder.Interpretation
public import Foundation.FirstOrder.Intuitionistic.Deduction
public import Foundation.FirstOrder.Intuitionistic.Formula
public import Foundation.FirstOrder.Intuitionistic.Rew
public import Foundation.FirstOrder.Kripke.Basic
public import Foundation.FirstOrder.Kripke.Intuitionistic
public import Foundation.FirstOrder.Kripke.WeakForcing
public import Foundation.FirstOrder.NegationTranslation.GoedelGentzen
public import Foundation.FirstOrder.Order.Le
public import Foundation.FirstOrder.Polarity
public import Foundation.FirstOrder.SetTheory.Basic
public import Foundation.FirstOrder.SetTheory.Basic.Axioms
public import Foundation.FirstOrder.SetTheory.Basic.Misc
public import Foundation.FirstOrder.SetTheory.Basic.Model
public import Foundation.FirstOrder.SetTheory.Function
public import Foundation.FirstOrder.SetTheory.LoewenheimSkolem
public import Foundation.FirstOrder.SetTheory.Ordinal
public import Foundation.FirstOrder.SetTheory.TransitiveModel
public import Foundation.FirstOrder.SetTheory.Universe
public import Foundation.FirstOrder.SetTheory.Z
public import Foundation.FirstOrder.Skolemization.Hull
public import Foundation.FirstOrder.Ultraproduct
public import Foundation.Init
public import Foundation.InterpretabilityLogic.Axioms
public import Foundation.InterpretabilityLogic.Entailment
public import Foundation.InterpretabilityLogic.Entailment.Basic
public import Foundation.InterpretabilityLogic.Entailment.CL
public import Foundation.InterpretabilityLogic.Entailment.IL
public import Foundation.InterpretabilityLogic.Entailment.ILMinus
public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J1
public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J2
public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J4
public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J5
public import Foundation.InterpretabilityLogic.Entailment.ILMinus_M
public import Foundation.InterpretabilityLogic.Entailment.IL_KW1Zero
public import Foundation.InterpretabilityLogic.Entailment.IL_KW2
public import Foundation.InterpretabilityLogic.Entailment.IL_M
public import Foundation.InterpretabilityLogic.Entailment.IL_M₀
public import Foundation.InterpretabilityLogic.Entailment.IL_M₀_W
public import Foundation.InterpretabilityLogic.Entailment.IL_P
public import Foundation.InterpretabilityLogic.Entailment.IL_R
public import Foundation.InterpretabilityLogic.Entailment.IL_R_W
public import Foundation.InterpretabilityLogic.Entailment.IL_Rstar
public import Foundation.InterpretabilityLogic.Entailment.IL_W
public import Foundation.InterpretabilityLogic.Entailment.IL_Wstar
public import Foundation.InterpretabilityLogic.Formula.Basic
public import Foundation.InterpretabilityLogic.Formula.OfModal
public import Foundation.InterpretabilityLogic.Formula.Substitution
public import Foundation.InterpretabilityLogic.Formula.ToModal
public import Foundation.InterpretabilityLogic.Hilbert.Axiom
public import Foundation.InterpretabilityLogic.Hilbert.Basic.Basic
public import Foundation.InterpretabilityLogic.Hilbert.Basic_Minimal
public import Foundation.InterpretabilityLogic.Hilbert.Minimal.Basic
public import Foundation.InterpretabilityLogic.Logic.Basic
public import Foundation.InterpretabilityLogic.LogicSymbol
public import Foundation.InterpretabilityLogic.Veltman.AxiomJ1
public import Foundation.InterpretabilityLogic.Veltman.AxiomJ2
public import Foundation.InterpretabilityLogic.Veltman.AxiomJ4
public import Foundation.InterpretabilityLogic.Veltman.AxiomJ5
public import Foundation.InterpretabilityLogic.Veltman.AxiomM
public import Foundation.InterpretabilityLogic.Veltman.AxiomM₀
public import Foundation.InterpretabilityLogic.Veltman.AxiomP
public import Foundation.InterpretabilityLogic.Veltman.AxiomR
public import Foundation.InterpretabilityLogic.Veltman.AxiomW
public import Foundation.InterpretabilityLogic.Veltman.Basic
public import Foundation.InterpretabilityLogic.Veltman.Hilbert
public import Foundation.InterpretabilityLogic.Veltman.Logic.CL
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J2
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J2_J5
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J4Plus
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J4Plus_J5
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J5
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J2Plus
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J2Plus_J5
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J4Plus
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J4Plus_J5
public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J5
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_F
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_M
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_M₀
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_M₀_W
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_P
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_P₀
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_R
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_R_W
public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_W
public import Foundation.LinearLogic.FirstOrder.Calculus
public import Foundation.LinearLogic.FirstOrder.ClassicalEmbedding
public import Foundation.LinearLogic.FirstOrder.Formula
public import Foundation.LinearLogic.FirstOrder.Rew
public import Foundation.LinearLogic.LogicSymbol
public import Foundation.LinearLogic.MLL
public import Foundation.Logic.Calculus
public import Foundation.Logic.Decidability
public import Foundation.Logic.Disjunctive
public import Foundation.Logic.Embedding
public import Foundation.Logic.Entailment
public import Foundation.Logic.ForcingRelation
public import Foundation.Logic.LindenbaumAlgebra
public import Foundation.Logic.LogicSymbol
public import Foundation.Logic.Semantics
public import Foundation.Meta.ClProver
public import Foundation.Meta.IntProver
public import Foundation.Meta.Lit
public import Foundation.Meta.Qq
public import Foundation.Meta.Test
public import Foundation.Meta.TwoSided
public import Foundation.Modal.Algebra.Basic
public import Foundation.Modal.Axioms
public import Foundation.Modal.Boxdot.Basic
public import Foundation.Modal.Boxdot.GLPoint3_GrzPoint3
public import Foundation.Modal.Boxdot.GL_Grz
public import Foundation.Modal.Boxdot.GL_S
public import Foundation.Modal.Boxdot.Grz_S
public import Foundation.Modal.Boxdot.Jerabek
public import Foundation.Modal.Boxdot.K4_S4
public import Foundation.Modal.Boxdot.Ver_Triv
public import Foundation.Modal.ComplementClosedConsistentFinset
public import Foundation.Modal.Entailment.AxiomGeach
public import Foundation.Modal.Entailment.Basic
public import Foundation.Modal.Entailment.DiaDuality
public import Foundation.Modal.Entailment.E
public import Foundation.Modal.Entailment.EM
public import Foundation.Modal.Entailment.EMC
public import Foundation.Modal.Entailment.EMCN
public import Foundation.Modal.Entailment.EMK
public import Foundation.Modal.Entailment.EN
public import Foundation.Modal.Entailment.END
public import Foundation.Modal.Entailment.ET
public import Foundation.Modal.Entailment.ET5
public import Foundation.Modal.Entailment.ETB
public import Foundation.Modal.Entailment.GL
public import Foundation.Modal.Entailment.Grz
public import Foundation.Modal.Entailment.K
public import Foundation.Modal.Entailment.K4
public import Foundation.Modal.Entailment.K4Hen
public import Foundation.Modal.Entailment.K4Henkin
public import Foundation.Modal.Entailment.K4Loeb
public import Foundation.Modal.Entailment.K5
public import Foundation.Modal.Entailment.KB
public import Foundation.Modal.Entailment.KD
public import Foundation.Modal.Entailment.KP
public import Foundation.Modal.Entailment.KT
public import Foundation.Modal.Entailment.KTc
public import Foundation.Modal.Entailment.N
public import Foundation.Modal.Entailment.S4
public import Foundation.Modal.Entailment.S5
public import Foundation.Modal.Entailment.S5Grz
public import Foundation.Modal.Entailment.Triv
public import Foundation.Modal.Entailment.Ver
public import Foundation.Modal.Formula.Basic
public import Foundation.Modal.Formula.Complement
public import Foundation.Modal.Formula.NNFormula
public import Foundation.Modal.Hilbert.Axiom
public import Foundation.Modal.Hilbert.GL_K4Loeb_K4Henkin_K4Hen
public import Foundation.Modal.Hilbert.NNFormula
public import Foundation.Modal.Hilbert.Normal.Basic
public import Foundation.Modal.Hilbert.WithHenkin.Basic
public import Foundation.Modal.Hilbert.WithLoeb.Basic
public import Foundation.Modal.Hilbert.WithRE.Basic
public import Foundation.Modal.Hilbert.WithRE_Normal
public import Foundation.Modal.Kripke
public import Foundation.Modal.Kripke.Algebra
public import Foundation.Modal.Kripke.Antisymmetric
public import Foundation.Modal.Kripke.Asymmetric
public import Foundation.Modal.Kripke.AxiomFourN
public import Foundation.Modal.Kripke.AxiomGeach
public import Foundation.Modal.Kripke.AxiomGrz
public import Foundation.Modal.Kripke.AxiomH
public import Foundation.Modal.Kripke.AxiomI
public import Foundation.Modal.Kripke.AxiomL
public import Foundation.Modal.Kripke.AxiomMcK
public import Foundation.Modal.Kripke.AxiomMk
public import Foundation.Modal.Kripke.AxiomPoint3
public import Foundation.Modal.Kripke.AxiomPoint4
public import Foundation.Modal.Kripke.AxiomVer
public import Foundation.Modal.Kripke.AxiomWeakPoint2
public import Foundation.Modal.Kripke.AxiomWeakPoint3
public import Foundation.Modal.Kripke.Balloon
public import Foundation.Modal.Kripke.Basic
public import Foundation.Modal.Kripke.Closure
public import Foundation.Modal.Kripke.Cluster
public import Foundation.Modal.Kripke.Completeness
public import Foundation.Modal.Kripke.ComplexityLimited
public import Foundation.Modal.Kripke.ExtendRoot
public import Foundation.Modal.Kripke.Filtration
public import Foundation.Modal.Kripke.Hilbert
public import Foundation.Modal.Kripke.Irreflexive
public import Foundation.Modal.Kripke.Irreflexivize
public import Foundation.Modal.Kripke.LinearFrame
public import Foundation.Modal.Kripke.Logic.GL.Completeness
public import Foundation.Modal.Kripke.Logic.GL.MDP
public import Foundation.Modal.Kripke.Logic.GL.Soundness
public import Foundation.Modal.Kripke.Logic.GL.Unnecessitation
public import Foundation.Modal.Kripke.Logic.GLPoint3
public import Foundation.Modal.Kripke.Logic.Grz.Completeness
public import Foundation.Modal.Kripke.Logic.Grz.Soundness
public import Foundation.Modal.Kripke.Logic.GrzPoint2
public import Foundation.Modal.Kripke.Logic.GrzPoint3
public import Foundation.Modal.Kripke.Logic.K
public import Foundation.Modal.Kripke.Logic.K4
public import Foundation.Modal.Kripke.Logic.K45
public import Foundation.Modal.Kripke.Logic.K4McK
public import Foundation.Modal.Kripke.Logic.K4Point2
public import Foundation.Modal.Kripke.Logic.K4Point3
public import Foundation.Modal.Kripke.Logic.K4n
public import Foundation.Modal.Kripke.Logic.K5
public import Foundation.Modal.Kripke.Logic.KB
public import Foundation.Modal.Kripke.Logic.KB4
public import Foundation.Modal.Kripke.Logic.KB5
public import Foundation.Modal.Kripke.Logic.KD
public import Foundation.Modal.Kripke.Logic.KD4
public import Foundation.Modal.Kripke.Logic.KD45
public import Foundation.Modal.Kripke.Logic.KD4Point3Z
public import Foundation.Modal.Kripke.Logic.KD5
public import Foundation.Modal.Kripke.Logic.KDB
public import Foundation.Modal.Kripke.Logic.KHen
public import Foundation.Modal.Kripke.Logic.KT
public import Foundation.Modal.Kripke.Logic.KT4B
public import Foundation.Modal.Kripke.Logic.KTB
public import Foundation.Modal.Kripke.Logic.KTMk
public import Foundation.Modal.Kripke.Logic.KTc
public import Foundation.Modal.Kripke.Logic.S4
public import Foundation.Modal.Kripke.Logic.S4H
public import Foundation.Modal.Kripke.Logic.S4McK
public import Foundation.Modal.Kripke.Logic.S4Point2
public import Foundation.Modal.Kripke.Logic.S4Point2McK
public import Foundation.Modal.Kripke.Logic.S4Point3
public import Foundation.Modal.Kripke.Logic.S4Point3McK
public import Foundation.Modal.Kripke.Logic.S4Point4
public import Foundation.Modal.Kripke.Logic.S4Point4McK
public import Foundation.Modal.Kripke.Logic.S5
public import Foundation.Modal.Kripke.Logic.S5Grz
public import Foundation.Modal.Kripke.Logic.Triv
public import Foundation.Modal.Kripke.Logic.Ver
public import Foundation.Modal.Kripke.NNFormula
public import Foundation.Modal.Kripke.Preservation
public import Foundation.Modal.Kripke.Rank
public import Foundation.Modal.Kripke.Root
public import Foundation.Modal.Kripke.Terminated
public import Foundation.Modal.Kripke.Tree
public import Foundation.Modal.Kripke.Undefinability
public import Foundation.Modal.Logic.Basic
public import Foundation.Modal.Logic.D.Basic
public import Foundation.Modal.Logic.GL.Independency
public import Foundation.Modal.Logic.GLPlusBoxBot.Basic
public import Foundation.Modal.Logic.GLPoint3OplusBoxBot.Basic
public import Foundation.Modal.Logic.Global
public import Foundation.Modal.Logic.S.Basic
public import Foundation.Modal.Logic.S.Consistent
public import Foundation.Modal.Logic.SumNormal
public import Foundation.Modal.Logic.SumQuasiNormal
public import Foundation.Modal.LogicSymbol
public import Foundation.Modal.Maximal.Basic
public import Foundation.Modal.Maximal.Makinson
public import Foundation.Modal.Maximal.Unprovability
public import Foundation.Modal.MaximalConsistentSet
public import Foundation.Modal.ModalCompanion.Corsi
public import Foundation.Modal.ModalCompanion.Corsi.VF
public import Foundation.Modal.ModalCompanion.Standard.Basic
public import Foundation.Modal.ModalCompanion.Standard.Cl
public import Foundation.Modal.ModalCompanion.Standard.Int
public import Foundation.Modal.ModalCompanion.Standard.KC
public import Foundation.Modal.ModalCompanion.Standard.LC
public import Foundation.Modal.Modality.Basic
public import Foundation.Modal.Modality.S5
public import Foundation.Modal.PLoN.Basic
public import Foundation.Modal.PLoN.Completeness
public import Foundation.Modal.PLoN.Hilbert
public import Foundation.Modal.PLoN.Logic
public import Foundation.Modal.PLoN.Logic.N
public import Foundation.Modal.Tableau
public import Foundation.Modal.VanBentham.StandardTranslation
public import Foundation.Propositional.Boolean.Basic
public import Foundation.Propositional.Boolean.Hilbert
public import Foundation.Propositional.Boolean.NNFormula
public import Foundation.Propositional.Boolean.Tait
public import Foundation.Propositional.Boolean.ZeroSubst
public import Foundation.Propositional.ConsistentTableau
public import Foundation.Propositional.Decidable
public import Foundation.Propositional.Dialectica.Basic
public import Foundation.Propositional.Entailment.AxiomDNE
public import Foundation.Propositional.Entailment.AxiomEFQ
public import Foundation.Propositional.Entailment.AxiomElimContra
public import Foundation.Propositional.Entailment.AxiomLEM
public import Foundation.Propositional.Entailment.AxiomPeirce
public import Foundation.Propositional.Entailment.Cl.Basic
public import Foundation.Propositional.Entailment.Cl.Łukasiewicz
public import Foundation.Propositional.Entailment.Corsi
public import Foundation.Propositional.Entailment.Corsi.Basic
public import Foundation.Propositional.Entailment.Corsi.F
public import Foundation.Propositional.Entailment.Corsi.VF
public import Foundation.Propositional.Entailment.Corsi.WF
public import Foundation.Propositional.Entailment.Int.Basic
public import Foundation.Propositional.Entailment.Int.DNE_of_LEM
public import Foundation.Propositional.Entailment.KC
public import Foundation.Propositional.Entailment.KreiselPutnam
public import Foundation.Propositional.Entailment.LC
public import Foundation.Propositional.Entailment.Minimal.Basic
public import Foundation.Propositional.Entailment.Scott
public import Foundation.Propositional.FMT.Axiom.Ser
public import Foundation.Propositional.FMT.Basic
public import Foundation.Propositional.FMT.Completeness
public import Foundation.Propositional.FMT.Hilbert.Basic
public import Foundation.Propositional.FMT.Hilbert.VF
public import Foundation.Propositional.FMT.Hilbert.VF_Ser
public import Foundation.Propositional.Formula.Basic
public import Foundation.Propositional.Formula.NNFormula
public import Foundation.Propositional.Heyting.Semantics
public import Foundation.Propositional.Hilbert.F.Basic
public import Foundation.Propositional.Hilbert.F.Deduction
public import Foundation.Propositional.Hilbert.F.Disjunctive
public import Foundation.Propositional.Hilbert.F_WF
public import Foundation.Propositional.Hilbert.Minimal.Basic
public import Foundation.Propositional.Hilbert.Minimal.Glivenko
public import Foundation.Propositional.Hilbert.VF.Basic
public import Foundation.Propositional.Hilbert.VF.Disjunctive
public import Foundation.Propositional.Hilbert.WF.Basic
public import Foundation.Propositional.Hilbert.WF_VF
public import Foundation.Propositional.Kripke.AxiomDummett
public import Foundation.Propositional.Kripke.AxiomKreiselPutnam
public import Foundation.Propositional.Kripke.AxiomLEM
public import Foundation.Propositional.Kripke.AxiomWLEM
public import Foundation.Propositional.Kripke.Basic
public import Foundation.Propositional.Kripke.Completeness
public import Foundation.Propositional.Kripke.Filtration
public import Foundation.Propositional.Kripke.Hilbert.Basic
public import Foundation.Propositional.Kripke.Hilbert.Cl
public import Foundation.Propositional.Kripke.Hilbert.Int.Basic
public import Foundation.Propositional.Kripke.Hilbert.Int.DP
public import Foundation.Propositional.Kripke.Hilbert.KC
public import Foundation.Propositional.Kripke.Hilbert.KreiselPutnam
public import Foundation.Propositional.Kripke.Hilbert.LC
public import Foundation.Propositional.Kripke.Preservation
public import Foundation.Propositional.Kripke.Rooted
public import Foundation.Propositional.Kripke2.Axiom.Corfl
public import Foundation.Propositional.Kripke2.Axiom.Hrd
public import Foundation.Propositional.Kripke2.Axiom.PCon
public import Foundation.Propositional.Kripke2.Axiom.PSCon
public import Foundation.Propositional.Kripke2.Axiom.Rfl
public import Foundation.Propositional.Kripke2.Axiom.Ser
public import Foundation.Propositional.Kripke2.Axiom.Sym
public import Foundation.Propositional.Kripke2.Axiom.Tra
public import Foundation.Propositional.Kripke2.Basic
public import Foundation.Propositional.Kripke2.Hilbert.Basic
public import Foundation.Propositional.Kripke2.Hilbert.F
public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl
public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Sym
public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Tra1
public import Foundation.Propositional.Kripke2.Hilbert.F_Ser
public import Foundation.Propositional.Kripke2.Hilbert.F_Sym
public import Foundation.Propositional.Kripke2.Hilbert.F_Tra1
public import Foundation.Propositional.Logic.Basic
public import Foundation.Propositional.Logic.Letterless_Int_Cl
public import Foundation.Propositional.Logic.PostComplete
public import Foundation.Propositional.Logic.Superintuitionistic
public import Foundation.Propositional.Neighborhood.NB.Basic
public import Foundation.Propositional.Neighborhood.NB.Hilbert.Basic
public import Foundation.Propositional.Neighborhood.NB.Hilbert.WF
public import Foundation.Propositional.Slash
public import Foundation.Propositional.Tait.Calculus
public import Foundation.Propositional.Translation
public import Foundation.ProvabilityLogic.Arithmetic
public import Foundation.ProvabilityLogic.Classification.LetterlessTrace
public import Foundation.ProvabilityLogic.Classification.Result
public import Foundation.ProvabilityLogic.Classification.Trace
public import Foundation.ProvabilityLogic.GL.Completeness
public import Foundation.ProvabilityLogic.GL.Soundness
public import Foundation.ProvabilityLogic.GL.Uniform
public import Foundation.ProvabilityLogic.GL.Unprovability
public import Foundation.ProvabilityLogic.Grz.Completeness
public import Foundation.ProvabilityLogic.N.Soundness
public import Foundation.ProvabilityLogic.Realization
public import Foundation.ProvabilityLogic.S.Completeness
public import Foundation.ProvabilityLogic.S.Soundness
public import Foundation.ProvabilityLogic.SolovaySentences
public import Foundation.SecondOrder.Derivation
public import Foundation.SecondOrder.Semantics
public import Foundation.SecondOrder.Syntax.Formula
public import Foundation.SecondOrder.Syntax.Rew
public import Foundation.Semantics.Algebra.Modal.Basic
public import Foundation.Semantics.Algebra.Modal.Magari
public import Foundation.Semantics.CoherenceSpace.Basic
public import Foundation.Semantics.CoherenceSpace.StableFunction
public import Foundation.Syntax.Predicate.Language
public import Foundation.Syntax.Predicate.Quantifier
public import Foundation.Syntax.Predicate.Relational
public import Foundation.Syntax.Predicate.Rew
public import Foundation.Syntax.Predicate.Term
public import Foundation.Vorspiel.AdjunctiveSet
public import Foundation.Vorspiel.Arithmetic
public import Foundation.Vorspiel.Computability
public import Foundation.Vorspiel.DMatrix
public import Foundation.Vorspiel.Denumerable
public import Foundation.Vorspiel.ENat
public import Foundation.Vorspiel.Empty
public import Foundation.Vorspiel.ExistsUnique
public import Foundation.Vorspiel.Fin.Basic
public import Foundation.Vorspiel.Fin.Matrix
public import Foundation.Vorspiel.Finset.Basic
public import Foundation.Vorspiel.Finset.Card
public import Foundation.Vorspiel.Fintype
public import Foundation.Vorspiel.Function
public import Foundation.Vorspiel.Graph
public import Foundation.Vorspiel.IsEmpty
public import Foundation.Vorspiel.List.Basic
public import Foundation.Vorspiel.List.Chain
public import Foundation.Vorspiel.List.ChainI
public import Foundation.Vorspiel.List.Perm
public import Foundation.Vorspiel.Matrix
public import Foundation.Vorspiel.Nat.Basic
public import Foundation.Vorspiel.Nat.Matrix
public import Foundation.Vorspiel.NotationClass
public import Foundation.Vorspiel.Option
public import Foundation.Vorspiel.Order
public import Foundation.Vorspiel.Part
public import Foundation.Vorspiel.Preorder
public import Foundation.Vorspiel.Quotient
public import Foundation.Vorspiel.Rel.Basic
public import Foundation.Vorspiel.Rel.CWF
public import Foundation.Vorspiel.Rel.Connected
public import Foundation.Vorspiel.Rel.Convergent
public import Foundation.Vorspiel.Rel.Coreflexive
public import Foundation.Vorspiel.Rel.Equality
public import Foundation.Vorspiel.Rel.Euclidean
public import Foundation.Vorspiel.Rel.Isolated
public import Foundation.Vorspiel.Rel.Serial
public import Foundation.Vorspiel.Rel.Universal
public import Foundation.Vorspiel.Rel.WCWF
public import Foundation.Vorspiel.Set.Basic
public import Foundation.Vorspiel.Set.Cofinite
public import Foundation.Vorspiel.Set.Fin
public import Foundation.Vorspiel.Small
public import Foundation.Vorspiel.String