Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(376 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(21 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(47 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(15 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(145 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(29 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(20 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(14 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(76 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)

Global Index

A

aand [inductive, in Loeb.util.Util]
aand_sind [definition, in Loeb.util.Util]
aand_rec [definition, in Loeb.util.Util]
aand_ind [definition, in Loeb.util.Util]
aand_rect [definition, in Loeb.util.Util]
add_cancel [lemma, in Loeb.internal_provability.Prov_Definition]
add_assoc [lemma, in Loeb.internal_provability.Prov_Definition]
add_one [lemma, in Loeb.internal_provability.Prov_Definition]
add_comm [lemma, in Loeb.internal_provability.Prov_Definition]
add_rec_right [lemma, in Loeb.internal_provability.Prov_Definition]
AllD [constructor, in Loeb.hilbert_system.Hilbert_System]
AllE [constructor, in Loeb.hilbert_system.Hilbert_System]
AllG [constructor, in Loeb.hilbert_system.Hilbert_System]
App [constructor, in Loeb.internal_provability.PA_Lists_Signature]
arg_embed [definition, in Loeb.Multivariate_ctq]
AxiomList [definition, in Loeb.internal_provability.Prov_Definition]
AxiomList_in_QEqLi_Axioms [lemma, in Loeb.internal_provability.Prov_Definition]
Axioms [section, in Loeb.internal_provability.QEqLiFull]
axioms_are_provable [lemma, in Loeb.internal_provability.Prov_Definition]
axiom_inclusion [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
ax_induction' [definition, in Loeb.internal_provability.QEqLiFull]
ax_imp_congr [definition, in Loeb.internal_provability.QEqLiFull]
ax_app_congr [definition, in Loeb.internal_provability.QEqLiFull]
ax_get_congr [definition, in Loeb.internal_provability.QEqLiFull]
ax_len_congr [definition, in Loeb.internal_provability.QEqLiFull]
ax_cons_congr [definition, in Loeb.internal_provability.QEqLiFull]
ax_impl [definition, in Loeb.internal_provability.QEqLiFull]
ax_get_app_right [definition, in Loeb.internal_provability.QEqLiFull]
ax_get_app_left [definition, in Loeb.internal_provability.QEqLiFull]
ax_len_app [definition, in Loeb.internal_provability.QEqLiFull]
ax_get_succ [definition, in Loeb.internal_provability.QEqLiFull]
ax_get_zero [definition, in Loeb.internal_provability.QEqLiFull]
ax_len_cons [definition, in Loeb.internal_provability.QEqLiFull]
ax_len_nil [definition, in Loeb.internal_provability.QEqLiFull]

B

binary_ctq [lemma, in Loeb.Multivariate_ctq]
bin_vector_inv [lemma, in Loeb.util.Vector_Lemmas]
bound_bin_fun [lemma, in Loeb.internal_provability.Prov_Definition]
bound_un_fun [lemma, in Loeb.internal_provability.Prov_Definition]
box_distr [lemma, in Loeb.internal_provability.Prov_Definition]
box_distr_Gödel_numeral [lemma, in Loeb.internal_provability.HBL]

C

cconj [constructor, in Loeb.util.Util]
CE1 [constructor, in Loeb.hilbert_system.Hilbert_System]
CE2 [constructor, in Loeb.hilbert_system.Hilbert_System]
CI [constructor, in Loeb.hilbert_system.Hilbert_System]
comparisons [section, in Loeb.internal_provability.PA_Lists_Signature]
CompatibilityLemmas [section, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_Pc [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_DE [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_DI2 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_DI1 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_CE2 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_CE1 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_CI [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_ctx [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_Exp [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_ExE [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_ExI [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_AllE [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_AllI [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_IE [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
Cons [constructor, in Loeb.internal_provability.PA_Lists_Signature]
contrapositive_elim [lemma, in Loeb.Limitative_Theorems]
CTQ_gives_Diagonal_Lemma [lemma, in Loeb.Diagonal_Lemma]
ctq_n_ary [lemma, in Loeb.Multivariate_ctq]

D

DE [constructor, in Loeb.hilbert_system.Hilbert_System]
dec [definition, in Loeb.Definitions]
decidable_pred_is_definable [lemma, in Loeb.Limitative_Theorems]
decider [definition, in Loeb.Definitions]
deduction_theorem [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
definable [definition, in Loeb.Limitative_Theorems]
defines_pred_strongly [definition, in Loeb.Limitative_Theorems]
defines_pred [definition, in Loeb.Limitative_Theorems]
Definitions [library]
DefProv [section, in Loeb.internal_provability.Prov_Definition]
DefProv.ax [variable, in Loeb.internal_provability.Prov_Definition]
DefProv.ax_bound [variable, in Loeb.internal_provability.Prov_Definition]
DefProv.göd [variable, in Loeb.internal_provability.Prov_Definition]
DefProv.Hax [variable, in Loeb.internal_provability.Prov_Definition]
DefProv.pei [variable, in Loeb.internal_provability.Prov_Definition]
diagonalisation [definition, in Loeb.Diagonal_Lemma]
diagonalisation_equivalence [lemma, in Loeb.Diagonal_Lemma]
Diagonal_Lemma_bound_counterexample [lemma, in Loeb.Diagonal_Lemma]
Diagonal_Lemma_mult_counterexample [lemma, in Loeb.Diagonal_Lemma]
diagonal_lemma [lemma, in Loeb.Diagonal_Lemma]
Diagonal_Lemma.φ_D_Hcapt [variable, in Loeb.Diagonal_Lemma]
Diagonal_Lemma.φ_D_is_Σ1 [variable, in Loeb.Diagonal_Lemma]
Diagonal_Lemma.φ_D_bound [variable, in Loeb.Diagonal_Lemma]
Diagonal_Lemma.φ_D [variable, in Loeb.Diagonal_Lemma]
Diagonal_Lemma.göd [variable, in Loeb.Diagonal_Lemma]
Diagonal_Lemma.pei [variable, in Loeb.Diagonal_Lemma]
Diagonal_Lemma [section, in Loeb.Diagonal_Lemma]
Diagonal_Lemma [library]
diag_G_closed [lemma, in Loeb.Diagonal_Lemma]
diag_G [definition, in Loeb.Diagonal_Lemma]
diag_F [definition, in Loeb.Diagonal_Lemma]
diag_göd_comm [lemma, in Loeb.Diagonal_Lemma]
diag_nat [definition, in Loeb.Diagonal_Lemma]
DI1 [constructor, in Loeb.hilbert_system.Hilbert_System]
DI2 [constructor, in Loeb.hilbert_system.Hilbert_System]
double_neg_elim_class [lemma, in Loeb.Limitative_Theorems]

E

Ebot [constructor, in Loeb.hilbert_system.Hilbert_System]
embed_eval_interchange [lemma, in Loeb.Multivariate_ctq]
empty_context_forall_times_intro [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
empty_context_AllI [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
encoding_ineq [lemma, in Loeb.internal_provability.Mostowski]
eqdec_preds [instance, in Loeb.Loeb]
eqdec_funcs [instance, in Loeb.Loeb]
eqdec_preds [instance, in Loeb.internal_provability.QEqLiFull]
eqdec_funcs [instance, in Loeb.internal_provability.QEqLiFull]
eqdec_preds' [instance, in Loeb.internal_provability.Mostowski]
eqdec_funcs' [instance, in Loeb.internal_provability.Mostowski]
eqdec_preds [instance, in Loeb.internal_provability.Mostowski]
eqdec_funcs [instance, in Loeb.internal_provability.Mostowski]
eqdec_preds [instance, in Loeb.internal_provability.Prov_Definition]
eqdec_funcs [instance, in Loeb.internal_provability.Prov_Definition]
eqdec_preds [instance, in Loeb.Limitative_Theorems]
eqdec_funcs [instance, in Loeb.Limitative_Theorems]
essential_undecidability [lemma, in Loeb.Limitative_Theorems]
ExE [constructor, in Loeb.hilbert_system.Hilbert_System]
ExI [constructor, in Loeb.hilbert_system.Hilbert_System]
ExternalMostowski [section, in Loeb.internal_provability.Mostowski]
ExternalMostowski.göd [variable, in Loeb.internal_provability.Mostowski]
ExternalMostowski.pei [variable, in Loeb.internal_provability.Mostowski]
External_Provability [library]
ext_prov_modus_ponens_counteraxample [lemma, in Loeb.internal_provability.Mostowski]
ext_prov_pred [definition, in Loeb.External_Provability]
Ext_prov.göd [variable, in Loeb.External_Provability]
Ext_prov.ctq [variable, in Loeb.External_Provability]
Ext_prov.pei [variable, in Loeb.External_Provability]
Ext_prov [section, in Loeb.External_Provability]
ex_sProv_T [lemma, in Loeb.External_Provability]
ex_prov_T [lemma, in Loeb.External_Provability]
ex_prov_T_util [lemma, in Loeb.External_Provability]

F

f [projection, in Loeb.Definitions]
forall_times_once [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
Formula_facts [section, in Loeb.util.Util]
form_inclusion [definition, in Loeb.internal_provability.PA_Lists_Signature]
form_inv [lemma, in Loeb.util.Util]

G

g [projection, in Loeb.Definitions]
Get [constructor, in Loeb.internal_provability.PA_Lists_Signature]
get_last_triple_app [lemma, in Loeb.internal_provability.Prov_Definition]
get_mid_index [lemma, in Loeb.internal_provability.Prov_Definition]
get_mid_index' [lemma, in Loeb.internal_provability.Prov_Definition]
get_low_index [lemma, in Loeb.internal_provability.Prov_Definition]
get_low_index' [lemma, in Loeb.internal_provability.Prov_Definition]
godel_first_incompleteness_strong_sep [lemma, in Loeb.Limitative_Theorems]
godel_first_incompleteness_Sig1_sound [lemma, in Loeb.Limitative_Theorems]
godel_first_incompleteness_tarski [lemma, in Loeb.Limitative_Theorems]
Godel's_second_incompleteness_theorem [lemma, in Loeb.Loeb]
god_not_strongly_definable [lemma, in Loeb.Limitative_Theorems]
goedelisation [record, in Loeb.Definitions]
Gödel [section, in Loeb.Limitative_Theorems]
Gödel.ctq [variable, in Loeb.Limitative_Theorems]
Gödel.göd [variable, in Loeb.Limitative_Theorems]
Gödel.pei [variable, in Loeb.Limitative_Theorems]

H

HBL [library]
HilAx [constructor, in Loeb.hilbert_system.Hilbert_System]
hilAx [inductive, in Loeb.hilbert_system.Hilbert_System]
hilAx_sind [definition, in Loeb.hilbert_system.Hilbert_System]
hilAx_ind [definition, in Loeb.hilbert_system.Hilbert_System]
Hilbert_System [library]
Hilbert_System_Deduction_Facts [library]
hilprv [inductive, in Loeb.hilbert_system.Hilbert_System]
hilprv_sind [definition, in Loeb.hilbert_system.Hilbert_System]
hilprv_ind [definition, in Loeb.hilbert_system.Hilbert_System]
Hil_ND_agree_theories [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
Hil_ND_agree [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
Hil_to_ND [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
HK [constructor, in Loeb.hilbert_system.Hilbert_System]
HS [constructor, in Loeb.hilbert_system.Hilbert_System]

I

identity [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
Imp [constructor, in Loeb.internal_provability.PA_Lists_Signature]
impl [definition, in Loeb.internal_provability.Mostowski]
impl_dec [definition, in Loeb.internal_provability.Mostowski]
impl_dec [definition, in Loeb.util.Util]
impl' [definition, in Loeb.internal_provability.Mostowski]
Indefinability [section, in Loeb.Limitative_Theorems]
Indefinability.ctq [variable, in Loeb.Limitative_Theorems]
Indefinability.göd [variable, in Loeb.Limitative_Theorems]
Indefinability.pei [variable, in Loeb.Limitative_Theorems]
index_destruct [lemma, in Loeb.internal_provability.Prov_Definition]
index_destruct' [lemma, in Loeb.internal_provability.Prov_Definition]
ineq_trans [lemma, in Loeb.internal_provability.Prov_Definition]
ineq_dec [lemma, in Loeb.internal_provability.Prov_Definition]
ineq_plus [lemma, in Loeb.internal_provability.Prov_Definition]
ineq_sandwich [lemma, in Loeb.internal_provability.Prov_Definition]
int_Lob's_theorem [lemma, in Loeb.Loeb]
inv [definition, in Loeb.Definitions]
inv_fg [projection, in Loeb.Definitions]
In_QEqLi [constructor, in Loeb.internal_provability.QEqLiFull]

L

Len [constructor, in Loeb.internal_provability.PA_Lists_Signature]
len_app_ineq' [lemma, in Loeb.internal_provability.Prov_Definition]
len_app_ineq [lemma, in Loeb.internal_provability.Prov_Definition]
len_app_plus_one [lemma, in Loeb.internal_provability.Prov_Definition]
less_by_one [lemma, in Loeb.internal_provability.Prov_Definition]
Li [definition, in Loeb.internal_provability.QEqLiFull]
Limitative_Theorems [library]
list_theory_provability [lemma, in Loeb.util.Util]
Lob's_theorem_from_int [lemma, in Loeb.Loeb]
Lob's_theorem [lemma, in Loeb.Loeb]
Lob's_lemma [lemma, in Loeb.Loeb]
Loeb [library]
Löb [section, in Loeb.Loeb]
Löb.box [variable, in Loeb.Loeb]
Löb.box_distr [variable, in Loeb.Loeb]
Löb.internal_necessitation [variable, in Loeb.Loeb]
Löb.modal_fixpoint [variable, in Loeb.Loeb]
Löb.necessitation [variable, in Loeb.Loeb]
Löb.pei [variable, in Loeb.Loeb]
Löb.T [variable, in Loeb.Loeb]
□ _ [notation, in Loeb.Loeb]

M

modus_ponens_step [lemma, in Loeb.internal_provability.Prov_Definition]
Mostowski [library]
mostowski_strong_sep [lemma, in Loeb.internal_provability.Mostowski]
mostowski_weak_repr [lemma, in Loeb.internal_provability.Mostowski]
mostowski_consistency_sentence [lemma, in Loeb.internal_provability.Mostowski]
mostowski_mod [definition, in Loeb.internal_provability.Mostowski]
MP [section, in Loeb.internal_provability.HBL]
MP [constructor, in Loeb.hilbert_system.Hilbert_System]
MP.ax [variable, in Loeb.internal_provability.HBL]
MP.ax_bound [variable, in Loeb.internal_provability.HBL]
MP.Hax [variable, in Loeb.internal_provability.HBL]
Multivariate_ctq [library]

N

ND_to_Hil [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
nec [section, in Loeb.internal_provability.HBL]
necessitation [lemma, in Loeb.internal_provability.HBL]
nec.ax [variable, in Loeb.internal_provability.HBL]
nec.ax_bound [variable, in Loeb.internal_provability.HBL]
nec.Hax [variable, in Loeb.internal_provability.HBL]
Nil [constructor, in Loeb.internal_provability.PA_Lists_Signature]
num_tprv_neg_enum [lemma, in Loeb.External_Provability]
num_tprv_enum [lemma, in Loeb.External_Provability]
num' [definition, in Loeb.internal_provability.PA_Lists_Signature]
num'_bound' [lemma, in Loeb.internal_provability.PA_Lists_Signature]
n_ary_subst_plus_zero_var [lemma, in Loeb.Multivariate_ctq]
n_ary_subst_update' [lemma, in Loeb.Multivariate_ctq]
n_ary_subst_update [lemma, in Loeb.Multivariate_ctq]
n_ary_subst [definition, in Loeb.Multivariate_ctq]
n_plus_one_ary_function [definition, in Loeb.Multivariate_ctq]
n_ary_ctq.ctq [variable, in Loeb.Multivariate_ctq]
n_ary_ctq.pei [variable, in Loeb.Multivariate_ctq]
n_ary_ctq [section, in Loeb.Multivariate_ctq]

O

operational_S [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
operational_K [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]

P

PAle [definition, in Loeb.internal_provability.PA_Lists_Signature]
PAle_subst [lemma, in Loeb.internal_provability.PA_Lists_Signature]
PAle' [definition, in Loeb.internal_provability.PA_Lists_Signature]
PAle'_subst [lemma, in Loeb.internal_provability.PA_Lists_Signature]
PAlt [definition, in Loeb.internal_provability.PA_Lists_Signature]
PAlt_subst [lemma, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_formulas_eq [lemma, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_signature [instance, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_eq [definition, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_ar [definition, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_sind [definition, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_rec [definition, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_ind [definition, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_rect [definition, in Loeb.internal_provability.PA_Lists_Signature]
PA_func [constructor, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs [inductive, in Loeb.internal_provability.PA_Lists_Signature]
PA_li_Leibniz [instance, in Loeb.internal_provability.QEqLiFull]
PA_Lists_Signature [library]
PC [constructor, in Loeb.hilbert_system.Hilbert_System]
peirce_to_class_theory [lemma, in Loeb.util.Util]
peirce_to_class [lemma, in Loeb.util.Util]
prf [definition, in Loeb.internal_provability.Mostowski]
prf [definition, in Loeb.internal_provability.Prov_Definition]
prf_form_mostowski_consistency_sentence [lemma, in Loeb.internal_provability.Mostowski]
prf_form_mostowski_represents_prf [lemma, in Loeb.internal_provability.Mostowski]
prf_form_mostowski [definition, in Loeb.internal_provability.Mostowski]
prf_decider' [definition, in Loeb.internal_provability.Mostowski]
prf_decider [definition, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski [section, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.göd [variable, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.HEnum [variable, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.Hprf_form [variable, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.Hprf_form_bnd [variable, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.pei [variable, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.prf_form [variable, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.T [variable, in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.T_enumerator [variable, in Loeb.internal_provability.Mostowski]
proof_MP'_correct [lemma, in Loeb.internal_provability.Mostowski]
proof_MP' [definition, in Loeb.internal_provability.Mostowski]
proof_MP [definition, in Loeb.internal_provability.Mostowski]
prov [definition, in Loeb.internal_provability.Mostowski]
prov [definition, in Loeb.internal_provability.Prov_Definition]
Prov_Definition [library]
prv_enum_red [lemma, in Loeb.External_Provability]

Q

QEqImpl [constructor, in Loeb.internal_provability.QEqLiFull]
QEqInduction [constructor, in Loeb.internal_provability.QEqLiFull]
QEqLi [definition, in Loeb.internal_provability.QEqLiFull]
QEqLiFull [inductive, in Loeb.internal_provability.QEqLiFull]
QEqLiFull [library]
QEqLiFull_leibniz [lemma, in Loeb.internal_provability.QEqLiFull]
QEqLiFull_sind [definition, in Loeb.internal_provability.QEqLiFull]
QEqLiFull_ind [definition, in Loeb.internal_provability.QEqLiFull]
QEqLi_leibniz [lemma, in Loeb.internal_provability.QEqLiFull]
QEqLi_leibniz_t [lemma, in Loeb.internal_provability.QEqLiFull]
QEqLi_rewriting [section, in Loeb.internal_provability.QEqLiFull]
Qeq_generalisation [lemma, in Loeb.util.Util]
Qeq_consistent [lemma, in Loeb.util.Util]
QLi [definition, in Loeb.internal_provability.QEqLiFull]
qq_representation [lemma, in Loeb.Diagonal_Lemma]
qq_closed [lemma, in Loeb.Definitions]
quantifed_hilAx_derivable [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
quine_quote [definition, in Loeb.Definitions]

R

Robinson_facts [section, in Loeb.util.Util]

S

Sig1_sound_weak_representability [lemma, in Loeb.External_Provability]
Sig1_sound_consistent [lemma, in Loeb.External_Provability]
Sig1_sound [definition, in Loeb.External_Provability]
singleton_list_access [lemma, in Loeb.internal_provability.Prov_Definition]
SoundnessLemmas [section, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_PC [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_ExE [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_ExI [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_AllD [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_AllG [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_AllE [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_Ebot [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_DE [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_DI2 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_DI1 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_CE2 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_CE1 [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_CI [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_HS [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_HK [lemma, in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_prov_pred [definition, in Loeb.External_Provability]
stable [definition, in Loeb.Limitative_Theorems]
stable_classical [lemma, in Loeb.Limitative_Theorems]
strongly_definable [definition, in Loeb.Limitative_Theorems]
subst_bound_2_with_term_subst [lemma, in Loeb.Diagonal_Lemma]
subst_deriv_preservance [lemma, in Loeb.Multivariate_ctq]
subst_bound_2 [lemma, in Loeb.util.Util]
subst_bound_1 [lemma, in Loeb.util.Util]

T

Tarski [section, in Loeb.Limitative_Theorems]
Tarski's_Theorem [lemma, in Loeb.Limitative_Theorems]
Tarski.ctq [variable, in Loeb.Limitative_Theorems]
Tarski.göd [variable, in Loeb.Limitative_Theorems]
term_inclusion [definition, in Loeb.internal_provability.PA_Lists_Signature]
ThAx [constructor, in Loeb.hilbert_system.Hilbert_System]
thilprv [definition, in Loeb.hilbert_system.Hilbert_System]
thm_god_not_definable [lemma, in Loeb.Limitative_Theorems]
Translations [section, in Loeb.util.Util]

U

un_vector_inv [lemma, in Loeb.util.Vector_Lemmas]
Util [library]

V

vector_inv_two_elems [lemma, in Loeb.util.Vector_Lemmas]
vector_eval [definition, in Loeb.Multivariate_ctq]
Vector_Lemmas [library]

W

well_formed_propagation [lemma, in Loeb.internal_provability.Prov_Definition]
well_formed_bound [lemma, in Loeb.internal_provability.Prov_Definition]
well_formed [definition, in Loeb.internal_provability.Prov_Definition]

X

x_plus_zero [lemma, in Loeb.internal_provability.Prov_Definition]

Z

zero_vector_is_nil [lemma, in Loeb.util.Vector_Lemmas]

other

_ ⧀=l' _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ ⧀=l _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ ⧀l _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ === _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ ~> _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ +++ _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ G _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
len _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ ::: _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
[|] (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ ⊗ _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ ⊕ _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
σ _ (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
zero (PA_li_Notation) [notation, in Loeb.internal_provability.PA_Lists_Signature]
_ ⊢HTC _ [notation, in Loeb.hilbert_system.Hilbert_System]
_ ⊢HTI _ [notation, in Loeb.hilbert_system.Hilbert_System]
_ ⊢HT _ [notation, in Loeb.hilbert_system.Hilbert_System]
_ ⊢HC _ [notation, in Loeb.hilbert_system.Hilbert_System]
_ ⊢HI _ [notation, in Loeb.hilbert_system.Hilbert_System]
_ ⊢H _ [notation, in Loeb.hilbert_system.Hilbert_System]
Σ1_convervativity' [lemma, in Loeb.util.Util]
σ_large_injective [lemma, in Loeb.internal_provability.Prov_Definition]

Notation Index

L

□ _ [in Loeb.Loeb]

other

_ ⧀=l' _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ ⧀=l _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ ⧀l _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ === _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ ~> _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ +++ _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ G _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
len _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ ::: _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
[|] (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ ⊗ _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ ⊕ _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
σ _ (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
zero (PA_li_Notation) [in Loeb.internal_provability.PA_Lists_Signature]
_ ⊢HTC _ [in Loeb.hilbert_system.Hilbert_System]
_ ⊢HTI _ [in Loeb.hilbert_system.Hilbert_System]
_ ⊢HT _ [in Loeb.hilbert_system.Hilbert_System]
_ ⊢HC _ [in Loeb.hilbert_system.Hilbert_System]
_ ⊢HI _ [in Loeb.hilbert_system.Hilbert_System]
_ ⊢H _ [in Loeb.hilbert_system.Hilbert_System]

Variable Index

D

DefProv.ax [in Loeb.internal_provability.Prov_Definition]
DefProv.ax_bound [in Loeb.internal_provability.Prov_Definition]
DefProv.göd [in Loeb.internal_provability.Prov_Definition]
DefProv.Hax [in Loeb.internal_provability.Prov_Definition]
DefProv.pei [in Loeb.internal_provability.Prov_Definition]
Diagonal_Lemma.φ_D_Hcapt [in Loeb.Diagonal_Lemma]
Diagonal_Lemma.φ_D_is_Σ1 [in Loeb.Diagonal_Lemma]
Diagonal_Lemma.φ_D_bound [in Loeb.Diagonal_Lemma]
Diagonal_Lemma.φ_D [in Loeb.Diagonal_Lemma]
Diagonal_Lemma.göd [in Loeb.Diagonal_Lemma]
Diagonal_Lemma.pei [in Loeb.Diagonal_Lemma]

E

ExternalMostowski.göd [in Loeb.internal_provability.Mostowski]
ExternalMostowski.pei [in Loeb.internal_provability.Mostowski]
Ext_prov.göd [in Loeb.External_Provability]
Ext_prov.ctq [in Loeb.External_Provability]
Ext_prov.pei [in Loeb.External_Provability]

G

Gödel.ctq [in Loeb.Limitative_Theorems]
Gödel.göd [in Loeb.Limitative_Theorems]
Gödel.pei [in Loeb.Limitative_Theorems]

I

Indefinability.ctq [in Loeb.Limitative_Theorems]
Indefinability.göd [in Loeb.Limitative_Theorems]
Indefinability.pei [in Loeb.Limitative_Theorems]

L

Löb.box [in Loeb.Loeb]
Löb.box_distr [in Loeb.Loeb]
Löb.internal_necessitation [in Loeb.Loeb]
Löb.modal_fixpoint [in Loeb.Loeb]
Löb.necessitation [in Loeb.Loeb]
Löb.pei [in Loeb.Loeb]
Löb.T [in Loeb.Loeb]

M

MP.ax [in Loeb.internal_provability.HBL]
MP.ax_bound [in Loeb.internal_provability.HBL]
MP.Hax [in Loeb.internal_provability.HBL]

N

nec.ax [in Loeb.internal_provability.HBL]
nec.ax_bound [in Loeb.internal_provability.HBL]
nec.Hax [in Loeb.internal_provability.HBL]
n_ary_ctq.ctq [in Loeb.Multivariate_ctq]
n_ary_ctq.pei [in Loeb.Multivariate_ctq]

P

ProofPredicateMostowski.göd [in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.HEnum [in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.Hprf_form [in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.Hprf_form_bnd [in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.pei [in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.prf_form [in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.T [in Loeb.internal_provability.Mostowski]
ProofPredicateMostowski.T_enumerator [in Loeb.internal_provability.Mostowski]

T

Tarski.ctq [in Loeb.Limitative_Theorems]
Tarski.göd [in Loeb.Limitative_Theorems]

Library Index

D

Definitions
Diagonal_Lemma

E

External_Provability

H

HBL
Hilbert_System
Hilbert_System_Deduction_Facts

L

Limitative_Theorems
Loeb

M

Mostowski
Multivariate_ctq

P

PA_Lists_Signature
Prov_Definition

Q

QEqLiFull

U

Util

V

Vector_Lemmas

Lemma Index

A

add_cancel [in Loeb.internal_provability.Prov_Definition]
add_assoc [in Loeb.internal_provability.Prov_Definition]
add_one [in Loeb.internal_provability.Prov_Definition]
add_comm [in Loeb.internal_provability.Prov_Definition]
add_rec_right [in Loeb.internal_provability.Prov_Definition]
AxiomList_in_QEqLi_Axioms [in Loeb.internal_provability.Prov_Definition]
axioms_are_provable [in Loeb.internal_provability.Prov_Definition]
axiom_inclusion [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]

B

binary_ctq [in Loeb.Multivariate_ctq]
bin_vector_inv [in Loeb.util.Vector_Lemmas]
bound_bin_fun [in Loeb.internal_provability.Prov_Definition]
bound_un_fun [in Loeb.internal_provability.Prov_Definition]
box_distr [in Loeb.internal_provability.Prov_Definition]
box_distr_Gödel_numeral [in Loeb.internal_provability.HBL]

C

compat_Pc [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_DE [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_DI2 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_DI1 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_CE2 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_CE1 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_CI [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_ctx [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_Exp [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_ExE [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_ExI [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_AllE [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_AllI [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
compat_IE [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
contrapositive_elim [in Loeb.Limitative_Theorems]
CTQ_gives_Diagonal_Lemma [in Loeb.Diagonal_Lemma]
ctq_n_ary [in Loeb.Multivariate_ctq]

D

decidable_pred_is_definable [in Loeb.Limitative_Theorems]
deduction_theorem [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
diagonalisation_equivalence [in Loeb.Diagonal_Lemma]
Diagonal_Lemma_bound_counterexample [in Loeb.Diagonal_Lemma]
Diagonal_Lemma_mult_counterexample [in Loeb.Diagonal_Lemma]
diagonal_lemma [in Loeb.Diagonal_Lemma]
diag_G_closed [in Loeb.Diagonal_Lemma]
diag_göd_comm [in Loeb.Diagonal_Lemma]
double_neg_elim_class [in Loeb.Limitative_Theorems]

E

embed_eval_interchange [in Loeb.Multivariate_ctq]
empty_context_forall_times_intro [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
empty_context_AllI [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
encoding_ineq [in Loeb.internal_provability.Mostowski]
essential_undecidability [in Loeb.Limitative_Theorems]
ext_prov_modus_ponens_counteraxample [in Loeb.internal_provability.Mostowski]
ex_sProv_T [in Loeb.External_Provability]
ex_prov_T [in Loeb.External_Provability]
ex_prov_T_util [in Loeb.External_Provability]

F

forall_times_once [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
form_inv [in Loeb.util.Util]

G

get_last_triple_app [in Loeb.internal_provability.Prov_Definition]
get_mid_index [in Loeb.internal_provability.Prov_Definition]
get_mid_index' [in Loeb.internal_provability.Prov_Definition]
get_low_index [in Loeb.internal_provability.Prov_Definition]
get_low_index' [in Loeb.internal_provability.Prov_Definition]
godel_first_incompleteness_strong_sep [in Loeb.Limitative_Theorems]
godel_first_incompleteness_Sig1_sound [in Loeb.Limitative_Theorems]
godel_first_incompleteness_tarski [in Loeb.Limitative_Theorems]
Godel's_second_incompleteness_theorem [in Loeb.Loeb]
god_not_strongly_definable [in Loeb.Limitative_Theorems]

H

Hil_ND_agree_theories [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
Hil_ND_agree [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
Hil_to_ND [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]

I

identity [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
index_destruct [in Loeb.internal_provability.Prov_Definition]
index_destruct' [in Loeb.internal_provability.Prov_Definition]
ineq_trans [in Loeb.internal_provability.Prov_Definition]
ineq_dec [in Loeb.internal_provability.Prov_Definition]
ineq_plus [in Loeb.internal_provability.Prov_Definition]
ineq_sandwich [in Loeb.internal_provability.Prov_Definition]
int_Lob's_theorem [in Loeb.Loeb]

L

len_app_ineq' [in Loeb.internal_provability.Prov_Definition]
len_app_ineq [in Loeb.internal_provability.Prov_Definition]
len_app_plus_one [in Loeb.internal_provability.Prov_Definition]
less_by_one [in Loeb.internal_provability.Prov_Definition]
list_theory_provability [in Loeb.util.Util]
Lob's_theorem_from_int [in Loeb.Loeb]
Lob's_theorem [in Loeb.Loeb]
Lob's_lemma [in Loeb.Loeb]

M

modus_ponens_step [in Loeb.internal_provability.Prov_Definition]
mostowski_strong_sep [in Loeb.internal_provability.Mostowski]
mostowski_weak_repr [in Loeb.internal_provability.Mostowski]
mostowski_consistency_sentence [in Loeb.internal_provability.Mostowski]

N

ND_to_Hil [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
necessitation [in Loeb.internal_provability.HBL]
num_tprv_neg_enum [in Loeb.External_Provability]
num_tprv_enum [in Loeb.External_Provability]
num'_bound' [in Loeb.internal_provability.PA_Lists_Signature]
n_ary_subst_plus_zero_var [in Loeb.Multivariate_ctq]
n_ary_subst_update' [in Loeb.Multivariate_ctq]
n_ary_subst_update [in Loeb.Multivariate_ctq]

O

operational_S [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
operational_K [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]

P

PAle_subst [in Loeb.internal_provability.PA_Lists_Signature]
PAle'_subst [in Loeb.internal_provability.PA_Lists_Signature]
PAlt_subst [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_formulas_eq [in Loeb.internal_provability.PA_Lists_Signature]
peirce_to_class_theory [in Loeb.util.Util]
peirce_to_class [in Loeb.util.Util]
prf_form_mostowski_consistency_sentence [in Loeb.internal_provability.Mostowski]
prf_form_mostowski_represents_prf [in Loeb.internal_provability.Mostowski]
proof_MP'_correct [in Loeb.internal_provability.Mostowski]
prv_enum_red [in Loeb.External_Provability]

Q

QEqLiFull_leibniz [in Loeb.internal_provability.QEqLiFull]
QEqLi_leibniz [in Loeb.internal_provability.QEqLiFull]
QEqLi_leibniz_t [in Loeb.internal_provability.QEqLiFull]
Qeq_generalisation [in Loeb.util.Util]
Qeq_consistent [in Loeb.util.Util]
qq_representation [in Loeb.Diagonal_Lemma]
qq_closed [in Loeb.Definitions]
quantifed_hilAx_derivable [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]

S

Sig1_sound_weak_representability [in Loeb.External_Provability]
Sig1_sound_consistent [in Loeb.External_Provability]
singleton_list_access [in Loeb.internal_provability.Prov_Definition]
sound_PC [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_ExE [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_ExI [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_AllD [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_AllG [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_AllE [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_Ebot [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_DE [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_DI2 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_DI1 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_CE2 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_CE1 [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_CI [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_HS [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
sound_HK [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]
stable_classical [in Loeb.Limitative_Theorems]
subst_bound_2_with_term_subst [in Loeb.Diagonal_Lemma]
subst_deriv_preservance [in Loeb.Multivariate_ctq]
subst_bound_2 [in Loeb.util.Util]
subst_bound_1 [in Loeb.util.Util]

T

Tarski's_Theorem [in Loeb.Limitative_Theorems]
thm_god_not_definable [in Loeb.Limitative_Theorems]

U

un_vector_inv [in Loeb.util.Vector_Lemmas]

V

vector_inv_two_elems [in Loeb.util.Vector_Lemmas]

W

well_formed_propagation [in Loeb.internal_provability.Prov_Definition]
well_formed_bound [in Loeb.internal_provability.Prov_Definition]

X

x_plus_zero [in Loeb.internal_provability.Prov_Definition]

Z

zero_vector_is_nil [in Loeb.util.Vector_Lemmas]

other

Σ1_convervativity' [in Loeb.util.Util]
σ_large_injective [in Loeb.internal_provability.Prov_Definition]

Constructor Index

A

AllD [in Loeb.hilbert_system.Hilbert_System]
AllE [in Loeb.hilbert_system.Hilbert_System]
AllG [in Loeb.hilbert_system.Hilbert_System]
App [in Loeb.internal_provability.PA_Lists_Signature]

C

cconj [in Loeb.util.Util]
CE1 [in Loeb.hilbert_system.Hilbert_System]
CE2 [in Loeb.hilbert_system.Hilbert_System]
CI [in Loeb.hilbert_system.Hilbert_System]
Cons [in Loeb.internal_provability.PA_Lists_Signature]

D

DE [in Loeb.hilbert_system.Hilbert_System]
DI1 [in Loeb.hilbert_system.Hilbert_System]
DI2 [in Loeb.hilbert_system.Hilbert_System]

E

Ebot [in Loeb.hilbert_system.Hilbert_System]
ExE [in Loeb.hilbert_system.Hilbert_System]
ExI [in Loeb.hilbert_system.Hilbert_System]

G

Get [in Loeb.internal_provability.PA_Lists_Signature]

H

HilAx [in Loeb.hilbert_system.Hilbert_System]
HK [in Loeb.hilbert_system.Hilbert_System]
HS [in Loeb.hilbert_system.Hilbert_System]

I

Imp [in Loeb.internal_provability.PA_Lists_Signature]
In_QEqLi [in Loeb.internal_provability.QEqLiFull]

L

Len [in Loeb.internal_provability.PA_Lists_Signature]

M

MP [in Loeb.hilbert_system.Hilbert_System]

N

Nil [in Loeb.internal_provability.PA_Lists_Signature]

P

PA_func [in Loeb.internal_provability.PA_Lists_Signature]
PC [in Loeb.hilbert_system.Hilbert_System]

Q

QEqImpl [in Loeb.internal_provability.QEqLiFull]
QEqInduction [in Loeb.internal_provability.QEqLiFull]

T

ThAx [in Loeb.hilbert_system.Hilbert_System]

Projection Index

F

f [in Loeb.Definitions]

G

g [in Loeb.Definitions]

I

inv_fg [in Loeb.Definitions]

Inductive Index

A

aand [in Loeb.util.Util]

H

hilAx [in Loeb.hilbert_system.Hilbert_System]
hilprv [in Loeb.hilbert_system.Hilbert_System]

P

PA_li_funcs [in Loeb.internal_provability.PA_Lists_Signature]

Q

QEqLiFull [in Loeb.internal_provability.QEqLiFull]

Section Index

A

Axioms [in Loeb.internal_provability.QEqLiFull]

C

comparisons [in Loeb.internal_provability.PA_Lists_Signature]
CompatibilityLemmas [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]

D

DefProv [in Loeb.internal_provability.Prov_Definition]
Diagonal_Lemma [in Loeb.Diagonal_Lemma]

E

ExternalMostowski [in Loeb.internal_provability.Mostowski]
Ext_prov [in Loeb.External_Provability]

F

Formula_facts [in Loeb.util.Util]

G

Gödel [in Loeb.Limitative_Theorems]

I

Indefinability [in Loeb.Limitative_Theorems]

L

Löb [in Loeb.Loeb]

M

MP [in Loeb.internal_provability.HBL]

N

nec [in Loeb.internal_provability.HBL]
n_ary_ctq [in Loeb.Multivariate_ctq]

P

ProofPredicateMostowski [in Loeb.internal_provability.Mostowski]

Q

QEqLi_rewriting [in Loeb.internal_provability.QEqLiFull]

R

Robinson_facts [in Loeb.util.Util]

S

SoundnessLemmas [in Loeb.hilbert_system.Hilbert_System_Deduction_Facts]

T

Tarski [in Loeb.Limitative_Theorems]
Translations [in Loeb.util.Util]

Instance Index

E

eqdec_preds [in Loeb.Loeb]
eqdec_funcs [in Loeb.Loeb]
eqdec_preds [in Loeb.internal_provability.QEqLiFull]
eqdec_funcs [in Loeb.internal_provability.QEqLiFull]
eqdec_preds' [in Loeb.internal_provability.Mostowski]
eqdec_funcs' [in Loeb.internal_provability.Mostowski]
eqdec_preds [in Loeb.internal_provability.Mostowski]
eqdec_funcs [in Loeb.internal_provability.Mostowski]
eqdec_preds [in Loeb.internal_provability.Prov_Definition]
eqdec_funcs [in Loeb.internal_provability.Prov_Definition]
eqdec_preds [in Loeb.Limitative_Theorems]
eqdec_funcs [in Loeb.Limitative_Theorems]

P

PA_li_funcs_signature [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_Leibniz [in Loeb.internal_provability.QEqLiFull]

Definition Index

A

aand_sind [in Loeb.util.Util]
aand_rec [in Loeb.util.Util]
aand_ind [in Loeb.util.Util]
aand_rect [in Loeb.util.Util]
arg_embed [in Loeb.Multivariate_ctq]
AxiomList [in Loeb.internal_provability.Prov_Definition]
ax_induction' [in Loeb.internal_provability.QEqLiFull]
ax_imp_congr [in Loeb.internal_provability.QEqLiFull]
ax_app_congr [in Loeb.internal_provability.QEqLiFull]
ax_get_congr [in Loeb.internal_provability.QEqLiFull]
ax_len_congr [in Loeb.internal_provability.QEqLiFull]
ax_cons_congr [in Loeb.internal_provability.QEqLiFull]
ax_impl [in Loeb.internal_provability.QEqLiFull]
ax_get_app_right [in Loeb.internal_provability.QEqLiFull]
ax_get_app_left [in Loeb.internal_provability.QEqLiFull]
ax_len_app [in Loeb.internal_provability.QEqLiFull]
ax_get_succ [in Loeb.internal_provability.QEqLiFull]
ax_get_zero [in Loeb.internal_provability.QEqLiFull]
ax_len_cons [in Loeb.internal_provability.QEqLiFull]
ax_len_nil [in Loeb.internal_provability.QEqLiFull]

D

dec [in Loeb.Definitions]
decider [in Loeb.Definitions]
definable [in Loeb.Limitative_Theorems]
defines_pred_strongly [in Loeb.Limitative_Theorems]
defines_pred [in Loeb.Limitative_Theorems]
diagonalisation [in Loeb.Diagonal_Lemma]
diag_G [in Loeb.Diagonal_Lemma]
diag_F [in Loeb.Diagonal_Lemma]
diag_nat [in Loeb.Diagonal_Lemma]

E

ext_prov_pred [in Loeb.External_Provability]

F

form_inclusion [in Loeb.internal_provability.PA_Lists_Signature]

H

hilAx_sind [in Loeb.hilbert_system.Hilbert_System]
hilAx_ind [in Loeb.hilbert_system.Hilbert_System]
hilprv_sind [in Loeb.hilbert_system.Hilbert_System]
hilprv_ind [in Loeb.hilbert_system.Hilbert_System]

I

impl [in Loeb.internal_provability.Mostowski]
impl_dec [in Loeb.internal_provability.Mostowski]
impl_dec [in Loeb.util.Util]
impl' [in Loeb.internal_provability.Mostowski]
inv [in Loeb.Definitions]

L

Li [in Loeb.internal_provability.QEqLiFull]

M

mostowski_mod [in Loeb.internal_provability.Mostowski]

N

num' [in Loeb.internal_provability.PA_Lists_Signature]
n_ary_subst [in Loeb.Multivariate_ctq]
n_plus_one_ary_function [in Loeb.Multivariate_ctq]

P

PAle [in Loeb.internal_provability.PA_Lists_Signature]
PAle' [in Loeb.internal_provability.PA_Lists_Signature]
PAlt [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_eq [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_ar [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_sind [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_rec [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_ind [in Loeb.internal_provability.PA_Lists_Signature]
PA_li_funcs_rect [in Loeb.internal_provability.PA_Lists_Signature]
prf [in Loeb.internal_provability.Mostowski]
prf [in Loeb.internal_provability.Prov_Definition]
prf_form_mostowski [in Loeb.internal_provability.Mostowski]
prf_decider' [in Loeb.internal_provability.Mostowski]
prf_decider [in Loeb.internal_provability.Mostowski]
proof_MP' [in Loeb.internal_provability.Mostowski]
proof_MP [in Loeb.internal_provability.Mostowski]
prov [in Loeb.internal_provability.Mostowski]
prov [in Loeb.internal_provability.Prov_Definition]

Q

QEqLi [in Loeb.internal_provability.QEqLiFull]
QEqLiFull_sind [in Loeb.internal_provability.QEqLiFull]
QEqLiFull_ind [in Loeb.internal_provability.QEqLiFull]
QLi [in Loeb.internal_provability.QEqLiFull]
quine_quote [in Loeb.Definitions]

S

Sig1_sound [in Loeb.External_Provability]
sound_prov_pred [in Loeb.External_Provability]
stable [in Loeb.Limitative_Theorems]
strongly_definable [in Loeb.Limitative_Theorems]

T

term_inclusion [in Loeb.internal_provability.PA_Lists_Signature]
thilprv [in Loeb.hilbert_system.Hilbert_System]

V

vector_eval [in Loeb.Multivariate_ctq]

W

well_formed [in Loeb.internal_provability.Prov_Definition]

Record Index

G

goedelisation [in Loeb.Definitions]

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(376 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(21 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(47 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(15 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(145 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(29 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(3 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(20 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(14 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(76 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1 entry)