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-3 7((¬ φ → ¬ ψ) → (ψφ))
ax-mp 8φ    &   (φψ)       ψ
wa 96wff (φ ψ)
wb 97wff (φψ)
ax-ia1 98((φ ψ) → φ)
ax-ia2 99((φ ψ) → ψ)
ax-ia3 100(φ → (ψ → (φ ψ)))
df-bi 109(((φψ) → ((φψ) (ψφ))) (((φψ) (ψφ)) → (φψ)))
ax-in1 527((φ → ¬ φ) → ¬ φ)
ax-in2 528φ → (φψ))
wo 606wff (φ ψ)
ax-io 607(((φ χ) → ψ) ↔ ((φψ) (χψ)))
w3o 902wff (φ ψ χ)
w3a 903wff (φ ψ χ)
df-3or 904((φ ψ χ) ↔ ((φ ψ) χ))
df-3an 905((φ ψ χ) ↔ ((φ ψ) χ))
ax-meredith 1251(((((φψ) → (¬ χ → ¬ θ)) → χ) → τ) → ((τφ) → (θφ)))
wnand 1279wff (φ ψ)
df-nand 1280((φ ψ) ↔ ¬ (φ ψ))
wtru 1310wff
wfal 1311wff
df-tru 1313( ⊤ ↔ (φφ))
df-fal 1314( ⊥ ↔ ¬ ⊤ )
wal 1335wff xφ
ax-5 1336(x(φψ) → (xφxψ))
ax-6 1337xφx ¬ xφ)
ax-7 1338(xyφyxφ)
ax-gen 1339φ       xφ
wex 1374wff xφ
ax-ie1 1375(xφxxφ)
ax-ie2 1376(x(ψxψ) → (x(φψ) ↔ (xφψ)))
cv 1382class x
wceq 1383wff A = B
wcel 1385wff A B
ax-8 1387(x = y → (x = zy = z))
ax-10 1388(x x = yy y = x)
ax-11 1389(x = y → (yφx(x = yφ)))
ax-i11e 1390(x = y → (yφx(x = y φ)))
ax-i12 1391(z z = x (z z = y z(x = yz x = y)))
ax-4 1392(xφφ)
ax-13 1395(x = y → (x zy z))
ax-14 1396(x = y → (z xz y))
ax-17 1402(φxφ)
ax-i9 1417x x = y
ax-5o 1425(x(xφψ) → (xφxψ))
ax-6o 1428x ¬ xφφ)
ax-ial 1430(xφxxφ)
ax-i5r 1431((xφxψ) → x(xφψ))
ax-9o 1558(x(x = yxφ) → φ)
ax-10o 1576(x x = y → (xφyφ))
wsbc 1604wff [A / x]φ
df-sb 1606([y / x]φ ↔ ((x = yφ) x(x = y φ)))
ax-16 1644(x x = y → (φxφ))
ax-11o 1654x x = y → (x = y → (φx(x = yφ))))
ax-15 1807z z = x → (¬ z z = y → (x yz x y)))
weu 1829wff ∃!xφ
wmo 1830wff ∃*xφ
df-eu 1833(∃!xφyx(φx = y))
df-mo 1834(∃*xφ ↔ (xφ∃!xφ))
  Copyright terms: Public domain W3C validator