ILE Home Intuitionistic Logic Explorer This is the Unicode version.
Change to GIF version

List of Syntax, Axioms (ax-) and Definitions (df-)
RefExpression (see link for any distinct variable requirements)
wn 3wff ¬ φ
wi 4wff (φψ)
ax-1 5(φ → (ψφ))
ax-2 6((φ → (ψχ)) → ((φψ) → (φχ)))
ax-mp 7φ    &   (φψ)       ψ
wa 95wff (φ ψ)
wb 96wff (φψ)
ax-ia1 97((φ ψ) → φ)
ax-ia2 98((φ ψ) → ψ)
ax-ia3 99(φ → (ψ → (φ ψ)))
df-bi 108(((φψ) → ((φψ) (ψφ))) (((φψ) (ψφ)) → (φψ)))
ax-in1 527((φ → ¬ φ) → ¬ φ)
ax-in2 528φ → (φψ))
wo 609wff (φ ψ)
ax-io 610(((φ χ) → ψ) ↔ ((φψ) (χψ)))
wdc 718wff DECID φ
df-dc 719(DECID φ ↔ (φ ¬ φ))
w3o 846wff (φ ψ χ)
w3a 847wff (φ ψ χ)
df-3or 848((φ ψ χ) ↔ ((φ ψ) χ))
df-3an 849((φ ψ χ) ↔ ((φ ψ) χ))
wtru 1192wff
wfal 1193wff
df-tru 1195( ⊤ ↔ (φφ))
df-fal 1196( ⊥ ↔ ¬ ⊤ )
wxo 1211wff (φψ)
df-xor 1212((φψ) ↔ ((φ ψ) ¬ (φ ψ)))
wal 1271wff xφ
ax-5 1272(x(φψ) → (xφxψ))
ax-7 1273(xyφyxφ)
ax-gen 1274φ       xφ
wnf 1285wff xφ
df-nf 1286(Ⅎxφx(φxφ))
wex 1318wff xφ
ax-ie1 1319(xφxxφ)
ax-ie2 1320(x(ψxψ) → (x(φψ) ↔ (xφψ)))
cv 1328class x
wceq 1329wff A = B
wcel 1331wff A B
ax-8 1333(x = y → (x = zy = z))
ax-10 1334(x x = yy y = x)
ax-11 1335(x = y → (yφx(x = yφ)))
ax-i12 1336(z z = x (z z = y z(x = yz x = y)))
ax-bnd 1337(z z = x (z z = y xz(x = yz x = y)))
ax-4 1338(xφφ)
ax-13 1342(x = y → (x zy z))
ax-14 1343(x = y → (z xz y))
ax-17 1356(φxφ)
ax-i9 1360x x = y
ax-ial 1365(xφxxφ)
ax-i5r 1366((xφxψ) → x(xφψ))
ax-10o 1522(x x = y → (xφyφ))
wsbc 1563wff [A / x]φ
df-sb 1565([y / x]φ ↔ ((x = yφ) x(x = y φ)))
ax-16 1613(x x = y → (φxφ))
ax-11o 1622x x = y → (x = y → (φx(x = yφ))))
weu 1812wff ∃!xφ
wmo 1813wff ∃*xφ
df-eu 1815(∃!xφyx(φx = y))
df-mo 1816(∃*xφ ↔ (xφ∃!xφ))
ax-ext 1906(z(z xz y) → x = y)
cab 1909class {xφ}
df-clab 1910(x {yφ} ↔ [x / y]φ)
df-cleq 1916(x(x yx z) → y = z)       (A = Bx(x Ax B))
df-clel 1919(A Bx(x = A x B))
wnfc 2046wff xA
df-nfc 2048(xAyx y A)
wne 2085wff AB
wnel 2086wff AB
df-ne 2087(AB ↔ ¬ A = B)
df-nel 2088(AB ↔ ¬ A B)
wral 2175wff x A φ
wrex 2176wff x A φ
wreu 2177wff ∃!x A φ
wrmo 2178wff ∃*x Aφ
crab 2179class {x Aφ}
df-ral 2180(x A φx(x Aφ))
df-rex 2181(x A φx(x A φ))
df-reu 2182(∃!x A φ∃!x(x A φ))
df-rmo 2183(∃*x Aφ∃*x(x A φ))
df-rab 2184{x Aφ} = {x ∣ (x A φ)}
cvv 2418class V
df-v 2420V = {xx = x}
wcdeq 2604wff CondEq(x = yφ)
df-cdeq 2605(CondEq(x = yφ) ↔ (x = yφ))
ax-3 2621((¬ φ → ¬ ψ) → (ψφ))
  Copyright terms: Public domain W3C validator