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

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

 Symbol ASCII ( ) -> -. wff |- & => ph ps ch th ta et ze si rh mu la ka /\ <-> \/ STAB STAB DECID DECID A. setvar x class = A B T. y F. \/_ z w v u t F/ E. e. [ / ] f g s E! E* { | } ./\ .\/ .<_ .< .+ .- .X. ./ .^ .0. .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 CondEq CondEq [. ]. [_ ]_ \ u. i^i C_ (/) , if ~P <. >. U. |^| U_ |^|_ Disj Disj_ |-> Tr EXMID EXMID _E _I Po Or FrFor FrFor Fr Se Se We Ord On Lim suc _om X. `' dom ran |` " o. Rel iota : Fun Fn --> -1-1-> -onto-> -1-1-onto-> ` Isom iota_ oF oR 1st 2nd tpos tpos Smo recs recs rec frec frec 1o 2o 3o 4o +o .o ↑o ^oi Er /. ^m ^pm X_ ~~ ~<_ Fin sup inf inf ⊔ |_| inl inl inr inr case case ⊔d |_|d Omni Omni ℕ∞ NN+oo Markov Markov card N. +N .N = QQ RR+ -e +e *e (,) (,] [,) [,] ... ..^ ..^ |_ ⌈ |^ mod == seq ^ ! _C ♯ # shift Re Im * sqrt abs +- ~~> sum_ exp _e sin cos tan _pi || gcd lcm lcm Prime numer numer denom denom phi Struct Struct ndx sSet sSet Slot Slot Base ↾s |`s +g .r *r Scalar Scalar .s .i TopSet TopSet le oc dist UnifSet Hom comp comp ↾t |`t TopOpen topGen Xt_ 0g g gsum s Xs_ s ^s PsMet PsMet *Met Met ball fBas filGen MetOpen metUnif metUnif Top TopOn TopOn TopSp TopBases int cls Clsd nei Cn CnP ~~>t *MetSp MetSp toMetSp toMetSp -cn-> DECIDin DECID_in Δ0 Delta0 BOUNDED Bdd BOUNDED Bdd_ Ind Ind ! A!
 Copyright terms: Public domain W3C validator