Logikai operátorok
¬ -logikai negáció
∧ -konjunktció
∨ -diszjunktció
⇒ -implikáció
⇔ -ekvivalencia
Egyenlőség
= -az egyenlőség minden típusra használható a predikátumok kivételével.
Kvantálás
Q x1 : S1; ...;xn : Sn | p • q
ahol Q az ∀ ,∃! vagy az ∃ egyike
Jelentése :
∀ x1 : S1; ... ;xn : Sn (p ⇒ q)
∃ x1 : S1; ... ;xn : Sn (p ∧ q)
Rövidítés:
∀ : T • q for ∀ x: T | true • q
Halmaz operátorok
∈ - eleme-e? reláció
⊂ - részhalamaz reláció
S1 és S2 azonos típusúnak kell lennie
S1 ⊂ S2 ⇔ (∀ x : S1 | x ∈ S2)
× -direkt szorzat
(x1,x2,...,xn) ∈ S1 × S2 × ... × Sn ⇔ (x1 ∈ S1 &and ... ∧ xn ∈ Sn)
℘ - hatványhalmaz
S' ∈ ℘(S) ⇔ S' ⊂ S
∪ -metszet
A résztvevő halmazoknak azonos T típusúnak kell lenniük:
x ∈ S1 ∪ S2 ⇔ (x ∈ S1 ∨ x ∈ S2)
x ∈ ∪ S ⇔ (∃ S' : T • x ∈ S')
∩ - halmaz metszet
∖ - halmaz különbség
Reláció operátorok
Domain dom R
dom R = {a : S; b : T | a ↦ b ∈ R • a }
Range ranR
ranR = {a : S; b : T | a ↦ b ∈ R • b }