mmascii - Intuitionistic Logic Explorer

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
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
1𝑜	1o
2𝑜	2o
3𝑜	3o
4𝑜	4o
+𝑜	+o
·𝑜	.o
↑𝑜	^oi
Er	Er
/	/.
≈	~~
≼	~<_
Fin	Fin
sup	sup
inf	inf
card	card
N	N.
+N	+N
·N	.N
<N	<N
+pQ	+pQ
·pQ	.pQ
<pQ	<pQ
~Q	~Q
Q	Q.
1Q	1Q
+Q	+Q
·Q	.Q
*Q	*Q
<Q	<Q
~Q0	~Q0
Q0	Q0.
0Q0	0Q0
+Q0	+Q0
·Q0	.Q0
P	P.
1P	1P
+P	+P.
·P	.P.
<P	<P
~R	~R
R	R.
0R	0R
1R	1R
-1R	-1R
+R	+R
·R	.R
<R	<R
<ℝ	<RR
ℂ	CC
ℝ	RR
0	0
1	1
i	_i
+	+
·	x.
≤	<_
+∞	+oo
-∞	-oo
ℝ*	RR*
<	<
−	-
-	-u
#ℝ	#RR
#	#
ℕ	NN
2	2
3	3
4	4
5	5
6	6
7	7
8	8
9	9
10	10
ℕ0	NN0
ℤ	ZZ
;	;
ℤ≥	ZZ>=
ℚ	QQ
ℝ+	RR+
-𝑒	-e
+𝑒	+e
·e	*e
(,)	(,)
(,]	(,]
[,)	[,)
[,]	[,]
...	...
..^	..^
⌊	|_
⌈	|^
mod	mod
≡	==
seq	seq
↑	^
!	!
C	_C
shift	shift
ℜ	Re
ℑ	Im
∗	*
√	sqrt
abs	abs
±	+-
⇝	~~>
Σ	sum_
∥	||
gcd	gcd
lcm	lcm
ℙ	Prime
Δ0	Delta0
BOUNDED	Bdd
BOUNDED	Bdd_
Ind	Ind
∀!	A!