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

Symbol to ASCII Correspondence for Text-Only Browsers (in order of appearance in \$c and \$v statements in the database)

 Symbol ASCII ( ( ) ) → -> ¬ -. wff wff ⊢ |- & & ⇒ => 𝜑 ph 𝜓 ps 𝜒 ch 𝜃 th 𝜏 ta 𝜂 et 𝜁 ze 𝜎 si 𝜌 rh 𝜇 mu 𝜆 la 𝜅 ka ∧ /\ ↔ <-> ∨ \/ STAB STAB DECID DECID ∀ A. setvar setvar 𝑥 x class class = = 𝐴 A 𝐵 B ⊤ T. 𝑦 y ⊥ F. ⊻ \/_ 𝑧 z 𝑤 w 𝑣 v 𝑢 u 𝑡 t Ⅎ F/ ∃ E. ∈ e. [ [ / / ] ] 𝑓 f 𝑔 g 𝑠 s ∃! E! ∃* E* { { ∣ | } } ∧ ./\ ∨ .\/ ≤ .<_ < .< + .+ − .- × .X. / ./ ↑ .^ 0 .0. 1 .1. ∥ .|| ∼ .~ ⊥ ._|_ ⨣ .+^ ✚ .+b ⊕ .(+) ∗ .* · .x. ∙ .xb , ., ⊗ .(x) 𝟎 .0b 𝐶 C 𝐷 D 𝑃 P 𝑄 Q 𝑅 R 𝑆 S 𝑇 T 𝑈 U 𝑒 e ℎ h 𝑖 i 𝑗 j 𝑘 k 𝑚 m 𝑛 n 𝑜 o 𝐸 E 𝐹 F 𝐺 G 𝐻 H 𝐼 I 𝐽 J 𝐾 K 𝐿 L 𝑀 M 𝑁 N 𝑉 V 𝑊 W 𝑋 X 𝑌 Y 𝑍 Z 𝑂 O 𝑟 r 𝑞 q 𝑝 p 𝑎 a 𝑏 b 𝑐 c 𝑑 d 𝑙 l Ⅎ F/_ ≠ =/= ∉ e/ V _V CondEq CondEq [ [. ] ]. ⦋ [_ ⦌ ]_ ∖ \ ∪ u. ∩ i^i ⊆ C_ ⊊ C. ∅ (/) , , if if 𝒫 ~P ⟨ <. ⟩ >. ∪ U. ∩ |^| ∪ U_ ∩ |^|_ Disj Disj_ ↦ |-> Tr Tr E _E I _I Po Po Or Or Se Se Ord Ord On On Lim Lim suc suc ω _om × X. ◡ `' dom dom ran ran ↾ |` “ " ∘ o. Rel Rel ℩ iota : : Fun Fun Fn Fn ⟶ --> –1-1→ -1-1-> –onto→ -onto-> –1-1-onto→ -1-1-onto-> ‘ ` Isom Isom ℩ iota_ ∘𝑓 oF ∘𝑟 oR 1st 1st 2nd 2nd tpos tpos Smo Smo recs recs rec rec frec frec 1𝑜 1o 2𝑜 2o 3𝑜 3o 4𝑜 4o +𝑜 +o ·𝑜 .o ↑𝑜 ^oi Er Er / /. ≈ ~~ ≼ ~<_ Fin Fin card card N N. +N +N ·N .N = ℚ QQ ℝ+ RR+ -𝑒 -e +𝑒 +e ·e *e (,) (,) (,] (,] [,) [,) [,] [,] ... ... ..^ ..^ seq seq ↑ ^ shift shift ℜ Re ℑ Im ∗ * √ sqrt abs abs ± +- ⇝ ~~> Σ sum_ Δ0 Delta0 BOUNDED Bdd BOUNDED Bdd_ Ind Ind ∀! A!
 Copyright terms: Public domain W3C validator