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_ ∅ (/) , , if if 𝒫 ~P ⟨ <. ⟩ >. ∪ U. ∩ |^| ∪ U_ ∩ |^|_ Disj Disj_ ↦ |-> Tr Tr EXMID EXMID E _E I _I Po Po Or Or FrFor FrFor Fr Fr Se Se We We 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 1o 1o 2o 2o 3o 3o 4o 4o +o +o ·o .o ↑o ^oi Er Er / /. ↑𝑚 ^m ↑pm ^pm X X_ ≈ ~~ ≼ ~<_ Fin Fin fi fi sup sup inf inf ⊔ |_| inl inl inr inr case case ⊔d |_|d Omni Omni ℕ∞ NN+oo Markov Markov WOmni WOmni card card CHOICE CHOICE CCHOICE CCHOICE N N. +N +N ·N .N = ℚ QQ ℝ+ RR+ -𝑒 -e +𝑒 +e ·e *e (,) (,) (,] (,] [,) [,) [,] [,] ... ... ..^ ..^ ⌊ |_ ⌈ |^ mod mod ≡ == seq seq ↑ ^ ! ! C _C ♯ # shift shift ℜ Re ℑ Im ∗ * √ sqrt abs abs ± +- ⇝ ~~> Σ sum_ ∏ prod_ exp exp e _e sin sin cos cos tan tan π _pi τ _tau ∥ || gcd gcd lcm lcm ℙ Prime numer numer denom denom ϕ phi Struct Struct ndx ndx sSet sSet Slot Slot Base Base ↾s |`s +g +g .r .r *𝑟 *r Scalar Scalar ·𝑠 .s ·𝑖 .i TopSet TopSet le le oc oc dist dist UnifSet UnifSet Hom Hom comp comp ↾t |`t TopOpen TopOpen topGen topGen ∏t Xt_ 0g 0g Σg gsum Xs Xs_ ↑s ^s PsMet PsMet ∞Met *Met Met Met ball ball fBas fBas filGen filGen MetOpen MetOpen metUnif metUnif Top Top TopOn TopOn TopSp TopSp TopBases TopBases int int cls cls Clsd Clsd nei nei Cn Cn CnP CnP ⇝𝑡 ~~>t ×t tX Homeo Homeo ∞MetSp *MetSp MetSp MetSp toMetSp toMetSp –cn→ -cn-> limℂ limCC D _D log log DECIDin DECID_in Δ0 Delta0 BOUNDED Bdd BOUNDED Bdd_ Ind Ind ∀! A!
 Copyright terms: Public domain W3C validator