Intuitionistic Logic Explorer |
This is the GIF version. Change to Unicode version |
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. | |
[ | |
/ | |
] | |
f | |
g | |
s | |
E! | |
E* | |
e. | |
{ | |
| | |
} | |
./\ | |
.\/ | |
.<_ | |
.< | |
.+ | |
.- | |
.X. | |
./ | |
.^ | |
.0. | |
.1. | |
.|| | |
.~ | |
._|_ | |
.+^ | |
.+b | |
.(+) | |
.* | |
.x. | |
.xb | |
., | |
.(x) | |
.o. | |
.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 | |
fi | |
sup | |
inf | inf |
⊔ | |_| |
inl | inl |
inr | inr |
case | case |
⊔d | |_|d |
ℕ∞ | NN+oo |
Omni | Omni |
Markov | Markov |
WOmni | WOmni |
card | |
CHOICE | CHOICE |
CCHOICE | CCHOICE |
N. | |
+N | |
.N | |
<N | |
+pQ | |
.pQ | |
<pQ | |
~Q | |
Q. | |
1Q | |
+Q | |
.Q | |
*Q | |
<Q | |
~Q0 | ~Q0 |
Q0 | Q0. |
0Q0 | 0Q0 |
+Q0 | +Q0 |
·Q0 | .Q0 |
P. | |
1P | |
+P. | |
.P. | |
<P | |
~R | |
R. | |
0R | |
1R | |
-1R | |
+R | |
.R | |
<R | |
<RR | |
CC | |
RR | |
0 | |
1 | |
_i | |
+ | |
x. | |
<_ | |
+oo | |
-oo | |
RR* | |
< | |
- | |
-u | |
#ℝ | #RR |
# | =//= |
NN | |
2 | |
3 | |
4 | |
5 | |
6 | |
7 | |
8 | |
9 | |
NN0 | |
NN0* | NN0* |
ZZ | |
; | ; |
ZZ>= | |
RR+ | |
-e | |
+e | |
*e | |
(,) | |
(,] | |
[,) | |
[,] | |
... | |
..^ | ..^ |
|_ | |
⌈ | |^ |
mod | |
== | |
seq | |
^ | |
! | |
_C | |
♯ | # |
shift | |
Re | |
Im | |
* | |
sqrt | |
abs | |
+- | |
~~> | |
sum_ | |
prod_ | |
exp | |
_e | |
sin | |
cos | |
tan | |
_pi | |
_tau | |
|| | |
gcd | |
lcm | lcm |
Prime | |
numer | numer |
denom | denom |
odZ | |
phi | |
pCnt | |
Z[i] | |
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 |
+f | |
Mgm | Mgm |
Smgrp | Smgrp |
Mnd | |
MndHom | MndHom |
SubMnd | SubMnd |
Grp | |
invg | |
-g | |
PsMet | PsMet |
*Met | |
Met | |
ball | |
fBas | |
filGen | |
MetOpen | |
metUnif | metUnif |
Top | |
TopOn | TopOn |
TopSp | |
TopBases | |
int | |
cls | |
Clsd | |
nei | |
Cn | |
CnP | |
~~>t | |
tX | |
Homeo | |
*MetSp | |
MetSp | |
toMetSp | toMetSp |
-cn-> | |
lim | limCC |
_D | |
log | |
^c | |
logb | logb |
/L | |
DECIDin | DECID_in |
Δ0 | Delta0 |
BOUNDED | Bdd |
BOUNDED | Bdd_ |
Ind | Ind |
! | A! |
Copyright terms: Public domain | W3C validator |