| 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 | (2304 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 | (59 entries) |
| Binder 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 | (1577 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 | (65 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 | (9 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 | (332 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 | (60 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 | (8 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 | (19 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 | (42 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 | (115 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 | (4 entries) |
Global Index
A
A [definition, in Tennenbaum.Tennenbaum]Add [definition, in Tennenbaum.CTT]
Add_rec [lemma, in Tennenbaum.Peano]
add_le_mono [lemma, in Tennenbaum.Peano]
add_lt_mono [lemma, in Tennenbaum.Peano]
add_eq [lemma, in Tennenbaum.Peano]
add_asso [lemma, in Tennenbaum.Peano]
add_comm [lemma, in Tennenbaum.Peano]
add_rec_r [lemma, in Tennenbaum.Peano]
add_zero_r [lemma, in Tennenbaum.Peano]
add_rec [lemma, in Tennenbaum.Peano]
add_zero [lemma, in Tennenbaum.Peano]
All [constructor, in Tennenbaum.Tarski]
AllE [constructor, in Tennenbaum.Deduction]
AllI [constructor, in Tennenbaum.Deduction]
alpha:105 [binder, in Tennenbaum.Deduction]
alpha:37 [binder, in Tennenbaum.Peano]
alpha:389 [binder, in Tennenbaum.Tennenbaum]
alpha:95 [binder, in Tennenbaum.Deduction]
AP [definition, in Tennenbaum.Tennenbaum]
AP_EQ [lemma, in Tennenbaum.Tennenbaum]
ar_preds [projection, in Tennenbaum.FOL]
ar_syms [projection, in Tennenbaum.FOL]
atom [constructor, in Tennenbaum.FOL]
axioms:53 [binder, in Tennenbaum.Peano]
ax_mult_congr [definition, in Tennenbaum.Peano]
ax_add_congr [definition, in Tennenbaum.Peano]
ax_succ_congr [definition, in Tennenbaum.Peano]
ax_trans [definition, in Tennenbaum.Peano]
ax_sym [definition, in Tennenbaum.Peano]
ax_refl [definition, in Tennenbaum.Peano]
ax_zero_or_succ [definition, in Tennenbaum.Peano]
ax_induction [definition, in Tennenbaum.Peano]
ax_mult_rec [definition, in Tennenbaum.Peano]
ax_mult_zero [definition, in Tennenbaum.Peano]
ax_add_rec [definition, in Tennenbaum.Peano]
ax_add_zero [definition, in Tennenbaum.Peano]
ax_succ_inj [definition, in Tennenbaum.Peano]
ax_zero_succ [definition, in Tennenbaum.Peano]
ax:151 [binder, in Tennenbaum.Tennenbaum]
ax:164 [binder, in Tennenbaum.Tennenbaum]
ax:18 [binder, in Tennenbaum.Peano]
ax:224 [binder, in Tennenbaum.Peano]
ax:226 [binder, in Tennenbaum.Peano]
ax:52 [binder, in Tennenbaum.Peano]
a':76 [binder, in Tennenbaum.FOL]
a1:22 [binder, in Tennenbaum.NumberTheory]
a2:24 [binder, in Tennenbaum.NumberTheory]
A:1 [binder, in Tennenbaum.CTT]
A:103 [binder, in Tennenbaum.Deduction]
A:108 [binder, in Tennenbaum.Deduction]
A:11 [binder, in Tennenbaum.Deduction]
A:112 [binder, in Tennenbaum.Deduction]
A:130 [binder, in Tennenbaum.Deduction]
A:137 [binder, in Tennenbaum.Tennenbaum]
A:14 [binder, in Tennenbaum.CTT]
A:140 [binder, in Tennenbaum.Tennenbaum]
A:147 [binder, in Tennenbaum.Deduction]
A:15 [binder, in Tennenbaum.LogicFacts]
A:16 [binder, in Tennenbaum.Deduction]
A:162 [binder, in Tennenbaum.Deduction]
A:166 [binder, in Tennenbaum.Deduction]
A:17 [binder, in Tennenbaum.LogicFacts]
A:17 [binder, in Tennenbaum.CTT]
A:19 [binder, in Tennenbaum.LogicFacts]
A:190 [binder, in Tennenbaum.Deduction]
A:193 [binder, in Tennenbaum.FOL]
A:202 [binder, in Tennenbaum.Tennenbaum]
A:21 [binder, in Tennenbaum.LogicFacts]
A:21 [binder, in Tennenbaum.Tennenbaum]
A:21 [binder, in Tennenbaum.Deduction]
a:213 [binder, in Tennenbaum.Peano]
A:22 [binder, in Tennenbaum.LogicFacts]
A:22 [binder, in Tennenbaum.Tennenbaum]
A:221 [binder, in Tennenbaum.Deduction]
A:222 [binder, in Tennenbaum.Tennenbaum]
A:225 [binder, in Tennenbaum.FOL]
A:227 [binder, in Tennenbaum.Deduction]
A:23 [binder, in Tennenbaum.CTT]
A:24 [binder, in Tennenbaum.LogicFacts]
A:24 [binder, in Tennenbaum.Tennenbaum]
A:240 [binder, in Tennenbaum.Deduction]
A:243 [binder, in Tennenbaum.FOL]
A:246 [binder, in Tennenbaum.Deduction]
A:25 [binder, in Tennenbaum.Deduction]
A:253 [binder, in Tennenbaum.Deduction]
a:27 [binder, in Tennenbaum.NumberTheory]
A:27 [binder, in Tennenbaum.Peano]
A:284 [binder, in Tennenbaum.FOL]
A:29 [binder, in Tennenbaum.Tarski]
a:29 [binder, in Tennenbaum.NumberTheory]
A:298 [binder, in Tennenbaum.FOL]
a:30 [binder, in Tennenbaum.CantorPairing]
A:30 [binder, in Tennenbaum.CTT]
A:30 [binder, in Tennenbaum.Deduction]
a:300 [binder, in Tennenbaum.FOL]
A:303 [binder, in Tennenbaum.FOL]
A:305 [binder, in Tennenbaum.Peano]
a:312 [binder, in Tennenbaum.Tennenbaum]
a:317 [binder, in Tennenbaum.Tennenbaum]
A:318 [binder, in Tennenbaum.Tennenbaum]
a:320 [binder, in Tennenbaum.Tennenbaum]
A:348 [binder, in Tennenbaum.Peano]
A:35 [binder, in Tennenbaum.Deduction]
a:352 [binder, in Tennenbaum.Tennenbaum]
A:371 [binder, in Tennenbaum.Tennenbaum]
A:39 [binder, in Tennenbaum.Tarski]
A:39 [binder, in Tennenbaum.Deduction]
A:406 [binder, in Tennenbaum.Tennenbaum]
A:43 [binder, in Tennenbaum.Deduction]
a:45 [binder, in Tennenbaum.Peano]
A:47 [binder, in Tennenbaum.Tarski]
A:47 [binder, in Tennenbaum.Deduction]
a:48 [binder, in Tennenbaum.Peano]
a:5 [binder, in Tennenbaum.CTT]
A:52 [binder, in Tennenbaum.Deduction]
A:54 [binder, in Tennenbaum.Tarski]
A:57 [binder, in Tennenbaum.Deduction]
A:61 [binder, in Tennenbaum.FOL]
A:62 [binder, in Tennenbaum.Deduction]
A:67 [binder, in Tennenbaum.Deduction]
a:68 [binder, in Tennenbaum.NumberTheory]
A:69 [binder, in Tennenbaum.FOL]
A:7 [binder, in Tennenbaum.Tennenbaum]
a:70 [binder, in Tennenbaum.FOL]
a:71 [binder, in Tennenbaum.NumberTheory]
A:72 [binder, in Tennenbaum.Deduction]
A:77 [binder, in Tennenbaum.Deduction]
a:8 [binder, in Tennenbaum.CTT]
A:84 [binder, in Tennenbaum.Deduction]
A:90 [binder, in Tennenbaum.Deduction]
A:93 [binder, in Tennenbaum.Tarski]
A:98 [binder, in Tennenbaum.Tarski]
B
B [definition, in Tennenbaum.Tennenbaum]beta:106 [binder, in Tennenbaum.Deduction]
beta:96 [binder, in Tennenbaum.Deduction]
better_leibniz [lemma, in Tennenbaum.Peano]
bijection [definition, in Tennenbaum.CantorPairing]
Bij_Nat_NatNat [lemma, in Tennenbaum.CantorPairing]
bin [constructor, in Tennenbaum.FOL]
binary [definition, in Tennenbaum.Tennenbaum]
binop [projection, in Tennenbaum.FOL]
binop:177 [binder, in Tennenbaum.FOL]
bool_cases [lemma, in Tennenbaum.CTT]
bool_disjoint [lemma, in Tennenbaum.CTT]
bouded_func [constructor, in Tennenbaum.FOL]
bounded [inductive, in Tennenbaum.FOL]
Bounded [section, in Tennenbaum.FOL]
bounded_S_forall [lemma, in Tennenbaum.Tarski]
bounded_S_exists [lemma, in Tennenbaum.Tarski]
bounded_eval_t [lemma, in Tennenbaum.Tarski]
bounded_exists_Δ0_equiv [lemma, in Tennenbaum.Tennenbaum]
bounded_t_dec [lemma, in Tennenbaum.FOL]
bounded_up [lemma, in Tennenbaum.FOL]
bounded_up_t [lemma, in Tennenbaum.FOL]
bounded_subst [lemma, in Tennenbaum.FOL]
bounded_subst_t [lemma, in Tennenbaum.FOL]
bounded_L [definition, in Tennenbaum.FOL]
bounded_falsity [constructor, in Tennenbaum.FOL]
bounded_quant [constructor, in Tennenbaum.FOL]
bounded_eq [constructor, in Tennenbaum.FOL]
bounded_bin [constructor, in Tennenbaum.FOL]
bounded_atom [constructor, in Tennenbaum.FOL]
bounded_var [constructor, in Tennenbaum.FOL]
bounded_t [inductive, in Tennenbaum.FOL]
bound_ext [lemma, in Tennenbaum.Tarski]
B_I [constructor, in Tennenbaum.Tarski]
b1:23 [binder, in Tennenbaum.NumberTheory]
b1:267 [binder, in Tennenbaum.FOL]
b2:25 [binder, in Tennenbaum.NumberTheory]
b2:268 [binder, in Tennenbaum.FOL]
b:109 [binder, in Tennenbaum.Tennenbaum]
b:112 [binder, in Tennenbaum.Tennenbaum]
B:127 [binder, in Tennenbaum.Tennenbaum]
B:132 [binder, in Tennenbaum.Tennenbaum]
B:148 [binder, in Tennenbaum.Deduction]
B:16 [binder, in Tennenbaum.LogicFacts]
b:165 [binder, in Tennenbaum.Deduction]
B:18 [binder, in Tennenbaum.LogicFacts]
B:2 [binder, in Tennenbaum.CTT]
B:20 [binder, in Tennenbaum.LogicFacts]
B:203 [binder, in Tennenbaum.Tennenbaum]
b:214 [binder, in Tennenbaum.Peano]
b:220 [binder, in Tennenbaum.Deduction]
B:223 [binder, in Tennenbaum.Tennenbaum]
B:23 [binder, in Tennenbaum.LogicFacts]
B:23 [binder, in Tennenbaum.Tennenbaum]
b:248 [binder, in Tennenbaum.Deduction]
B:25 [binder, in Tennenbaum.LogicFacts]
b:255 [binder, in Tennenbaum.Deduction]
b:264 [binder, in Tennenbaum.FOL]
b:28 [binder, in Tennenbaum.NumberTheory]
B:299 [binder, in Tennenbaum.FOL]
b:30 [binder, in Tennenbaum.NumberTheory]
b:301 [binder, in Tennenbaum.FOL]
b:336 [binder, in Tennenbaum.Tennenbaum]
b:35 [binder, in Tennenbaum.FOL]
b:351 [binder, in Tennenbaum.Tennenbaum]
b:37 [binder, in Tennenbaum.FOL]
b:38 [binder, in Tennenbaum.FOL]
b:39 [binder, in Tennenbaum.FOL]
b:397 [binder, in Tennenbaum.Tennenbaum]
B:407 [binder, in Tennenbaum.Tennenbaum]
b:44 [binder, in Tennenbaum.CTT]
b:46 [binder, in Tennenbaum.Peano]
b:46 [binder, in Tennenbaum.FOL]
b:49 [binder, in Tennenbaum.Peano]
b:6 [binder, in Tennenbaum.CTT]
b:69 [binder, in Tennenbaum.NumberTheory]
b:72 [binder, in Tennenbaum.NumberTheory]
b:9 [binder, in Tennenbaum.CTT]
B:91 [binder, in Tennenbaum.Deduction]
C
C [constructor, in Tennenbaum.LogicFacts]Cantor [section, in Tennenbaum.CantorPairing]
CantorBound [lemma, in Tennenbaum.CantorPairing]
CantorPairing [library]
CE [lemma, in Tennenbaum.Deduction]
CE1 [constructor, in Tennenbaum.Deduction]
CE2 [constructor, in Tennenbaum.Deduction]
CI [constructor, in Tennenbaum.Deduction]
class [constructor, in Tennenbaum.Deduction]
Closed [section, in Tennenbaum.Tennenbaum]
closed_term_is_num [lemma, in Tennenbaum.Peano]
closed_num [lemma, in Tennenbaum.Tennenbaum]
Closed.axioms [variable, in Tennenbaum.Tennenbaum]
Closed.D [variable, in Tennenbaum.Tennenbaum]
Closed.Hcl [variable, in Tennenbaum.Tennenbaum]
Closed.H0 [variable, in Tennenbaum.Tennenbaum]
Closed.I [variable, in Tennenbaum.Tennenbaum]
Closed.phi [variable, in Tennenbaum.Tennenbaum]
⊨ _ [notation, in Tennenbaum.Tennenbaum]
code [definition, in Tennenbaum.CantorPairing]
code_next [lemma, in Tennenbaum.CantorPairing]
combine_context [lemma, in Tennenbaum.Deduction]
Conj [constructor, in Tennenbaum.Tarski]
containsL [definition, in Tennenbaum.Deduction]
CTT [library]
Ctx [constructor, in Tennenbaum.Deduction]
CT_Q [definition, in Tennenbaum.Tennenbaum]
Currying [lemma, in Tennenbaum.CTT]
C:3 [binder, in Tennenbaum.CTT]
c:50 [binder, in Tennenbaum.Peano]
D
DE [constructor, in Tennenbaum.Deduction]Dec [definition, in Tennenbaum.LogicFacts]
dec [definition, in Tennenbaum.LogicFacts]
Dec [definition, in Tennenbaum.Tennenbaum]
dec [definition, in Tennenbaum.FOL]
decDiv [definition, in Tennenbaum.Tennenbaum]
decode [definition, in Tennenbaum.CantorPairing]
dec_prime [lemma, in Tennenbaum.NumberTheory]
dec_irred_factor [lemma, in Tennenbaum.NumberTheory]
dec_irred [lemma, in Tennenbaum.NumberTheory]
dec_lt_bounded_forall [lemma, in Tennenbaum.LogicFacts]
dec_lt_bounded_exist [lemma, in Tennenbaum.LogicFacts]
dec_lt_bounded_exist' [lemma, in Tennenbaum.LogicFacts]
dec_lt_bounded_sig [lemma, in Tennenbaum.LogicFacts]
dec_neg [lemma, in Tennenbaum.LogicFacts]
dec_imp [lemma, in Tennenbaum.LogicFacts]
dec_disj [lemma, in Tennenbaum.LogicFacts]
dec_conj [lemma, in Tennenbaum.LogicFacts]
dec_transport [lemma, in Tennenbaum.LogicFacts]
dec_Divides [lemma, in Tennenbaum.Tennenbaum]
dec_num_lt [lemma, in Tennenbaum.Tennenbaum]
dec_Divides_temp [lemma, in Tennenbaum.Tennenbaum]
dec_Divides' [lemma, in Tennenbaum.Tennenbaum]
dec_closed_Δ0 [lemma, in Tennenbaum.Tennenbaum]
Dec_nat_equiv [lemma, in Tennenbaum.Tennenbaum]
Dec_equiv [lemma, in Tennenbaum.Tennenbaum]
dec_form [instance, in Tennenbaum.FOL]
dec_form_dep [lemma, in Tennenbaum.FOL]
dec_falsity [instance, in Tennenbaum.FOL]
dec_term [instance, in Tennenbaum.FOL]
dec_vec [instance, in Tennenbaum.FOL]
dec_vec_in [lemma, in Tennenbaum.FOL]
dec_list [instance, in Tennenbaum.Deduction]
Deduction [library]
Defs [section, in Tennenbaum.Tarski]
Delta_bounded_forall [constructor, in Tennenbaum.Tennenbaum]
Delta_bounded_exist [constructor, in Tennenbaum.Tennenbaum]
Delta_id [constructor, in Tennenbaum.Tennenbaum]
Delta_Impl [constructor, in Tennenbaum.Tennenbaum]
Delta_Disj [constructor, in Tennenbaum.Tennenbaum]
Delta_Conj [constructor, in Tennenbaum.Tennenbaum]
Delta_eq [constructor, in Tennenbaum.Tennenbaum]
Delta_fal [constructor, in Tennenbaum.Tennenbaum]
Delta0 [section, in Tennenbaum.Tennenbaum]
DE' [lemma, in Tennenbaum.Deduction]
Disj [constructor, in Tennenbaum.Tarski]
Disjoint_AB [lemma, in Tennenbaum.Tennenbaum]
distributive [lemma, in Tennenbaum.Peano]
Div [definition, in Tennenbaum.NumberTheory]
Divides [definition, in Tennenbaum.Tennenbaum]
Divides_Irred [definition, in Tennenbaum.Tennenbaum]
Divides_num [lemma, in Tennenbaum.Tennenbaum]
Div_lt [lemma, in Tennenbaum.NumberTheory]
DI1 [constructor, in Tennenbaum.Deduction]
DI2 [constructor, in Tennenbaum.Deduction]
DN [lemma, in Tennenbaum.Tennenbaum]
DN_exists [lemma, in Tennenbaum.Tennenbaum]
DN_implication [lemma, in Tennenbaum.Tennenbaum]
DN_forall_stable [lemma, in Tennenbaum.Tennenbaum]
d1:204 [binder, in Tennenbaum.Peano]
d2:206 [binder, in Tennenbaum.Peano]
d:107 [binder, in Tennenbaum.Peano]
d:113 [binder, in Tennenbaum.Peano]
D:121 [binder, in Tennenbaum.Deduction]
d:132 [binder, in Tennenbaum.Peano]
d:133 [binder, in Tennenbaum.Peano]
D:139 [binder, in Tennenbaum.Deduction]
d:162 [binder, in Tennenbaum.Tennenbaum]
d:166 [binder, in Tennenbaum.Peano]
d:169 [binder, in Tennenbaum.Peano]
d:171 [binder, in Tennenbaum.Peano]
d:173 [binder, in Tennenbaum.Peano]
d:188 [binder, in Tennenbaum.Tennenbaum]
d:192 [binder, in Tennenbaum.Peano]
d:198 [binder, in Tennenbaum.Peano]
d:209 [binder, in Tennenbaum.Peano]
D:219 [binder, in Tennenbaum.Peano]
d:22 [binder, in Tennenbaum.Peano]
D:225 [binder, in Tennenbaum.Tennenbaum]
d:23 [binder, in Tennenbaum.Tarski]
d:24 [binder, in Tennenbaum.Tarski]
d:284 [binder, in Tennenbaum.Tennenbaum]
d:287 [binder, in Tennenbaum.Tennenbaum]
d:289 [binder, in Tennenbaum.Tennenbaum]
d:291 [binder, in Tennenbaum.Tennenbaum]
d:293 [binder, in Tennenbaum.Tennenbaum]
d:295 [binder, in Tennenbaum.Tennenbaum]
d:297 [binder, in Tennenbaum.Tennenbaum]
d:301 [binder, in Tennenbaum.Tennenbaum]
D:31 [binder, in Tennenbaum.Tarski]
d:314 [binder, in Tennenbaum.Tennenbaum]
d:325 [binder, in Tennenbaum.Tennenbaum]
d:327 [binder, in Tennenbaum.Tennenbaum]
d:330 [binder, in Tennenbaum.Tennenbaum]
d:332 [binder, in Tennenbaum.Tennenbaum]
d:359 [binder, in Tennenbaum.Tennenbaum]
D:36 [binder, in Tennenbaum.Tarski]
d:374 [binder, in Tennenbaum.Tennenbaum]
D:40 [binder, in Tennenbaum.Tarski]
d:402 [binder, in Tennenbaum.Tennenbaum]
d:404 [binder, in Tennenbaum.Tennenbaum]
d:42 [binder, in Tennenbaum.NumberTheory]
d:43 [binder, in Tennenbaum.Peano]
D:44 [binder, in Tennenbaum.Tarski]
D:48 [binder, in Tennenbaum.Tarski]
d:5 [binder, in Tennenbaum.NumberTheory]
d:59 [binder, in Tennenbaum.Peano]
d:61 [binder, in Tennenbaum.Peano]
d:62 [binder, in Tennenbaum.Peano]
d:64 [binder, in Tennenbaum.Peano]
D:67 [binder, in Tennenbaum.Tennenbaum]
d:69 [binder, in Tennenbaum.Tennenbaum]
D:71 [binder, in Tennenbaum.Tennenbaum]
d:88 [binder, in Tennenbaum.Peano]
d:94 [binder, in Tennenbaum.Peano]
E
Enum [definition, in Tennenbaum.Tennenbaum]Enumerability [section, in Tennenbaum.FOL]
Enumerability [section, in Tennenbaum.Deduction]
Enumerability.enum_quantop' [variable, in Tennenbaum.FOL]
Enumerability.enum_binop' [variable, in Tennenbaum.FOL]
Enumerability.enum_Preds' [variable, in Tennenbaum.FOL]
Enumerability.enum_Funcs' [variable, in Tennenbaum.FOL]
Enumerability.enum_Preds' [variable, in Tennenbaum.Deduction]
Enumerability.enum_Funcs' [variable, in Tennenbaum.Deduction]
Enumerability.eq_dec_Preds [variable, in Tennenbaum.Deduction]
Enumerability.eq_dec_Funcs [variable, in Tennenbaum.Deduction]
Enumerability.list_quantop [variable, in Tennenbaum.FOL]
Enumerability.list_binop [variable, in Tennenbaum.FOL]
Enumerability.list_Preds [variable, in Tennenbaum.FOL]
Enumerability.list_Funcs [variable, in Tennenbaum.FOL]
Enumerability.list_Preds [variable, in Tennenbaum.Deduction]
Enumerability.list_Funcs [variable, in Tennenbaum.Deduction]
enumerable [definition, in Tennenbaum.Tennenbaum]
enumerable_form [lemma, in Tennenbaum.Tennenbaum]
enumerable_Q_prv [lemma, in Tennenbaum.Tennenbaum]
enumT_form [definition, in Tennenbaum.FOL]
enumT_term [lemma, in Tennenbaum.FOL]
enumT_quantop [lemma, in Tennenbaum.Deduction]
enumT_binop [lemma, in Tennenbaum.Deduction]
enum_surj [lemma, in Tennenbaum.Tennenbaum]
enum_form [lemma, in Tennenbaum.FOL]
enum_term [lemma, in Tennenbaum.FOL]
enum_tprv [lemma, in Tennenbaum.Deduction]
enum_containsL [lemma, in Tennenbaum.Deduction]
enum_p [lemma, in Tennenbaum.Deduction]
enum_el [lemma, in Tennenbaum.Deduction]
enum_prv [lemma, in Tennenbaum.Deduction]
enum_form' [instance, in Tennenbaum.Deduction]
enum_term' [instance, in Tennenbaum.Deduction]
enum_quantop [instance, in Tennenbaum.Deduction]
enum_binop [instance, in Tennenbaum.Deduction]
env [definition, in Tennenbaum.Tarski]
EQ [definition, in Tennenbaum.Peano]
EQ [definition, in Tennenbaum.Tennenbaum]
eq [constructor, in Tennenbaum.FOL]
EqDec [section, in Tennenbaum.FOL]
eqdec_quantop [instance, in Tennenbaum.Deduction]
eqdec_binop [instance, in Tennenbaum.Deduction]
EqDec.eq_dec_quantop [variable, in Tennenbaum.FOL]
EqDec.eq_dec_binop [variable, in Tennenbaum.FOL]
EqDec.eq_dec_Preds [variable, in Tennenbaum.FOL]
EqDec.eq_dec_Funcs [variable, in Tennenbaum.FOL]
eqd_bool [definition, in Tennenbaum.CTT]
eq_mult [lemma, in Tennenbaum.Peano]
eq_add [lemma, in Tennenbaum.Peano]
eq_succ [lemma, in Tennenbaum.Peano]
eq_dec [lemma, in Tennenbaum.Peano]
eq_trans [lemma, in Tennenbaum.Peano]
eq_sym [lemma, in Tennenbaum.Peano]
eq_dec_nat [lemma, in Tennenbaum.LogicFacts]
eq_bool_agree [lemma, in Tennenbaum.CTT]
eq_trans [lemma, in Tennenbaum.CTT]
eq_sym [lemma, in Tennenbaum.CTT]
eq_stable [lemma, in Tennenbaum.Tennenbaum]
eq_dep_falsity [lemma, in Tennenbaum.FOL]
Euclid [definition, in Tennenbaum.NumberTheory]
eval [definition, in Tennenbaum.Tarski]
eval_comp [lemma, in Tennenbaum.Tarski]
eval_ext [lemma, in Tennenbaum.Tarski]
eval_num [lemma, in Tennenbaum.Peano]
Ex [constructor, in Tennenbaum.Tarski]
ExE [constructor, in Tennenbaum.Deduction]
ExI [constructor, in Tennenbaum.Deduction]
exist_times [definition, in Tennenbaum.Tarski]
exist_times [definition, in Tennenbaum.Peano]
Exp [constructor, in Tennenbaum.Deduction]
Ex_lt [definition, in Tennenbaum.Tennenbaum]
e:170 [binder, in Tennenbaum.Peano]
e:239 [binder, in Tennenbaum.Tennenbaum]
e:241 [binder, in Tennenbaum.Tennenbaum]
e:243 [binder, in Tennenbaum.Tennenbaum]
e:245 [binder, in Tennenbaum.Tennenbaum]
e:247 [binder, in Tennenbaum.Tennenbaum]
e:251 [binder, in Tennenbaum.Tennenbaum]
e:253 [binder, in Tennenbaum.Tennenbaum]
e:259 [binder, in Tennenbaum.Tennenbaum]
e:261 [binder, in Tennenbaum.Tennenbaum]
e:263 [binder, in Tennenbaum.Tennenbaum]
e:265 [binder, in Tennenbaum.Tennenbaum]
e:267 [binder, in Tennenbaum.Tennenbaum]
e:269 [binder, in Tennenbaum.Tennenbaum]
e:271 [binder, in Tennenbaum.Tennenbaum]
e:285 [binder, in Tennenbaum.Tennenbaum]
e:37 [binder, in Tennenbaum.CTT]
e:375 [binder, in Tennenbaum.Tennenbaum]
e:376 [binder, in Tennenbaum.Tennenbaum]
e:377 [binder, in Tennenbaum.Tennenbaum]
e:378 [binder, in Tennenbaum.Tennenbaum]
e:379 [binder, in Tennenbaum.Tennenbaum]
e:380 [binder, in Tennenbaum.Tennenbaum]
e:381 [binder, in Tennenbaum.Tennenbaum]
e:382 [binder, in Tennenbaum.Tennenbaum]
e:383 [binder, in Tennenbaum.Tennenbaum]
e:391 [binder, in Tennenbaum.Tennenbaum]
e:408 [binder, in Tennenbaum.Tennenbaum]
e:42 [binder, in Tennenbaum.CTT]
F
f [definition, in Tennenbaum.Tennenbaum]Factor [lemma, in Tennenbaum.NumberTheory]
Fac_eq [lemma, in Tennenbaum.NumberTheory]
Fac_unique [lemma, in Tennenbaum.NumberTheory]
fac1 [lemma, in Tennenbaum.NumberTheory]
fac2 [lemma, in Tennenbaum.NumberTheory]
fac3 [lemma, in Tennenbaum.NumberTheory]
faktorial [definition, in Tennenbaum.NumberTheory]
falsity [constructor, in Tennenbaum.FOL]
falsity_on [constructor, in Tennenbaum.FOL]
falsity_off [constructor, in Tennenbaum.FOL]
falsity_flag [inductive, in Tennenbaum.FOL]
Faster1 [lemma, in Tennenbaum.Tennenbaum]
Faster2 [lemma, in Tennenbaum.Tennenbaum]
Faster3 [lemma, in Tennenbaum.Peano]
ff [instance, in Tennenbaum.Tennenbaum]
ff:102 [binder, in Tennenbaum.Tennenbaum]
ff:104 [binder, in Tennenbaum.Tennenbaum]
ff:107 [binder, in Tennenbaum.Tarski]
ff:111 [binder, in Tennenbaum.Deduction]
ff:113 [binder, in Tennenbaum.Tarski]
ff:116 [binder, in Tennenbaum.Deduction]
ff:117 [binder, in Tennenbaum.Tarski]
ff:118 [binder, in Tennenbaum.Deduction]
ff:122 [binder, in Tennenbaum.Tarski]
ff:125 [binder, in Tennenbaum.Tarski]
ff:125 [binder, in Tennenbaum.FOL]
ff:128 [binder, in Tennenbaum.Tarski]
ff:129 [binder, in Tennenbaum.Deduction]
ff:130 [binder, in Tennenbaum.FOL]
ff:131 [binder, in Tennenbaum.Tarski]
ff:134 [binder, in Tennenbaum.FOL]
ff:134 [binder, in Tennenbaum.Deduction]
ff:136 [binder, in Tennenbaum.Tarski]
ff:136 [binder, in Tennenbaum.FOL]
ff:136 [binder, in Tennenbaum.Deduction]
ff:14 [binder, in Tennenbaum.Deduction]
ff:140 [binder, in Tennenbaum.FOL]
ff:143 [binder, in Tennenbaum.FOL]
ff:146 [binder, in Tennenbaum.Deduction]
ff:156 [binder, in Tennenbaum.FOL]
ff:160 [binder, in Tennenbaum.Deduction]
ff:161 [binder, in Tennenbaum.Deduction]
ff:169 [binder, in Tennenbaum.FOL]
ff:172 [binder, in Tennenbaum.FOL]
ff:178 [binder, in Tennenbaum.FOL]
ff:18 [binder, in Tennenbaum.Tarski]
ff:182 [binder, in Tennenbaum.FOL]
ff:187 [binder, in Tennenbaum.FOL]
ff:19 [binder, in Tennenbaum.Deduction]
ff:191 [binder, in Tennenbaum.FOL]
ff:200 [binder, in Tennenbaum.FOL]
ff:209 [binder, in Tennenbaum.FOL]
ff:221 [binder, in Tennenbaum.FOL]
ff:224 [binder, in Tennenbaum.FOL]
ff:23 [binder, in Tennenbaum.Deduction]
ff:271 [binder, in Tennenbaum.FOL]
ff:28 [binder, in Tennenbaum.Tarski]
ff:28 [binder, in Tennenbaum.Deduction]
ff:314 [binder, in Tennenbaum.FOL]
ff:326 [binder, in Tennenbaum.FOL]
ff:327 [binder, in Tennenbaum.FOL]
ff:328 [binder, in Tennenbaum.FOL]
ff:33 [binder, in Tennenbaum.Deduction]
ff:41 [binder, in Tennenbaum.Deduction]
ff:45 [binder, in Tennenbaum.Deduction]
ff:5 [binder, in Tennenbaum.Deduction]
ff:50 [binder, in Tennenbaum.Deduction]
ff:51 [binder, in Tennenbaum.FOL]
ff:53 [binder, in Tennenbaum.Tarski]
ff:53 [binder, in Tennenbaum.FOL]
ff:55 [binder, in Tennenbaum.Deduction]
ff:60 [binder, in Tennenbaum.Deduction]
ff:65 [binder, in Tennenbaum.Deduction]
ff:69 [binder, in Tennenbaum.Tarski]
ff:70 [binder, in Tennenbaum.Deduction]
ff:74 [binder, in Tennenbaum.Tarski]
ff:75 [binder, in Tennenbaum.Tennenbaum]
ff:76 [binder, in Tennenbaum.Deduction]
ff:78 [binder, in Tennenbaum.Tennenbaum]
ff:79 [binder, in Tennenbaum.Tarski]
ff:81 [binder, in Tennenbaum.Tennenbaum]
ff:83 [binder, in Tennenbaum.Tarski]
ff:84 [binder, in Tennenbaum.Tennenbaum]
ff:87 [binder, in Tennenbaum.Tennenbaum]
ff:88 [binder, in Tennenbaum.Tarski]
ff:88 [binder, in Tennenbaum.Deduction]
ff:9 [binder, in Tennenbaum.Deduction]
ff:90 [binder, in Tennenbaum.Tennenbaum]
ff:92 [binder, in Tennenbaum.Tarski]
ff:93 [binder, in Tennenbaum.Tennenbaum]
ff:95 [binder, in Tennenbaum.Tennenbaum]
ff:97 [binder, in Tennenbaum.Tarski]
ff:97 [binder, in Tennenbaum.Tennenbaum]
ff:99 [binder, in Tennenbaum.Tennenbaum]
find_bounded_L [lemma, in Tennenbaum.FOL]
find_bounded [lemma, in Tennenbaum.FOL]
find_bounded_t [lemma, in Tennenbaum.FOL]
find_bounded_step [lemma, in Tennenbaum.FOL]
fixb [section, in Tennenbaum.Tarski]
fix_signature [section, in Tennenbaum.FOL]
FOL [library]
Forall [inductive, in Tennenbaum.FOL]
forall_times [definition, in Tennenbaum.Peano]
Forall_cons [constructor, in Tennenbaum.FOL]
Forall_nil [constructor, in Tennenbaum.FOL]
form [inductive, in Tennenbaum.FOL]
form_ind_falsity_on [lemma, in Tennenbaum.FOL]
fullsatis [definition, in Tennenbaum.Tarski]
full_operators [definition, in Tennenbaum.Tarski]
full_logic_quant [inductive, in Tennenbaum.Tarski]
full_logic_sym [inductive, in Tennenbaum.Tarski]
func [constructor, in Tennenbaum.FOL]
funcomp [definition, in Tennenbaum.FOL]
funcs_signature [record, in Tennenbaum.FOL]
f:1 [binder, in Tennenbaum.NumberTheory]
f:10 [binder, in Tennenbaum.CTT]
f:10 [binder, in Tennenbaum.FOL]
f:12 [binder, in Tennenbaum.CTT]
f:122 [binder, in Tennenbaum.Tennenbaum]
f:13 [binder, in Tennenbaum.CantorPairing]
f:147 [binder, in Tennenbaum.FOL]
f:153 [binder, in Tennenbaum.FOL]
f:166 [binder, in Tennenbaum.FOL]
f:17 [binder, in Tennenbaum.CantorPairing]
f:170 [binder, in Tennenbaum.Tennenbaum]
f:195 [binder, in Tennenbaum.Tennenbaum]
f:21 [binder, in Tennenbaum.FOL]
f:230 [binder, in Tennenbaum.Peano]
f:236 [binder, in Tennenbaum.Peano]
F:293 [binder, in Tennenbaum.FOL]
f:3 [binder, in Tennenbaum.CantorPairing]
f:3 [binder, in Tennenbaum.Peano]
f:30 [binder, in Tennenbaum.Tennenbaum]
f:316 [binder, in Tennenbaum.Peano]
f:321 [binder, in Tennenbaum.Peano]
f:35 [binder, in Tennenbaum.Tennenbaum]
f:368 [binder, in Tennenbaum.Tennenbaum]
f:4 [binder, in Tennenbaum.CTT]
f:4 [binder, in Tennenbaum.Tennenbaum]
f:40 [binder, in Tennenbaum.FOL]
f:48 [binder, in Tennenbaum.Tennenbaum]
f:56 [binder, in Tennenbaum.Tennenbaum]
f:61 [binder, in Tennenbaum.Tennenbaum]
f:7 [binder, in Tennenbaum.CTT]
F:81 [binder, in Tennenbaum.FOL]
f:86 [binder, in Tennenbaum.NumberTheory]
F:86 [binder, in Tennenbaum.FOL]
f:9 [binder, in Tennenbaum.CantorPairing]
f:9 [binder, in Tennenbaum.Tarski]
F:92 [binder, in Tennenbaum.FOL]
G
Gamma:255 [binder, in Tennenbaum.Peano]Gamma:259 [binder, in Tennenbaum.Peano]
grounded [lemma, in Tennenbaum.LogicFacts]
g:14 [binder, in Tennenbaum.CantorPairing]
G:219 [binder, in Tennenbaum.Tennenbaum]
G:230 [binder, in Tennenbaum.Tennenbaum]
g:8 [binder, in Tennenbaum.CantorPairing]
g:9 [binder, in Tennenbaum.FOL]
H
Homomorphism [section, in Tennenbaum.NumberTheory]Homomorphism.m [variable, in Tennenbaum.NumberTheory]
D _ [notation, in Tennenbaum.NumberTheory]
M _ [notation, in Tennenbaum.NumberTheory]
HX:255 [binder, in Tennenbaum.FOL]
H0:81 [binder, in Tennenbaum.Deduction]
H:222 [binder, in Tennenbaum.Deduction]
H:239 [binder, in Tennenbaum.Deduction]
H:243 [binder, in Tennenbaum.Deduction]
h:384 [binder, in Tennenbaum.Tennenbaum]
h:385 [binder, in Tennenbaum.Tennenbaum]
H:56 [binder, in Tennenbaum.FOL]
H:80 [binder, in Tennenbaum.Deduction]
I
IE [constructor, in Tennenbaum.Deduction]iEuclid [lemma, in Tennenbaum.Peano]
iEuclid' [lemma, in Tennenbaum.Peano]
iFac_unique [lemma, in Tennenbaum.Peano]
iFac_unique1 [lemma, in Tennenbaum.Peano]
iffT [definition, in Tennenbaum.LogicFacts]
IH:95 [binder, in Tennenbaum.FOL]
II [constructor, in Tennenbaum.Deduction]
impl [definition, in Tennenbaum.Tarski]
Impl [constructor, in Tennenbaum.Tarski]
impl_sat' [lemma, in Tennenbaum.Tarski]
impl_sat [lemma, in Tennenbaum.Tarski]
imps [lemma, in Tennenbaum.Deduction]
Incl [section, in Tennenbaum.Deduction]
incl_app [lemma, in Tennenbaum.Deduction]
_ ⊏ _ [notation, in Tennenbaum.Deduction]
induction [lemma, in Tennenbaum.Peano]
induction1 [lemma, in Tennenbaum.Peano]
induction2 [lemma, in Tennenbaum.Peano]
Inform [definition, in Tennenbaum.Tennenbaum]
infty_irred [lemma, in Tennenbaum.NumberTheory]
inj [definition, in Tennenbaum.CantorPairing]
inj_decode [lemma, in Tennenbaum.CantorPairing]
inj_next [lemma, in Tennenbaum.CantorPairing]
inj_Irred [lemma, in Tennenbaum.NumberTheory]
inj_pair2_eq_dec' [lemma, in Tennenbaum.FOL]
Insep [definition, in Tennenbaum.Tennenbaum]
Inseparable [lemma, in Tennenbaum.Tennenbaum]
Insep_2 [lemma, in Tennenbaum.Tennenbaum]
Insep_3 [lemma, in Tennenbaum.Tennenbaum]
Insep_1 [lemma, in Tennenbaum.Tennenbaum]
Insep1 [definition, in Tennenbaum.Tennenbaum]
Insep2 [definition, in Tennenbaum.Tennenbaum]
Insep3 [definition, in Tennenbaum.Tennenbaum]
interp [record, in Tennenbaum.Tarski]
interp_nat [definition, in Tennenbaum.Peano]
intu [constructor, in Tennenbaum.Deduction]
inu [definition, in Tennenbaum.Peano]
inu_nat_id [lemma, in Tennenbaum.Peano]
inu_mult_hom [lemma, in Tennenbaum.Peano]
inu_add_hom [lemma, in Tennenbaum.Peano]
inu_inj [lemma, in Tennenbaum.Peano]
inv [definition, in Tennenbaum.CantorPairing]
inversion_Δ0_forall [lemma, in Tennenbaum.Tennenbaum]
inversion_Δ0_bin [lemma, in Tennenbaum.Tennenbaum]
inversion_bounded_bin [lemma, in Tennenbaum.Tennenbaum]
inv_cd [lemma, in Tennenbaum.CantorPairing]
inv_dc [lemma, in Tennenbaum.CantorPairing]
in_hd_tl [lemma, in Tennenbaum.Peano]
in_hd [lemma, in Tennenbaum.Peano]
in_theory [definition, in Tennenbaum.Peano]
Irred [definition, in Tennenbaum.NumberTheory]
irred [definition, in Tennenbaum.NumberTheory]
irred_Irred [lemma, in Tennenbaum.NumberTheory]
irred_integral_domain [lemma, in Tennenbaum.NumberTheory]
irred_Mod_eq [lemma, in Tennenbaum.NumberTheory]
irred_factor [lemma, in Tennenbaum.NumberTheory]
irred_bounded [lemma, in Tennenbaum.NumberTheory]
irred' [definition, in Tennenbaum.NumberTheory]
irred1 [lemma, in Tennenbaum.NumberTheory]
iter [definition, in Tennenbaum.Peano]
iter [definition, in Tennenbaum.FOL]
iter_switch [lemma, in Tennenbaum.Peano]
iter_switch [lemma, in Tennenbaum.FOL]
i_P [projection, in Tennenbaum.Tarski]
i_f [projection, in Tennenbaum.Tarski]
I:122 [binder, in Tennenbaum.Deduction]
I:13 [binder, in Tennenbaum.Tarski]
I:140 [binder, in Tennenbaum.Deduction]
I:220 [binder, in Tennenbaum.Peano]
I:32 [binder, in Tennenbaum.Tarski]
I:37 [binder, in Tennenbaum.Tarski]
I:41 [binder, in Tennenbaum.Tarski]
I:45 [binder, in Tennenbaum.Tarski]
I:49 [binder, in Tennenbaum.Tarski]
I:68 [binder, in Tennenbaum.Tennenbaum]
I:72 [binder, in Tennenbaum.Tennenbaum]
J
join [definition, in Tennenbaum.Peano]K
k:1 [binder, in Tennenbaum.Tennenbaum]k:106 [binder, in Tennenbaum.Tarski]
k:118 [binder, in Tennenbaum.Tennenbaum]
k:184 [binder, in Tennenbaum.Tennenbaum]
k:199 [binder, in Tennenbaum.FOL]
k:205 [binder, in Tennenbaum.FOL]
k:208 [binder, in Tennenbaum.FOL]
k:210 [binder, in Tennenbaum.Peano]
k:212 [binder, in Tennenbaum.FOL]
k:239 [binder, in Tennenbaum.Peano]
k:244 [binder, in Tennenbaum.Peano]
k:245 [binder, in Tennenbaum.Peano]
k:305 [binder, in Tennenbaum.Tennenbaum]
k:307 [binder, in Tennenbaum.Tennenbaum]
k:33 [binder, in Tennenbaum.NumberTheory]
k:36 [binder, in Tennenbaum.NumberTheory]
k:64 [binder, in Tennenbaum.NumberTheory]
L
LEM_bounded_exist [lemma, in Tennenbaum.Tennenbaum]LEM_bounded_exist_sat' [lemma, in Tennenbaum.Tennenbaum]
LEM_bounded_exist_sat [lemma, in Tennenbaum.Tennenbaum]
LEM_binary [lemma, in Tennenbaum.Tennenbaum]
LEM_num_lt [lemma, in Tennenbaum.Tennenbaum]
LEM_Divides [lemma, in Tennenbaum.Tennenbaum]
lessthen_num [lemma, in Tennenbaum.Peano]
le_le_trans [lemma, in Tennenbaum.Peano]
list_prod_in [lemma, in Tennenbaum.FOL]
list_quantop [definition, in Tennenbaum.Deduction]
list_binop [definition, in Tennenbaum.Deduction]
LogicFacts [library]
lt_nat_equiv [lemma, in Tennenbaum.NumberTheory]
lt_rect [lemma, in Tennenbaum.NumberTheory]
lt_le_trans [lemma, in Tennenbaum.Peano]
lt_S [lemma, in Tennenbaum.Peano]
lt_le_equiv1 [lemma, in Tennenbaum.Peano]
lt_neq [lemma, in Tennenbaum.Peano]
lt_SS [lemma, in Tennenbaum.Peano]
lt_dec [lemma, in Tennenbaum.LogicFacts]
lt_equiv [lemma, in Tennenbaum.Tennenbaum]
L_form_cml [lemma, in Tennenbaum.FOL]
L_form [definition, in Tennenbaum.FOL]
L_term_cml [lemma, in Tennenbaum.FOL]
L_term [definition, in Tennenbaum.FOL]
L_tded [definition, in Tennenbaum.Deduction]
L_con [definition, in Tennenbaum.Deduction]
L_ded [definition, in Tennenbaum.Deduction]
L:223 [binder, in Tennenbaum.Deduction]
L:231 [binder, in Tennenbaum.Deduction]
L:236 [binder, in Tennenbaum.Deduction]
L:245 [binder, in Tennenbaum.Deduction]
L:249 [binder, in Tennenbaum.Deduction]
L:257 [binder, in Tennenbaum.Deduction]
L:308 [binder, in Tennenbaum.FOL]
l:68 [binder, in Tennenbaum.FOL]
M
map_tl [lemma, in Tennenbaum.Peano]map_hd [lemma, in Tennenbaum.Peano]
McCarty_ [lemma, in Tennenbaum.Tennenbaum]
McCarty_nat [lemma, in Tennenbaum.Tennenbaum]
McCarty' [lemma, in Tennenbaum.Tennenbaum]
Mod [definition, in Tennenbaum.NumberTheory]
Models [section, in Tennenbaum.Peano]
Models.D [variable, in Tennenbaum.Peano]
Models.I [variable, in Tennenbaum.Peano]
Models.PA_Model.Euclid [section, in Tennenbaum.Peano]
_ i≤ _ [notation, in Tennenbaum.Peano]
Models.PA_Model.Induction.pred [variable, in Tennenbaum.Peano]
Models.PA_Model.Induction.phi [variable, in Tennenbaum.Peano]
_ [[ _ ]] [notation, in Tennenbaum.Peano]
Models.PA_Model.Induction [section, in Tennenbaum.Peano]
Models.PA_Model [section, in Tennenbaum.Peano]
_ ⊏ _ [notation, in Tennenbaum.Peano]
_ ∈ _ [notation, in Tennenbaum.Peano]
_ i⧀ _ [notation, in Tennenbaum.Peano]
⊨ _ [notation, in Tennenbaum.Peano]
ModMod_is_Mod [lemma, in Tennenbaum.NumberTheory]
Mod_mult_hom [lemma, in Tennenbaum.NumberTheory]
Mod_mult_hom_l [lemma, in Tennenbaum.NumberTheory]
Mod_add_hom [lemma, in Tennenbaum.NumberTheory]
Mod_plus_multiple [lemma, in Tennenbaum.NumberTheory]
Mod_id [lemma, in Tennenbaum.NumberTheory]
Mod_le [lemma, in Tennenbaum.NumberTheory]
Mod_divides [lemma, in Tennenbaum.NumberTheory]
Mod_lt [lemma, in Tennenbaum.NumberTheory]
Mod_bound [lemma, in Tennenbaum.NumberTheory]
Mod0_is_0 [lemma, in Tennenbaum.NumberTheory]
mono_inj [lemma, in Tennenbaum.NumberTheory]
MP [definition, in Tennenbaum.Tennenbaum]
Mult [constructor, in Tennenbaum.Peano]
Mult_rec [lemma, in Tennenbaum.Peano]
mult_le_mono [lemma, in Tennenbaum.Peano]
mult_asso [lemma, in Tennenbaum.Peano]
mult_comm [lemma, in Tennenbaum.Peano]
mult_rec_r [lemma, in Tennenbaum.Peano]
mult_zero_r [lemma, in Tennenbaum.Peano]
mult_rec [lemma, in Tennenbaum.Peano]
mult_zero [lemma, in Tennenbaum.Peano]
m:15 [binder, in Tennenbaum.CTT]
m:18 [binder, in Tennenbaum.CTT]
m:193 [binder, in Tennenbaum.Tennenbaum]
m:233 [binder, in Tennenbaum.Deduction]
m:238 [binder, in Tennenbaum.Deduction]
m:279 [binder, in Tennenbaum.Tennenbaum]
m:311 [binder, in Tennenbaum.FOL]
m:313 [binder, in Tennenbaum.FOL]
m:39 [binder, in Tennenbaum.NumberTheory]
m:65 [binder, in Tennenbaum.NumberTheory]
N
ND [section, in Tennenbaum.Peano]ND_def [section, in Tennenbaum.Deduction]
_ ⊢ _ [notation, in Tennenbaum.Deduction]
ND_def [section, in Tennenbaum.Deduction]
ND.p [variable, in Tennenbaum.Peano]
negb [definition, in Tennenbaum.CTT]
neg_lt_bounded_forall [lemma, in Tennenbaum.LogicFacts]
neg_imp [lemma, in Tennenbaum.LogicFacts]
neg_and [lemma, in Tennenbaum.LogicFacts]
neg_equiv_Δ0 [lemma, in Tennenbaum.Tennenbaum]
next [definition, in Tennenbaum.CantorPairing]
NNN_N [lemma, in Tennenbaum.Tennenbaum]
nolessthen_zero [lemma, in Tennenbaum.Peano]
nolessthen_zero [lemma, in Tennenbaum.Tennenbaum]
not_lt_zero_prv [lemma, in Tennenbaum.Peano]
num [definition, in Tennenbaum.Peano]
NumberTheory [library]
num_lt_dec [lemma, in Tennenbaum.Peano]
num_nlt [lemma, in Tennenbaum.Peano]
num_lt [lemma, in Tennenbaum.Peano]
num_eq_dec [lemma, in Tennenbaum.Peano]
num_neq [lemma, in Tennenbaum.Peano]
num_eq [lemma, in Tennenbaum.Peano]
num_lt_prv [lemma, in Tennenbaum.Peano]
num_mult_homomorphism [lemma, in Tennenbaum.Peano]
num_add_homomorphism [lemma, in Tennenbaum.Peano]
num_subst [lemma, in Tennenbaum.Peano]
num_lt_nonStd [lemma, in Tennenbaum.Tennenbaum]
n00_next [lemma, in Tennenbaum.CantorPairing]
n:102 [binder, in Tennenbaum.Tarski]
n:102 [binder, in Tennenbaum.Peano]
n:103 [binder, in Tennenbaum.FOL]
n:104 [binder, in Tennenbaum.Peano]
n:106 [binder, in Tennenbaum.Peano]
n:106 [binder, in Tennenbaum.FOL]
N:108 [binder, in Tennenbaum.Tarski]
n:108 [binder, in Tennenbaum.Peano]
n:108 [binder, in Tennenbaum.Tennenbaum]
n:110 [binder, in Tennenbaum.Peano]
n:112 [binder, in Tennenbaum.Tarski]
n:112 [binder, in Tennenbaum.Peano]
n:114 [binder, in Tennenbaum.Peano]
n:116 [binder, in Tennenbaum.Peano]
n:117 [binder, in Tennenbaum.Tennenbaum]
n:117 [binder, in Tennenbaum.FOL]
N:118 [binder, in Tennenbaum.Tarski]
n:118 [binder, in Tennenbaum.FOL]
n:12 [binder, in Tennenbaum.Peano]
N:120 [binder, in Tennenbaum.Tennenbaum]
n:120 [binder, in Tennenbaum.FOL]
n:121 [binder, in Tennenbaum.Peano]
n:121 [binder, in Tennenbaum.FOL]
N:123 [binder, in Tennenbaum.Tarski]
n:123 [binder, in Tennenbaum.Peano]
n:124 [binder, in Tennenbaum.FOL]
N:126 [binder, in Tennenbaum.Tarski]
N:126 [binder, in Tennenbaum.Tennenbaum]
n:128 [binder, in Tennenbaum.Peano]
N:129 [binder, in Tennenbaum.Tarski]
n:129 [binder, in Tennenbaum.Tennenbaum]
n:129 [binder, in Tennenbaum.FOL]
n:130 [binder, in Tennenbaum.Peano]
N:131 [binder, in Tennenbaum.Tennenbaum]
n:133 [binder, in Tennenbaum.FOL]
N:134 [binder, in Tennenbaum.Tarski]
n:134 [binder, in Tennenbaum.Tennenbaum]
n:135 [binder, in Tennenbaum.Peano]
N:137 [binder, in Tennenbaum.Tarski]
n:137 [binder, in Tennenbaum.Peano]
n:143 [binder, in Tennenbaum.Peano]
n:145 [binder, in Tennenbaum.Peano]
n:148 [binder, in Tennenbaum.FOL]
n:153 [binder, in Tennenbaum.Peano]
n:154 [binder, in Tennenbaum.FOL]
n:155 [binder, in Tennenbaum.Peano]
n:158 [binder, in Tennenbaum.Deduction]
n:159 [binder, in Tennenbaum.Deduction]
n:16 [binder, in Tennenbaum.CTT]
n:160 [binder, in Tennenbaum.Peano]
n:162 [binder, in Tennenbaum.Peano]
n:162 [binder, in Tennenbaum.FOL]
n:167 [binder, in Tennenbaum.Deduction]
n:173 [binder, in Tennenbaum.FOL]
n:175 [binder, in Tennenbaum.Tennenbaum]
n:179 [binder, in Tennenbaum.FOL]
n:180 [binder, in Tennenbaum.Tennenbaum]
n:182 [binder, in Tennenbaum.Tennenbaum]
n:183 [binder, in Tennenbaum.FOL]
n:187 [binder, in Tennenbaum.Tennenbaum]
n:188 [binder, in Tennenbaum.FOL]
n:19 [binder, in Tennenbaum.CTT]
n:190 [binder, in Tennenbaum.FOL]
n:192 [binder, in Tennenbaum.Tennenbaum]
n:192 [binder, in Tennenbaum.FOL]
n:194 [binder, in Tennenbaum.Peano]
n:194 [binder, in Tennenbaum.Tennenbaum]
n:195 [binder, in Tennenbaum.FOL]
n:196 [binder, in Tennenbaum.Peano]
n:197 [binder, in Tennenbaum.Tennenbaum]
n:198 [binder, in Tennenbaum.Tennenbaum]
n:200 [binder, in Tennenbaum.Tennenbaum]
n:201 [binder, in Tennenbaum.Tennenbaum]
n:201 [binder, in Tennenbaum.FOL]
n:204 [binder, in Tennenbaum.Tennenbaum]
n:206 [binder, in Tennenbaum.Tennenbaum]
n:206 [binder, in Tennenbaum.FOL]
n:207 [binder, in Tennenbaum.Tennenbaum]
n:208 [binder, in Tennenbaum.Peano]
n:208 [binder, in Tennenbaum.Tennenbaum]
n:210 [binder, in Tennenbaum.FOL]
n:211 [binder, in Tennenbaum.Tennenbaum]
n:213 [binder, in Tennenbaum.Tennenbaum]
n:213 [binder, in Tennenbaum.FOL]
n:214 [binder, in Tennenbaum.Tennenbaum]
n:215 [binder, in Tennenbaum.Tennenbaum]
n:215 [binder, in Tennenbaum.FOL]
n:218 [binder, in Tennenbaum.Tennenbaum]
n:218 [binder, in Tennenbaum.FOL]
n:220 [binder, in Tennenbaum.Tennenbaum]
n:220 [binder, in Tennenbaum.FOL]
n:221 [binder, in Tennenbaum.Tennenbaum]
n:223 [binder, in Tennenbaum.FOL]
n:224 [binder, in Tennenbaum.Tennenbaum]
n:224 [binder, in Tennenbaum.Deduction]
n:226 [binder, in Tennenbaum.Tennenbaum]
n:226 [binder, in Tennenbaum.FOL]
n:227 [binder, in Tennenbaum.Peano]
n:227 [binder, in Tennenbaum.Tennenbaum]
n:228 [binder, in Tennenbaum.FOL]
n:231 [binder, in Tennenbaum.Peano]
n:231 [binder, in Tennenbaum.Tennenbaum]
n:232 [binder, in Tennenbaum.Tennenbaum]
n:234 [binder, in Tennenbaum.FOL]
n:237 [binder, in Tennenbaum.Peano]
n:241 [binder, in Tennenbaum.FOL]
n:248 [binder, in Tennenbaum.Peano]
n:249 [binder, in Tennenbaum.Tennenbaum]
n:249 [binder, in Tennenbaum.FOL]
n:250 [binder, in Tennenbaum.Deduction]
N:254 [binder, in Tennenbaum.Peano]
n:255 [binder, in Tennenbaum.Tennenbaum]
n:256 [binder, in Tennenbaum.FOL]
N:258 [binder, in Tennenbaum.Peano]
n:26 [binder, in Tennenbaum.CantorPairing]
N:26 [binder, in Tennenbaum.LogicFacts]
n:262 [binder, in Tennenbaum.Peano]
n:282 [binder, in Tennenbaum.Tennenbaum]
n:283 [binder, in Tennenbaum.Tennenbaum]
n:285 [binder, in Tennenbaum.FOL]
n:286 [binder, in Tennenbaum.Tennenbaum]
n:288 [binder, in Tennenbaum.Tennenbaum]
n:290 [binder, in Tennenbaum.Tennenbaum]
n:290 [binder, in Tennenbaum.FOL]
n:292 [binder, in Tennenbaum.Tennenbaum]
n:294 [binder, in Tennenbaum.Tennenbaum]
n:296 [binder, in Tennenbaum.Tennenbaum]
n:30 [binder, in Tennenbaum.Peano]
n:300 [binder, in Tennenbaum.Tennenbaum]
n:302 [binder, in Tennenbaum.Tennenbaum]
n:303 [binder, in Tennenbaum.Tennenbaum]
n:304 [binder, in Tennenbaum.FOL]
n:306 [binder, in Tennenbaum.Peano]
n:309 [binder, in Tennenbaum.FOL]
n:31 [binder, in Tennenbaum.CantorPairing]
N:31 [binder, in Tennenbaum.LogicFacts]
n:311 [binder, in Tennenbaum.Tennenbaum]
n:315 [binder, in Tennenbaum.Peano]
n:315 [binder, in Tennenbaum.FOL]
n:316 [binder, in Tennenbaum.Tennenbaum]
n:319 [binder, in Tennenbaum.Tennenbaum]
n:32 [binder, in Tennenbaum.Tennenbaum]
n:320 [binder, in Tennenbaum.Peano]
n:322 [binder, in Tennenbaum.Tennenbaum]
n:324 [binder, in Tennenbaum.Peano]
n:327 [binder, in Tennenbaum.Peano]
n:330 [binder, in Tennenbaum.Peano]
n:333 [binder, in Tennenbaum.Peano]
n:336 [binder, in Tennenbaum.Peano]
n:339 [binder, in Tennenbaum.Tennenbaum]
n:34 [binder, in Tennenbaum.Peano]
n:341 [binder, in Tennenbaum.Tennenbaum]
n:342 [binder, in Tennenbaum.Tennenbaum]
n:344 [binder, in Tennenbaum.Tennenbaum]
n:346 [binder, in Tennenbaum.Tennenbaum]
n:35 [binder, in Tennenbaum.Peano]
N:35 [binder, in Tennenbaum.LogicFacts]
n:353 [binder, in Tennenbaum.Tennenbaum]
n:355 [binder, in Tennenbaum.Tennenbaum]
n:357 [binder, in Tennenbaum.Tennenbaum]
n:360 [binder, in Tennenbaum.Tennenbaum]
n:361 [binder, in Tennenbaum.Tennenbaum]
n:363 [binder, in Tennenbaum.Tennenbaum]
n:369 [binder, in Tennenbaum.Tennenbaum]
n:37 [binder, in Tennenbaum.Tennenbaum]
n:370 [binder, in Tennenbaum.Tennenbaum]
n:373 [binder, in Tennenbaum.Tennenbaum]
N:38 [binder, in Tennenbaum.NumberTheory]
N:38 [binder, in Tennenbaum.LogicFacts]
n:39 [binder, in Tennenbaum.Peano]
n:392 [binder, in Tennenbaum.Tennenbaum]
n:393 [binder, in Tennenbaum.Tennenbaum]
n:394 [binder, in Tennenbaum.Tennenbaum]
n:395 [binder, in Tennenbaum.Tennenbaum]
n:4 [binder, in Tennenbaum.FOL]
n:40 [binder, in Tennenbaum.CantorPairing]
N:41 [binder, in Tennenbaum.LogicFacts]
n:47 [binder, in Tennenbaum.LogicFacts]
n:50 [binder, in Tennenbaum.LogicFacts]
n:50 [binder, in Tennenbaum.Tennenbaum]
n:51 [binder, in Tennenbaum.LogicFacts]
n:52 [binder, in Tennenbaum.NumberTheory]
n:52 [binder, in Tennenbaum.LogicFacts]
n:54 [binder, in Tennenbaum.NumberTheory]
n:56 [binder, in Tennenbaum.NumberTheory]
N:58 [binder, in Tennenbaum.NumberTheory]
N:60 [binder, in Tennenbaum.NumberTheory]
n:60 [binder, in Tennenbaum.Peano]
n:63 [binder, in Tennenbaum.NumberTheory]
n:63 [binder, in Tennenbaum.Peano]
n:63 [binder, in Tennenbaum.LogicFacts]
n:63 [binder, in Tennenbaum.FOL]
n:66 [binder, in Tennenbaum.LogicFacts]
n:66 [binder, in Tennenbaum.FOL]
n:67 [binder, in Tennenbaum.NumberTheory]
n:68 [binder, in Tennenbaum.Peano]
n:69 [binder, in Tennenbaum.Peano]
n:69 [binder, in Tennenbaum.LogicFacts]
n:70 [binder, in Tennenbaum.Peano]
n:70 [binder, in Tennenbaum.LogicFacts]
n:70 [binder, in Tennenbaum.Tennenbaum]
n:71 [binder, in Tennenbaum.FOL]
n:74 [binder, in Tennenbaum.NumberTheory]
n:74 [binder, in Tennenbaum.FOL]
n:77 [binder, in Tennenbaum.NumberTheory]
n:77 [binder, in Tennenbaum.Peano]
n:77 [binder, in Tennenbaum.FOL]
n:78 [binder, in Tennenbaum.NumberTheory]
n:78 [binder, in Tennenbaum.Peano]
n:80 [binder, in Tennenbaum.Peano]
N:81 [binder, in Tennenbaum.NumberTheory]
n:82 [binder, in Tennenbaum.Peano]
n:83 [binder, in Tennenbaum.NumberTheory]
n:83 [binder, in Tennenbaum.Peano]
n:85 [binder, in Tennenbaum.Peano]
n:87 [binder, in Tennenbaum.Peano]
n:88 [binder, in Tennenbaum.NumberTheory]
n:89 [binder, in Tennenbaum.Peano]
n:9 [binder, in Tennenbaum.Peano]
n:90 [binder, in Tennenbaum.NumberTheory]
n:91 [binder, in Tennenbaum.Peano]
n:93 [binder, in Tennenbaum.Peano]
n:95 [binder, in Tennenbaum.Peano]
n:97 [binder, in Tennenbaum.Peano]
O
obj_Insep [definition, in Tennenbaum.Tennenbaum]on_std_equiv [lemma, in Tennenbaum.Tennenbaum]
operators [record, in Tennenbaum.FOL]
ops:161 [binder, in Tennenbaum.FOL]
ops:259 [binder, in Tennenbaum.FOL]
ops:274 [binder, in Tennenbaum.FOL]
ops:32 [binder, in Tennenbaum.FOL]
ops:331 [binder, in Tennenbaum.FOL]
ops:99 [binder, in Tennenbaum.FOL]
op:321 [binder, in Tennenbaum.FOL]
op:324 [binder, in Tennenbaum.FOL]
Overspill [lemma, in Tennenbaum.Tennenbaum]
Overspill_DN [lemma, in Tennenbaum.Tennenbaum]
Overspill_DN' [lemma, in Tennenbaum.Tennenbaum]
P
PA [inductive, in Tennenbaum.Peano]PAsat [definition, in Tennenbaum.Peano]
pat:23 [binder, in Tennenbaum.CantorPairing]
pat:36 [binder, in Tennenbaum.CantorPairing]
PA_std_axioms [lemma, in Tennenbaum.Peano]
PA_induction [constructor, in Tennenbaum.Peano]
PA_Q [constructor, in Tennenbaum.Peano]
PA_preds_signature [instance, in Tennenbaum.Peano]
PA_funcs_signature [instance, in Tennenbaum.Peano]
PA_preds_ar [definition, in Tennenbaum.Peano]
PA_preds [inductive, in Tennenbaum.Peano]
PA_funcs_ar [definition, in Tennenbaum.Peano]
PA_funcs [inductive, in Tennenbaum.Peano]
PA_consistent [lemma, in Tennenbaum.Tennenbaum]
Pc [constructor, in Tennenbaum.Deduction]
Peano [library]
Peirce [lemma, in Tennenbaum.Deduction]
peirce [inductive, in Tennenbaum.Deduction]
phi1:269 [binder, in Tennenbaum.FOL]
phi2:270 [binder, in Tennenbaum.FOL]
phi:100 [binder, in Tennenbaum.Tarski]
phi:101 [binder, in Tennenbaum.Deduction]
phi:104 [binder, in Tennenbaum.Deduction]
phi:107 [binder, in Tennenbaum.Deduction]
phi:109 [binder, in Tennenbaum.Tarski]
phi:113 [binder, in Tennenbaum.Deduction]
phi:115 [binder, in Tennenbaum.Tennenbaum]
phi:116 [binder, in Tennenbaum.Tarski]
phi:117 [binder, in Tennenbaum.Deduction]
phi:119 [binder, in Tennenbaum.Tarski]
phi:12 [binder, in Tennenbaum.Deduction]
phi:120 [binder, in Tennenbaum.Deduction]
phi:124 [binder, in Tennenbaum.Tarski]
phi:126 [binder, in Tennenbaum.FOL]
phi:127 [binder, in Tennenbaum.Tarski]
phi:13 [binder, in Tennenbaum.Peano]
phi:130 [binder, in Tennenbaum.Tarski]
phi:130 [binder, in Tennenbaum.Tennenbaum]
phi:131 [binder, in Tennenbaum.FOL]
phi:131 [binder, in Tennenbaum.Deduction]
phi:133 [binder, in Tennenbaum.Tarski]
phi:135 [binder, in Tennenbaum.FOL]
phi:135 [binder, in Tennenbaum.Deduction]
phi:137 [binder, in Tennenbaum.FOL]
phi:138 [binder, in Tennenbaum.Deduction]
phi:139 [binder, in Tennenbaum.Tarski]
phi:141 [binder, in Tennenbaum.FOL]
phi:15 [binder, in Tennenbaum.Peano]
phi:158 [binder, in Tennenbaum.FOL]
phi:163 [binder, in Tennenbaum.Deduction]
phi:17 [binder, in Tennenbaum.Deduction]
phi:170 [binder, in Tennenbaum.Deduction]
phi:173 [binder, in Tennenbaum.Deduction]
phi:175 [binder, in Tennenbaum.Deduction]
phi:176 [binder, in Tennenbaum.Deduction]
phi:178 [binder, in Tennenbaum.Deduction]
phi:180 [binder, in Tennenbaum.FOL]
phi:180 [binder, in Tennenbaum.Deduction]
phi:182 [binder, in Tennenbaum.Deduction]
phi:184 [binder, in Tennenbaum.Deduction]
phi:186 [binder, in Tennenbaum.Deduction]
phi:188 [binder, in Tennenbaum.Deduction]
phi:189 [binder, in Tennenbaum.FOL]
phi:19 [binder, in Tennenbaum.Peano]
phi:191 [binder, in Tennenbaum.Deduction]
phi:192 [binder, in Tennenbaum.Deduction]
phi:194 [binder, in Tennenbaum.FOL]
phi:194 [binder, in Tennenbaum.Deduction]
phi:196 [binder, in Tennenbaum.Deduction]
phi:198 [binder, in Tennenbaum.Deduction]
phi:199 [binder, in Tennenbaum.Tennenbaum]
phi:20 [binder, in Tennenbaum.Tarski]
phi:200 [binder, in Tennenbaum.Deduction]
phi:202 [binder, in Tennenbaum.FOL]
phi:202 [binder, in Tennenbaum.Deduction]
phi:204 [binder, in Tennenbaum.Deduction]
phi:206 [binder, in Tennenbaum.Deduction]
phi:208 [binder, in Tennenbaum.Deduction]
phi:210 [binder, in Tennenbaum.Deduction]
phi:211 [binder, in Tennenbaum.FOL]
phi:212 [binder, in Tennenbaum.Deduction]
phi:215 [binder, in Tennenbaum.Deduction]
phi:218 [binder, in Tennenbaum.Deduction]
phi:22 [binder, in Tennenbaum.Deduction]
phi:222 [binder, in Tennenbaum.FOL]
phi:228 [binder, in Tennenbaum.Deduction]
phi:24 [binder, in Tennenbaum.Peano]
phi:246 [binder, in Tennenbaum.Peano]
phi:249 [binder, in Tennenbaum.Peano]
phi:25 [binder, in Tennenbaum.Peano]
phi:252 [binder, in Tennenbaum.Peano]
phi:256 [binder, in Tennenbaum.Peano]
phi:257 [binder, in Tennenbaum.Peano]
phi:26 [binder, in Tennenbaum.Peano]
phi:265 [binder, in Tennenbaum.FOL]
phi:27 [binder, in Tennenbaum.Deduction]
phi:30 [binder, in Tennenbaum.Tarski]
phi:303 [binder, in Tennenbaum.Peano]
phi:32 [binder, in Tennenbaum.Deduction]
phi:323 [binder, in Tennenbaum.FOL]
phi:325 [binder, in Tennenbaum.FOL]
phi:35 [binder, in Tennenbaum.Tarski]
phi:36 [binder, in Tennenbaum.Deduction]
phi:40 [binder, in Tennenbaum.Deduction]
phi:43 [binder, in Tennenbaum.Tarski]
phi:44 [binder, in Tennenbaum.Deduction]
phi:48 [binder, in Tennenbaum.Deduction]
phi:53 [binder, in Tennenbaum.Deduction]
phi:55 [binder, in Tennenbaum.Tarski]
phi:58 [binder, in Tennenbaum.FOL]
phi:58 [binder, in Tennenbaum.Deduction]
phi:63 [binder, in Tennenbaum.Deduction]
phi:68 [binder, in Tennenbaum.Deduction]
phi:72 [binder, in Tennenbaum.Tarski]
phi:73 [binder, in Tennenbaum.Deduction]
phi:77 [binder, in Tennenbaum.Tarski]
phi:78 [binder, in Tennenbaum.Deduction]
phi:82 [binder, in Tennenbaum.Tarski]
phi:83 [binder, in Tennenbaum.Deduction]
phi:86 [binder, in Tennenbaum.Tarski]
Phi:90 [binder, in Tennenbaum.Tarski]
phi:92 [binder, in Tennenbaum.Deduction]
phi:95 [binder, in Tennenbaum.Tarski]
phi:98 [binder, in Tennenbaum.Deduction]
Plus [constructor, in Tennenbaum.Peano]
preds [projection, in Tennenbaum.FOL]
preds_signature [record, in Tennenbaum.FOL]
preThm4 [lemma, in Tennenbaum.Tennenbaum]
preThm4_nat [lemma, in Tennenbaum.Tennenbaum]
preThm4' [lemma, in Tennenbaum.Tennenbaum]
preWitness [lemma, in Tennenbaum.LogicFacts]
prime [definition, in Tennenbaum.NumberTheory]
PrimeDec [section, in Tennenbaum.NumberTheory]
PrimeInf [section, in Tennenbaum.NumberTheory]
_ ! [notation, in Tennenbaum.NumberTheory]
prime_irred_equiv [lemma, in Tennenbaum.NumberTheory]
ProductWO [lemma, in Tennenbaum.LogicFacts]
prv [inductive, in Tennenbaum.Deduction]
psi:101 [binder, in Tennenbaum.Tarski]
psi:102 [binder, in Tennenbaum.Deduction]
psi:114 [binder, in Tennenbaum.Deduction]
psi:115 [binder, in Tennenbaum.Deduction]
psi:124 [binder, in Tennenbaum.Deduction]
psi:13 [binder, in Tennenbaum.Deduction]
psi:132 [binder, in Tennenbaum.Deduction]
psi:133 [binder, in Tennenbaum.Deduction]
psi:14 [binder, in Tennenbaum.Peano]
psi:142 [binder, in Tennenbaum.Deduction]
psi:145 [binder, in Tennenbaum.FOL]
psi:145 [binder, in Tennenbaum.Deduction]
psi:171 [binder, in Tennenbaum.Deduction]
psi:172 [binder, in Tennenbaum.Deduction]
psi:174 [binder, in Tennenbaum.Deduction]
psi:18 [binder, in Tennenbaum.Deduction]
psi:181 [binder, in Tennenbaum.FOL]
psi:185 [binder, in Tennenbaum.Deduction]
psi:187 [binder, in Tennenbaum.Deduction]
psi:193 [binder, in Tennenbaum.Deduction]
psi:195 [binder, in Tennenbaum.Deduction]
psi:197 [binder, in Tennenbaum.Deduction]
psi:199 [binder, in Tennenbaum.Deduction]
psi:201 [binder, in Tennenbaum.Deduction]
psi:203 [binder, in Tennenbaum.Deduction]
psi:205 [binder, in Tennenbaum.Deduction]
psi:207 [binder, in Tennenbaum.Deduction]
psi:209 [binder, in Tennenbaum.Deduction]
psi:211 [binder, in Tennenbaum.Deduction]
psi:214 [binder, in Tennenbaum.Deduction]
psi:217 [binder, in Tennenbaum.Deduction]
psi:222 [binder, in Tennenbaum.Peano]
psi:242 [binder, in Tennenbaum.Deduction]
psi:25 [binder, in Tennenbaum.Tarski]
psi:250 [binder, in Tennenbaum.Peano]
psi:266 [binder, in Tennenbaum.FOL]
psi:322 [binder, in Tennenbaum.FOL]
psi:34 [binder, in Tennenbaum.Tarski]
psi:37 [binder, in Tennenbaum.Deduction]
psi:49 [binder, in Tennenbaum.Deduction]
psi:54 [binder, in Tennenbaum.Deduction]
psi:59 [binder, in Tennenbaum.Deduction]
psi:64 [binder, in Tennenbaum.Deduction]
psi:69 [binder, in Tennenbaum.Deduction]
psi:74 [binder, in Tennenbaum.Deduction]
psi:79 [binder, in Tennenbaum.Deduction]
psi:85 [binder, in Tennenbaum.Deduction]
psi:96 [binder, in Tennenbaum.Tarski]
psi:99 [binder, in Tennenbaum.Deduction]
p:10 [binder, in Tennenbaum.Deduction]
P:11 [binder, in Tennenbaum.Tarski]
p:11 [binder, in Tennenbaum.CTT]
p:12 [binder, in Tennenbaum.Tennenbaum]
P:125 [binder, in Tennenbaum.Deduction]
P:127 [binder, in Tennenbaum.Deduction]
p:13 [binder, in Tennenbaum.CTT]
p:15 [binder, in Tennenbaum.Deduction]
p:164 [binder, in Tennenbaum.Deduction]
p:17 [binder, in Tennenbaum.Tennenbaum]
p:173 [binder, in Tennenbaum.Tennenbaum]
P:174 [binder, in Tennenbaum.FOL]
p:176 [binder, in Tennenbaum.Tennenbaum]
p:20 [binder, in Tennenbaum.Deduction]
p:219 [binder, in Tennenbaum.Deduction]
p:230 [binder, in Tennenbaum.Deduction]
P:232 [binder, in Tennenbaum.FOL]
p:235 [binder, in Tennenbaum.Deduction]
P:236 [binder, in Tennenbaum.FOL]
p:24 [binder, in Tennenbaum.Deduction]
P:244 [binder, in Tennenbaum.FOL]
p:245 [binder, in Tennenbaum.FOL]
p:247 [binder, in Tennenbaum.Deduction]
p:25 [binder, in Tennenbaum.CantorPairing]
p:254 [binder, in Tennenbaum.Deduction]
p:26 [binder, in Tennenbaum.Tennenbaum]
p:27 [binder, in Tennenbaum.LogicFacts]
p:29 [binder, in Tennenbaum.CantorPairing]
p:29 [binder, in Tennenbaum.Tennenbaum]
p:29 [binder, in Tennenbaum.Deduction]
P:3 [binder, in Tennenbaum.LogicFacts]
P:319 [binder, in Tennenbaum.FOL]
p:32 [binder, in Tennenbaum.LogicFacts]
p:34 [binder, in Tennenbaum.Tennenbaum]
p:34 [binder, in Tennenbaum.Deduction]
p:36 [binder, in Tennenbaum.LogicFacts]
P:36 [binder, in Tennenbaum.FOL]
p:37 [binder, in Tennenbaum.CantorPairing]
p:38 [binder, in Tennenbaum.Deduction]
p:39 [binder, in Tennenbaum.LogicFacts]
p:39 [binder, in Tennenbaum.Tennenbaum]
p:396 [binder, in Tennenbaum.Tennenbaum]
p:42 [binder, in Tennenbaum.LogicFacts]
p:42 [binder, in Tennenbaum.Deduction]
p:46 [binder, in Tennenbaum.Deduction]
P:49 [binder, in Tennenbaum.FOL]
p:5 [binder, in Tennenbaum.LogicFacts]
p:51 [binder, in Tennenbaum.NumberTheory]
p:51 [binder, in Tennenbaum.Deduction]
p:52 [binder, in Tennenbaum.Tennenbaum]
p:53 [binder, in Tennenbaum.NumberTheory]
p:53 [binder, in Tennenbaum.Tennenbaum]
p:55 [binder, in Tennenbaum.NumberTheory]
p:55 [binder, in Tennenbaum.Tennenbaum]
p:56 [binder, in Tennenbaum.LogicFacts]
p:56 [binder, in Tennenbaum.Deduction]
p:57 [binder, in Tennenbaum.NumberTheory]
p:6 [binder, in Tennenbaum.Deduction]
p:60 [binder, in Tennenbaum.Tennenbaum]
p:61 [binder, in Tennenbaum.Deduction]
P:62 [binder, in Tennenbaum.FOL]
p:66 [binder, in Tennenbaum.Deduction]
P:7 [binder, in Tennenbaum.Peano]
p:70 [binder, in Tennenbaum.NumberTheory]
p:71 [binder, in Tennenbaum.Deduction]
p:73 [binder, in Tennenbaum.NumberTheory]
p:79 [binder, in Tennenbaum.FOL]
p:8 [binder, in Tennenbaum.LogicFacts]
p:82 [binder, in Tennenbaum.NumberTheory]
p:84 [binder, in Tennenbaum.FOL]
p:89 [binder, in Tennenbaum.Deduction]
p:9 [binder, in Tennenbaum.Tennenbaum]
p:90 [binder, in Tennenbaum.FOL]
Q
Q [definition, in Tennenbaum.Peano]qT [lemma, in Tennenbaum.LogicFacts]
quant [constructor, in Tennenbaum.FOL]
quantop [projection, in Tennenbaum.FOL]
quantop:186 [binder, in Tennenbaum.FOL]
Q_prv.G [variable, in Tennenbaum.Peano]
Q_prv.Gamma [variable, in Tennenbaum.Peano]
Q_prv.p [variable, in Tennenbaum.Peano]
Q_prv [section, in Tennenbaum.Peano]
Q_prv.G [variable, in Tennenbaum.Peano]
Q_prv.Gamma [variable, in Tennenbaum.Peano]
Q_prv.p [variable, in Tennenbaum.Peano]
Q_prv [section, in Tennenbaum.Peano]
Q_std_axioms [lemma, in Tennenbaum.Peano]
Q_Δ0_complete' [lemma, in Tennenbaum.Tennenbaum]
Q_Δ0_complete [lemma, in Tennenbaum.Tennenbaum]
Q_neg_equiv_Δ0 [lemma, in Tennenbaum.Tennenbaum]
Q_dec_closed_Δ0' [lemma, in Tennenbaum.Tennenbaum]
Q_dec_closed_Δ0 [lemma, in Tennenbaum.Tennenbaum]
Q_neg_equiv [lemma, in Tennenbaum.Tennenbaum]
Q_dec [definition, in Tennenbaum.Tennenbaum]
Q_contra [lemma, in Tennenbaum.Tennenbaum]
Q_consistent [lemma, in Tennenbaum.Tennenbaum]
q1:199 [binder, in Tennenbaum.Peano]
q2:201 [binder, in Tennenbaum.Peano]
Q:128 [binder, in Tennenbaum.Deduction]
q:191 [binder, in Tennenbaum.Peano]
q:203 [binder, in Tennenbaum.Peano]
q:42 [binder, in Tennenbaum.FOL]
q:7 [binder, in Tennenbaum.NumberTheory]
q:9 [binder, in Tennenbaum.LogicFacts]
R
reflexivity [lemma, in Tennenbaum.Peano]rho:103 [binder, in Tennenbaum.Peano]
rho:105 [binder, in Tennenbaum.Peano]
rho:109 [binder, in Tennenbaum.Peano]
rho:110 [binder, in Tennenbaum.Tarski]
rho:111 [binder, in Tennenbaum.Peano]
rho:114 [binder, in Tennenbaum.Tarski]
rho:115 [binder, in Tennenbaum.Peano]
rho:117 [binder, in Tennenbaum.Peano]
rho:122 [binder, in Tennenbaum.Peano]
rho:123 [binder, in Tennenbaum.Deduction]
rho:124 [binder, in Tennenbaum.Peano]
rho:129 [binder, in Tennenbaum.Peano]
rho:131 [binder, in Tennenbaum.Peano]
rho:132 [binder, in Tennenbaum.Tarski]
rho:135 [binder, in Tennenbaum.Tarski]
rho:136 [binder, in Tennenbaum.Peano]
rho:138 [binder, in Tennenbaum.Tarski]
rho:138 [binder, in Tennenbaum.Peano]
rho:14 [binder, in Tennenbaum.Tarski]
rho:141 [binder, in Tennenbaum.Deduction]
rho:144 [binder, in Tennenbaum.Peano]
rho:145 [binder, in Tennenbaum.Tennenbaum]
rho:146 [binder, in Tennenbaum.Peano]
rho:154 [binder, in Tennenbaum.Peano]
rho:154 [binder, in Tennenbaum.Tennenbaum]
rho:155 [binder, in Tennenbaum.Tennenbaum]
rho:156 [binder, in Tennenbaum.Peano]
rho:156 [binder, in Tennenbaum.Tennenbaum]
rho:157 [binder, in Tennenbaum.Tennenbaum]
rho:158 [binder, in Tennenbaum.Tennenbaum]
rho:159 [binder, in Tennenbaum.Tennenbaum]
rho:161 [binder, in Tennenbaum.Peano]
rho:163 [binder, in Tennenbaum.Peano]
rho:163 [binder, in Tennenbaum.Tennenbaum]
rho:169 [binder, in Tennenbaum.Tennenbaum]
rho:172 [binder, in Tennenbaum.Peano]
rho:174 [binder, in Tennenbaum.Peano]
rho:186 [binder, in Tennenbaum.Tennenbaum]
rho:19 [binder, in Tennenbaum.Tarski]
rho:195 [binder, in Tennenbaum.Peano]
rho:197 [binder, in Tennenbaum.Peano]
rho:221 [binder, in Tennenbaum.Peano]
rho:223 [binder, in Tennenbaum.Peano]
rho:225 [binder, in Tennenbaum.Peano]
rho:242 [binder, in Tennenbaum.Tennenbaum]
rho:244 [binder, in Tennenbaum.Tennenbaum]
rho:246 [binder, in Tennenbaum.Tennenbaum]
rho:248 [binder, in Tennenbaum.Tennenbaum]
rho:250 [binder, in Tennenbaum.Tennenbaum]
rho:252 [binder, in Tennenbaum.Tennenbaum]
rho:254 [binder, in Tennenbaum.Tennenbaum]
rho:256 [binder, in Tennenbaum.Tennenbaum]
rho:264 [binder, in Tennenbaum.Peano]
rho:266 [binder, in Tennenbaum.Tennenbaum]
rho:268 [binder, in Tennenbaum.Tennenbaum]
rho:270 [binder, in Tennenbaum.Tennenbaum]
rho:272 [binder, in Tennenbaum.Tennenbaum]
rho:28 [binder, in Tennenbaum.Peano]
rho:304 [binder, in Tennenbaum.Peano]
rho:315 [binder, in Tennenbaum.Tennenbaum]
rho:326 [binder, in Tennenbaum.Tennenbaum]
rho:328 [binder, in Tennenbaum.Tennenbaum]
rho:33 [binder, in Tennenbaum.Tarski]
rho:331 [binder, in Tennenbaum.Tennenbaum]
rho:333 [binder, in Tennenbaum.Tennenbaum]
rho:340 [binder, in Tennenbaum.Tennenbaum]
rho:345 [binder, in Tennenbaum.Tennenbaum]
rho:354 [binder, in Tennenbaum.Tennenbaum]
rho:356 [binder, in Tennenbaum.Tennenbaum]
rho:358 [binder, in Tennenbaum.Tennenbaum]
rho:36 [binder, in Tennenbaum.Peano]
rho:362 [binder, in Tennenbaum.Tennenbaum]
rho:364 [binder, in Tennenbaum.Tennenbaum]
rho:38 [binder, in Tennenbaum.Tarski]
rho:38 [binder, in Tennenbaum.Peano]
rho:403 [binder, in Tennenbaum.Tennenbaum]
rho:405 [binder, in Tennenbaum.Tennenbaum]
rho:41 [binder, in Tennenbaum.Peano]
rho:42 [binder, in Tennenbaum.Tarski]
rho:44 [binder, in Tennenbaum.Peano]
rho:46 [binder, in Tennenbaum.Tarski]
rho:47 [binder, in Tennenbaum.Peano]
rho:50 [binder, in Tennenbaum.Tarski]
rho:51 [binder, in Tennenbaum.Peano]
rho:62 [binder, in Tennenbaum.Tarski]
rho:65 [binder, in Tennenbaum.Peano]
rho:66 [binder, in Tennenbaum.Tarski]
rho:70 [binder, in Tennenbaum.Tarski]
rho:75 [binder, in Tennenbaum.Tarski]
rho:79 [binder, in Tennenbaum.Peano]
rho:80 [binder, in Tennenbaum.Tarski]
rho:81 [binder, in Tennenbaum.Peano]
rho:84 [binder, in Tennenbaum.Tarski]
rho:84 [binder, in Tennenbaum.Peano]
rho:86 [binder, in Tennenbaum.Peano]
rho:89 [binder, in Tennenbaum.Tarski]
rho:90 [binder, in Tennenbaum.Peano]
rho:92 [binder, in Tennenbaum.Peano]
rho:94 [binder, in Tennenbaum.Tarski]
rho:96 [binder, in Tennenbaum.Peano]
rho:98 [binder, in Tennenbaum.Peano]
rho:99 [binder, in Tennenbaum.Tarski]
RT_strong [definition, in Tennenbaum.Tennenbaum]
RT_weak [definition, in Tennenbaum.Tennenbaum]
r1:200 [binder, in Tennenbaum.Peano]
r1:205 [binder, in Tennenbaum.Peano]
r2:202 [binder, in Tennenbaum.Peano]
r2:207 [binder, in Tennenbaum.Peano]
r:193 [binder, in Tennenbaum.Peano]
r:304 [binder, in Tennenbaum.Tennenbaum]
r:306 [binder, in Tennenbaum.Tennenbaum]
r:43 [binder, in Tennenbaum.NumberTheory]
r:8 [binder, in Tennenbaum.NumberTheory]
S
sat [definition, in Tennenbaum.Tarski]satis [definition, in Tennenbaum.Tarski]
sat_closed [lemma, in Tennenbaum.Tarski]
sat_single [lemma, in Tennenbaum.Tarski]
sat_subst [lemma, in Tennenbaum.Tarski]
sat_comp [lemma, in Tennenbaum.Tarski]
sat_ext' [lemma, in Tennenbaum.Tarski]
sat_ext [lemma, in Tennenbaum.Tarski]
scons [definition, in Tennenbaum.FOL]
Semidec [definition, in Tennenbaum.Tennenbaum]
Sigma_exists [constructor, in Tennenbaum.Tennenbaum]
Sigma_Delta [constructor, in Tennenbaum.Tennenbaum]
sigma:101 [binder, in Tennenbaum.FOL]
sigma:104 [binder, in Tennenbaum.Tarski]
sigma:105 [binder, in Tennenbaum.FOL]
sigma:109 [binder, in Tennenbaum.FOL]
sigma:111 [binder, in Tennenbaum.Tarski]
sigma:115 [binder, in Tennenbaum.Tarski]
sigma:115 [binder, in Tennenbaum.FOL]
sigma:116 [binder, in Tennenbaum.Tennenbaum]
sigma:119 [binder, in Tennenbaum.FOL]
sigma:122 [binder, in Tennenbaum.FOL]
sigma:127 [binder, in Tennenbaum.FOL]
sigma:128 [binder, in Tennenbaum.Tennenbaum]
sigma:132 [binder, in Tennenbaum.FOL]
sigma:133 [binder, in Tennenbaum.Tennenbaum]
sigma:138 [binder, in Tennenbaum.FOL]
sigma:140 [binder, in Tennenbaum.Tarski]
sigma:157 [binder, in Tennenbaum.FOL]
sigma:197 [binder, in Tennenbaum.FOL]
sigma:203 [binder, in Tennenbaum.FOL]
sigma:241 [binder, in Tennenbaum.Peano]
sigma:243 [binder, in Tennenbaum.Peano]
sigma:247 [binder, in Tennenbaum.Peano]
sigma:251 [binder, in Tennenbaum.Peano]
sigma:253 [binder, in Tennenbaum.Peano]
sigma:260 [binder, in Tennenbaum.Peano]
sigma:302 [binder, in Tennenbaum.Peano]
sigma:33 [binder, in Tennenbaum.Peano]
sigma:335 [binder, in Tennenbaum.Tennenbaum]
sigma:85 [binder, in Tennenbaum.Tarski]
sig_preds_dec:240 [binder, in Tennenbaum.FOL]
sig_funcs_dec:239 [binder, in Tennenbaum.FOL]
size_rect [lemma, in Tennenbaum.CantorPairing]
soundness [lemma, in Tennenbaum.Deduction]
Soundness [section, in Tennenbaum.Deduction]
soundness_class' [lemma, in Tennenbaum.Deduction]
soundness_class [lemma, in Tennenbaum.Deduction]
soundness' [lemma, in Tennenbaum.Deduction]
Soundness.LEM [variable, in Tennenbaum.Deduction]
Stable [definition, in Tennenbaum.Tennenbaum]
stable [definition, in Tennenbaum.Tennenbaum]
stable_lemma [lemma, in Tennenbaum.Tennenbaum]
StandartModel [section, in Tennenbaum.Peano]
std [definition, in Tennenbaum.Tennenbaum]
stdModel [definition, in Tennenbaum.Tennenbaum]
stdModel_equiv [lemma, in Tennenbaum.Tennenbaum]
std_mult' [lemma, in Tennenbaum.Tennenbaum]
std_mult [lemma, in Tennenbaum.Tennenbaum]
std_add [lemma, in Tennenbaum.Tennenbaum]
Subst [section, in Tennenbaum.FOL]
subst_exist_sat2 [lemma, in Tennenbaum.Tarski]
subst_exist_sat [lemma, in Tennenbaum.Tarski]
subst_forall_prv [lemma, in Tennenbaum.Peano]
subst_exist_prv [lemma, in Tennenbaum.Peano]
subst_bounded [lemma, in Tennenbaum.Peano]
subst_bounded_term [lemma, in Tennenbaum.Peano]
subst_up_var [lemma, in Tennenbaum.Peano]
subst_bound [lemma, in Tennenbaum.Tennenbaum]
subst_bound_t [lemma, in Tennenbaum.Tennenbaum]
subst_Δ0 [lemma, in Tennenbaum.Tennenbaum]
subst_shift [lemma, in Tennenbaum.FOL]
subst_comp [lemma, in Tennenbaum.FOL]
subst_var [lemma, in Tennenbaum.FOL]
subst_id [lemma, in Tennenbaum.FOL]
subst_ext [lemma, in Tennenbaum.FOL]
subst_term_shift [lemma, in Tennenbaum.FOL]
subst_term_comp [lemma, in Tennenbaum.FOL]
subst_term_var [lemma, in Tennenbaum.FOL]
subst_term_id [lemma, in Tennenbaum.FOL]
subst_term_ext [lemma, in Tennenbaum.FOL]
subst_form [definition, in Tennenbaum.FOL]
subst_term [definition, in Tennenbaum.FOL]
Succ [constructor, in Tennenbaum.Peano]
Succ_inj [lemma, in Tennenbaum.Peano]
succ_inj' [lemma, in Tennenbaum.Peano]
succ_inj [lemma, in Tennenbaum.Peano]
sum_is_zero [lemma, in Tennenbaum.Peano]
surj [definition, in Tennenbaum.Tennenbaum]
surj_form [definition, in Tennenbaum.Tennenbaum]
switch_exists [lemma, in Tennenbaum.Tarski]
switch_up_num [lemma, in Tennenbaum.Peano]
switch_num [lemma, in Tennenbaum.Peano]
switch_nat_num [lemma, in Tennenbaum.Tennenbaum]
switch_conj_imp [lemma, in Tennenbaum.Deduction]
symmetry [lemma, in Tennenbaum.Peano]
syms [projection, in Tennenbaum.FOL]
s:112 [binder, in Tennenbaum.FOL]
s:142 [binder, in Tennenbaum.FOL]
s:184 [binder, in Tennenbaum.FOL]
s:335 [binder, in Tennenbaum.Peano]
s:343 [binder, in Tennenbaum.Peano]
s:353 [binder, in Tennenbaum.Peano]
s:45 [binder, in Tennenbaum.FOL]
s:80 [binder, in Tennenbaum.Tennenbaum]
T
T [inductive, in Tennenbaum.LogicFacts]Tarski [section, in Tennenbaum.Tarski]
Tarski [section, in Tennenbaum.Tarski]
Tarski [library]
Tarski.D [variable, in Tennenbaum.Tarski]
Tarski.Ext [section, in Tennenbaum.Tarski]
Tarski.I [variable, in Tennenbaum.Tarski]
Tarski.Semantics [section, in Tennenbaum.Tarski]
Tarski.Semantics.domain [variable, in Tennenbaum.Tarski]
Tarski.Substs [section, in Tennenbaum.Tarski]
tau:102 [binder, in Tennenbaum.FOL]
tau:105 [binder, in Tennenbaum.Tarski]
tau:110 [binder, in Tennenbaum.FOL]
tau:116 [binder, in Tennenbaum.FOL]
tau:123 [binder, in Tennenbaum.FOL]
tau:128 [binder, in Tennenbaum.FOL]
tau:139 [binder, in Tennenbaum.FOL]
tau:198 [binder, in Tennenbaum.FOL]
tau:204 [binder, in Tennenbaum.FOL]
Tennebaum_ [lemma, in Tennenbaum.Tennenbaum]
Tennenbaum [lemma, in Tennenbaum.Tennenbaum]
Tennenbaum [section, in Tennenbaum.Tennenbaum]
Tennenbaum [library]
Tennenbaum_strenghened2 [lemma, in Tennenbaum.Tennenbaum]
Tennenbaum_strenghened1 [lemma, in Tennenbaum.Tennenbaum]
Tennenbaum_wo [lemma, in Tennenbaum.Tennenbaum]
Tennenbaum_enum [lemma, in Tennenbaum.Tennenbaum]
Tennenbaum.axioms [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.D [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.dec_eq [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.I [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Insep [section, in Tennenbaum.Tennenbaum]
Tennenbaum.Insep.surj_form_ [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm [section, in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm.Coding [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm.Hψ [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm.ψ [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.McCarty [section, in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill [section, in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.Hα [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.nStd [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.stable_std [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.α [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1 [section, in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1.binary_α [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1.Δ0_α [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1.α [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4 [section, in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hypoth [section, in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hypoth.nonStd [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hypoth.stable_std [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hψ [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.ψ [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill.nnnStd [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill.Hα [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill.α [variable, in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill [section, in Tennenbaum.Tennenbaum]
_ i⧀ _ [notation, in Tennenbaum.Tennenbaum]
N⊨ _ [notation, in Tennenbaum.Tennenbaum]
⊨ _ [notation, in Tennenbaum.Tennenbaum]
term [inductive, in Tennenbaum.FOL]
term_lt_dec [lemma, in Tennenbaum.Peano]
term_eq_dec [lemma, in Tennenbaum.Peano]
term_ind [lemma, in Tennenbaum.FOL]
term_rect [lemma, in Tennenbaum.FOL]
term_rect' [lemma, in Tennenbaum.FOL]
theory [definition, in Tennenbaum.Peano]
theta:213 [binder, in Tennenbaum.Deduction]
theta:216 [binder, in Tennenbaum.Deduction]
theta:75 [binder, in Tennenbaum.Deduction]
Thm4 [lemma, in Tennenbaum.Tennenbaum]
Thm5 [lemma, in Tennenbaum.Tennenbaum]
tprv [definition, in Tennenbaum.Deduction]
transitivity [lemma, in Tennenbaum.Peano]
trichotomy [lemma, in Tennenbaum.Peano]
trunc [lemma, in Tennenbaum.Tennenbaum]
tsoundness [lemma, in Tennenbaum.Deduction]
tsoundness_class [lemma, in Tennenbaum.Deduction]
t:100 [binder, in Tennenbaum.FOL]
T:100 [binder, in Tennenbaum.Deduction]
t:103 [binder, in Tennenbaum.Tarski]
t:104 [binder, in Tennenbaum.FOL]
t:107 [binder, in Tennenbaum.FOL]
t:108 [binder, in Tennenbaum.FOL]
t:111 [binder, in Tennenbaum.FOL]
t:113 [binder, in Tennenbaum.FOL]
T:119 [binder, in Tennenbaum.Deduction]
t:124 [binder, in Tennenbaum.Tennenbaum]
t:125 [binder, in Tennenbaum.Tennenbaum]
T:137 [binder, in Tennenbaum.Deduction]
T:149 [binder, in Tennenbaum.Deduction]
t:15 [binder, in Tennenbaum.Tarski]
t:159 [binder, in Tennenbaum.Peano]
t:168 [binder, in Tennenbaum.FOL]
t:176 [binder, in Tennenbaum.FOL]
t:177 [binder, in Tennenbaum.Deduction]
t:179 [binder, in Tennenbaum.Deduction]
t:181 [binder, in Tennenbaum.Deduction]
t:183 [binder, in Tennenbaum.Peano]
t:183 [binder, in Tennenbaum.Deduction]
t:185 [binder, in Tennenbaum.FOL]
t:186 [binder, in Tennenbaum.Peano]
t:189 [binder, in Tennenbaum.Peano]
t:196 [binder, in Tennenbaum.FOL]
t:207 [binder, in Tennenbaum.FOL]
t:216 [binder, in Tennenbaum.FOL]
t:217 [binder, in Tennenbaum.FOL]
t:219 [binder, in Tennenbaum.FOL]
T:23 [binder, in Tennenbaum.Peano]
t:23 [binder, in Tennenbaum.FOL]
T:241 [binder, in Tennenbaum.Deduction]
t:242 [binder, in Tennenbaum.Peano]
t:242 [binder, in Tennenbaum.FOL]
T:244 [binder, in Tennenbaum.Deduction]
T:256 [binder, in Tennenbaum.Deduction]
t:26 [binder, in Tennenbaum.Deduction]
t:27 [binder, in Tennenbaum.CTT]
t:270 [binder, in Tennenbaum.Peano]
t:29 [binder, in Tennenbaum.CTT]
t:31 [binder, in Tennenbaum.Deduction]
t:344 [binder, in Tennenbaum.Peano]
t:354 [binder, in Tennenbaum.Peano]
t:38 [binder, in Tennenbaum.CTT]
t:43 [binder, in Tennenbaum.CTT]
t:44 [binder, in Tennenbaum.FOL]
t:50 [binder, in Tennenbaum.FOL]
t:64 [binder, in Tennenbaum.Tarski]
t:68 [binder, in Tennenbaum.Tarski]
t:79 [binder, in Tennenbaum.Tennenbaum]
t:80 [binder, in Tennenbaum.FOL]
T:82 [binder, in Tennenbaum.Deduction]
t:85 [binder, in Tennenbaum.FOL]
t:88 [binder, in Tennenbaum.FOL]
t:91 [binder, in Tennenbaum.Tarski]
t:91 [binder, in Tennenbaum.FOL]
t:94 [binder, in Tennenbaum.FOL]
T:97 [binder, in Tennenbaum.Deduction]
U
unary [definition, in Tennenbaum.Tennenbaum]unique [lemma, in Tennenbaum.NumberTheory]
Uniqueness [section, in Tennenbaum.NumberTheory]
Uniqueness.m [variable, in Tennenbaum.NumberTheory]
Unnamed_thm [definition, in Tennenbaum.NumberTheory]
Unnamed_thm [definition, in Tennenbaum.Peano]
up [definition, in Tennenbaum.FOL]
up_decompose [lemma, in Tennenbaum.Peano]
up_decompose [lemma, in Tennenbaum.FOL]
up_form [lemma, in Tennenbaum.FOL]
up_funcomp [lemma, in Tennenbaum.FOL]
up_var [lemma, in Tennenbaum.FOL]
up_ext [lemma, in Tennenbaum.FOL]
up_term [lemma, in Tennenbaum.FOL]
u:321 [binder, in Tennenbaum.Tennenbaum]
V
valid [definition, in Tennenbaum.Tarski]valid_L [definition, in Tennenbaum.Tarski]
valid_ctx [definition, in Tennenbaum.Tarski]
var [constructor, in Tennenbaum.FOL]
vec [definition, in Tennenbaum.FOL]
vecs_from_correct [lemma, in Tennenbaum.FOL]
vecs_from [definition, in Tennenbaum.FOL]
vec_in_hd_tl [lemma, in Tennenbaum.Peano]
vec_in_hd [lemma, in Tennenbaum.Peano]
vec_inv2 [lemma, in Tennenbaum.Peano]
vec_inv1 [lemma, in Tennenbaum.Peano]
vec_nil_eq [lemma, in Tennenbaum.Peano]
vec_map_preimage [lemma, in Tennenbaum.Tennenbaum]
vec_forall_cml [lemma, in Tennenbaum.FOL]
vec_all_dec [lemma, in Tennenbaum.FOL]
vec_cons_inv [lemma, in Tennenbaum.FOL]
vec_inS [constructor, in Tennenbaum.FOL]
vec_inB [constructor, in Tennenbaum.FOL]
vec_in [inductive, in Tennenbaum.FOL]
Void [inductive, in Tennenbaum.CTT]
v':251 [binder, in Tennenbaum.FOL]
v:121 [binder, in Tennenbaum.Tennenbaum]
v:167 [binder, in Tennenbaum.FOL]
v:175 [binder, in Tennenbaum.FOL]
v:214 [binder, in Tennenbaum.FOL]
v:229 [binder, in Tennenbaum.FOL]
v:235 [binder, in Tennenbaum.FOL]
v:250 [binder, in Tennenbaum.FOL]
v:263 [binder, in Tennenbaum.Peano]
v:288 [binder, in Tennenbaum.FOL]
v:294 [binder, in Tennenbaum.FOL]
v:305 [binder, in Tennenbaum.FOL]
v:308 [binder, in Tennenbaum.Peano]
v:310 [binder, in Tennenbaum.Peano]
v:310 [binder, in Tennenbaum.FOL]
v:312 [binder, in Tennenbaum.Peano]
v:317 [binder, in Tennenbaum.Peano]
v:320 [binder, in Tennenbaum.FOL]
v:322 [binder, in Tennenbaum.Peano]
v:325 [binder, in Tennenbaum.Peano]
v:328 [binder, in Tennenbaum.Peano]
v:331 [binder, in Tennenbaum.Peano]
v:334 [binder, in Tennenbaum.Peano]
v:75 [binder, in Tennenbaum.FOL]
v:78 [binder, in Tennenbaum.FOL]
v:82 [binder, in Tennenbaum.FOL]
v:87 [binder, in Tennenbaum.FOL]
v:93 [binder, in Tennenbaum.FOL]
W
Weak [lemma, in Tennenbaum.Deduction]weak_Overspill_DN' [lemma, in Tennenbaum.Tennenbaum]
weak_Overspill [lemma, in Tennenbaum.Tennenbaum]
weak_std_equiv [lemma, in Tennenbaum.Tennenbaum]
Witness [lemma, in Tennenbaum.LogicFacts]
WitnessOperator [section, in Tennenbaum.LogicFacts]
WitnessOperator.Dec_q [variable, in Tennenbaum.LogicFacts]
WitnessOperator.q [variable, in Tennenbaum.LogicFacts]
WO [definition, in Tennenbaum.Tennenbaum]
X
xi:114 [binder, in Tennenbaum.FOL]xi:144 [binder, in Tennenbaum.FOL]
xi:3 [binder, in Tennenbaum.FOL]
xi:63 [binder, in Tennenbaum.Tarski]
xi:67 [binder, in Tennenbaum.Tarski]
xi:71 [binder, in Tennenbaum.Tarski]
xi:76 [binder, in Tennenbaum.Tarski]
xi:81 [binder, in Tennenbaum.Tarski]
x':5 [binder, in Tennenbaum.CantorPairing]
x1:278 [binder, in Tennenbaum.Peano]
x1:282 [binder, in Tennenbaum.Peano]
x2:280 [binder, in Tennenbaum.Peano]
x2:284 [binder, in Tennenbaum.Peano]
X:1 [binder, in Tennenbaum.CantorPairing]
X:1 [binder, in Tennenbaum.LogicFacts]
X:1 [binder, in Tennenbaum.FOL]
x:10 [binder, in Tennenbaum.CantorPairing]
x:10 [binder, in Tennenbaum.NumberTheory]
x:10 [binder, in Tennenbaum.LogicFacts]
x:10 [binder, in Tennenbaum.Tennenbaum]
X:11 [binder, in Tennenbaum.CantorPairing]
x:11 [binder, in Tennenbaum.LogicFacts]
X:11 [binder, in Tennenbaum.Tennenbaum]
x:11 [binder, in Tennenbaum.FOL]
x:118 [binder, in Tennenbaum.Peano]
X:119 [binder, in Tennenbaum.Tennenbaum]
x:12 [binder, in Tennenbaum.NumberTheory]
x:123 [binder, in Tennenbaum.Tennenbaum]
x:125 [binder, in Tennenbaum.Peano]
x:13 [binder, in Tennenbaum.LogicFacts]
x:13 [binder, in Tennenbaum.Tennenbaum]
x:134 [binder, in Tennenbaum.Peano]
X:136 [binder, in Tennenbaum.Tennenbaum]
x:138 [binder, in Tennenbaum.Tennenbaum]
x:139 [binder, in Tennenbaum.Peano]
X:139 [binder, in Tennenbaum.Tennenbaum]
x:14 [binder, in Tennenbaum.NumberTheory]
x:14 [binder, in Tennenbaum.Tennenbaum]
x:141 [binder, in Tennenbaum.Peano]
x:141 [binder, in Tennenbaum.Tennenbaum]
X:146 [binder, in Tennenbaum.FOL]
x:147 [binder, in Tennenbaum.Peano]
x:149 [binder, in Tennenbaum.Peano]
x:149 [binder, in Tennenbaum.FOL]
X:15 [binder, in Tennenbaum.CantorPairing]
x:15 [binder, in Tennenbaum.Tennenbaum]
x:151 [binder, in Tennenbaum.Peano]
X:152 [binder, in Tennenbaum.FOL]
x:155 [binder, in Tennenbaum.FOL]
x:157 [binder, in Tennenbaum.Peano]
x:16 [binder, in Tennenbaum.NumberTheory]
X:16 [binder, in Tennenbaum.Tennenbaum]
x:164 [binder, in Tennenbaum.Peano]
x:165 [binder, in Tennenbaum.FOL]
x:166 [binder, in Tennenbaum.Tennenbaum]
x:167 [binder, in Tennenbaum.Peano]
x:172 [binder, in Tennenbaum.Tennenbaum]
x:175 [binder, in Tennenbaum.Peano]
x:178 [binder, in Tennenbaum.Peano]
x:178 [binder, in Tennenbaum.Tennenbaum]
x:179 [binder, in Tennenbaum.Tennenbaum]
x:18 [binder, in Tennenbaum.CantorPairing]
x:18 [binder, in Tennenbaum.NumberTheory]
x:18 [binder, in Tennenbaum.Tennenbaum]
x:181 [binder, in Tennenbaum.Peano]
x:184 [binder, in Tennenbaum.Peano]
x:187 [binder, in Tennenbaum.Peano]
x:19 [binder, in Tennenbaum.CantorPairing]
x:19 [binder, in Tennenbaum.Tennenbaum]
x:190 [binder, in Tennenbaum.Peano]
x:2 [binder, in Tennenbaum.NumberTheory]
X:2 [binder, in Tennenbaum.Tennenbaum]
x:2 [binder, in Tennenbaum.FOL]
x:20 [binder, in Tennenbaum.NumberTheory]
x:20 [binder, in Tennenbaum.CTT]
x:20 [binder, in Tennenbaum.Tennenbaum]
x:211 [binder, in Tennenbaum.Peano]
x:215 [binder, in Tennenbaum.Peano]
x:217 [binder, in Tennenbaum.Peano]
x:22 [binder, in Tennenbaum.CantorPairing]
X:227 [binder, in Tennenbaum.FOL]
X:229 [binder, in Tennenbaum.Peano]
X:229 [binder, in Tennenbaum.Deduction]
x:230 [binder, in Tennenbaum.FOL]
x:232 [binder, in Tennenbaum.Peano]
x:232 [binder, in Tennenbaum.Deduction]
X:233 [binder, in Tennenbaum.FOL]
X:234 [binder, in Tennenbaum.Deduction]
X:235 [binder, in Tennenbaum.Peano]
x:236 [binder, in Tennenbaum.Tennenbaum]
x:237 [binder, in Tennenbaum.FOL]
x:237 [binder, in Tennenbaum.Deduction]
x:238 [binder, in Tennenbaum.Peano]
x:238 [binder, in Tennenbaum.FOL]
x:24 [binder, in Tennenbaum.CTT]
x:240 [binder, in Tennenbaum.Peano]
x:246 [binder, in Tennenbaum.FOL]
X:248 [binder, in Tennenbaum.FOL]
X:25 [binder, in Tennenbaum.Tennenbaum]
x:252 [binder, in Tennenbaum.FOL]
X:254 [binder, in Tennenbaum.FOL]
x:26 [binder, in Tennenbaum.NumberTheory]
x:26 [binder, in Tennenbaum.CTT]
X:261 [binder, in Tennenbaum.Peano]
x:27 [binder, in Tennenbaum.Tennenbaum]
x:271 [binder, in Tennenbaum.Peano]
x:273 [binder, in Tennenbaum.Peano]
x:273 [binder, in Tennenbaum.Tennenbaum]
x:275 [binder, in Tennenbaum.Tennenbaum]
x:276 [binder, in Tennenbaum.Peano]
x:277 [binder, in Tennenbaum.Tennenbaum]
x:28 [binder, in Tennenbaum.LogicFacts]
x:28 [binder, in Tennenbaum.CTT]
x:28 [binder, in Tennenbaum.Tennenbaum]
x:280 [binder, in Tennenbaum.Tennenbaum]
X:283 [binder, in Tennenbaum.FOL]
x:286 [binder, in Tennenbaum.Peano]
x:287 [binder, in Tennenbaum.Peano]
x:289 [binder, in Tennenbaum.Peano]
x:289 [binder, in Tennenbaum.FOL]
x:29 [binder, in Tennenbaum.LogicFacts]
x:291 [binder, in Tennenbaum.Peano]
x:293 [binder, in Tennenbaum.Peano]
x:295 [binder, in Tennenbaum.Peano]
X:295 [binder, in Tennenbaum.FOL]
x:297 [binder, in Tennenbaum.Peano]
x:297 [binder, in Tennenbaum.FOL]
x:298 [binder, in Tennenbaum.Tennenbaum]
x:3 [binder, in Tennenbaum.NumberTheory]
x:30 [binder, in Tennenbaum.LogicFacts]
X:302 [binder, in Tennenbaum.FOL]
x:306 [binder, in Tennenbaum.FOL]
X:307 [binder, in Tennenbaum.Peano]
X:307 [binder, in Tennenbaum.FOL]
X:309 [binder, in Tennenbaum.Peano]
x:309 [binder, in Tennenbaum.Tennenbaum]
x:31 [binder, in Tennenbaum.NumberTheory]
x:31 [binder, in Tennenbaum.CTT]
x:31 [binder, in Tennenbaum.Tennenbaum]
X:311 [binder, in Tennenbaum.Peano]
x:312 [binder, in Tennenbaum.FOL]
X:313 [binder, in Tennenbaum.Peano]
x:313 [binder, in Tennenbaum.Tennenbaum]
X:318 [binder, in Tennenbaum.Peano]
X:323 [binder, in Tennenbaum.Peano]
X:326 [binder, in Tennenbaum.Peano]
X:329 [binder, in Tennenbaum.Peano]
x:33 [binder, in Tennenbaum.LogicFacts]
X:33 [binder, in Tennenbaum.Tennenbaum]
X:332 [binder, in Tennenbaum.Peano]
x:337 [binder, in Tennenbaum.Peano]
x:337 [binder, in Tennenbaum.Tennenbaum]
x:339 [binder, in Tennenbaum.Peano]
x:34 [binder, in Tennenbaum.LogicFacts]
x:34 [binder, in Tennenbaum.CTT]
x:341 [binder, in Tennenbaum.Peano]
x:345 [binder, in Tennenbaum.Peano]
x:347 [binder, in Tennenbaum.Peano]
x:348 [binder, in Tennenbaum.Tennenbaum]
x:349 [binder, in Tennenbaum.Peano]
x:35 [binder, in Tennenbaum.CantorPairing]
x:35 [binder, in Tennenbaum.NumberTheory]
x:351 [binder, in Tennenbaum.Peano]
x:36 [binder, in Tennenbaum.Tennenbaum]
x:365 [binder, in Tennenbaum.Tennenbaum]
X:367 [binder, in Tennenbaum.Tennenbaum]
x:37 [binder, in Tennenbaum.NumberTheory]
x:37 [binder, in Tennenbaum.LogicFacts]
X:372 [binder, in Tennenbaum.Tennenbaum]
x:38 [binder, in Tennenbaum.CantorPairing]
X:38 [binder, in Tennenbaum.Tennenbaum]
x:387 [binder, in Tennenbaum.Tennenbaum]
x:39 [binder, in Tennenbaum.CTT]
x:398 [binder, in Tennenbaum.Tennenbaum]
x:4 [binder, in Tennenbaum.CantorPairing]
X:4 [binder, in Tennenbaum.LogicFacts]
x:40 [binder, in Tennenbaum.NumberTheory]
x:40 [binder, in Tennenbaum.LogicFacts]
x:40 [binder, in Tennenbaum.Tennenbaum]
x:400 [binder, in Tennenbaum.Tennenbaum]
X:41 [binder, in Tennenbaum.Tennenbaum]
x:411 [binder, in Tennenbaum.Tennenbaum]
x:412 [binder, in Tennenbaum.Tennenbaum]
x:42 [binder, in Tennenbaum.Peano]
x:42 [binder, in Tennenbaum.Tennenbaum]
x:43 [binder, in Tennenbaum.LogicFacts]
x:44 [binder, in Tennenbaum.NumberTheory]
x:44 [binder, in Tennenbaum.LogicFacts]
X:44 [binder, in Tennenbaum.Tennenbaum]
x:45 [binder, in Tennenbaum.CTT]
x:45 [binder, in Tennenbaum.Tennenbaum]
x:46 [binder, in Tennenbaum.NumberTheory]
X:47 [binder, in Tennenbaum.Tennenbaum]
x:48 [binder, in Tennenbaum.NumberTheory]
x:49 [binder, in Tennenbaum.Tennenbaum]
x:50 [binder, in Tennenbaum.NumberTheory]
X:51 [binder, in Tennenbaum.Tennenbaum]
x:53 [binder, in Tennenbaum.LogicFacts]
x:54 [binder, in Tennenbaum.Peano]
x:54 [binder, in Tennenbaum.LogicFacts]
X:54 [binder, in Tennenbaum.Tennenbaum]
x:55 [binder, in Tennenbaum.Peano]
x:55 [binder, in Tennenbaum.LogicFacts]
x:57 [binder, in Tennenbaum.Peano]
x:57 [binder, in Tennenbaum.LogicFacts]
x:57 [binder, in Tennenbaum.Tennenbaum]
x:58 [binder, in Tennenbaum.Tennenbaum]
x:59 [binder, in Tennenbaum.NumberTheory]
x:59 [binder, in Tennenbaum.LogicFacts]
x:59 [binder, in Tennenbaum.Tennenbaum]
X:6 [binder, in Tennenbaum.CantorPairing]
x:6 [binder, in Tennenbaum.NumberTheory]
x:6 [binder, in Tennenbaum.LogicFacts]
x:6 [binder, in Tennenbaum.Tennenbaum]
X:6 [binder, in Tennenbaum.FOL]
x:61 [binder, in Tennenbaum.NumberTheory]
x:61 [binder, in Tennenbaum.LogicFacts]
x:62 [binder, in Tennenbaum.Tennenbaum]
x:63 [binder, in Tennenbaum.Tennenbaum]
x:64 [binder, in Tennenbaum.LogicFacts]
x:64 [binder, in Tennenbaum.Tennenbaum]
x:65 [binder, in Tennenbaum.Tarski]
x:65 [binder, in Tennenbaum.Tennenbaum]
x:66 [binder, in Tennenbaum.NumberTheory]
x:66 [binder, in Tennenbaum.Tennenbaum]
x:67 [binder, in Tennenbaum.LogicFacts]
x:67 [binder, in Tennenbaum.FOL]
X:7 [binder, in Tennenbaum.LogicFacts]
x:71 [binder, in Tennenbaum.Peano]
x:73 [binder, in Tennenbaum.Tarski]
x:73 [binder, in Tennenbaum.Peano]
x:75 [binder, in Tennenbaum.Peano]
x:78 [binder, in Tennenbaum.Tarski]
x:79 [binder, in Tennenbaum.NumberTheory]
X:8 [binder, in Tennenbaum.Tennenbaum]
x:83 [binder, in Tennenbaum.FOL]
x:87 [binder, in Tennenbaum.Tarski]
x:87 [binder, in Tennenbaum.NumberTheory]
x:89 [binder, in Tennenbaum.NumberTheory]
x:89 [binder, in Tennenbaum.FOL]
x:91 [binder, in Tennenbaum.NumberTheory]
x:92 [binder, in Tennenbaum.NumberTheory]
x:96 [binder, in Tennenbaum.FOL]
x:99 [binder, in Tennenbaum.Peano]
Y
y1:279 [binder, in Tennenbaum.Peano]y1:283 [binder, in Tennenbaum.Peano]
y2:281 [binder, in Tennenbaum.Peano]
y2:285 [binder, in Tennenbaum.Peano]
y:100 [binder, in Tennenbaum.Peano]
y:11 [binder, in Tennenbaum.NumberTheory]
y:119 [binder, in Tennenbaum.Peano]
Y:12 [binder, in Tennenbaum.CantorPairing]
y:12 [binder, in Tennenbaum.LogicFacts]
y:126 [binder, in Tennenbaum.Peano]
y:13 [binder, in Tennenbaum.NumberTheory]
y:14 [binder, in Tennenbaum.LogicFacts]
y:140 [binder, in Tennenbaum.Peano]
y:142 [binder, in Tennenbaum.Peano]
y:142 [binder, in Tennenbaum.Tennenbaum]
y:148 [binder, in Tennenbaum.Peano]
y:15 [binder, in Tennenbaum.NumberTheory]
y:150 [binder, in Tennenbaum.Peano]
y:152 [binder, in Tennenbaum.Peano]
y:158 [binder, in Tennenbaum.Peano]
y:165 [binder, in Tennenbaum.Peano]
y:167 [binder, in Tennenbaum.Tennenbaum]
y:168 [binder, in Tennenbaum.Peano]
y:17 [binder, in Tennenbaum.NumberTheory]
y:177 [binder, in Tennenbaum.Peano]
y:180 [binder, in Tennenbaum.Peano]
y:182 [binder, in Tennenbaum.Peano]
y:185 [binder, in Tennenbaum.Peano]
y:188 [binder, in Tennenbaum.Peano]
y:19 [binder, in Tennenbaum.NumberTheory]
Y:2 [binder, in Tennenbaum.CantorPairing]
Y:2 [binder, in Tennenbaum.LogicFacts]
y:20 [binder, in Tennenbaum.CantorPairing]
y:21 [binder, in Tennenbaum.CantorPairing]
y:212 [binder, in Tennenbaum.Peano]
y:216 [binder, in Tennenbaum.Peano]
y:218 [binder, in Tennenbaum.Peano]
y:231 [binder, in Tennenbaum.FOL]
y:247 [binder, in Tennenbaum.FOL]
y:25 [binder, in Tennenbaum.CTT]
y:253 [binder, in Tennenbaum.FOL]
y:272 [binder, in Tennenbaum.Peano]
y:274 [binder, in Tennenbaum.Peano]
y:274 [binder, in Tennenbaum.Tennenbaum]
y:276 [binder, in Tennenbaum.Tennenbaum]
y:277 [binder, in Tennenbaum.Peano]
y:278 [binder, in Tennenbaum.Tennenbaum]
y:281 [binder, in Tennenbaum.Tennenbaum]
y:288 [binder, in Tennenbaum.Peano]
y:290 [binder, in Tennenbaum.Peano]
y:292 [binder, in Tennenbaum.Peano]
y:294 [binder, in Tennenbaum.Peano]
y:296 [binder, in Tennenbaum.Peano]
Y:296 [binder, in Tennenbaum.FOL]
y:298 [binder, in Tennenbaum.Peano]
y:299 [binder, in Tennenbaum.Tennenbaum]
Y:3 [binder, in Tennenbaum.Tennenbaum]
Y:314 [binder, in Tennenbaum.Peano]
Y:319 [binder, in Tennenbaum.Peano]
y:32 [binder, in Tennenbaum.NumberTheory]
y:32 [binder, in Tennenbaum.CTT]
y:338 [binder, in Tennenbaum.Peano]
y:34 [binder, in Tennenbaum.CantorPairing]
y:34 [binder, in Tennenbaum.NumberTheory]
y:340 [binder, in Tennenbaum.Peano]
y:342 [binder, in Tennenbaum.Peano]
y:346 [binder, in Tennenbaum.Peano]
y:35 [binder, in Tennenbaum.CTT]
y:350 [binder, in Tennenbaum.Peano]
y:352 [binder, in Tennenbaum.Peano]
y:366 [binder, in Tennenbaum.Tennenbaum]
y:39 [binder, in Tennenbaum.CantorPairing]
y:4 [binder, in Tennenbaum.NumberTheory]
y:40 [binder, in Tennenbaum.CTT]
y:401 [binder, in Tennenbaum.Tennenbaum]
y:409 [binder, in Tennenbaum.Tennenbaum]
y:410 [binder, in Tennenbaum.Tennenbaum]
y:43 [binder, in Tennenbaum.Tennenbaum]
y:45 [binder, in Tennenbaum.NumberTheory]
y:46 [binder, in Tennenbaum.CTT]
y:46 [binder, in Tennenbaum.Tennenbaum]
y:47 [binder, in Tennenbaum.NumberTheory]
y:49 [binder, in Tennenbaum.NumberTheory]
y:5 [binder, in Tennenbaum.Tennenbaum]
y:56 [binder, in Tennenbaum.Peano]
y:58 [binder, in Tennenbaum.Peano]
y:58 [binder, in Tennenbaum.LogicFacts]
y:60 [binder, in Tennenbaum.LogicFacts]
y:62 [binder, in Tennenbaum.NumberTheory]
y:62 [binder, in Tennenbaum.LogicFacts]
y:65 [binder, in Tennenbaum.LogicFacts]
y:68 [binder, in Tennenbaum.LogicFacts]
Y:7 [binder, in Tennenbaum.CantorPairing]
Y:7 [binder, in Tennenbaum.FOL]
y:72 [binder, in Tennenbaum.Peano]
y:74 [binder, in Tennenbaum.Peano]
y:76 [binder, in Tennenbaum.Peano]
y:80 [binder, in Tennenbaum.NumberTheory]
y:9 [binder, in Tennenbaum.NumberTheory]
Z
Zero [constructor, in Tennenbaum.Peano]zero_or_next [lemma, in Tennenbaum.CantorPairing]
Zero_succ [lemma, in Tennenbaum.Peano]
zero_or_succ [lemma, in Tennenbaum.Peano]
zero_succ [lemma, in Tennenbaum.Peano]
z:101 [binder, in Tennenbaum.Peano]
z:120 [binder, in Tennenbaum.Peano]
z:127 [binder, in Tennenbaum.Peano]
z:176 [binder, in Tennenbaum.Peano]
z:179 [binder, in Tennenbaum.Peano]
z:275 [binder, in Tennenbaum.Peano]
z:33 [binder, in Tennenbaum.CTT]
z:36 [binder, in Tennenbaum.CTT]
z:41 [binder, in Tennenbaum.CTT]
Z:8 [binder, in Tennenbaum.FOL]
other
_ i⊗ _ (PA_Notation) [notation, in Tennenbaum.Peano]_ i⊕ _ (PA_Notation) [notation, in Tennenbaum.Peano]
iσ _ (PA_Notation) [notation, in Tennenbaum.Peano]
i0 (PA_Notation) [notation, in Tennenbaum.Peano]
_ i= _ (PA_Notation) [notation, in Tennenbaum.Peano]
_ ⧀ _ (PA_Notation) [notation, in Tennenbaum.Peano]
_ == _ (PA_Notation) [notation, in Tennenbaum.Peano]
_ ⊗ _ (PA_Notation) [notation, in Tennenbaum.Peano]
_ ⊕ _ (PA_Notation) [notation, in Tennenbaum.Peano]
σ _ (PA_Notation) [notation, in Tennenbaum.Peano]
zero (PA_Notation) [notation, in Tennenbaum.Peano]
↑ (subst_scope) [notation, in Tennenbaum.FOL]
_ .. (subst_scope) [notation, in Tennenbaum.FOL]
_ >> _ (subst_scope) [notation, in Tennenbaum.FOL]
_ .: _ (subst_scope) [notation, in Tennenbaum.FOL]
_ [ _ ] (subst_scope) [notation, in Tennenbaum.FOL]
_ `[ _ ] (subst_scope) [notation, in Tennenbaum.FOL]
$ _ (subst_scope) [notation, in Tennenbaum.FOL]
_ <--> _ (syn) [notation, in Tennenbaum.Tarski]
_ --> _ (syn) [notation, in Tennenbaum.Tarski]
_ ∨ _ (syn) [notation, in Tennenbaum.Tarski]
_ ∧ _ (syn) [notation, in Tennenbaum.Tarski]
¬ _ (syn) [notation, in Tennenbaum.Tarski]
∀ _ (syn) [notation, in Tennenbaum.Tarski]
∃ _ (syn) [notation, in Tennenbaum.Tarski]
⊥ (syn) [notation, in Tennenbaum.Tarski]
_ ==> _ [notation, in Tennenbaum.Tarski]
_ ⊫ _ [notation, in Tennenbaum.Tarski]
_ ⊨ _ [notation, in Tennenbaum.Tarski]
_ ∗ _ [notation, in Tennenbaum.Peano]
_ <=> _ [notation, in Tennenbaum.LogicFacts]
_ ∣ _ [notation, in Tennenbaum.Tennenbaum]
_ <<= _ [notation, in Tennenbaum.Tennenbaum]
_ el _ [notation, in Tennenbaum.Tennenbaum]
_ ⊢TC _ [notation, in Tennenbaum.Deduction]
_ ⊢TI _ [notation, in Tennenbaum.Deduction]
_ ⊢T _ [notation, in Tennenbaum.Deduction]
_ ⊢M _ [notation, in Tennenbaum.Deduction]
_ ⊢I _ [notation, in Tennenbaum.Deduction]
_ ⊢C _ [notation, in Tennenbaum.Deduction]
_ ⊢ _ [notation, in Tennenbaum.Deduction]
_ <<= _ [notation, in Tennenbaum.Deduction]
_ el _ [notation, in Tennenbaum.Deduction]
PA⊨ _ [notation, in Tennenbaum.Peano]
Γ1:93 [binder, in Tennenbaum.Deduction]
Γ2:94 [binder, in Tennenbaum.Deduction]
Δ0 [inductive, in Tennenbaum.Tennenbaum]
Δ0_absolutness' [lemma, in Tennenbaum.Tennenbaum]
Δ0_absolutness [lemma, in Tennenbaum.Tennenbaum]
Δ0_complete' [lemma, in Tennenbaum.Tennenbaum]
Δ0_complete [lemma, in Tennenbaum.Tennenbaum]
Δ0' [inductive, in Tennenbaum.Tennenbaum]
Σ [definition, in Tennenbaum.CantorPairing]
Σ_preds:59 [binder, in Tennenbaum.Tarski]
Σ_funcs:58 [binder, in Tennenbaum.Tarski]
Σ_preds:52 [binder, in Tennenbaum.Tarski]
Σ_funcs:51 [binder, in Tennenbaum.Tarski]
Σ_preds:27 [binder, in Tennenbaum.Tarski]
Σ_funcs:26 [binder, in Tennenbaum.Tarski]
Σ_preds:6 [binder, in Tennenbaum.Tarski]
Σ_funcs:5 [binder, in Tennenbaum.Tarski]
Σ_preds:330 [binder, in Tennenbaum.FOL]
Σ_funcs:329 [binder, in Tennenbaum.FOL]
Σ_preds:273 [binder, in Tennenbaum.FOL]
Σ_funcs:272 [binder, in Tennenbaum.FOL]
Σ_preds:258 [binder, in Tennenbaum.FOL]
Σ_funcs:257 [binder, in Tennenbaum.FOL]
Σ_preds:160 [binder, in Tennenbaum.FOL]
Σ_funcs:159 [binder, in Tennenbaum.FOL]
Σ_preds:98 [binder, in Tennenbaum.FOL]
Σ_funcs:97 [binder, in Tennenbaum.FOL]
Σ_preds:26 [binder, in Tennenbaum.FOL]
Σ_funcs:18 [binder, in Tennenbaum.FOL]
Σ_preds:151 [binder, in Tennenbaum.Deduction]
Σ_funcs:150 [binder, in Tennenbaum.Deduction]
Σ_preds:144 [binder, in Tennenbaum.Deduction]
Σ_funcs:143 [binder, in Tennenbaum.Deduction]
Σ_preds:110 [binder, in Tennenbaum.Deduction]
Σ_funcs:109 [binder, in Tennenbaum.Deduction]
Σ_preds:87 [binder, in Tennenbaum.Deduction]
Σ_funcs:86 [binder, in Tennenbaum.Deduction]
Σ_preds:4 [binder, in Tennenbaum.Deduction]
Σ_funcs:3 [binder, in Tennenbaum.Deduction]
Σ1 [inductive, in Tennenbaum.Tennenbaum]
Σ1_complete [lemma, in Tennenbaum.Tennenbaum]
Σ1_complete' [lemma, in Tennenbaum.Tennenbaum]
α:103 [binder, in Tennenbaum.Tennenbaum]
α:105 [binder, in Tennenbaum.Tennenbaum]
α:106 [binder, in Tennenbaum.Tennenbaum]
α:110 [binder, in Tennenbaum.Tennenbaum]
α:113 [binder, in Tennenbaum.Tennenbaum]
α:135 [binder, in Tennenbaum.Tennenbaum]
α:153 [binder, in Tennenbaum.Tennenbaum]
α:181 [binder, in Tennenbaum.Tennenbaum]
α:183 [binder, in Tennenbaum.Tennenbaum]
α:185 [binder, in Tennenbaum.Tennenbaum]
α:209 [binder, in Tennenbaum.Tennenbaum]
α:216 [binder, in Tennenbaum.Tennenbaum]
α:228 [binder, in Tennenbaum.Tennenbaum]
α:29 [binder, in Tennenbaum.Peano]
α:338 [binder, in Tennenbaum.Tennenbaum]
α:343 [binder, in Tennenbaum.Tennenbaum]
α:350 [binder, in Tennenbaum.Tennenbaum]
α:40 [binder, in Tennenbaum.Peano]
α:73 [binder, in Tennenbaum.Tennenbaum]
α:74 [binder, in Tennenbaum.Tennenbaum]
α:82 [binder, in Tennenbaum.Tennenbaum]
α:85 [binder, in Tennenbaum.Tennenbaum]
α:88 [binder, in Tennenbaum.Tennenbaum]
α:94 [binder, in Tennenbaum.Tennenbaum]
α:96 [binder, in Tennenbaum.Tennenbaum]
α:98 [binder, in Tennenbaum.Tennenbaum]
β:107 [binder, in Tennenbaum.Tennenbaum]
β:111 [binder, in Tennenbaum.Tennenbaum]
β:210 [binder, in Tennenbaum.Tennenbaum]
β:217 [binder, in Tennenbaum.Tennenbaum]
β:229 [binder, in Tennenbaum.Tennenbaum]
β:83 [binder, in Tennenbaum.Tennenbaum]
β:86 [binder, in Tennenbaum.Tennenbaum]
β:89 [binder, in Tennenbaum.Tennenbaum]
ρ:240 [binder, in Tennenbaum.Tennenbaum]
ρ:264 [binder, in Tennenbaum.Tennenbaum]
σ:16 [binder, in Tennenbaum.CantorPairing]
σ:22 [binder, in Tennenbaum.FOL]
σ:55 [binder, in Tennenbaum.FOL]
σ:57 [binder, in Tennenbaum.FOL]
φ:41 [binder, in Tennenbaum.FOL]
φ:43 [binder, in Tennenbaum.FOL]
φ:47 [binder, in Tennenbaum.FOL]
ψ_equiv [lemma, in Tennenbaum.Tennenbaum]
ψ_repr [lemma, in Tennenbaum.Tennenbaum]
ψ:171 [binder, in Tennenbaum.Tennenbaum]
ψ:48 [binder, in Tennenbaum.FOL]
ϕ:114 [binder, in Tennenbaum.Tennenbaum]
ϕ:143 [binder, in Tennenbaum.Tennenbaum]
ϕ:144 [binder, in Tennenbaum.Tennenbaum]
ϕ:174 [binder, in Tennenbaum.Tennenbaum]
ϕ:177 [binder, in Tennenbaum.Tennenbaum]
ϕ:205 [binder, in Tennenbaum.Tennenbaum]
ϕ:212 [binder, in Tennenbaum.Tennenbaum]
ϕ:238 [binder, in Tennenbaum.Tennenbaum]
ϕ:262 [binder, in Tennenbaum.Tennenbaum]
ϕ:323 [binder, in Tennenbaum.Tennenbaum]
ϕ:324 [binder, in Tennenbaum.Tennenbaum]
ϕ:329 [binder, in Tennenbaum.Tennenbaum]
ϕ:334 [binder, in Tennenbaum.Tennenbaum]
ϕ:399 [binder, in Tennenbaum.Tennenbaum]
Notation Index
C
⊨ _ [in Tennenbaum.Tennenbaum]H
D _ [in Tennenbaum.NumberTheory]M _ [in Tennenbaum.NumberTheory]
I
_ ⊏ _ [in Tennenbaum.Deduction]M
_ i≤ _ [in Tennenbaum.Peano]_ [[ _ ]] [in Tennenbaum.Peano]
_ ⊏ _ [in Tennenbaum.Peano]
_ ∈ _ [in Tennenbaum.Peano]
_ i⧀ _ [in Tennenbaum.Peano]
⊨ _ [in Tennenbaum.Peano]
N
_ ⊢ _ [in Tennenbaum.Deduction]P
_ ! [in Tennenbaum.NumberTheory]T
_ i⧀ _ [in Tennenbaum.Tennenbaum]N⊨ _ [in Tennenbaum.Tennenbaum]
⊨ _ [in Tennenbaum.Tennenbaum]
other
_ i⊗ _ (PA_Notation) [in Tennenbaum.Peano]_ i⊕ _ (PA_Notation) [in Tennenbaum.Peano]
iσ _ (PA_Notation) [in Tennenbaum.Peano]
i0 (PA_Notation) [in Tennenbaum.Peano]
_ i= _ (PA_Notation) [in Tennenbaum.Peano]
_ ⧀ _ (PA_Notation) [in Tennenbaum.Peano]
_ == _ (PA_Notation) [in Tennenbaum.Peano]
_ ⊗ _ (PA_Notation) [in Tennenbaum.Peano]
_ ⊕ _ (PA_Notation) [in Tennenbaum.Peano]
σ _ (PA_Notation) [in Tennenbaum.Peano]
zero (PA_Notation) [in Tennenbaum.Peano]
↑ (subst_scope) [in Tennenbaum.FOL]
_ .. (subst_scope) [in Tennenbaum.FOL]
_ >> _ (subst_scope) [in Tennenbaum.FOL]
_ .: _ (subst_scope) [in Tennenbaum.FOL]
_ [ _ ] (subst_scope) [in Tennenbaum.FOL]
_ `[ _ ] (subst_scope) [in Tennenbaum.FOL]
$ _ (subst_scope) [in Tennenbaum.FOL]
_ <--> _ (syn) [in Tennenbaum.Tarski]
_ --> _ (syn) [in Tennenbaum.Tarski]
_ ∨ _ (syn) [in Tennenbaum.Tarski]
_ ∧ _ (syn) [in Tennenbaum.Tarski]
¬ _ (syn) [in Tennenbaum.Tarski]
∀ _ (syn) [in Tennenbaum.Tarski]
∃ _ (syn) [in Tennenbaum.Tarski]
⊥ (syn) [in Tennenbaum.Tarski]
_ ==> _ [in Tennenbaum.Tarski]
_ ⊫ _ [in Tennenbaum.Tarski]
_ ⊨ _ [in Tennenbaum.Tarski]
_ ∗ _ [in Tennenbaum.Peano]
_ <=> _ [in Tennenbaum.LogicFacts]
_ ∣ _ [in Tennenbaum.Tennenbaum]
_ <<= _ [in Tennenbaum.Tennenbaum]
_ el _ [in Tennenbaum.Tennenbaum]
_ ⊢TC _ [in Tennenbaum.Deduction]
_ ⊢TI _ [in Tennenbaum.Deduction]
_ ⊢T _ [in Tennenbaum.Deduction]
_ ⊢M _ [in Tennenbaum.Deduction]
_ ⊢I _ [in Tennenbaum.Deduction]
_ ⊢C _ [in Tennenbaum.Deduction]
_ ⊢ _ [in Tennenbaum.Deduction]
_ <<= _ [in Tennenbaum.Deduction]
_ el _ [in Tennenbaum.Deduction]
PA⊨ _ [in Tennenbaum.Peano]
Binder Index
A
alpha:105 [in Tennenbaum.Deduction]alpha:37 [in Tennenbaum.Peano]
alpha:389 [in Tennenbaum.Tennenbaum]
alpha:95 [in Tennenbaum.Deduction]
axioms:53 [in Tennenbaum.Peano]
ax:151 [in Tennenbaum.Tennenbaum]
ax:164 [in Tennenbaum.Tennenbaum]
ax:18 [in Tennenbaum.Peano]
ax:224 [in Tennenbaum.Peano]
ax:226 [in Tennenbaum.Peano]
ax:52 [in Tennenbaum.Peano]
a':76 [in Tennenbaum.FOL]
a1:22 [in Tennenbaum.NumberTheory]
a2:24 [in Tennenbaum.NumberTheory]
A:1 [in Tennenbaum.CTT]
A:103 [in Tennenbaum.Deduction]
A:108 [in Tennenbaum.Deduction]
A:11 [in Tennenbaum.Deduction]
A:112 [in Tennenbaum.Deduction]
A:130 [in Tennenbaum.Deduction]
A:137 [in Tennenbaum.Tennenbaum]
A:14 [in Tennenbaum.CTT]
A:140 [in Tennenbaum.Tennenbaum]
A:147 [in Tennenbaum.Deduction]
A:15 [in Tennenbaum.LogicFacts]
A:16 [in Tennenbaum.Deduction]
A:162 [in Tennenbaum.Deduction]
A:166 [in Tennenbaum.Deduction]
A:17 [in Tennenbaum.LogicFacts]
A:17 [in Tennenbaum.CTT]
A:19 [in Tennenbaum.LogicFacts]
A:190 [in Tennenbaum.Deduction]
A:193 [in Tennenbaum.FOL]
A:202 [in Tennenbaum.Tennenbaum]
A:21 [in Tennenbaum.LogicFacts]
A:21 [in Tennenbaum.Tennenbaum]
A:21 [in Tennenbaum.Deduction]
a:213 [in Tennenbaum.Peano]
A:22 [in Tennenbaum.LogicFacts]
A:22 [in Tennenbaum.Tennenbaum]
A:221 [in Tennenbaum.Deduction]
A:222 [in Tennenbaum.Tennenbaum]
A:225 [in Tennenbaum.FOL]
A:227 [in Tennenbaum.Deduction]
A:23 [in Tennenbaum.CTT]
A:24 [in Tennenbaum.LogicFacts]
A:24 [in Tennenbaum.Tennenbaum]
A:240 [in Tennenbaum.Deduction]
A:243 [in Tennenbaum.FOL]
A:246 [in Tennenbaum.Deduction]
A:25 [in Tennenbaum.Deduction]
A:253 [in Tennenbaum.Deduction]
a:27 [in Tennenbaum.NumberTheory]
A:27 [in Tennenbaum.Peano]
A:284 [in Tennenbaum.FOL]
A:29 [in Tennenbaum.Tarski]
a:29 [in Tennenbaum.NumberTheory]
A:298 [in Tennenbaum.FOL]
a:30 [in Tennenbaum.CantorPairing]
A:30 [in Tennenbaum.CTT]
A:30 [in Tennenbaum.Deduction]
a:300 [in Tennenbaum.FOL]
A:303 [in Tennenbaum.FOL]
A:305 [in Tennenbaum.Peano]
a:312 [in Tennenbaum.Tennenbaum]
a:317 [in Tennenbaum.Tennenbaum]
A:318 [in Tennenbaum.Tennenbaum]
a:320 [in Tennenbaum.Tennenbaum]
A:348 [in Tennenbaum.Peano]
A:35 [in Tennenbaum.Deduction]
a:352 [in Tennenbaum.Tennenbaum]
A:371 [in Tennenbaum.Tennenbaum]
A:39 [in Tennenbaum.Tarski]
A:39 [in Tennenbaum.Deduction]
A:406 [in Tennenbaum.Tennenbaum]
A:43 [in Tennenbaum.Deduction]
a:45 [in Tennenbaum.Peano]
A:47 [in Tennenbaum.Tarski]
A:47 [in Tennenbaum.Deduction]
a:48 [in Tennenbaum.Peano]
a:5 [in Tennenbaum.CTT]
A:52 [in Tennenbaum.Deduction]
A:54 [in Tennenbaum.Tarski]
A:57 [in Tennenbaum.Deduction]
A:61 [in Tennenbaum.FOL]
A:62 [in Tennenbaum.Deduction]
A:67 [in Tennenbaum.Deduction]
a:68 [in Tennenbaum.NumberTheory]
A:69 [in Tennenbaum.FOL]
A:7 [in Tennenbaum.Tennenbaum]
a:70 [in Tennenbaum.FOL]
a:71 [in Tennenbaum.NumberTheory]
A:72 [in Tennenbaum.Deduction]
A:77 [in Tennenbaum.Deduction]
a:8 [in Tennenbaum.CTT]
A:84 [in Tennenbaum.Deduction]
A:90 [in Tennenbaum.Deduction]
A:93 [in Tennenbaum.Tarski]
A:98 [in Tennenbaum.Tarski]
B
beta:106 [in Tennenbaum.Deduction]beta:96 [in Tennenbaum.Deduction]
binop:177 [in Tennenbaum.FOL]
b1:23 [in Tennenbaum.NumberTheory]
b1:267 [in Tennenbaum.FOL]
b2:25 [in Tennenbaum.NumberTheory]
b2:268 [in Tennenbaum.FOL]
b:109 [in Tennenbaum.Tennenbaum]
b:112 [in Tennenbaum.Tennenbaum]
B:127 [in Tennenbaum.Tennenbaum]
B:132 [in Tennenbaum.Tennenbaum]
B:148 [in Tennenbaum.Deduction]
B:16 [in Tennenbaum.LogicFacts]
b:165 [in Tennenbaum.Deduction]
B:18 [in Tennenbaum.LogicFacts]
B:2 [in Tennenbaum.CTT]
B:20 [in Tennenbaum.LogicFacts]
B:203 [in Tennenbaum.Tennenbaum]
b:214 [in Tennenbaum.Peano]
b:220 [in Tennenbaum.Deduction]
B:223 [in Tennenbaum.Tennenbaum]
B:23 [in Tennenbaum.LogicFacts]
B:23 [in Tennenbaum.Tennenbaum]
b:248 [in Tennenbaum.Deduction]
B:25 [in Tennenbaum.LogicFacts]
b:255 [in Tennenbaum.Deduction]
b:264 [in Tennenbaum.FOL]
b:28 [in Tennenbaum.NumberTheory]
B:299 [in Tennenbaum.FOL]
b:30 [in Tennenbaum.NumberTheory]
b:301 [in Tennenbaum.FOL]
b:336 [in Tennenbaum.Tennenbaum]
b:35 [in Tennenbaum.FOL]
b:351 [in Tennenbaum.Tennenbaum]
b:37 [in Tennenbaum.FOL]
b:38 [in Tennenbaum.FOL]
b:39 [in Tennenbaum.FOL]
b:397 [in Tennenbaum.Tennenbaum]
B:407 [in Tennenbaum.Tennenbaum]
b:44 [in Tennenbaum.CTT]
b:46 [in Tennenbaum.Peano]
b:46 [in Tennenbaum.FOL]
b:49 [in Tennenbaum.Peano]
b:6 [in Tennenbaum.CTT]
b:69 [in Tennenbaum.NumberTheory]
b:72 [in Tennenbaum.NumberTheory]
b:9 [in Tennenbaum.CTT]
B:91 [in Tennenbaum.Deduction]
C
C:3 [in Tennenbaum.CTT]c:50 [in Tennenbaum.Peano]
D
d1:204 [in Tennenbaum.Peano]d2:206 [in Tennenbaum.Peano]
d:107 [in Tennenbaum.Peano]
d:113 [in Tennenbaum.Peano]
D:121 [in Tennenbaum.Deduction]
d:132 [in Tennenbaum.Peano]
d:133 [in Tennenbaum.Peano]
D:139 [in Tennenbaum.Deduction]
d:162 [in Tennenbaum.Tennenbaum]
d:166 [in Tennenbaum.Peano]
d:169 [in Tennenbaum.Peano]
d:171 [in Tennenbaum.Peano]
d:173 [in Tennenbaum.Peano]
d:188 [in Tennenbaum.Tennenbaum]
d:192 [in Tennenbaum.Peano]
d:198 [in Tennenbaum.Peano]
d:209 [in Tennenbaum.Peano]
D:219 [in Tennenbaum.Peano]
d:22 [in Tennenbaum.Peano]
D:225 [in Tennenbaum.Tennenbaum]
d:23 [in Tennenbaum.Tarski]
d:24 [in Tennenbaum.Tarski]
d:284 [in Tennenbaum.Tennenbaum]
d:287 [in Tennenbaum.Tennenbaum]
d:289 [in Tennenbaum.Tennenbaum]
d:291 [in Tennenbaum.Tennenbaum]
d:293 [in Tennenbaum.Tennenbaum]
d:295 [in Tennenbaum.Tennenbaum]
d:297 [in Tennenbaum.Tennenbaum]
d:301 [in Tennenbaum.Tennenbaum]
D:31 [in Tennenbaum.Tarski]
d:314 [in Tennenbaum.Tennenbaum]
d:325 [in Tennenbaum.Tennenbaum]
d:327 [in Tennenbaum.Tennenbaum]
d:330 [in Tennenbaum.Tennenbaum]
d:332 [in Tennenbaum.Tennenbaum]
d:359 [in Tennenbaum.Tennenbaum]
D:36 [in Tennenbaum.Tarski]
d:374 [in Tennenbaum.Tennenbaum]
D:40 [in Tennenbaum.Tarski]
d:402 [in Tennenbaum.Tennenbaum]
d:404 [in Tennenbaum.Tennenbaum]
d:42 [in Tennenbaum.NumberTheory]
d:43 [in Tennenbaum.Peano]
D:44 [in Tennenbaum.Tarski]
D:48 [in Tennenbaum.Tarski]
d:5 [in Tennenbaum.NumberTheory]
d:59 [in Tennenbaum.Peano]
d:61 [in Tennenbaum.Peano]
d:62 [in Tennenbaum.Peano]
d:64 [in Tennenbaum.Peano]
D:67 [in Tennenbaum.Tennenbaum]
d:69 [in Tennenbaum.Tennenbaum]
D:71 [in Tennenbaum.Tennenbaum]
d:88 [in Tennenbaum.Peano]
d:94 [in Tennenbaum.Peano]
E
e:170 [in Tennenbaum.Peano]e:239 [in Tennenbaum.Tennenbaum]
e:241 [in Tennenbaum.Tennenbaum]
e:243 [in Tennenbaum.Tennenbaum]
e:245 [in Tennenbaum.Tennenbaum]
e:247 [in Tennenbaum.Tennenbaum]
e:251 [in Tennenbaum.Tennenbaum]
e:253 [in Tennenbaum.Tennenbaum]
e:259 [in Tennenbaum.Tennenbaum]
e:261 [in Tennenbaum.Tennenbaum]
e:263 [in Tennenbaum.Tennenbaum]
e:265 [in Tennenbaum.Tennenbaum]
e:267 [in Tennenbaum.Tennenbaum]
e:269 [in Tennenbaum.Tennenbaum]
e:271 [in Tennenbaum.Tennenbaum]
e:285 [in Tennenbaum.Tennenbaum]
e:37 [in Tennenbaum.CTT]
e:375 [in Tennenbaum.Tennenbaum]
e:376 [in Tennenbaum.Tennenbaum]
e:377 [in Tennenbaum.Tennenbaum]
e:378 [in Tennenbaum.Tennenbaum]
e:379 [in Tennenbaum.Tennenbaum]
e:380 [in Tennenbaum.Tennenbaum]
e:381 [in Tennenbaum.Tennenbaum]
e:382 [in Tennenbaum.Tennenbaum]
e:383 [in Tennenbaum.Tennenbaum]
e:391 [in Tennenbaum.Tennenbaum]
e:408 [in Tennenbaum.Tennenbaum]
e:42 [in Tennenbaum.CTT]
F
ff:102 [in Tennenbaum.Tennenbaum]ff:104 [in Tennenbaum.Tennenbaum]
ff:107 [in Tennenbaum.Tarski]
ff:111 [in Tennenbaum.Deduction]
ff:113 [in Tennenbaum.Tarski]
ff:116 [in Tennenbaum.Deduction]
ff:117 [in Tennenbaum.Tarski]
ff:118 [in Tennenbaum.Deduction]
ff:122 [in Tennenbaum.Tarski]
ff:125 [in Tennenbaum.Tarski]
ff:125 [in Tennenbaum.FOL]
ff:128 [in Tennenbaum.Tarski]
ff:129 [in Tennenbaum.Deduction]
ff:130 [in Tennenbaum.FOL]
ff:131 [in Tennenbaum.Tarski]
ff:134 [in Tennenbaum.FOL]
ff:134 [in Tennenbaum.Deduction]
ff:136 [in Tennenbaum.Tarski]
ff:136 [in Tennenbaum.FOL]
ff:136 [in Tennenbaum.Deduction]
ff:14 [in Tennenbaum.Deduction]
ff:140 [in Tennenbaum.FOL]
ff:143 [in Tennenbaum.FOL]
ff:146 [in Tennenbaum.Deduction]
ff:156 [in Tennenbaum.FOL]
ff:160 [in Tennenbaum.Deduction]
ff:161 [in Tennenbaum.Deduction]
ff:169 [in Tennenbaum.FOL]
ff:172 [in Tennenbaum.FOL]
ff:178 [in Tennenbaum.FOL]
ff:18 [in Tennenbaum.Tarski]
ff:182 [in Tennenbaum.FOL]
ff:187 [in Tennenbaum.FOL]
ff:19 [in Tennenbaum.Deduction]
ff:191 [in Tennenbaum.FOL]
ff:200 [in Tennenbaum.FOL]
ff:209 [in Tennenbaum.FOL]
ff:221 [in Tennenbaum.FOL]
ff:224 [in Tennenbaum.FOL]
ff:23 [in Tennenbaum.Deduction]
ff:271 [in Tennenbaum.FOL]
ff:28 [in Tennenbaum.Tarski]
ff:28 [in Tennenbaum.Deduction]
ff:314 [in Tennenbaum.FOL]
ff:326 [in Tennenbaum.FOL]
ff:327 [in Tennenbaum.FOL]
ff:328 [in Tennenbaum.FOL]
ff:33 [in Tennenbaum.Deduction]
ff:41 [in Tennenbaum.Deduction]
ff:45 [in Tennenbaum.Deduction]
ff:5 [in Tennenbaum.Deduction]
ff:50 [in Tennenbaum.Deduction]
ff:51 [in Tennenbaum.FOL]
ff:53 [in Tennenbaum.Tarski]
ff:53 [in Tennenbaum.FOL]
ff:55 [in Tennenbaum.Deduction]
ff:60 [in Tennenbaum.Deduction]
ff:65 [in Tennenbaum.Deduction]
ff:69 [in Tennenbaum.Tarski]
ff:70 [in Tennenbaum.Deduction]
ff:74 [in Tennenbaum.Tarski]
ff:75 [in Tennenbaum.Tennenbaum]
ff:76 [in Tennenbaum.Deduction]
ff:78 [in Tennenbaum.Tennenbaum]
ff:79 [in Tennenbaum.Tarski]
ff:81 [in Tennenbaum.Tennenbaum]
ff:83 [in Tennenbaum.Tarski]
ff:84 [in Tennenbaum.Tennenbaum]
ff:87 [in Tennenbaum.Tennenbaum]
ff:88 [in Tennenbaum.Tarski]
ff:88 [in Tennenbaum.Deduction]
ff:9 [in Tennenbaum.Deduction]
ff:90 [in Tennenbaum.Tennenbaum]
ff:92 [in Tennenbaum.Tarski]
ff:93 [in Tennenbaum.Tennenbaum]
ff:95 [in Tennenbaum.Tennenbaum]
ff:97 [in Tennenbaum.Tarski]
ff:97 [in Tennenbaum.Tennenbaum]
ff:99 [in Tennenbaum.Tennenbaum]
f:1 [in Tennenbaum.NumberTheory]
f:10 [in Tennenbaum.CTT]
f:10 [in Tennenbaum.FOL]
f:12 [in Tennenbaum.CTT]
f:122 [in Tennenbaum.Tennenbaum]
f:13 [in Tennenbaum.CantorPairing]
f:147 [in Tennenbaum.FOL]
f:153 [in Tennenbaum.FOL]
f:166 [in Tennenbaum.FOL]
f:17 [in Tennenbaum.CantorPairing]
f:170 [in Tennenbaum.Tennenbaum]
f:195 [in Tennenbaum.Tennenbaum]
f:21 [in Tennenbaum.FOL]
f:230 [in Tennenbaum.Peano]
f:236 [in Tennenbaum.Peano]
F:293 [in Tennenbaum.FOL]
f:3 [in Tennenbaum.CantorPairing]
f:3 [in Tennenbaum.Peano]
f:30 [in Tennenbaum.Tennenbaum]
f:316 [in Tennenbaum.Peano]
f:321 [in Tennenbaum.Peano]
f:35 [in Tennenbaum.Tennenbaum]
f:368 [in Tennenbaum.Tennenbaum]
f:4 [in Tennenbaum.CTT]
f:4 [in Tennenbaum.Tennenbaum]
f:40 [in Tennenbaum.FOL]
f:48 [in Tennenbaum.Tennenbaum]
f:56 [in Tennenbaum.Tennenbaum]
f:61 [in Tennenbaum.Tennenbaum]
f:7 [in Tennenbaum.CTT]
F:81 [in Tennenbaum.FOL]
f:86 [in Tennenbaum.NumberTheory]
F:86 [in Tennenbaum.FOL]
f:9 [in Tennenbaum.CantorPairing]
f:9 [in Tennenbaum.Tarski]
F:92 [in Tennenbaum.FOL]
G
Gamma:255 [in Tennenbaum.Peano]Gamma:259 [in Tennenbaum.Peano]
g:14 [in Tennenbaum.CantorPairing]
G:219 [in Tennenbaum.Tennenbaum]
G:230 [in Tennenbaum.Tennenbaum]
g:8 [in Tennenbaum.CantorPairing]
g:9 [in Tennenbaum.FOL]
H
HX:255 [in Tennenbaum.FOL]H0:81 [in Tennenbaum.Deduction]
H:222 [in Tennenbaum.Deduction]
H:239 [in Tennenbaum.Deduction]
H:243 [in Tennenbaum.Deduction]
h:384 [in Tennenbaum.Tennenbaum]
h:385 [in Tennenbaum.Tennenbaum]
H:56 [in Tennenbaum.FOL]
H:80 [in Tennenbaum.Deduction]
I
IH:95 [in Tennenbaum.FOL]I:122 [in Tennenbaum.Deduction]
I:13 [in Tennenbaum.Tarski]
I:140 [in Tennenbaum.Deduction]
I:220 [in Tennenbaum.Peano]
I:32 [in Tennenbaum.Tarski]
I:37 [in Tennenbaum.Tarski]
I:41 [in Tennenbaum.Tarski]
I:45 [in Tennenbaum.Tarski]
I:49 [in Tennenbaum.Tarski]
I:68 [in Tennenbaum.Tennenbaum]
I:72 [in Tennenbaum.Tennenbaum]
K
k:1 [in Tennenbaum.Tennenbaum]k:106 [in Tennenbaum.Tarski]
k:118 [in Tennenbaum.Tennenbaum]
k:184 [in Tennenbaum.Tennenbaum]
k:199 [in Tennenbaum.FOL]
k:205 [in Tennenbaum.FOL]
k:208 [in Tennenbaum.FOL]
k:210 [in Tennenbaum.Peano]
k:212 [in Tennenbaum.FOL]
k:239 [in Tennenbaum.Peano]
k:244 [in Tennenbaum.Peano]
k:245 [in Tennenbaum.Peano]
k:305 [in Tennenbaum.Tennenbaum]
k:307 [in Tennenbaum.Tennenbaum]
k:33 [in Tennenbaum.NumberTheory]
k:36 [in Tennenbaum.NumberTheory]
k:64 [in Tennenbaum.NumberTheory]
L
L:223 [in Tennenbaum.Deduction]L:231 [in Tennenbaum.Deduction]
L:236 [in Tennenbaum.Deduction]
L:245 [in Tennenbaum.Deduction]
L:249 [in Tennenbaum.Deduction]
L:257 [in Tennenbaum.Deduction]
L:308 [in Tennenbaum.FOL]
l:68 [in Tennenbaum.FOL]
M
m:15 [in Tennenbaum.CTT]m:18 [in Tennenbaum.CTT]
m:193 [in Tennenbaum.Tennenbaum]
m:233 [in Tennenbaum.Deduction]
m:238 [in Tennenbaum.Deduction]
m:279 [in Tennenbaum.Tennenbaum]
m:311 [in Tennenbaum.FOL]
m:313 [in Tennenbaum.FOL]
m:39 [in Tennenbaum.NumberTheory]
m:65 [in Tennenbaum.NumberTheory]
N
n:102 [in Tennenbaum.Tarski]n:102 [in Tennenbaum.Peano]
n:103 [in Tennenbaum.FOL]
n:104 [in Tennenbaum.Peano]
n:106 [in Tennenbaum.Peano]
n:106 [in Tennenbaum.FOL]
N:108 [in Tennenbaum.Tarski]
n:108 [in Tennenbaum.Peano]
n:108 [in Tennenbaum.Tennenbaum]
n:110 [in Tennenbaum.Peano]
n:112 [in Tennenbaum.Tarski]
n:112 [in Tennenbaum.Peano]
n:114 [in Tennenbaum.Peano]
n:116 [in Tennenbaum.Peano]
n:117 [in Tennenbaum.Tennenbaum]
n:117 [in Tennenbaum.FOL]
N:118 [in Tennenbaum.Tarski]
n:118 [in Tennenbaum.FOL]
n:12 [in Tennenbaum.Peano]
N:120 [in Tennenbaum.Tennenbaum]
n:120 [in Tennenbaum.FOL]
n:121 [in Tennenbaum.Peano]
n:121 [in Tennenbaum.FOL]
N:123 [in Tennenbaum.Tarski]
n:123 [in Tennenbaum.Peano]
n:124 [in Tennenbaum.FOL]
N:126 [in Tennenbaum.Tarski]
N:126 [in Tennenbaum.Tennenbaum]
n:128 [in Tennenbaum.Peano]
N:129 [in Tennenbaum.Tarski]
n:129 [in Tennenbaum.Tennenbaum]
n:129 [in Tennenbaum.FOL]
n:130 [in Tennenbaum.Peano]
N:131 [in Tennenbaum.Tennenbaum]
n:133 [in Tennenbaum.FOL]
N:134 [in Tennenbaum.Tarski]
n:134 [in Tennenbaum.Tennenbaum]
n:135 [in Tennenbaum.Peano]
N:137 [in Tennenbaum.Tarski]
n:137 [in Tennenbaum.Peano]
n:143 [in Tennenbaum.Peano]
n:145 [in Tennenbaum.Peano]
n:148 [in Tennenbaum.FOL]
n:153 [in Tennenbaum.Peano]
n:154 [in Tennenbaum.FOL]
n:155 [in Tennenbaum.Peano]
n:158 [in Tennenbaum.Deduction]
n:159 [in Tennenbaum.Deduction]
n:16 [in Tennenbaum.CTT]
n:160 [in Tennenbaum.Peano]
n:162 [in Tennenbaum.Peano]
n:162 [in Tennenbaum.FOL]
n:167 [in Tennenbaum.Deduction]
n:173 [in Tennenbaum.FOL]
n:175 [in Tennenbaum.Tennenbaum]
n:179 [in Tennenbaum.FOL]
n:180 [in Tennenbaum.Tennenbaum]
n:182 [in Tennenbaum.Tennenbaum]
n:183 [in Tennenbaum.FOL]
n:187 [in Tennenbaum.Tennenbaum]
n:188 [in Tennenbaum.FOL]
n:19 [in Tennenbaum.CTT]
n:190 [in Tennenbaum.FOL]
n:192 [in Tennenbaum.Tennenbaum]
n:192 [in Tennenbaum.FOL]
n:194 [in Tennenbaum.Peano]
n:194 [in Tennenbaum.Tennenbaum]
n:195 [in Tennenbaum.FOL]
n:196 [in Tennenbaum.Peano]
n:197 [in Tennenbaum.Tennenbaum]
n:198 [in Tennenbaum.Tennenbaum]
n:200 [in Tennenbaum.Tennenbaum]
n:201 [in Tennenbaum.Tennenbaum]
n:201 [in Tennenbaum.FOL]
n:204 [in Tennenbaum.Tennenbaum]
n:206 [in Tennenbaum.Tennenbaum]
n:206 [in Tennenbaum.FOL]
n:207 [in Tennenbaum.Tennenbaum]
n:208 [in Tennenbaum.Peano]
n:208 [in Tennenbaum.Tennenbaum]
n:210 [in Tennenbaum.FOL]
n:211 [in Tennenbaum.Tennenbaum]
n:213 [in Tennenbaum.Tennenbaum]
n:213 [in Tennenbaum.FOL]
n:214 [in Tennenbaum.Tennenbaum]
n:215 [in Tennenbaum.Tennenbaum]
n:215 [in Tennenbaum.FOL]
n:218 [in Tennenbaum.Tennenbaum]
n:218 [in Tennenbaum.FOL]
n:220 [in Tennenbaum.Tennenbaum]
n:220 [in Tennenbaum.FOL]
n:221 [in Tennenbaum.Tennenbaum]
n:223 [in Tennenbaum.FOL]
n:224 [in Tennenbaum.Tennenbaum]
n:224 [in Tennenbaum.Deduction]
n:226 [in Tennenbaum.Tennenbaum]
n:226 [in Tennenbaum.FOL]
n:227 [in Tennenbaum.Peano]
n:227 [in Tennenbaum.Tennenbaum]
n:228 [in Tennenbaum.FOL]
n:231 [in Tennenbaum.Peano]
n:231 [in Tennenbaum.Tennenbaum]
n:232 [in Tennenbaum.Tennenbaum]
n:234 [in Tennenbaum.FOL]
n:237 [in Tennenbaum.Peano]
n:241 [in Tennenbaum.FOL]
n:248 [in Tennenbaum.Peano]
n:249 [in Tennenbaum.Tennenbaum]
n:249 [in Tennenbaum.FOL]
n:250 [in Tennenbaum.Deduction]
N:254 [in Tennenbaum.Peano]
n:255 [in Tennenbaum.Tennenbaum]
n:256 [in Tennenbaum.FOL]
N:258 [in Tennenbaum.Peano]
n:26 [in Tennenbaum.CantorPairing]
N:26 [in Tennenbaum.LogicFacts]
n:262 [in Tennenbaum.Peano]
n:282 [in Tennenbaum.Tennenbaum]
n:283 [in Tennenbaum.Tennenbaum]
n:285 [in Tennenbaum.FOL]
n:286 [in Tennenbaum.Tennenbaum]
n:288 [in Tennenbaum.Tennenbaum]
n:290 [in Tennenbaum.Tennenbaum]
n:290 [in Tennenbaum.FOL]
n:292 [in Tennenbaum.Tennenbaum]
n:294 [in Tennenbaum.Tennenbaum]
n:296 [in Tennenbaum.Tennenbaum]
n:30 [in Tennenbaum.Peano]
n:300 [in Tennenbaum.Tennenbaum]
n:302 [in Tennenbaum.Tennenbaum]
n:303 [in Tennenbaum.Tennenbaum]
n:304 [in Tennenbaum.FOL]
n:306 [in Tennenbaum.Peano]
n:309 [in Tennenbaum.FOL]
n:31 [in Tennenbaum.CantorPairing]
N:31 [in Tennenbaum.LogicFacts]
n:311 [in Tennenbaum.Tennenbaum]
n:315 [in Tennenbaum.Peano]
n:315 [in Tennenbaum.FOL]
n:316 [in Tennenbaum.Tennenbaum]
n:319 [in Tennenbaum.Tennenbaum]
n:32 [in Tennenbaum.Tennenbaum]
n:320 [in Tennenbaum.Peano]
n:322 [in Tennenbaum.Tennenbaum]
n:324 [in Tennenbaum.Peano]
n:327 [in Tennenbaum.Peano]
n:330 [in Tennenbaum.Peano]
n:333 [in Tennenbaum.Peano]
n:336 [in Tennenbaum.Peano]
n:339 [in Tennenbaum.Tennenbaum]
n:34 [in Tennenbaum.Peano]
n:341 [in Tennenbaum.Tennenbaum]
n:342 [in Tennenbaum.Tennenbaum]
n:344 [in Tennenbaum.Tennenbaum]
n:346 [in Tennenbaum.Tennenbaum]
n:35 [in Tennenbaum.Peano]
N:35 [in Tennenbaum.LogicFacts]
n:353 [in Tennenbaum.Tennenbaum]
n:355 [in Tennenbaum.Tennenbaum]
n:357 [in Tennenbaum.Tennenbaum]
n:360 [in Tennenbaum.Tennenbaum]
n:361 [in Tennenbaum.Tennenbaum]
n:363 [in Tennenbaum.Tennenbaum]
n:369 [in Tennenbaum.Tennenbaum]
n:37 [in Tennenbaum.Tennenbaum]
n:370 [in Tennenbaum.Tennenbaum]
n:373 [in Tennenbaum.Tennenbaum]
N:38 [in Tennenbaum.NumberTheory]
N:38 [in Tennenbaum.LogicFacts]
n:39 [in Tennenbaum.Peano]
n:392 [in Tennenbaum.Tennenbaum]
n:393 [in Tennenbaum.Tennenbaum]
n:394 [in Tennenbaum.Tennenbaum]
n:395 [in Tennenbaum.Tennenbaum]
n:4 [in Tennenbaum.FOL]
n:40 [in Tennenbaum.CantorPairing]
N:41 [in Tennenbaum.LogicFacts]
n:47 [in Tennenbaum.LogicFacts]
n:50 [in Tennenbaum.LogicFacts]
n:50 [in Tennenbaum.Tennenbaum]
n:51 [in Tennenbaum.LogicFacts]
n:52 [in Tennenbaum.NumberTheory]
n:52 [in Tennenbaum.LogicFacts]
n:54 [in Tennenbaum.NumberTheory]
n:56 [in Tennenbaum.NumberTheory]
N:58 [in Tennenbaum.NumberTheory]
N:60 [in Tennenbaum.NumberTheory]
n:60 [in Tennenbaum.Peano]
n:63 [in Tennenbaum.NumberTheory]
n:63 [in Tennenbaum.Peano]
n:63 [in Tennenbaum.LogicFacts]
n:63 [in Tennenbaum.FOL]
n:66 [in Tennenbaum.LogicFacts]
n:66 [in Tennenbaum.FOL]
n:67 [in Tennenbaum.NumberTheory]
n:68 [in Tennenbaum.Peano]
n:69 [in Tennenbaum.Peano]
n:69 [in Tennenbaum.LogicFacts]
n:70 [in Tennenbaum.Peano]
n:70 [in Tennenbaum.LogicFacts]
n:70 [in Tennenbaum.Tennenbaum]
n:71 [in Tennenbaum.FOL]
n:74 [in Tennenbaum.NumberTheory]
n:74 [in Tennenbaum.FOL]
n:77 [in Tennenbaum.NumberTheory]
n:77 [in Tennenbaum.Peano]
n:77 [in Tennenbaum.FOL]
n:78 [in Tennenbaum.NumberTheory]
n:78 [in Tennenbaum.Peano]
n:80 [in Tennenbaum.Peano]
N:81 [in Tennenbaum.NumberTheory]
n:82 [in Tennenbaum.Peano]
n:83 [in Tennenbaum.NumberTheory]
n:83 [in Tennenbaum.Peano]
n:85 [in Tennenbaum.Peano]
n:87 [in Tennenbaum.Peano]
n:88 [in Tennenbaum.NumberTheory]
n:89 [in Tennenbaum.Peano]
n:9 [in Tennenbaum.Peano]
n:90 [in Tennenbaum.NumberTheory]
n:91 [in Tennenbaum.Peano]
n:93 [in Tennenbaum.Peano]
n:95 [in Tennenbaum.Peano]
n:97 [in Tennenbaum.Peano]
O
ops:161 [in Tennenbaum.FOL]ops:259 [in Tennenbaum.FOL]
ops:274 [in Tennenbaum.FOL]
ops:32 [in Tennenbaum.FOL]
ops:331 [in Tennenbaum.FOL]
ops:99 [in Tennenbaum.FOL]
op:321 [in Tennenbaum.FOL]
op:324 [in Tennenbaum.FOL]
P
pat:23 [in Tennenbaum.CantorPairing]pat:36 [in Tennenbaum.CantorPairing]
phi1:269 [in Tennenbaum.FOL]
phi2:270 [in Tennenbaum.FOL]
phi:100 [in Tennenbaum.Tarski]
phi:101 [in Tennenbaum.Deduction]
phi:104 [in Tennenbaum.Deduction]
phi:107 [in Tennenbaum.Deduction]
phi:109 [in Tennenbaum.Tarski]
phi:113 [in Tennenbaum.Deduction]
phi:115 [in Tennenbaum.Tennenbaum]
phi:116 [in Tennenbaum.Tarski]
phi:117 [in Tennenbaum.Deduction]
phi:119 [in Tennenbaum.Tarski]
phi:12 [in Tennenbaum.Deduction]
phi:120 [in Tennenbaum.Deduction]
phi:124 [in Tennenbaum.Tarski]
phi:126 [in Tennenbaum.FOL]
phi:127 [in Tennenbaum.Tarski]
phi:13 [in Tennenbaum.Peano]
phi:130 [in Tennenbaum.Tarski]
phi:130 [in Tennenbaum.Tennenbaum]
phi:131 [in Tennenbaum.FOL]
phi:131 [in Tennenbaum.Deduction]
phi:133 [in Tennenbaum.Tarski]
phi:135 [in Tennenbaum.FOL]
phi:135 [in Tennenbaum.Deduction]
phi:137 [in Tennenbaum.FOL]
phi:138 [in Tennenbaum.Deduction]
phi:139 [in Tennenbaum.Tarski]
phi:141 [in Tennenbaum.FOL]
phi:15 [in Tennenbaum.Peano]
phi:158 [in Tennenbaum.FOL]
phi:163 [in Tennenbaum.Deduction]
phi:17 [in Tennenbaum.Deduction]
phi:170 [in Tennenbaum.Deduction]
phi:173 [in Tennenbaum.Deduction]
phi:175 [in Tennenbaum.Deduction]
phi:176 [in Tennenbaum.Deduction]
phi:178 [in Tennenbaum.Deduction]
phi:180 [in Tennenbaum.FOL]
phi:180 [in Tennenbaum.Deduction]
phi:182 [in Tennenbaum.Deduction]
phi:184 [in Tennenbaum.Deduction]
phi:186 [in Tennenbaum.Deduction]
phi:188 [in Tennenbaum.Deduction]
phi:189 [in Tennenbaum.FOL]
phi:19 [in Tennenbaum.Peano]
phi:191 [in Tennenbaum.Deduction]
phi:192 [in Tennenbaum.Deduction]
phi:194 [in Tennenbaum.FOL]
phi:194 [in Tennenbaum.Deduction]
phi:196 [in Tennenbaum.Deduction]
phi:198 [in Tennenbaum.Deduction]
phi:199 [in Tennenbaum.Tennenbaum]
phi:20 [in Tennenbaum.Tarski]
phi:200 [in Tennenbaum.Deduction]
phi:202 [in Tennenbaum.FOL]
phi:202 [in Tennenbaum.Deduction]
phi:204 [in Tennenbaum.Deduction]
phi:206 [in Tennenbaum.Deduction]
phi:208 [in Tennenbaum.Deduction]
phi:210 [in Tennenbaum.Deduction]
phi:211 [in Tennenbaum.FOL]
phi:212 [in Tennenbaum.Deduction]
phi:215 [in Tennenbaum.Deduction]
phi:218 [in Tennenbaum.Deduction]
phi:22 [in Tennenbaum.Deduction]
phi:222 [in Tennenbaum.FOL]
phi:228 [in Tennenbaum.Deduction]
phi:24 [in Tennenbaum.Peano]
phi:246 [in Tennenbaum.Peano]
phi:249 [in Tennenbaum.Peano]
phi:25 [in Tennenbaum.Peano]
phi:252 [in Tennenbaum.Peano]
phi:256 [in Tennenbaum.Peano]
phi:257 [in Tennenbaum.Peano]
phi:26 [in Tennenbaum.Peano]
phi:265 [in Tennenbaum.FOL]
phi:27 [in Tennenbaum.Deduction]
phi:30 [in Tennenbaum.Tarski]
phi:303 [in Tennenbaum.Peano]
phi:32 [in Tennenbaum.Deduction]
phi:323 [in Tennenbaum.FOL]
phi:325 [in Tennenbaum.FOL]
phi:35 [in Tennenbaum.Tarski]
phi:36 [in Tennenbaum.Deduction]
phi:40 [in Tennenbaum.Deduction]
phi:43 [in Tennenbaum.Tarski]
phi:44 [in Tennenbaum.Deduction]
phi:48 [in Tennenbaum.Deduction]
phi:53 [in Tennenbaum.Deduction]
phi:55 [in Tennenbaum.Tarski]
phi:58 [in Tennenbaum.FOL]
phi:58 [in Tennenbaum.Deduction]
phi:63 [in Tennenbaum.Deduction]
phi:68 [in Tennenbaum.Deduction]
phi:72 [in Tennenbaum.Tarski]
phi:73 [in Tennenbaum.Deduction]
phi:77 [in Tennenbaum.Tarski]
phi:78 [in Tennenbaum.Deduction]
phi:82 [in Tennenbaum.Tarski]
phi:83 [in Tennenbaum.Deduction]
phi:86 [in Tennenbaum.Tarski]
Phi:90 [in Tennenbaum.Tarski]
phi:92 [in Tennenbaum.Deduction]
phi:95 [in Tennenbaum.Tarski]
phi:98 [in Tennenbaum.Deduction]
psi:101 [in Tennenbaum.Tarski]
psi:102 [in Tennenbaum.Deduction]
psi:114 [in Tennenbaum.Deduction]
psi:115 [in Tennenbaum.Deduction]
psi:124 [in Tennenbaum.Deduction]
psi:13 [in Tennenbaum.Deduction]
psi:132 [in Tennenbaum.Deduction]
psi:133 [in Tennenbaum.Deduction]
psi:14 [in Tennenbaum.Peano]
psi:142 [in Tennenbaum.Deduction]
psi:145 [in Tennenbaum.FOL]
psi:145 [in Tennenbaum.Deduction]
psi:171 [in Tennenbaum.Deduction]
psi:172 [in Tennenbaum.Deduction]
psi:174 [in Tennenbaum.Deduction]
psi:18 [in Tennenbaum.Deduction]
psi:181 [in Tennenbaum.FOL]
psi:185 [in Tennenbaum.Deduction]
psi:187 [in Tennenbaum.Deduction]
psi:193 [in Tennenbaum.Deduction]
psi:195 [in Tennenbaum.Deduction]
psi:197 [in Tennenbaum.Deduction]
psi:199 [in Tennenbaum.Deduction]
psi:201 [in Tennenbaum.Deduction]
psi:203 [in Tennenbaum.Deduction]
psi:205 [in Tennenbaum.Deduction]
psi:207 [in Tennenbaum.Deduction]
psi:209 [in Tennenbaum.Deduction]
psi:211 [in Tennenbaum.Deduction]
psi:214 [in Tennenbaum.Deduction]
psi:217 [in Tennenbaum.Deduction]
psi:222 [in Tennenbaum.Peano]
psi:242 [in Tennenbaum.Deduction]
psi:25 [in Tennenbaum.Tarski]
psi:250 [in Tennenbaum.Peano]
psi:266 [in Tennenbaum.FOL]
psi:322 [in Tennenbaum.FOL]
psi:34 [in Tennenbaum.Tarski]
psi:37 [in Tennenbaum.Deduction]
psi:49 [in Tennenbaum.Deduction]
psi:54 [in Tennenbaum.Deduction]
psi:59 [in Tennenbaum.Deduction]
psi:64 [in Tennenbaum.Deduction]
psi:69 [in Tennenbaum.Deduction]
psi:74 [in Tennenbaum.Deduction]
psi:79 [in Tennenbaum.Deduction]
psi:85 [in Tennenbaum.Deduction]
psi:96 [in Tennenbaum.Tarski]
psi:99 [in Tennenbaum.Deduction]
p:10 [in Tennenbaum.Deduction]
P:11 [in Tennenbaum.Tarski]
p:11 [in Tennenbaum.CTT]
p:12 [in Tennenbaum.Tennenbaum]
P:125 [in Tennenbaum.Deduction]
P:127 [in Tennenbaum.Deduction]
p:13 [in Tennenbaum.CTT]
p:15 [in Tennenbaum.Deduction]
p:164 [in Tennenbaum.Deduction]
p:17 [in Tennenbaum.Tennenbaum]
p:173 [in Tennenbaum.Tennenbaum]
P:174 [in Tennenbaum.FOL]
p:176 [in Tennenbaum.Tennenbaum]
p:20 [in Tennenbaum.Deduction]
p:219 [in Tennenbaum.Deduction]
p:230 [in Tennenbaum.Deduction]
P:232 [in Tennenbaum.FOL]
p:235 [in Tennenbaum.Deduction]
P:236 [in Tennenbaum.FOL]
p:24 [in Tennenbaum.Deduction]
P:244 [in Tennenbaum.FOL]
p:245 [in Tennenbaum.FOL]
p:247 [in Tennenbaum.Deduction]
p:25 [in Tennenbaum.CantorPairing]
p:254 [in Tennenbaum.Deduction]
p:26 [in Tennenbaum.Tennenbaum]
p:27 [in Tennenbaum.LogicFacts]
p:29 [in Tennenbaum.CantorPairing]
p:29 [in Tennenbaum.Tennenbaum]
p:29 [in Tennenbaum.Deduction]
P:3 [in Tennenbaum.LogicFacts]
P:319 [in Tennenbaum.FOL]
p:32 [in Tennenbaum.LogicFacts]
p:34 [in Tennenbaum.Tennenbaum]
p:34 [in Tennenbaum.Deduction]
p:36 [in Tennenbaum.LogicFacts]
P:36 [in Tennenbaum.FOL]
p:37 [in Tennenbaum.CantorPairing]
p:38 [in Tennenbaum.Deduction]
p:39 [in Tennenbaum.LogicFacts]
p:39 [in Tennenbaum.Tennenbaum]
p:396 [in Tennenbaum.Tennenbaum]
p:42 [in Tennenbaum.LogicFacts]
p:42 [in Tennenbaum.Deduction]
p:46 [in Tennenbaum.Deduction]
P:49 [in Tennenbaum.FOL]
p:5 [in Tennenbaum.LogicFacts]
p:51 [in Tennenbaum.NumberTheory]
p:51 [in Tennenbaum.Deduction]
p:52 [in Tennenbaum.Tennenbaum]
p:53 [in Tennenbaum.NumberTheory]
p:53 [in Tennenbaum.Tennenbaum]
p:55 [in Tennenbaum.NumberTheory]
p:55 [in Tennenbaum.Tennenbaum]
p:56 [in Tennenbaum.LogicFacts]
p:56 [in Tennenbaum.Deduction]
p:57 [in Tennenbaum.NumberTheory]
p:6 [in Tennenbaum.Deduction]
p:60 [in Tennenbaum.Tennenbaum]
p:61 [in Tennenbaum.Deduction]
P:62 [in Tennenbaum.FOL]
p:66 [in Tennenbaum.Deduction]
P:7 [in Tennenbaum.Peano]
p:70 [in Tennenbaum.NumberTheory]
p:71 [in Tennenbaum.Deduction]
p:73 [in Tennenbaum.NumberTheory]
p:79 [in Tennenbaum.FOL]
p:8 [in Tennenbaum.LogicFacts]
p:82 [in Tennenbaum.NumberTheory]
p:84 [in Tennenbaum.FOL]
p:89 [in Tennenbaum.Deduction]
p:9 [in Tennenbaum.Tennenbaum]
p:90 [in Tennenbaum.FOL]
Q
quantop:186 [in Tennenbaum.FOL]q1:199 [in Tennenbaum.Peano]
q2:201 [in Tennenbaum.Peano]
Q:128 [in Tennenbaum.Deduction]
q:191 [in Tennenbaum.Peano]
q:203 [in Tennenbaum.Peano]
q:42 [in Tennenbaum.FOL]
q:7 [in Tennenbaum.NumberTheory]
q:9 [in Tennenbaum.LogicFacts]
R
rho:103 [in Tennenbaum.Peano]rho:105 [in Tennenbaum.Peano]
rho:109 [in Tennenbaum.Peano]
rho:110 [in Tennenbaum.Tarski]
rho:111 [in Tennenbaum.Peano]
rho:114 [in Tennenbaum.Tarski]
rho:115 [in Tennenbaum.Peano]
rho:117 [in Tennenbaum.Peano]
rho:122 [in Tennenbaum.Peano]
rho:123 [in Tennenbaum.Deduction]
rho:124 [in Tennenbaum.Peano]
rho:129 [in Tennenbaum.Peano]
rho:131 [in Tennenbaum.Peano]
rho:132 [in Tennenbaum.Tarski]
rho:135 [in Tennenbaum.Tarski]
rho:136 [in Tennenbaum.Peano]
rho:138 [in Tennenbaum.Tarski]
rho:138 [in Tennenbaum.Peano]
rho:14 [in Tennenbaum.Tarski]
rho:141 [in Tennenbaum.Deduction]
rho:144 [in Tennenbaum.Peano]
rho:145 [in Tennenbaum.Tennenbaum]
rho:146 [in Tennenbaum.Peano]
rho:154 [in Tennenbaum.Peano]
rho:154 [in Tennenbaum.Tennenbaum]
rho:155 [in Tennenbaum.Tennenbaum]
rho:156 [in Tennenbaum.Peano]
rho:156 [in Tennenbaum.Tennenbaum]
rho:157 [in Tennenbaum.Tennenbaum]
rho:158 [in Tennenbaum.Tennenbaum]
rho:159 [in Tennenbaum.Tennenbaum]
rho:161 [in Tennenbaum.Peano]
rho:163 [in Tennenbaum.Peano]
rho:163 [in Tennenbaum.Tennenbaum]
rho:169 [in Tennenbaum.Tennenbaum]
rho:172 [in Tennenbaum.Peano]
rho:174 [in Tennenbaum.Peano]
rho:186 [in Tennenbaum.Tennenbaum]
rho:19 [in Tennenbaum.Tarski]
rho:195 [in Tennenbaum.Peano]
rho:197 [in Tennenbaum.Peano]
rho:221 [in Tennenbaum.Peano]
rho:223 [in Tennenbaum.Peano]
rho:225 [in Tennenbaum.Peano]
rho:242 [in Tennenbaum.Tennenbaum]
rho:244 [in Tennenbaum.Tennenbaum]
rho:246 [in Tennenbaum.Tennenbaum]
rho:248 [in Tennenbaum.Tennenbaum]
rho:250 [in Tennenbaum.Tennenbaum]
rho:252 [in Tennenbaum.Tennenbaum]
rho:254 [in Tennenbaum.Tennenbaum]
rho:256 [in Tennenbaum.Tennenbaum]
rho:264 [in Tennenbaum.Peano]
rho:266 [in Tennenbaum.Tennenbaum]
rho:268 [in Tennenbaum.Tennenbaum]
rho:270 [in Tennenbaum.Tennenbaum]
rho:272 [in Tennenbaum.Tennenbaum]
rho:28 [in Tennenbaum.Peano]
rho:304 [in Tennenbaum.Peano]
rho:315 [in Tennenbaum.Tennenbaum]
rho:326 [in Tennenbaum.Tennenbaum]
rho:328 [in Tennenbaum.Tennenbaum]
rho:33 [in Tennenbaum.Tarski]
rho:331 [in Tennenbaum.Tennenbaum]
rho:333 [in Tennenbaum.Tennenbaum]
rho:340 [in Tennenbaum.Tennenbaum]
rho:345 [in Tennenbaum.Tennenbaum]
rho:354 [in Tennenbaum.Tennenbaum]
rho:356 [in Tennenbaum.Tennenbaum]
rho:358 [in Tennenbaum.Tennenbaum]
rho:36 [in Tennenbaum.Peano]
rho:362 [in Tennenbaum.Tennenbaum]
rho:364 [in Tennenbaum.Tennenbaum]
rho:38 [in Tennenbaum.Tarski]
rho:38 [in Tennenbaum.Peano]
rho:403 [in Tennenbaum.Tennenbaum]
rho:405 [in Tennenbaum.Tennenbaum]
rho:41 [in Tennenbaum.Peano]
rho:42 [in Tennenbaum.Tarski]
rho:44 [in Tennenbaum.Peano]
rho:46 [in Tennenbaum.Tarski]
rho:47 [in Tennenbaum.Peano]
rho:50 [in Tennenbaum.Tarski]
rho:51 [in Tennenbaum.Peano]
rho:62 [in Tennenbaum.Tarski]
rho:65 [in Tennenbaum.Peano]
rho:66 [in Tennenbaum.Tarski]
rho:70 [in Tennenbaum.Tarski]
rho:75 [in Tennenbaum.Tarski]
rho:79 [in Tennenbaum.Peano]
rho:80 [in Tennenbaum.Tarski]
rho:81 [in Tennenbaum.Peano]
rho:84 [in Tennenbaum.Tarski]
rho:84 [in Tennenbaum.Peano]
rho:86 [in Tennenbaum.Peano]
rho:89 [in Tennenbaum.Tarski]
rho:90 [in Tennenbaum.Peano]
rho:92 [in Tennenbaum.Peano]
rho:94 [in Tennenbaum.Tarski]
rho:96 [in Tennenbaum.Peano]
rho:98 [in Tennenbaum.Peano]
rho:99 [in Tennenbaum.Tarski]
r1:200 [in Tennenbaum.Peano]
r1:205 [in Tennenbaum.Peano]
r2:202 [in Tennenbaum.Peano]
r2:207 [in Tennenbaum.Peano]
r:193 [in Tennenbaum.Peano]
r:304 [in Tennenbaum.Tennenbaum]
r:306 [in Tennenbaum.Tennenbaum]
r:43 [in Tennenbaum.NumberTheory]
r:8 [in Tennenbaum.NumberTheory]
S
sigma:101 [in Tennenbaum.FOL]sigma:104 [in Tennenbaum.Tarski]
sigma:105 [in Tennenbaum.FOL]
sigma:109 [in Tennenbaum.FOL]
sigma:111 [in Tennenbaum.Tarski]
sigma:115 [in Tennenbaum.Tarski]
sigma:115 [in Tennenbaum.FOL]
sigma:116 [in Tennenbaum.Tennenbaum]
sigma:119 [in Tennenbaum.FOL]
sigma:122 [in Tennenbaum.FOL]
sigma:127 [in Tennenbaum.FOL]
sigma:128 [in Tennenbaum.Tennenbaum]
sigma:132 [in Tennenbaum.FOL]
sigma:133 [in Tennenbaum.Tennenbaum]
sigma:138 [in Tennenbaum.FOL]
sigma:140 [in Tennenbaum.Tarski]
sigma:157 [in Tennenbaum.FOL]
sigma:197 [in Tennenbaum.FOL]
sigma:203 [in Tennenbaum.FOL]
sigma:241 [in Tennenbaum.Peano]
sigma:243 [in Tennenbaum.Peano]
sigma:247 [in Tennenbaum.Peano]
sigma:251 [in Tennenbaum.Peano]
sigma:253 [in Tennenbaum.Peano]
sigma:260 [in Tennenbaum.Peano]
sigma:302 [in Tennenbaum.Peano]
sigma:33 [in Tennenbaum.Peano]
sigma:335 [in Tennenbaum.Tennenbaum]
sigma:85 [in Tennenbaum.Tarski]
sig_preds_dec:240 [in Tennenbaum.FOL]
sig_funcs_dec:239 [in Tennenbaum.FOL]
s:112 [in Tennenbaum.FOL]
s:142 [in Tennenbaum.FOL]
s:184 [in Tennenbaum.FOL]
s:335 [in Tennenbaum.Peano]
s:343 [in Tennenbaum.Peano]
s:353 [in Tennenbaum.Peano]
s:45 [in Tennenbaum.FOL]
s:80 [in Tennenbaum.Tennenbaum]
T
tau:102 [in Tennenbaum.FOL]tau:105 [in Tennenbaum.Tarski]
tau:110 [in Tennenbaum.FOL]
tau:116 [in Tennenbaum.FOL]
tau:123 [in Tennenbaum.FOL]
tau:128 [in Tennenbaum.FOL]
tau:139 [in Tennenbaum.FOL]
tau:198 [in Tennenbaum.FOL]
tau:204 [in Tennenbaum.FOL]
theta:213 [in Tennenbaum.Deduction]
theta:216 [in Tennenbaum.Deduction]
theta:75 [in Tennenbaum.Deduction]
t:100 [in Tennenbaum.FOL]
T:100 [in Tennenbaum.Deduction]
t:103 [in Tennenbaum.Tarski]
t:104 [in Tennenbaum.FOL]
t:107 [in Tennenbaum.FOL]
t:108 [in Tennenbaum.FOL]
t:111 [in Tennenbaum.FOL]
t:113 [in Tennenbaum.FOL]
T:119 [in Tennenbaum.Deduction]
t:124 [in Tennenbaum.Tennenbaum]
t:125 [in Tennenbaum.Tennenbaum]
T:137 [in Tennenbaum.Deduction]
T:149 [in Tennenbaum.Deduction]
t:15 [in Tennenbaum.Tarski]
t:159 [in Tennenbaum.Peano]
t:168 [in Tennenbaum.FOL]
t:176 [in Tennenbaum.FOL]
t:177 [in Tennenbaum.Deduction]
t:179 [in Tennenbaum.Deduction]
t:181 [in Tennenbaum.Deduction]
t:183 [in Tennenbaum.Peano]
t:183 [in Tennenbaum.Deduction]
t:185 [in Tennenbaum.FOL]
t:186 [in Tennenbaum.Peano]
t:189 [in Tennenbaum.Peano]
t:196 [in Tennenbaum.FOL]
t:207 [in Tennenbaum.FOL]
t:216 [in Tennenbaum.FOL]
t:217 [in Tennenbaum.FOL]
t:219 [in Tennenbaum.FOL]
T:23 [in Tennenbaum.Peano]
t:23 [in Tennenbaum.FOL]
T:241 [in Tennenbaum.Deduction]
t:242 [in Tennenbaum.Peano]
t:242 [in Tennenbaum.FOL]
T:244 [in Tennenbaum.Deduction]
T:256 [in Tennenbaum.Deduction]
t:26 [in Tennenbaum.Deduction]
t:27 [in Tennenbaum.CTT]
t:270 [in Tennenbaum.Peano]
t:29 [in Tennenbaum.CTT]
t:31 [in Tennenbaum.Deduction]
t:344 [in Tennenbaum.Peano]
t:354 [in Tennenbaum.Peano]
t:38 [in Tennenbaum.CTT]
t:43 [in Tennenbaum.CTT]
t:44 [in Tennenbaum.FOL]
t:50 [in Tennenbaum.FOL]
t:64 [in Tennenbaum.Tarski]
t:68 [in Tennenbaum.Tarski]
t:79 [in Tennenbaum.Tennenbaum]
t:80 [in Tennenbaum.FOL]
T:82 [in Tennenbaum.Deduction]
t:85 [in Tennenbaum.FOL]
t:88 [in Tennenbaum.FOL]
t:91 [in Tennenbaum.Tarski]
t:91 [in Tennenbaum.FOL]
t:94 [in Tennenbaum.FOL]
T:97 [in Tennenbaum.Deduction]
U
u:321 [in Tennenbaum.Tennenbaum]V
v':251 [in Tennenbaum.FOL]v:121 [in Tennenbaum.Tennenbaum]
v:167 [in Tennenbaum.FOL]
v:175 [in Tennenbaum.FOL]
v:214 [in Tennenbaum.FOL]
v:229 [in Tennenbaum.FOL]
v:235 [in Tennenbaum.FOL]
v:250 [in Tennenbaum.FOL]
v:263 [in Tennenbaum.Peano]
v:288 [in Tennenbaum.FOL]
v:294 [in Tennenbaum.FOL]
v:305 [in Tennenbaum.FOL]
v:308 [in Tennenbaum.Peano]
v:310 [in Tennenbaum.Peano]
v:310 [in Tennenbaum.FOL]
v:312 [in Tennenbaum.Peano]
v:317 [in Tennenbaum.Peano]
v:320 [in Tennenbaum.FOL]
v:322 [in Tennenbaum.Peano]
v:325 [in Tennenbaum.Peano]
v:328 [in Tennenbaum.Peano]
v:331 [in Tennenbaum.Peano]
v:334 [in Tennenbaum.Peano]
v:75 [in Tennenbaum.FOL]
v:78 [in Tennenbaum.FOL]
v:82 [in Tennenbaum.FOL]
v:87 [in Tennenbaum.FOL]
v:93 [in Tennenbaum.FOL]
X
xi:114 [in Tennenbaum.FOL]xi:144 [in Tennenbaum.FOL]
xi:3 [in Tennenbaum.FOL]
xi:63 [in Tennenbaum.Tarski]
xi:67 [in Tennenbaum.Tarski]
xi:71 [in Tennenbaum.Tarski]
xi:76 [in Tennenbaum.Tarski]
xi:81 [in Tennenbaum.Tarski]
x':5 [in Tennenbaum.CantorPairing]
x1:278 [in Tennenbaum.Peano]
x1:282 [in Tennenbaum.Peano]
x2:280 [in Tennenbaum.Peano]
x2:284 [in Tennenbaum.Peano]
X:1 [in Tennenbaum.CantorPairing]
X:1 [in Tennenbaum.LogicFacts]
X:1 [in Tennenbaum.FOL]
x:10 [in Tennenbaum.CantorPairing]
x:10 [in Tennenbaum.NumberTheory]
x:10 [in Tennenbaum.LogicFacts]
x:10 [in Tennenbaum.Tennenbaum]
X:11 [in Tennenbaum.CantorPairing]
x:11 [in Tennenbaum.LogicFacts]
X:11 [in Tennenbaum.Tennenbaum]
x:11 [in Tennenbaum.FOL]
x:118 [in Tennenbaum.Peano]
X:119 [in Tennenbaum.Tennenbaum]
x:12 [in Tennenbaum.NumberTheory]
x:123 [in Tennenbaum.Tennenbaum]
x:125 [in Tennenbaum.Peano]
x:13 [in Tennenbaum.LogicFacts]
x:13 [in Tennenbaum.Tennenbaum]
x:134 [in Tennenbaum.Peano]
X:136 [in Tennenbaum.Tennenbaum]
x:138 [in Tennenbaum.Tennenbaum]
x:139 [in Tennenbaum.Peano]
X:139 [in Tennenbaum.Tennenbaum]
x:14 [in Tennenbaum.NumberTheory]
x:14 [in Tennenbaum.Tennenbaum]
x:141 [in Tennenbaum.Peano]
x:141 [in Tennenbaum.Tennenbaum]
X:146 [in Tennenbaum.FOL]
x:147 [in Tennenbaum.Peano]
x:149 [in Tennenbaum.Peano]
x:149 [in Tennenbaum.FOL]
X:15 [in Tennenbaum.CantorPairing]
x:15 [in Tennenbaum.Tennenbaum]
x:151 [in Tennenbaum.Peano]
X:152 [in Tennenbaum.FOL]
x:155 [in Tennenbaum.FOL]
x:157 [in Tennenbaum.Peano]
x:16 [in Tennenbaum.NumberTheory]
X:16 [in Tennenbaum.Tennenbaum]
x:164 [in Tennenbaum.Peano]
x:165 [in Tennenbaum.FOL]
x:166 [in Tennenbaum.Tennenbaum]
x:167 [in Tennenbaum.Peano]
x:172 [in Tennenbaum.Tennenbaum]
x:175 [in Tennenbaum.Peano]
x:178 [in Tennenbaum.Peano]
x:178 [in Tennenbaum.Tennenbaum]
x:179 [in Tennenbaum.Tennenbaum]
x:18 [in Tennenbaum.CantorPairing]
x:18 [in Tennenbaum.NumberTheory]
x:18 [in Tennenbaum.Tennenbaum]
x:181 [in Tennenbaum.Peano]
x:184 [in Tennenbaum.Peano]
x:187 [in Tennenbaum.Peano]
x:19 [in Tennenbaum.CantorPairing]
x:19 [in Tennenbaum.Tennenbaum]
x:190 [in Tennenbaum.Peano]
x:2 [in Tennenbaum.NumberTheory]
X:2 [in Tennenbaum.Tennenbaum]
x:2 [in Tennenbaum.FOL]
x:20 [in Tennenbaum.NumberTheory]
x:20 [in Tennenbaum.CTT]
x:20 [in Tennenbaum.Tennenbaum]
x:211 [in Tennenbaum.Peano]
x:215 [in Tennenbaum.Peano]
x:217 [in Tennenbaum.Peano]
x:22 [in Tennenbaum.CantorPairing]
X:227 [in Tennenbaum.FOL]
X:229 [in Tennenbaum.Peano]
X:229 [in Tennenbaum.Deduction]
x:230 [in Tennenbaum.FOL]
x:232 [in Tennenbaum.Peano]
x:232 [in Tennenbaum.Deduction]
X:233 [in Tennenbaum.FOL]
X:234 [in Tennenbaum.Deduction]
X:235 [in Tennenbaum.Peano]
x:236 [in Tennenbaum.Tennenbaum]
x:237 [in Tennenbaum.FOL]
x:237 [in Tennenbaum.Deduction]
x:238 [in Tennenbaum.Peano]
x:238 [in Tennenbaum.FOL]
x:24 [in Tennenbaum.CTT]
x:240 [in Tennenbaum.Peano]
x:246 [in Tennenbaum.FOL]
X:248 [in Tennenbaum.FOL]
X:25 [in Tennenbaum.Tennenbaum]
x:252 [in Tennenbaum.FOL]
X:254 [in Tennenbaum.FOL]
x:26 [in Tennenbaum.NumberTheory]
x:26 [in Tennenbaum.CTT]
X:261 [in Tennenbaum.Peano]
x:27 [in Tennenbaum.Tennenbaum]
x:271 [in Tennenbaum.Peano]
x:273 [in Tennenbaum.Peano]
x:273 [in Tennenbaum.Tennenbaum]
x:275 [in Tennenbaum.Tennenbaum]
x:276 [in Tennenbaum.Peano]
x:277 [in Tennenbaum.Tennenbaum]
x:28 [in Tennenbaum.LogicFacts]
x:28 [in Tennenbaum.CTT]
x:28 [in Tennenbaum.Tennenbaum]
x:280 [in Tennenbaum.Tennenbaum]
X:283 [in Tennenbaum.FOL]
x:286 [in Tennenbaum.Peano]
x:287 [in Tennenbaum.Peano]
x:289 [in Tennenbaum.Peano]
x:289 [in Tennenbaum.FOL]
x:29 [in Tennenbaum.LogicFacts]
x:291 [in Tennenbaum.Peano]
x:293 [in Tennenbaum.Peano]
x:295 [in Tennenbaum.Peano]
X:295 [in Tennenbaum.FOL]
x:297 [in Tennenbaum.Peano]
x:297 [in Tennenbaum.FOL]
x:298 [in Tennenbaum.Tennenbaum]
x:3 [in Tennenbaum.NumberTheory]
x:30 [in Tennenbaum.LogicFacts]
X:302 [in Tennenbaum.FOL]
x:306 [in Tennenbaum.FOL]
X:307 [in Tennenbaum.Peano]
X:307 [in Tennenbaum.FOL]
X:309 [in Tennenbaum.Peano]
x:309 [in Tennenbaum.Tennenbaum]
x:31 [in Tennenbaum.NumberTheory]
x:31 [in Tennenbaum.CTT]
x:31 [in Tennenbaum.Tennenbaum]
X:311 [in Tennenbaum.Peano]
x:312 [in Tennenbaum.FOL]
X:313 [in Tennenbaum.Peano]
x:313 [in Tennenbaum.Tennenbaum]
X:318 [in Tennenbaum.Peano]
X:323 [in Tennenbaum.Peano]
X:326 [in Tennenbaum.Peano]
X:329 [in Tennenbaum.Peano]
x:33 [in Tennenbaum.LogicFacts]
X:33 [in Tennenbaum.Tennenbaum]
X:332 [in Tennenbaum.Peano]
x:337 [in Tennenbaum.Peano]
x:337 [in Tennenbaum.Tennenbaum]
x:339 [in Tennenbaum.Peano]
x:34 [in Tennenbaum.LogicFacts]
x:34 [in Tennenbaum.CTT]
x:341 [in Tennenbaum.Peano]
x:345 [in Tennenbaum.Peano]
x:347 [in Tennenbaum.Peano]
x:348 [in Tennenbaum.Tennenbaum]
x:349 [in Tennenbaum.Peano]
x:35 [in Tennenbaum.CantorPairing]
x:35 [in Tennenbaum.NumberTheory]
x:351 [in Tennenbaum.Peano]
x:36 [in Tennenbaum.Tennenbaum]
x:365 [in Tennenbaum.Tennenbaum]
X:367 [in Tennenbaum.Tennenbaum]
x:37 [in Tennenbaum.NumberTheory]
x:37 [in Tennenbaum.LogicFacts]
X:372 [in Tennenbaum.Tennenbaum]
x:38 [in Tennenbaum.CantorPairing]
X:38 [in Tennenbaum.Tennenbaum]
x:387 [in Tennenbaum.Tennenbaum]
x:39 [in Tennenbaum.CTT]
x:398 [in Tennenbaum.Tennenbaum]
x:4 [in Tennenbaum.CantorPairing]
X:4 [in Tennenbaum.LogicFacts]
x:40 [in Tennenbaum.NumberTheory]
x:40 [in Tennenbaum.LogicFacts]
x:40 [in Tennenbaum.Tennenbaum]
x:400 [in Tennenbaum.Tennenbaum]
X:41 [in Tennenbaum.Tennenbaum]
x:411 [in Tennenbaum.Tennenbaum]
x:412 [in Tennenbaum.Tennenbaum]
x:42 [in Tennenbaum.Peano]
x:42 [in Tennenbaum.Tennenbaum]
x:43 [in Tennenbaum.LogicFacts]
x:44 [in Tennenbaum.NumberTheory]
x:44 [in Tennenbaum.LogicFacts]
X:44 [in Tennenbaum.Tennenbaum]
x:45 [in Tennenbaum.CTT]
x:45 [in Tennenbaum.Tennenbaum]
x:46 [in Tennenbaum.NumberTheory]
X:47 [in Tennenbaum.Tennenbaum]
x:48 [in Tennenbaum.NumberTheory]
x:49 [in Tennenbaum.Tennenbaum]
x:50 [in Tennenbaum.NumberTheory]
X:51 [in Tennenbaum.Tennenbaum]
x:53 [in Tennenbaum.LogicFacts]
x:54 [in Tennenbaum.Peano]
x:54 [in Tennenbaum.LogicFacts]
X:54 [in Tennenbaum.Tennenbaum]
x:55 [in Tennenbaum.Peano]
x:55 [in Tennenbaum.LogicFacts]
x:57 [in Tennenbaum.Peano]
x:57 [in Tennenbaum.LogicFacts]
x:57 [in Tennenbaum.Tennenbaum]
x:58 [in Tennenbaum.Tennenbaum]
x:59 [in Tennenbaum.NumberTheory]
x:59 [in Tennenbaum.LogicFacts]
x:59 [in Tennenbaum.Tennenbaum]
X:6 [in Tennenbaum.CantorPairing]
x:6 [in Tennenbaum.NumberTheory]
x:6 [in Tennenbaum.LogicFacts]
x:6 [in Tennenbaum.Tennenbaum]
X:6 [in Tennenbaum.FOL]
x:61 [in Tennenbaum.NumberTheory]
x:61 [in Tennenbaum.LogicFacts]
x:62 [in Tennenbaum.Tennenbaum]
x:63 [in Tennenbaum.Tennenbaum]
x:64 [in Tennenbaum.LogicFacts]
x:64 [in Tennenbaum.Tennenbaum]
x:65 [in Tennenbaum.Tarski]
x:65 [in Tennenbaum.Tennenbaum]
x:66 [in Tennenbaum.NumberTheory]
x:66 [in Tennenbaum.Tennenbaum]
x:67 [in Tennenbaum.LogicFacts]
x:67 [in Tennenbaum.FOL]
X:7 [in Tennenbaum.LogicFacts]
x:71 [in Tennenbaum.Peano]
x:73 [in Tennenbaum.Tarski]
x:73 [in Tennenbaum.Peano]
x:75 [in Tennenbaum.Peano]
x:78 [in Tennenbaum.Tarski]
x:79 [in Tennenbaum.NumberTheory]
X:8 [in Tennenbaum.Tennenbaum]
x:83 [in Tennenbaum.FOL]
x:87 [in Tennenbaum.Tarski]
x:87 [in Tennenbaum.NumberTheory]
x:89 [in Tennenbaum.NumberTheory]
x:89 [in Tennenbaum.FOL]
x:91 [in Tennenbaum.NumberTheory]
x:92 [in Tennenbaum.NumberTheory]
x:96 [in Tennenbaum.FOL]
x:99 [in Tennenbaum.Peano]
Y
y1:279 [in Tennenbaum.Peano]y1:283 [in Tennenbaum.Peano]
y2:281 [in Tennenbaum.Peano]
y2:285 [in Tennenbaum.Peano]
y:100 [in Tennenbaum.Peano]
y:11 [in Tennenbaum.NumberTheory]
y:119 [in Tennenbaum.Peano]
Y:12 [in Tennenbaum.CantorPairing]
y:12 [in Tennenbaum.LogicFacts]
y:126 [in Tennenbaum.Peano]
y:13 [in Tennenbaum.NumberTheory]
y:14 [in Tennenbaum.LogicFacts]
y:140 [in Tennenbaum.Peano]
y:142 [in Tennenbaum.Peano]
y:142 [in Tennenbaum.Tennenbaum]
y:148 [in Tennenbaum.Peano]
y:15 [in Tennenbaum.NumberTheory]
y:150 [in Tennenbaum.Peano]
y:152 [in Tennenbaum.Peano]
y:158 [in Tennenbaum.Peano]
y:165 [in Tennenbaum.Peano]
y:167 [in Tennenbaum.Tennenbaum]
y:168 [in Tennenbaum.Peano]
y:17 [in Tennenbaum.NumberTheory]
y:177 [in Tennenbaum.Peano]
y:180 [in Tennenbaum.Peano]
y:182 [in Tennenbaum.Peano]
y:185 [in Tennenbaum.Peano]
y:188 [in Tennenbaum.Peano]
y:19 [in Tennenbaum.NumberTheory]
Y:2 [in Tennenbaum.CantorPairing]
Y:2 [in Tennenbaum.LogicFacts]
y:20 [in Tennenbaum.CantorPairing]
y:21 [in Tennenbaum.CantorPairing]
y:212 [in Tennenbaum.Peano]
y:216 [in Tennenbaum.Peano]
y:218 [in Tennenbaum.Peano]
y:231 [in Tennenbaum.FOL]
y:247 [in Tennenbaum.FOL]
y:25 [in Tennenbaum.CTT]
y:253 [in Tennenbaum.FOL]
y:272 [in Tennenbaum.Peano]
y:274 [in Tennenbaum.Peano]
y:274 [in Tennenbaum.Tennenbaum]
y:276 [in Tennenbaum.Tennenbaum]
y:277 [in Tennenbaum.Peano]
y:278 [in Tennenbaum.Tennenbaum]
y:281 [in Tennenbaum.Tennenbaum]
y:288 [in Tennenbaum.Peano]
y:290 [in Tennenbaum.Peano]
y:292 [in Tennenbaum.Peano]
y:294 [in Tennenbaum.Peano]
y:296 [in Tennenbaum.Peano]
Y:296 [in Tennenbaum.FOL]
y:298 [in Tennenbaum.Peano]
y:299 [in Tennenbaum.Tennenbaum]
Y:3 [in Tennenbaum.Tennenbaum]
Y:314 [in Tennenbaum.Peano]
Y:319 [in Tennenbaum.Peano]
y:32 [in Tennenbaum.NumberTheory]
y:32 [in Tennenbaum.CTT]
y:338 [in Tennenbaum.Peano]
y:34 [in Tennenbaum.CantorPairing]
y:34 [in Tennenbaum.NumberTheory]
y:340 [in Tennenbaum.Peano]
y:342 [in Tennenbaum.Peano]
y:346 [in Tennenbaum.Peano]
y:35 [in Tennenbaum.CTT]
y:350 [in Tennenbaum.Peano]
y:352 [in Tennenbaum.Peano]
y:366 [in Tennenbaum.Tennenbaum]
y:39 [in Tennenbaum.CantorPairing]
y:4 [in Tennenbaum.NumberTheory]
y:40 [in Tennenbaum.CTT]
y:401 [in Tennenbaum.Tennenbaum]
y:409 [in Tennenbaum.Tennenbaum]
y:410 [in Tennenbaum.Tennenbaum]
y:43 [in Tennenbaum.Tennenbaum]
y:45 [in Tennenbaum.NumberTheory]
y:46 [in Tennenbaum.CTT]
y:46 [in Tennenbaum.Tennenbaum]
y:47 [in Tennenbaum.NumberTheory]
y:49 [in Tennenbaum.NumberTheory]
y:5 [in Tennenbaum.Tennenbaum]
y:56 [in Tennenbaum.Peano]
y:58 [in Tennenbaum.Peano]
y:58 [in Tennenbaum.LogicFacts]
y:60 [in Tennenbaum.LogicFacts]
y:62 [in Tennenbaum.NumberTheory]
y:62 [in Tennenbaum.LogicFacts]
y:65 [in Tennenbaum.LogicFacts]
y:68 [in Tennenbaum.LogicFacts]
Y:7 [in Tennenbaum.CantorPairing]
Y:7 [in Tennenbaum.FOL]
y:72 [in Tennenbaum.Peano]
y:74 [in Tennenbaum.Peano]
y:76 [in Tennenbaum.Peano]
y:80 [in Tennenbaum.NumberTheory]
y:9 [in Tennenbaum.NumberTheory]
Z
z:101 [in Tennenbaum.Peano]z:120 [in Tennenbaum.Peano]
z:127 [in Tennenbaum.Peano]
z:176 [in Tennenbaum.Peano]
z:179 [in Tennenbaum.Peano]
z:275 [in Tennenbaum.Peano]
z:33 [in Tennenbaum.CTT]
z:36 [in Tennenbaum.CTT]
z:41 [in Tennenbaum.CTT]
Z:8 [in Tennenbaum.FOL]
other
Γ1:93 [in Tennenbaum.Deduction]Γ2:94 [in Tennenbaum.Deduction]
Σ_preds:59 [in Tennenbaum.Tarski]
Σ_funcs:58 [in Tennenbaum.Tarski]
Σ_preds:52 [in Tennenbaum.Tarski]
Σ_funcs:51 [in Tennenbaum.Tarski]
Σ_preds:27 [in Tennenbaum.Tarski]
Σ_funcs:26 [in Tennenbaum.Tarski]
Σ_preds:6 [in Tennenbaum.Tarski]
Σ_funcs:5 [in Tennenbaum.Tarski]
Σ_preds:330 [in Tennenbaum.FOL]
Σ_funcs:329 [in Tennenbaum.FOL]
Σ_preds:273 [in Tennenbaum.FOL]
Σ_funcs:272 [in Tennenbaum.FOL]
Σ_preds:258 [in Tennenbaum.FOL]
Σ_funcs:257 [in Tennenbaum.FOL]
Σ_preds:160 [in Tennenbaum.FOL]
Σ_funcs:159 [in Tennenbaum.FOL]
Σ_preds:98 [in Tennenbaum.FOL]
Σ_funcs:97 [in Tennenbaum.FOL]
Σ_preds:26 [in Tennenbaum.FOL]
Σ_funcs:18 [in Tennenbaum.FOL]
Σ_preds:151 [in Tennenbaum.Deduction]
Σ_funcs:150 [in Tennenbaum.Deduction]
Σ_preds:144 [in Tennenbaum.Deduction]
Σ_funcs:143 [in Tennenbaum.Deduction]
Σ_preds:110 [in Tennenbaum.Deduction]
Σ_funcs:109 [in Tennenbaum.Deduction]
Σ_preds:87 [in Tennenbaum.Deduction]
Σ_funcs:86 [in Tennenbaum.Deduction]
Σ_preds:4 [in Tennenbaum.Deduction]
Σ_funcs:3 [in Tennenbaum.Deduction]
α:103 [in Tennenbaum.Tennenbaum]
α:105 [in Tennenbaum.Tennenbaum]
α:106 [in Tennenbaum.Tennenbaum]
α:110 [in Tennenbaum.Tennenbaum]
α:113 [in Tennenbaum.Tennenbaum]
α:135 [in Tennenbaum.Tennenbaum]
α:153 [in Tennenbaum.Tennenbaum]
α:181 [in Tennenbaum.Tennenbaum]
α:183 [in Tennenbaum.Tennenbaum]
α:185 [in Tennenbaum.Tennenbaum]
α:209 [in Tennenbaum.Tennenbaum]
α:216 [in Tennenbaum.Tennenbaum]
α:228 [in Tennenbaum.Tennenbaum]
α:29 [in Tennenbaum.Peano]
α:338 [in Tennenbaum.Tennenbaum]
α:343 [in Tennenbaum.Tennenbaum]
α:350 [in Tennenbaum.Tennenbaum]
α:40 [in Tennenbaum.Peano]
α:73 [in Tennenbaum.Tennenbaum]
α:74 [in Tennenbaum.Tennenbaum]
α:82 [in Tennenbaum.Tennenbaum]
α:85 [in Tennenbaum.Tennenbaum]
α:88 [in Tennenbaum.Tennenbaum]
α:94 [in Tennenbaum.Tennenbaum]
α:96 [in Tennenbaum.Tennenbaum]
α:98 [in Tennenbaum.Tennenbaum]
β:107 [in Tennenbaum.Tennenbaum]
β:111 [in Tennenbaum.Tennenbaum]
β:210 [in Tennenbaum.Tennenbaum]
β:217 [in Tennenbaum.Tennenbaum]
β:229 [in Tennenbaum.Tennenbaum]
β:83 [in Tennenbaum.Tennenbaum]
β:86 [in Tennenbaum.Tennenbaum]
β:89 [in Tennenbaum.Tennenbaum]
ρ:240 [in Tennenbaum.Tennenbaum]
ρ:264 [in Tennenbaum.Tennenbaum]
σ:16 [in Tennenbaum.CantorPairing]
σ:22 [in Tennenbaum.FOL]
σ:55 [in Tennenbaum.FOL]
σ:57 [in Tennenbaum.FOL]
φ:41 [in Tennenbaum.FOL]
φ:43 [in Tennenbaum.FOL]
φ:47 [in Tennenbaum.FOL]
ψ:171 [in Tennenbaum.Tennenbaum]
ψ:48 [in Tennenbaum.FOL]
ϕ:114 [in Tennenbaum.Tennenbaum]
ϕ:143 [in Tennenbaum.Tennenbaum]
ϕ:144 [in Tennenbaum.Tennenbaum]
ϕ:174 [in Tennenbaum.Tennenbaum]
ϕ:177 [in Tennenbaum.Tennenbaum]
ϕ:205 [in Tennenbaum.Tennenbaum]
ϕ:212 [in Tennenbaum.Tennenbaum]
ϕ:238 [in Tennenbaum.Tennenbaum]
ϕ:262 [in Tennenbaum.Tennenbaum]
ϕ:323 [in Tennenbaum.Tennenbaum]
ϕ:324 [in Tennenbaum.Tennenbaum]
ϕ:329 [in Tennenbaum.Tennenbaum]
ϕ:334 [in Tennenbaum.Tennenbaum]
ϕ:399 [in Tennenbaum.Tennenbaum]
Variable Index
C
Closed.axioms [in Tennenbaum.Tennenbaum]Closed.D [in Tennenbaum.Tennenbaum]
Closed.Hcl [in Tennenbaum.Tennenbaum]
Closed.H0 [in Tennenbaum.Tennenbaum]
Closed.I [in Tennenbaum.Tennenbaum]
Closed.phi [in Tennenbaum.Tennenbaum]
E
Enumerability.enum_quantop' [in Tennenbaum.FOL]Enumerability.enum_binop' [in Tennenbaum.FOL]
Enumerability.enum_Preds' [in Tennenbaum.FOL]
Enumerability.enum_Funcs' [in Tennenbaum.FOL]
Enumerability.enum_Preds' [in Tennenbaum.Deduction]
Enumerability.enum_Funcs' [in Tennenbaum.Deduction]
Enumerability.eq_dec_Preds [in Tennenbaum.Deduction]
Enumerability.eq_dec_Funcs [in Tennenbaum.Deduction]
Enumerability.list_quantop [in Tennenbaum.FOL]
Enumerability.list_binop [in Tennenbaum.FOL]
Enumerability.list_Preds [in Tennenbaum.FOL]
Enumerability.list_Funcs [in Tennenbaum.FOL]
Enumerability.list_Preds [in Tennenbaum.Deduction]
Enumerability.list_Funcs [in Tennenbaum.Deduction]
EqDec.eq_dec_quantop [in Tennenbaum.FOL]
EqDec.eq_dec_binop [in Tennenbaum.FOL]
EqDec.eq_dec_Preds [in Tennenbaum.FOL]
EqDec.eq_dec_Funcs [in Tennenbaum.FOL]
H
Homomorphism.m [in Tennenbaum.NumberTheory]M
Models.D [in Tennenbaum.Peano]Models.I [in Tennenbaum.Peano]
Models.PA_Model.Induction.pred [in Tennenbaum.Peano]
Models.PA_Model.Induction.phi [in Tennenbaum.Peano]
N
ND.p [in Tennenbaum.Peano]Q
Q_prv.G [in Tennenbaum.Peano]Q_prv.Gamma [in Tennenbaum.Peano]
Q_prv.p [in Tennenbaum.Peano]
Q_prv.G [in Tennenbaum.Peano]
Q_prv.Gamma [in Tennenbaum.Peano]
Q_prv.p [in Tennenbaum.Peano]
S
Soundness.LEM [in Tennenbaum.Deduction]T
Tarski.D [in Tennenbaum.Tarski]Tarski.I [in Tennenbaum.Tarski]
Tarski.Semantics.domain [in Tennenbaum.Tarski]
Tennenbaum.axioms [in Tennenbaum.Tennenbaum]
Tennenbaum.D [in Tennenbaum.Tennenbaum]
Tennenbaum.dec_eq [in Tennenbaum.Tennenbaum]
Tennenbaum.I [in Tennenbaum.Tennenbaum]
Tennenbaum.Insep.surj_form_ [in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm.Coding [in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm.Hψ [in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm.ψ [in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.Hα [in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.nStd [in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.stable_std [in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill.α [in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1.binary_α [in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1.Δ0_α [in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1.α [in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hypoth.nonStd [in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hypoth.stable_std [in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hψ [in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.ψ [in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill.nnnStd [in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill.Hα [in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill.α [in Tennenbaum.Tennenbaum]
U
Uniqueness.m [in Tennenbaum.NumberTheory]W
WitnessOperator.Dec_q [in Tennenbaum.LogicFacts]WitnessOperator.q [in Tennenbaum.LogicFacts]
Library Index
C
CantorPairingCTT
D
DeductionF
FOLL
LogicFactsN
NumberTheoryP
PeanoT
TarskiTennenbaum
Lemma Index
A
Add_rec [in Tennenbaum.Peano]add_le_mono [in Tennenbaum.Peano]
add_lt_mono [in Tennenbaum.Peano]
add_eq [in Tennenbaum.Peano]
add_asso [in Tennenbaum.Peano]
add_comm [in Tennenbaum.Peano]
add_rec_r [in Tennenbaum.Peano]
add_zero_r [in Tennenbaum.Peano]
add_rec [in Tennenbaum.Peano]
add_zero [in Tennenbaum.Peano]
AP_EQ [in Tennenbaum.Tennenbaum]
B
better_leibniz [in Tennenbaum.Peano]Bij_Nat_NatNat [in Tennenbaum.CantorPairing]
bool_cases [in Tennenbaum.CTT]
bool_disjoint [in Tennenbaum.CTT]
bounded_S_forall [in Tennenbaum.Tarski]
bounded_S_exists [in Tennenbaum.Tarski]
bounded_eval_t [in Tennenbaum.Tarski]
bounded_exists_Δ0_equiv [in Tennenbaum.Tennenbaum]
bounded_t_dec [in Tennenbaum.FOL]
bounded_up [in Tennenbaum.FOL]
bounded_up_t [in Tennenbaum.FOL]
bounded_subst [in Tennenbaum.FOL]
bounded_subst_t [in Tennenbaum.FOL]
bound_ext [in Tennenbaum.Tarski]
C
CantorBound [in Tennenbaum.CantorPairing]CE [in Tennenbaum.Deduction]
closed_term_is_num [in Tennenbaum.Peano]
closed_num [in Tennenbaum.Tennenbaum]
code_next [in Tennenbaum.CantorPairing]
combine_context [in Tennenbaum.Deduction]
Currying [in Tennenbaum.CTT]
D
dec_prime [in Tennenbaum.NumberTheory]dec_irred_factor [in Tennenbaum.NumberTheory]
dec_irred [in Tennenbaum.NumberTheory]
dec_lt_bounded_forall [in Tennenbaum.LogicFacts]
dec_lt_bounded_exist [in Tennenbaum.LogicFacts]
dec_lt_bounded_exist' [in Tennenbaum.LogicFacts]
dec_lt_bounded_sig [in Tennenbaum.LogicFacts]
dec_neg [in Tennenbaum.LogicFacts]
dec_imp [in Tennenbaum.LogicFacts]
dec_disj [in Tennenbaum.LogicFacts]
dec_conj [in Tennenbaum.LogicFacts]
dec_transport [in Tennenbaum.LogicFacts]
dec_Divides [in Tennenbaum.Tennenbaum]
dec_num_lt [in Tennenbaum.Tennenbaum]
dec_Divides_temp [in Tennenbaum.Tennenbaum]
dec_Divides' [in Tennenbaum.Tennenbaum]
dec_closed_Δ0 [in Tennenbaum.Tennenbaum]
Dec_nat_equiv [in Tennenbaum.Tennenbaum]
Dec_equiv [in Tennenbaum.Tennenbaum]
dec_form_dep [in Tennenbaum.FOL]
dec_vec_in [in Tennenbaum.FOL]
DE' [in Tennenbaum.Deduction]
Disjoint_AB [in Tennenbaum.Tennenbaum]
distributive [in Tennenbaum.Peano]
Divides_num [in Tennenbaum.Tennenbaum]
Div_lt [in Tennenbaum.NumberTheory]
DN [in Tennenbaum.Tennenbaum]
DN_exists [in Tennenbaum.Tennenbaum]
DN_implication [in Tennenbaum.Tennenbaum]
DN_forall_stable [in Tennenbaum.Tennenbaum]
E
enumerable_form [in Tennenbaum.Tennenbaum]enumerable_Q_prv [in Tennenbaum.Tennenbaum]
enumT_term [in Tennenbaum.FOL]
enumT_quantop [in Tennenbaum.Deduction]
enumT_binop [in Tennenbaum.Deduction]
enum_surj [in Tennenbaum.Tennenbaum]
enum_form [in Tennenbaum.FOL]
enum_term [in Tennenbaum.FOL]
enum_tprv [in Tennenbaum.Deduction]
enum_containsL [in Tennenbaum.Deduction]
enum_p [in Tennenbaum.Deduction]
enum_el [in Tennenbaum.Deduction]
enum_prv [in Tennenbaum.Deduction]
eq_mult [in Tennenbaum.Peano]
eq_add [in Tennenbaum.Peano]
eq_succ [in Tennenbaum.Peano]
eq_dec [in Tennenbaum.Peano]
eq_trans [in Tennenbaum.Peano]
eq_sym [in Tennenbaum.Peano]
eq_dec_nat [in Tennenbaum.LogicFacts]
eq_bool_agree [in Tennenbaum.CTT]
eq_trans [in Tennenbaum.CTT]
eq_sym [in Tennenbaum.CTT]
eq_stable [in Tennenbaum.Tennenbaum]
eq_dep_falsity [in Tennenbaum.FOL]
eval_comp [in Tennenbaum.Tarski]
eval_ext [in Tennenbaum.Tarski]
eval_num [in Tennenbaum.Peano]
F
Factor [in Tennenbaum.NumberTheory]Fac_eq [in Tennenbaum.NumberTheory]
Fac_unique [in Tennenbaum.NumberTheory]
fac1 [in Tennenbaum.NumberTheory]
fac2 [in Tennenbaum.NumberTheory]
fac3 [in Tennenbaum.NumberTheory]
Faster1 [in Tennenbaum.Tennenbaum]
Faster2 [in Tennenbaum.Tennenbaum]
Faster3 [in Tennenbaum.Peano]
find_bounded_L [in Tennenbaum.FOL]
find_bounded [in Tennenbaum.FOL]
find_bounded_t [in Tennenbaum.FOL]
find_bounded_step [in Tennenbaum.FOL]
form_ind_falsity_on [in Tennenbaum.FOL]
G
grounded [in Tennenbaum.LogicFacts]I
iEuclid [in Tennenbaum.Peano]iEuclid' [in Tennenbaum.Peano]
iFac_unique [in Tennenbaum.Peano]
iFac_unique1 [in Tennenbaum.Peano]
impl_sat' [in Tennenbaum.Tarski]
impl_sat [in Tennenbaum.Tarski]
imps [in Tennenbaum.Deduction]
incl_app [in Tennenbaum.Deduction]
induction [in Tennenbaum.Peano]
induction1 [in Tennenbaum.Peano]
induction2 [in Tennenbaum.Peano]
infty_irred [in Tennenbaum.NumberTheory]
inj_decode [in Tennenbaum.CantorPairing]
inj_next [in Tennenbaum.CantorPairing]
inj_Irred [in Tennenbaum.NumberTheory]
inj_pair2_eq_dec' [in Tennenbaum.FOL]
Inseparable [in Tennenbaum.Tennenbaum]
Insep_2 [in Tennenbaum.Tennenbaum]
Insep_3 [in Tennenbaum.Tennenbaum]
Insep_1 [in Tennenbaum.Tennenbaum]
inu_nat_id [in Tennenbaum.Peano]
inu_mult_hom [in Tennenbaum.Peano]
inu_add_hom [in Tennenbaum.Peano]
inu_inj [in Tennenbaum.Peano]
inversion_Δ0_forall [in Tennenbaum.Tennenbaum]
inversion_Δ0_bin [in Tennenbaum.Tennenbaum]
inversion_bounded_bin [in Tennenbaum.Tennenbaum]
inv_cd [in Tennenbaum.CantorPairing]
inv_dc [in Tennenbaum.CantorPairing]
in_hd_tl [in Tennenbaum.Peano]
in_hd [in Tennenbaum.Peano]
irred_Irred [in Tennenbaum.NumberTheory]
irred_integral_domain [in Tennenbaum.NumberTheory]
irred_Mod_eq [in Tennenbaum.NumberTheory]
irred_factor [in Tennenbaum.NumberTheory]
irred_bounded [in Tennenbaum.NumberTheory]
irred1 [in Tennenbaum.NumberTheory]
iter_switch [in Tennenbaum.Peano]
iter_switch [in Tennenbaum.FOL]
L
LEM_bounded_exist [in Tennenbaum.Tennenbaum]LEM_bounded_exist_sat' [in Tennenbaum.Tennenbaum]
LEM_bounded_exist_sat [in Tennenbaum.Tennenbaum]
LEM_binary [in Tennenbaum.Tennenbaum]
LEM_num_lt [in Tennenbaum.Tennenbaum]
LEM_Divides [in Tennenbaum.Tennenbaum]
lessthen_num [in Tennenbaum.Peano]
le_le_trans [in Tennenbaum.Peano]
list_prod_in [in Tennenbaum.FOL]
lt_nat_equiv [in Tennenbaum.NumberTheory]
lt_rect [in Tennenbaum.NumberTheory]
lt_le_trans [in Tennenbaum.Peano]
lt_S [in Tennenbaum.Peano]
lt_le_equiv1 [in Tennenbaum.Peano]
lt_neq [in Tennenbaum.Peano]
lt_SS [in Tennenbaum.Peano]
lt_dec [in Tennenbaum.LogicFacts]
lt_equiv [in Tennenbaum.Tennenbaum]
L_form_cml [in Tennenbaum.FOL]
L_term_cml [in Tennenbaum.FOL]
M
map_tl [in Tennenbaum.Peano]map_hd [in Tennenbaum.Peano]
McCarty_ [in Tennenbaum.Tennenbaum]
McCarty_nat [in Tennenbaum.Tennenbaum]
McCarty' [in Tennenbaum.Tennenbaum]
ModMod_is_Mod [in Tennenbaum.NumberTheory]
Mod_mult_hom [in Tennenbaum.NumberTheory]
Mod_mult_hom_l [in Tennenbaum.NumberTheory]
Mod_add_hom [in Tennenbaum.NumberTheory]
Mod_plus_multiple [in Tennenbaum.NumberTheory]
Mod_id [in Tennenbaum.NumberTheory]
Mod_le [in Tennenbaum.NumberTheory]
Mod_divides [in Tennenbaum.NumberTheory]
Mod_lt [in Tennenbaum.NumberTheory]
Mod_bound [in Tennenbaum.NumberTheory]
Mod0_is_0 [in Tennenbaum.NumberTheory]
mono_inj [in Tennenbaum.NumberTheory]
Mult_rec [in Tennenbaum.Peano]
mult_le_mono [in Tennenbaum.Peano]
mult_asso [in Tennenbaum.Peano]
mult_comm [in Tennenbaum.Peano]
mult_rec_r [in Tennenbaum.Peano]
mult_zero_r [in Tennenbaum.Peano]
mult_rec [in Tennenbaum.Peano]
mult_zero [in Tennenbaum.Peano]
N
neg_lt_bounded_forall [in Tennenbaum.LogicFacts]neg_imp [in Tennenbaum.LogicFacts]
neg_and [in Tennenbaum.LogicFacts]
neg_equiv_Δ0 [in Tennenbaum.Tennenbaum]
NNN_N [in Tennenbaum.Tennenbaum]
nolessthen_zero [in Tennenbaum.Peano]
nolessthen_zero [in Tennenbaum.Tennenbaum]
not_lt_zero_prv [in Tennenbaum.Peano]
num_lt_dec [in Tennenbaum.Peano]
num_nlt [in Tennenbaum.Peano]
num_lt [in Tennenbaum.Peano]
num_eq_dec [in Tennenbaum.Peano]
num_neq [in Tennenbaum.Peano]
num_eq [in Tennenbaum.Peano]
num_lt_prv [in Tennenbaum.Peano]
num_mult_homomorphism [in Tennenbaum.Peano]
num_add_homomorphism [in Tennenbaum.Peano]
num_subst [in Tennenbaum.Peano]
num_lt_nonStd [in Tennenbaum.Tennenbaum]
n00_next [in Tennenbaum.CantorPairing]
O
on_std_equiv [in Tennenbaum.Tennenbaum]Overspill [in Tennenbaum.Tennenbaum]
Overspill_DN [in Tennenbaum.Tennenbaum]
Overspill_DN' [in Tennenbaum.Tennenbaum]
P
PA_std_axioms [in Tennenbaum.Peano]PA_consistent [in Tennenbaum.Tennenbaum]
Peirce [in Tennenbaum.Deduction]
preThm4 [in Tennenbaum.Tennenbaum]
preThm4_nat [in Tennenbaum.Tennenbaum]
preThm4' [in Tennenbaum.Tennenbaum]
preWitness [in Tennenbaum.LogicFacts]
prime_irred_equiv [in Tennenbaum.NumberTheory]
ProductWO [in Tennenbaum.LogicFacts]
Q
qT [in Tennenbaum.LogicFacts]Q_std_axioms [in Tennenbaum.Peano]
Q_Δ0_complete' [in Tennenbaum.Tennenbaum]
Q_Δ0_complete [in Tennenbaum.Tennenbaum]
Q_neg_equiv_Δ0 [in Tennenbaum.Tennenbaum]
Q_dec_closed_Δ0' [in Tennenbaum.Tennenbaum]
Q_dec_closed_Δ0 [in Tennenbaum.Tennenbaum]
Q_neg_equiv [in Tennenbaum.Tennenbaum]
Q_contra [in Tennenbaum.Tennenbaum]
Q_consistent [in Tennenbaum.Tennenbaum]
R
reflexivity [in Tennenbaum.Peano]S
sat_closed [in Tennenbaum.Tarski]sat_single [in Tennenbaum.Tarski]
sat_subst [in Tennenbaum.Tarski]
sat_comp [in Tennenbaum.Tarski]
sat_ext' [in Tennenbaum.Tarski]
sat_ext [in Tennenbaum.Tarski]
size_rect [in Tennenbaum.CantorPairing]
soundness [in Tennenbaum.Deduction]
soundness_class' [in Tennenbaum.Deduction]
soundness_class [in Tennenbaum.Deduction]
soundness' [in Tennenbaum.Deduction]
stable_lemma [in Tennenbaum.Tennenbaum]
stdModel_equiv [in Tennenbaum.Tennenbaum]
std_mult' [in Tennenbaum.Tennenbaum]
std_mult [in Tennenbaum.Tennenbaum]
std_add [in Tennenbaum.Tennenbaum]
subst_exist_sat2 [in Tennenbaum.Tarski]
subst_exist_sat [in Tennenbaum.Tarski]
subst_forall_prv [in Tennenbaum.Peano]
subst_exist_prv [in Tennenbaum.Peano]
subst_bounded [in Tennenbaum.Peano]
subst_bounded_term [in Tennenbaum.Peano]
subst_up_var [in Tennenbaum.Peano]
subst_bound [in Tennenbaum.Tennenbaum]
subst_bound_t [in Tennenbaum.Tennenbaum]
subst_Δ0 [in Tennenbaum.Tennenbaum]
subst_shift [in Tennenbaum.FOL]
subst_comp [in Tennenbaum.FOL]
subst_var [in Tennenbaum.FOL]
subst_id [in Tennenbaum.FOL]
subst_ext [in Tennenbaum.FOL]
subst_term_shift [in Tennenbaum.FOL]
subst_term_comp [in Tennenbaum.FOL]
subst_term_var [in Tennenbaum.FOL]
subst_term_id [in Tennenbaum.FOL]
subst_term_ext [in Tennenbaum.FOL]
Succ_inj [in Tennenbaum.Peano]
succ_inj' [in Tennenbaum.Peano]
succ_inj [in Tennenbaum.Peano]
sum_is_zero [in Tennenbaum.Peano]
switch_exists [in Tennenbaum.Tarski]
switch_up_num [in Tennenbaum.Peano]
switch_num [in Tennenbaum.Peano]
switch_nat_num [in Tennenbaum.Tennenbaum]
switch_conj_imp [in Tennenbaum.Deduction]
symmetry [in Tennenbaum.Peano]
T
Tennebaum_ [in Tennenbaum.Tennenbaum]Tennenbaum [in Tennenbaum.Tennenbaum]
Tennenbaum_strenghened2 [in Tennenbaum.Tennenbaum]
Tennenbaum_strenghened1 [in Tennenbaum.Tennenbaum]
Tennenbaum_wo [in Tennenbaum.Tennenbaum]
Tennenbaum_enum [in Tennenbaum.Tennenbaum]
term_lt_dec [in Tennenbaum.Peano]
term_eq_dec [in Tennenbaum.Peano]
term_ind [in Tennenbaum.FOL]
term_rect [in Tennenbaum.FOL]
term_rect' [in Tennenbaum.FOL]
Thm4 [in Tennenbaum.Tennenbaum]
Thm5 [in Tennenbaum.Tennenbaum]
transitivity [in Tennenbaum.Peano]
trichotomy [in Tennenbaum.Peano]
trunc [in Tennenbaum.Tennenbaum]
tsoundness [in Tennenbaum.Deduction]
tsoundness_class [in Tennenbaum.Deduction]
U
unique [in Tennenbaum.NumberTheory]up_decompose [in Tennenbaum.Peano]
up_decompose [in Tennenbaum.FOL]
up_form [in Tennenbaum.FOL]
up_funcomp [in Tennenbaum.FOL]
up_var [in Tennenbaum.FOL]
up_ext [in Tennenbaum.FOL]
up_term [in Tennenbaum.FOL]
V
vecs_from_correct [in Tennenbaum.FOL]vec_in_hd_tl [in Tennenbaum.Peano]
vec_in_hd [in Tennenbaum.Peano]
vec_inv2 [in Tennenbaum.Peano]
vec_inv1 [in Tennenbaum.Peano]
vec_nil_eq [in Tennenbaum.Peano]
vec_map_preimage [in Tennenbaum.Tennenbaum]
vec_forall_cml [in Tennenbaum.FOL]
vec_all_dec [in Tennenbaum.FOL]
vec_cons_inv [in Tennenbaum.FOL]
W
Weak [in Tennenbaum.Deduction]weak_Overspill_DN' [in Tennenbaum.Tennenbaum]
weak_Overspill [in Tennenbaum.Tennenbaum]
weak_std_equiv [in Tennenbaum.Tennenbaum]
Witness [in Tennenbaum.LogicFacts]
Z
zero_or_next [in Tennenbaum.CantorPairing]Zero_succ [in Tennenbaum.Peano]
zero_or_succ [in Tennenbaum.Peano]
zero_succ [in Tennenbaum.Peano]
other
Δ0_absolutness' [in Tennenbaum.Tennenbaum]Δ0_absolutness [in Tennenbaum.Tennenbaum]
Δ0_complete' [in Tennenbaum.Tennenbaum]
Δ0_complete [in Tennenbaum.Tennenbaum]
Σ1_complete [in Tennenbaum.Tennenbaum]
Σ1_complete' [in Tennenbaum.Tennenbaum]
ψ_equiv [in Tennenbaum.Tennenbaum]
ψ_repr [in Tennenbaum.Tennenbaum]
Constructor Index
A
All [in Tennenbaum.Tarski]AllE [in Tennenbaum.Deduction]
AllI [in Tennenbaum.Deduction]
atom [in Tennenbaum.FOL]
B
bin [in Tennenbaum.FOL]bouded_func [in Tennenbaum.FOL]
bounded_falsity [in Tennenbaum.FOL]
bounded_quant [in Tennenbaum.FOL]
bounded_eq [in Tennenbaum.FOL]
bounded_bin [in Tennenbaum.FOL]
bounded_atom [in Tennenbaum.FOL]
bounded_var [in Tennenbaum.FOL]
B_I [in Tennenbaum.Tarski]
C
C [in Tennenbaum.LogicFacts]CE1 [in Tennenbaum.Deduction]
CE2 [in Tennenbaum.Deduction]
CI [in Tennenbaum.Deduction]
class [in Tennenbaum.Deduction]
Conj [in Tennenbaum.Tarski]
Ctx [in Tennenbaum.Deduction]
D
DE [in Tennenbaum.Deduction]Delta_bounded_forall [in Tennenbaum.Tennenbaum]
Delta_bounded_exist [in Tennenbaum.Tennenbaum]
Delta_id [in Tennenbaum.Tennenbaum]
Delta_Impl [in Tennenbaum.Tennenbaum]
Delta_Disj [in Tennenbaum.Tennenbaum]
Delta_Conj [in Tennenbaum.Tennenbaum]
Delta_eq [in Tennenbaum.Tennenbaum]
Delta_fal [in Tennenbaum.Tennenbaum]
Disj [in Tennenbaum.Tarski]
DI1 [in Tennenbaum.Deduction]
DI2 [in Tennenbaum.Deduction]
E
eq [in Tennenbaum.FOL]Ex [in Tennenbaum.Tarski]
ExE [in Tennenbaum.Deduction]
ExI [in Tennenbaum.Deduction]
Exp [in Tennenbaum.Deduction]
F
falsity [in Tennenbaum.FOL]falsity_on [in Tennenbaum.FOL]
falsity_off [in Tennenbaum.FOL]
Forall_cons [in Tennenbaum.FOL]
Forall_nil [in Tennenbaum.FOL]
func [in Tennenbaum.FOL]
I
IE [in Tennenbaum.Deduction]II [in Tennenbaum.Deduction]
Impl [in Tennenbaum.Tarski]
intu [in Tennenbaum.Deduction]
M
Mult [in Tennenbaum.Peano]P
PA_induction [in Tennenbaum.Peano]PA_Q [in Tennenbaum.Peano]
Pc [in Tennenbaum.Deduction]
Plus [in Tennenbaum.Peano]
Q
quant [in Tennenbaum.FOL]S
Sigma_exists [in Tennenbaum.Tennenbaum]Sigma_Delta [in Tennenbaum.Tennenbaum]
Succ [in Tennenbaum.Peano]
V
var [in Tennenbaum.FOL]vec_inS [in Tennenbaum.FOL]
vec_inB [in Tennenbaum.FOL]
Z
Zero [in Tennenbaum.Peano]Projection Index
A
ar_preds [in Tennenbaum.FOL]ar_syms [in Tennenbaum.FOL]
B
binop [in Tennenbaum.FOL]I
i_P [in Tennenbaum.Tarski]i_f [in Tennenbaum.Tarski]
P
preds [in Tennenbaum.FOL]Q
quantop [in Tennenbaum.FOL]S
syms [in Tennenbaum.FOL]Inductive Index
B
bounded [in Tennenbaum.FOL]bounded_t [in Tennenbaum.FOL]
F
falsity_flag [in Tennenbaum.FOL]Forall [in Tennenbaum.FOL]
form [in Tennenbaum.FOL]
full_logic_quant [in Tennenbaum.Tarski]
full_logic_sym [in Tennenbaum.Tarski]
P
PA [in Tennenbaum.Peano]PA_preds [in Tennenbaum.Peano]
PA_funcs [in Tennenbaum.Peano]
peirce [in Tennenbaum.Deduction]
prv [in Tennenbaum.Deduction]
T
T [in Tennenbaum.LogicFacts]term [in Tennenbaum.FOL]
V
vec_in [in Tennenbaum.FOL]Void [in Tennenbaum.CTT]
other
Δ0 [in Tennenbaum.Tennenbaum]Δ0' [in Tennenbaum.Tennenbaum]
Σ1 [in Tennenbaum.Tennenbaum]
Section Index
B
Bounded [in Tennenbaum.FOL]C
Cantor [in Tennenbaum.CantorPairing]Closed [in Tennenbaum.Tennenbaum]
D
Defs [in Tennenbaum.Tarski]Delta0 [in Tennenbaum.Tennenbaum]
E
Enumerability [in Tennenbaum.FOL]Enumerability [in Tennenbaum.Deduction]
EqDec [in Tennenbaum.FOL]
F
fixb [in Tennenbaum.Tarski]fix_signature [in Tennenbaum.FOL]
H
Homomorphism [in Tennenbaum.NumberTheory]I
Incl [in Tennenbaum.Deduction]M
Models [in Tennenbaum.Peano]Models.PA_Model.Euclid [in Tennenbaum.Peano]
Models.PA_Model.Induction [in Tennenbaum.Peano]
Models.PA_Model [in Tennenbaum.Peano]
N
ND [in Tennenbaum.Peano]ND_def [in Tennenbaum.Deduction]
ND_def [in Tennenbaum.Deduction]
P
PrimeDec [in Tennenbaum.NumberTheory]PrimeInf [in Tennenbaum.NumberTheory]
Q
Q_prv [in Tennenbaum.Peano]Q_prv [in Tennenbaum.Peano]
S
Soundness [in Tennenbaum.Deduction]StandartModel [in Tennenbaum.Peano]
Subst [in Tennenbaum.FOL]
T
Tarski [in Tennenbaum.Tarski]Tarski [in Tennenbaum.Tarski]
Tarski.Ext [in Tennenbaum.Tarski]
Tarski.Semantics [in Tennenbaum.Tarski]
Tarski.Substs [in Tennenbaum.Tarski]
Tennenbaum [in Tennenbaum.Tennenbaum]
Tennenbaum.Insep [in Tennenbaum.Tennenbaum]
Tennenbaum.Makholm [in Tennenbaum.Tennenbaum]
Tennenbaum.McCarty [in Tennenbaum.Tennenbaum]
Tennenbaum.Overspill [in Tennenbaum.Tennenbaum]
Tennenbaum.Sigma1 [in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4 [in Tennenbaum.Tennenbaum]
Tennenbaum.Thm4.Hypoth [in Tennenbaum.Tennenbaum]
Tennenbaum.weak_Overspill [in Tennenbaum.Tennenbaum]
U
Uniqueness [in Tennenbaum.NumberTheory]W
WitnessOperator [in Tennenbaum.LogicFacts]Instance Index
D
dec_form [in Tennenbaum.FOL]dec_falsity [in Tennenbaum.FOL]
dec_term [in Tennenbaum.FOL]
dec_vec [in Tennenbaum.FOL]
dec_list [in Tennenbaum.Deduction]
E
enum_form' [in Tennenbaum.Deduction]enum_term' [in Tennenbaum.Deduction]
enum_quantop [in Tennenbaum.Deduction]
enum_binop [in Tennenbaum.Deduction]
eqdec_quantop [in Tennenbaum.Deduction]
eqdec_binop [in Tennenbaum.Deduction]
F
ff [in Tennenbaum.Tennenbaum]P
PA_preds_signature [in Tennenbaum.Peano]PA_funcs_signature [in Tennenbaum.Peano]
Definition Index
A
A [in Tennenbaum.Tennenbaum]Add [in Tennenbaum.CTT]
AP [in Tennenbaum.Tennenbaum]
ax_mult_congr [in Tennenbaum.Peano]
ax_add_congr [in Tennenbaum.Peano]
ax_succ_congr [in Tennenbaum.Peano]
ax_trans [in Tennenbaum.Peano]
ax_sym [in Tennenbaum.Peano]
ax_refl [in Tennenbaum.Peano]
ax_zero_or_succ [in Tennenbaum.Peano]
ax_induction [in Tennenbaum.Peano]
ax_mult_rec [in Tennenbaum.Peano]
ax_mult_zero [in Tennenbaum.Peano]
ax_add_rec [in Tennenbaum.Peano]
ax_add_zero [in Tennenbaum.Peano]
ax_succ_inj [in Tennenbaum.Peano]
ax_zero_succ [in Tennenbaum.Peano]
B
B [in Tennenbaum.Tennenbaum]bijection [in Tennenbaum.CantorPairing]
binary [in Tennenbaum.Tennenbaum]
bounded_L [in Tennenbaum.FOL]
C
code [in Tennenbaum.CantorPairing]containsL [in Tennenbaum.Deduction]
CT_Q [in Tennenbaum.Tennenbaum]
D
Dec [in Tennenbaum.LogicFacts]dec [in Tennenbaum.LogicFacts]
Dec [in Tennenbaum.Tennenbaum]
dec [in Tennenbaum.FOL]
decDiv [in Tennenbaum.Tennenbaum]
decode [in Tennenbaum.CantorPairing]
Div [in Tennenbaum.NumberTheory]
Divides [in Tennenbaum.Tennenbaum]
Divides_Irred [in Tennenbaum.Tennenbaum]
E
Enum [in Tennenbaum.Tennenbaum]enumerable [in Tennenbaum.Tennenbaum]
enumT_form [in Tennenbaum.FOL]
env [in Tennenbaum.Tarski]
EQ [in Tennenbaum.Peano]
EQ [in Tennenbaum.Tennenbaum]
eqd_bool [in Tennenbaum.CTT]
Euclid [in Tennenbaum.NumberTheory]
eval [in Tennenbaum.Tarski]
exist_times [in Tennenbaum.Tarski]
exist_times [in Tennenbaum.Peano]
Ex_lt [in Tennenbaum.Tennenbaum]
F
f [in Tennenbaum.Tennenbaum]faktorial [in Tennenbaum.NumberTheory]
forall_times [in Tennenbaum.Peano]
fullsatis [in Tennenbaum.Tarski]
full_operators [in Tennenbaum.Tarski]
funcomp [in Tennenbaum.FOL]
I
iffT [in Tennenbaum.LogicFacts]impl [in Tennenbaum.Tarski]
Inform [in Tennenbaum.Tennenbaum]
inj [in Tennenbaum.CantorPairing]
Insep [in Tennenbaum.Tennenbaum]
Insep1 [in Tennenbaum.Tennenbaum]
Insep2 [in Tennenbaum.Tennenbaum]
Insep3 [in Tennenbaum.Tennenbaum]
interp_nat [in Tennenbaum.Peano]
inu [in Tennenbaum.Peano]
inv [in Tennenbaum.CantorPairing]
in_theory [in Tennenbaum.Peano]
Irred [in Tennenbaum.NumberTheory]
irred [in Tennenbaum.NumberTheory]
irred' [in Tennenbaum.NumberTheory]
iter [in Tennenbaum.Peano]
iter [in Tennenbaum.FOL]
J
join [in Tennenbaum.Peano]L
list_quantop [in Tennenbaum.Deduction]list_binop [in Tennenbaum.Deduction]
L_form [in Tennenbaum.FOL]
L_term [in Tennenbaum.FOL]
L_tded [in Tennenbaum.Deduction]
L_con [in Tennenbaum.Deduction]
L_ded [in Tennenbaum.Deduction]
M
Mod [in Tennenbaum.NumberTheory]MP [in Tennenbaum.Tennenbaum]
N
negb [in Tennenbaum.CTT]next [in Tennenbaum.CantorPairing]
num [in Tennenbaum.Peano]
O
obj_Insep [in Tennenbaum.Tennenbaum]P
PAsat [in Tennenbaum.Peano]PA_preds_ar [in Tennenbaum.Peano]
PA_funcs_ar [in Tennenbaum.Peano]
prime [in Tennenbaum.NumberTheory]
Q
Q [in Tennenbaum.Peano]Q_dec [in Tennenbaum.Tennenbaum]
R
RT_strong [in Tennenbaum.Tennenbaum]RT_weak [in Tennenbaum.Tennenbaum]
S
sat [in Tennenbaum.Tarski]satis [in Tennenbaum.Tarski]
scons [in Tennenbaum.FOL]
Semidec [in Tennenbaum.Tennenbaum]
Stable [in Tennenbaum.Tennenbaum]
stable [in Tennenbaum.Tennenbaum]
std [in Tennenbaum.Tennenbaum]
stdModel [in Tennenbaum.Tennenbaum]
subst_form [in Tennenbaum.FOL]
subst_term [in Tennenbaum.FOL]
surj [in Tennenbaum.Tennenbaum]
surj_form [in Tennenbaum.Tennenbaum]
T
theory [in Tennenbaum.Peano]tprv [in Tennenbaum.Deduction]
U
unary [in Tennenbaum.Tennenbaum]Unnamed_thm [in Tennenbaum.NumberTheory]
Unnamed_thm [in Tennenbaum.Peano]
up [in Tennenbaum.FOL]
V
valid [in Tennenbaum.Tarski]valid_L [in Tennenbaum.Tarski]
valid_ctx [in Tennenbaum.Tarski]
vec [in Tennenbaum.FOL]
vecs_from [in Tennenbaum.FOL]
W
WO [in Tennenbaum.Tennenbaum]other
Σ [in Tennenbaum.CantorPairing]Record Index
F
funcs_signature [in Tennenbaum.FOL]I
interp [in Tennenbaum.Tarski]O
operators [in Tennenbaum.FOL]P
preds_signature [in Tennenbaum.FOL]| 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 | (2304 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 | (59 entries) |
| Binder 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 | (1577 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 | (65 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 | (9 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 | (332 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 | (60 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 | (8 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 | (19 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 | (42 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 | (115 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 | (4 entries) |