List of Syntax, Axioms (ax-) and
Definitions (df-)|
Ref | Expression (see link for any distinct variable requirements)
|
| wbot 1 | wff ⊥ |
| wmd 2 | wff (𝜑 ⅋ 𝜓) |
| wneg 3 | wff ~ 𝜑 |
| ax-ibot 4 | ⊦ 𝜑 ⇒ ⊦ (⊥ ⅋ 𝜑) |
| ax-ebot 5 | ⊦ (⊥ ⅋ 𝜑) ⇒ ⊦ 𝜑 |
| ax-cut 6 | ⊦ (𝜑 ⅋
𝜓)
& ⊦ (~
𝜓 ⅋ 𝜒) ⇒ ⊦ (𝜑 ⅋
𝜒) |
| ax-init 7 | ⊦ (~ 𝜑 ⅋
𝜑) |
| ax-mdco 8 | ⊦ (~ (𝜑 ⅋
𝜓) ⅋ (𝜓
⅋ 𝜑)) |
| ax-mdas 9 | ⊦ (~ ((𝜑 ⅋
𝜓) ⅋ 𝜒)
⅋ (𝜑 ⅋ (𝜓 ⅋ 𝜒))) |
| wtop 29 | wff ⊤ |
| wac 30 | wff (𝜑 & 𝜓) |
| ax-top 31 | ⊦ (~ 𝜑 ⅋
⊤) |
| ax-iac 32 | ⊦ (~ 𝜑 ⅋
𝜓)
& ⊦ (~
𝜑 ⅋ 𝜒) ⇒ ⊦ (~ 𝜑 ⅋
(𝜓 & 𝜒)) |
| ax-eac1 33 | ⊦ (~ 𝜑 ⅋
(𝜓 & 𝜒)) ⇒ ⊦ (~ 𝜑 ⅋
𝜓) |
| ax-eac2 34 | ⊦ (~ 𝜑 ⅋
(𝜓 & 𝜒)) ⇒ ⊦ (~ 𝜑 ⅋
𝜒) |
| wne 48 | wff ? 𝜑 |
| ax-ipe 49 | ⊦ (~ 𝜑 ⅋ ?
𝜓) ⇒ ⊦ (~ ? 𝜑 ⅋
? 𝜓) |
| ax-epe 50 | ⊦ (~ ? 𝜑 ⅋
? 𝜓) ⇒ ⊦ (~ 𝜑 ⅋ ?
𝜓) |
| ax-weak 51 | ⊦ (~ ⊥ ⅋ ? 𝜑) |
| ax-contr 52 | ⊦ (~ (? 𝜑
⅋ ? 𝜑) ⅋ ? 𝜑) |
| ax-pemc 53 | ⊦ ~ ? ⊥ |
| ax-dig 54 | ⊦ (~ ? (? 𝜑
⅋ ? 𝜓) ⅋ (? 𝜑 ⅋ ? 𝜓)) |
| wlb 55 | wff (𝜑 ⧟ 𝜓) |
| df-lb 56 | ⊦ ((~ (𝜑 ⧟
𝜓) ⅋ ((~ 𝜑
⅋ 𝜓) & (~ 𝜓 ⅋ 𝜑))) &
(~ ((~ 𝜑 ⅋ 𝜓) & (~ 𝜓 ⅋
𝜑)) ⅋ (𝜑
⧟ 𝜓))) |
| wli 61 | wff (𝜑 ⊸ 𝜓) |
| df-li 62 | ⊦ ((𝜑 ⊸
𝜓) ⧟ (~ 𝜑
⅋ 𝜓)) |
| wone 103 | wff 1 |
| df-one 104 | ⊦ (1 ⧟ ~ ⊥) |
| wmc 105 | wff (𝜑 ⊗ 𝜓) |
| df-mc 106 | ⊦ ((𝜑 ⊗
𝜓) ⧟ ~ (~ 𝜑 ⅋ ~ 𝜓)) |
| wzero 129 | wff 0 |
| df-zero 130 | ⊦ (0 ⧟ ~ ⊤) |
| wad 131 | wff (𝜑 ⊕ 𝜓) |
| df-ad 132 | ⊦ ((𝜑 ⊕
𝜓) ⧟ ~ (~ 𝜑 & ~ 𝜓)) |
| wpe 148 | wff ! 𝜑 |
| df-pe 149 | ⊦ (! 𝜑 ⧟ ~
? ~ 𝜑) |
| wim 180 | wff (𝜑 → 𝜓) |
| df-im 181 | ⊦ ((𝜑 →
𝜓) ⧟ (! 𝜑
⊸ 𝜓)) |
| wand 182 | wff (𝜑 ∧ 𝜓) |
| df-and 183 | ⊦ ((𝜑 ∧ 𝜓) ⧟ (! 𝜑 &
! 𝜓)) |
| wor 184 | wff (𝜑 ∨ 𝜓) |
| df-or 185 | ⊦ ((𝜑 ∨ 𝜓) ⧟ (! 𝜑
⊕ ! 𝜓)) |
| wnot 186 | wff ¬ 𝜑 |
| df-not 187 | ⊦ (¬ 𝜑
⧟ ~ ! 𝜑) |
| wbi 188 | wff (𝜑 ↔ 𝜓) |
| df-bi 189 | ⊦ ((𝜑 ↔
𝜓) ⧟ ((𝜑
→ 𝜓) ∧ (𝜓 → 𝜑))) |
| nvar 203 | nilad x |
| wse 204 | wff [X ≪ Y] 𝜑 |
| wre 205 | wff [X ≫ y] 𝜑 |
| wnu 206 | wff νx𝜑 |
| wsub 207 | wff [x ≔ Y] 𝜑 |
| ax-int 208 | ⊦ 𝜑 ⇒ ⊦ ~ νx~ 𝜑 |
| ax-nue 209 | ⊦ (νx𝜑 ⊸ 𝜑) |
| ax-nuf 210 | ⊦ (νxνx𝜑 ⊸ νx𝜑) |
| ax-ref 211 | ⊦ (νx[a ≫ x] 𝜑 ⊸ [a ≫ x] 𝜑) |
| ax-nnuf 212 | ⊦ (νx~ νx𝜑 ⊸ ~ νx𝜑) |
| ax-nui 213 | ⊦ (𝜑 ⊸
νx𝜑) |
| ax-nur 214 | ⊦ (νx[u ≪ x] 𝜑 ⊸ νy[u ≪ y] 𝜑) |
| ax-nuse 215 | ⊦ (νx[u ≪ v] 𝜑 ⧟ [u ≪ v] νx𝜑) |
| ax-nure 216 | ⊦ (νx[u ≫ v] 𝜑 ⧟ [u ≫ v] νx𝜑) |
| ax-nuad 217 | ⊦ (νx(𝜑 ⊕ 𝜓) ⧟
(νx𝜑 ⊕ νx𝜓)) |
| ax-numc 218 | ⊦ (νx(𝜑 ⊗ νx𝜓) ⧟ (νx𝜑 ⊗ νx𝜓)) |
| ax-nunu 219 | ⊦ (νxνy𝜑 ⧟ νyνx𝜑) |
| ax-subse1 220 | ⊦ ([x ≔ y] [x ≪ a] 𝜑 ⧟ [x ≔ y] [y
≪ a] 𝜑) |
| ax-subse2 221 | ⊦ ([x ≔ y] [a ≪ x] 𝜑 ⧟ [x ≔ y] [a
≪ y] 𝜑) |
| ax-subse3 222 | ⊦ ([x ≔ y] [u ≪ v] 𝜑 ⧟ [u ≪ v] [x
≔ y] 𝜑) |
| ax-subre1 223 | ⊦ ([x ≔ y] [x ≫ a] 𝜑 ⧟ [x ≔ y] [y
≫ a] 𝜑) |
| ax-subre2 224 | ⊦ ([x ≔ y] [u ≫ v] 𝜑 ⧟ [u ≫ v] [x
≔ y] 𝜑) |
| ax-subnu1 225 | ⊦ ([x ≔ y] νx𝜑 ⧟ νx𝜑) |
| ax-subnu2 226 | ⊦ ([x ≔ y] νu𝜑 ⧟ νu[x ≔ y] 𝜑) |
| ax-subid 227 | ⊦ ([x ≔ x] 𝜑 ⧟ 𝜑) |
| ax-send 228 | ⊦ (([z ≪ y] 𝜑 ⊗ [z ≫ x] 𝜓) ⊸ (𝜑 ⊗
[x ≔ y] 𝜓)) |
| ax-lock1 229 | ⊦ (νx? [x ≫ a] 1 ⊸
0) |
| ax-lock2 230 | ⊦ (νx? [x ≪ a] 1 ⊸
0) |
| wnse 240 | wff [X ◁ Y] 𝜑 |
| wnre 241 | wff [X ▷ y] 𝜑 |
| wnnu 242 | wff ∇x𝜑 |
| df-nse 243 | ⊦ ([X ◁ Y] 𝜑 ⧟ ~ [X ≪ Y] ~ 𝜑) |
| df-nre 244 | ⊦ ([X ▷ y] 𝜑 ⧟ ~ [X ≫ y] ~ 𝜑) |
| df-nnu 245 | ⊦ (∇x𝜑 ⧟ ~ νx~ 𝜑) |
| weq 246 | wff X = Y |
| df-eq 247 | ⊦ (X = Y ⧟ ∇a([a ≪ X] [a ≫ b] 1 ⧟ [a ≪ Y] [a ≫ b] 1)) |
| nnab 266 | nilad {x | 𝜑} |
| df-nab 267 | ⊦ ([x ≪ {y | 𝜑}] 𝜓 ⧟ (𝜑 ⊗
[y ≫ a] [x ≪ a] 𝜓)) |
| nvnab 271 | nilad {νx | 𝜑} |
| df-vnab 272 | ⊦ {νx | 𝜑} = {r | νx[r ≪ x]
𝜑} |
| nsub 277 | nilad [x ≔ Y] A |
| df-nsub 278 | ⊦ [x ≔ Y] F = {r |
νa[x ≔ y] [F ≫ f] [r ≪ f] 1} |
| nla 279 | nilad λxY |
| df-la 280 | ⊦ λxY = {νf | ! [f ≫ a] [a
≫ x] [a ≪ Y] 1} |
| nfv 281 | nilad (F' X) |
| df-fv 282 | ⊦ (F' X) = {r | νa[F ≪ a] [a ≪ X] [a ≫ y] [r ≪ y] 1} |
| nov 284 | nilad (AFB) |
| df-ov 285 | ⊦ (AFB) = ((F'
A)' B) |
| nss 286 | nilad S |
| nkk 287 | nilad K |
| nii 288 | nilad I |
| niota 289 | nilad ι |
| df-ss 290 | ⊦ S = λaλbλc((b' a)' (c' a)) |
| df-kk 291 | ⊦ K = λaλba |
| df-ii 292 | ⊦ I = λaa |
| df-iota 293 | ⊦ ι = λf((f' S)' K) |
| ntru 297 | nilad True |
| nfal 298 | nilad False |
| df-tru 299 | ⊦ True = λxλyx |
| df-fal 300 | ⊦ False = λxλyy |
| weqtru 301 | wff ⊨ P |
| weqfal 302 | wff ⊭ P |
| df-eqtru 303 | ⊦ (P = True ⧟
⊨ P) |
| df-eqfal 304 | ⊦ (P = False ⧟
⊭ P) |
| nlimpl 308 | nilad Impl |
| nland 309 | nilad And |
| nlor 310 | nilad Or |
| nlnot 311 | nilad Not |
| nliff 312 | nilad Iff |
| df-limpl 313 | ⊦ Impl = λaλb(baTrue) |
| df-land 314 | ⊦ And = λaλb(baFalse) |
| df-lor 315 | ⊦ Or = λaλb(Trueab) |
| df-lnot 316 | ⊦ Not = λaλxλy(yax) |
| df-liff 317 | ⊦ Iff = λaλb(ba(Not' b)) |
| wal 318 | wff ∀x𝜑 |
| wex 319 | wff ∃x𝜑 |
| wnf 320 | wff Ⅎx𝜑 |
| wel 322 | wff x ∈ y |
| ax-genOLD 323 | ⊦ 𝜑 ⇒ ⊦ ∀x𝜑 |
| ax-almd 324 | ⊦ (∀x(𝜑 ⊸ 𝜓) ⊸
(∀x𝜑 ⊸
∀x𝜓)) |
| ax-dis 325 | ⊦ (𝜑 ⊸
∀x𝜑) |
| ax-ex 326 | ⊦ ~ ∀x~ x = y |
| ax-eqeu 327 | ⊦ (x = y ⊸ (x = z ⊸ y = z)) |
| ax-eleq1 328 | ⊦ (x = y ⊸ (x ∈ z ⊸ y ∈ z)) |
| ax-eleq2 329 | ⊦ (x = y ⊸ (z ∈ x ⊸ z ∈ y)) |
| ax-negf 330 | ⊦ (~ ∀x𝜑 ⊸ ∀x~
∀x𝜑) |
| ax-alcom 331 | ⊦ (∀x∀y𝜑 ⊸ ∀y∀x𝜑) |
| ax-sub 332 | ⊦ (x = y ⊸ (∀y𝜑 ⊸ ∀x(x = y ⊸ 𝜑))) |
| ax-aleq 333 | ⊦ (~ x = y ⊸ (y = z ⊸ ∀x y = z)) |
| df-ex 334 | ⊦ (∃x𝜑 ⧟ ~ ∀x~ 𝜑) |
| df-nf 335 | ⊦ (Ⅎx𝜑 ⧟ (~ 𝜑
⊸ ∀x𝜑)) |